PHI 9 - Type Variables and Type Aliases #10

bkase · 2021-03-21T01:27:12Z

Merges in content from PHI 5 (type variables) with latex judgments
for bidirectional type elaboration and kind synthesis/analysis. Will
follow up with content from the PHI 3 (type aliases) later.

Merges in content from PHI 5 (type variables) with latex judgements for bidirectional type elaboration and kind synthesis/analysis. Will follow up with content from the PHI 3 (type aliases) later.

cyrus- · 2021-03-23T04:58:18Z

9-type-aliases-redux/latex/kind-judgements.tex

+\begin{minipage}{\linewidth}
+	\judgbox
+	{\elabAna{\hPhi}{\htau}{\hkappa_1}{\dtau}{\hkappa_2}{\Delta}}
+	{$\htau$ analyzes against type $\hkappa_1$ and


should say "kind" not "type"

cyrus- · 2021-03-23T05:09:47Z

9-type-aliases-redux/latex/kind-judgements.tex

+\newcommand{\kconsistent}[2]{#1 \sim #2}
+
+\newcommand{\hPhi}{\Phi}
+\newcommand{\EmptyhPhi}{\emptyset} % From hand-written notes, Canonical forms lemma; page 14


you can use \cdot for both

cyrus- · 2021-04-11T18:08:09Z

9-type-aliases-redux/9-type-aliases-redux.md

+```
+type TPat.t =
+  | EmptyHole(MetaVar.t)
+  | TyVar(VarErrStatus.t, TyId.t)


don't need a VarErrStatus here, since we're introducing a binding not consuming it

cyrus- · 2021-04-11T18:10:32Z

9-type-aliases-redux/9-type-aliases-redux.md

+
+So that we can still assign a type properly to the resulting `DExp.t` we add the following new syntax:
+
+`TyBindings(TyVarCtx.t, DHExp.t)` for abstract syntax


not sure why this needs to be a tyvarctx -- I think we can just turn each type alias line into a corresponding type alias expression in dhexp

I was thinking we could avoid having to deal with patterns in DHExp if we did it this way and this will scale if/when type-patterns get more complicated.

I can't think of a way to, in a single DHExp, capture all the possibilities of holes in different places of the UHExp type alias without copying all the rules over (or is this what you're suggesting?)

cyrus- · 2021-04-11T18:15:14Z

9-type-aliases-redux/latex/kind-judgements.tex

+\begin{minipage}{\linewidth}
+	\judgbox
+	{\kconsubkind{\Delta;\hPhi}{\hkappa_1}{\hkappa_2}}
+	{$\hkappa_1$ is a consistent subkind of $\hkappa_2$}


i think we need a transitivity rule here?

Consistent subkinding (and subtyping) isn’t transitive. Counter example:
S(Int) <~ ?
? <~ S(Bool)

but this is not true:
S(Int) <~ S(Bool)

Ah yeah, whoops.

Do you need a rule for S(t1) <~ S(t2) where t1 <~ t2?

I think not yet (until polymorphism) because currently:

S(tau) is only well-formed if tau has kind Ty

forall types tau_1 and tau_2, tau_1 <~ tau_2 iff tau_1 === tau_2 -- and this is covered by the KCRespectEquiv rule

cyrus- · 2021-04-11T18:15:53Z

9-type-aliases-redux/latex/kind-judgements.tex

+\begin{minipage}{\linewidth}
+	\judgbox
+	{\kformation{\Delta;\hPhi}{\hkappa}}
+	{$\hkappa$ forms a kind} \;\\


need rules for other kind forms

cyrus- · 2021-04-11T18:16:24Z

9-type-aliases-redux/latex/kind-judgements.tex

+\begin{minipage}{\linewidth}
+	\judgbox
+	{\kequiv{\Delta;\hPhi}{\hkappa_1}{\hkappa_2}}
+	{$\hkappa_1$ is equivalent to $\hkappa_2$} \;\\


need rules for other type forms

I'm confused what is you mean by other type forms -- I'm not clear what's missing here

cyrus- · 2021-04-11T18:16:54Z

9-type-aliases-redux/latex/kind-judgements.tex

+\begin{minipage}{\linewidth}
+	\judgbox
+	{\kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2}{\hkappa}}
+	{$\dtau_1$ is equivalent to $\dtau_2$ and has kind $\hkappa_2$} \;\\


^^ same as my reply, I'm not sure what's missing

hejohns · 2021-06-15T21:32:38Z

hejohns@8f53339
@cyrus- found typo while I was referencing this Phi during OH

hejohns · 2021-06-19T04:49:13Z

hejohns@4201af8
Is this a bug in KSVar?
related-- given
type V = Int in type T = V in ...
is T \equiv Int supposed to be derivable?

cyrus- · 2021-06-20T01:46:45Z

Looks right to me. Why do you think it may be a bug?

Yes, T \equiv Int should be derivable in that case.

hejohns · 2021-06-22T02:54:38Z

I must be missing something.
I'm unable to rigorously show T \equiv Int is NOT derivable, but there seems to me a problematic circularity where to show T \equiv Int with the current rules, you essentially have to show S(T) \equiv S(Int), which is only the conclusion of KESingEquiv, which has T \equiv Int as the premiss.
Similarly, trying to show T \equiv V and using transitivity seems to be impossible.
That said, type-aliases-2 handles this snippet just fine.
Will be at OH tomorrow.

hejohns · 2021-06-25T01:04:00Z

https://raw.githubusercontent.com/hejohns/hazel-etc/trunk/9-type-aliases/kind-judgements.ESDefine-simple.pdf
keeping let type line elaboration the same, adds a simple type equality judgment st t :: S(\tau) concludes t \equiv \tau

https://raw.githubusercontent.com/hejohns/hazel-etc/trunk/9-type-aliases/kind-judgements.ESDefine-weird-knd-ana.pdf
keeping let type line elaboration the same, adds a "weird" (@cyrus- ) kind ana judgment st t :: S(\tau) concludes t <= S(\tau)

https://raw.githubusercontent.com/hejohns/hazel-etc/trunk/9-type-aliases/kind-judgements.KSVar-natural.pdf
changes type var kind syn to be "natural", but requires let type line elaboration to be modified (see pdf), and some other ancillary details.

while the current let type line elaboration-- where the kind synthesized by the definition is added to the context-- seems natural at first, it may not be so. After all, you essentially want to singleton wrap/lift the type definition. Using the synthesized kind only serves this purpose if we define a somewhat unnatural KSVar rule, which definitely works, but rubs me the wrong way.
That said, forcing the more natural KSVar judgment results in a slightly quirky let type line elaboration rule(s)-- but to me, the quirkiness isn't as bad as the KSVar strangeness.

edit: had to be more careful with KSVar-natural. Should probably should go with ESDefine-simple after all.

hejohns · 2021-06-28T18:45:20Z

https://raw.githubusercontent.com/hejohns/hazel-etc/trunk/9-type-aliases/kind-judgements.subkind.pdf
one more option, similar to the rule in Stone, Harper 2006, where S(t) \consistentsubkind \kappa if t :: \kappa \in \Phi

as much as I want to modify KSVar, keeping it and adding this subkinding judgment is more decorous

cyrus- · 2021-06-29T04:41:47Z

I think adding a kind analysis rule for type variables is the right solution. I've attached an annotation with that rule, as well as some other notes to think about for both of you @bkase and @hejohns. We can discuss in OH.
Uploading kinding-notes-june29.pdf…

bkase · 2021-06-29T11:41:46Z

@cyrus- i think your upload failed, can you retry it?

cyrus- · 2021-06-29T14:37:34Z

kinding-notes-june29.pdf

hejohns · 2021-06-30T22:38:33Z

https://raw.githubusercontent.com/hejohns/hazel-etc/trunk/9-type-aliases/kind-judgements.statics.pdf
for tomorrow's OH

hejohns · 2021-07-04T01:40:37Z

https://raw.githubusercontent.com/hejohns/hazel-etc/trunk/9-type-aliases/mphi-9-type-aliases/mphi.pdf
This should be self readable for the interested/bored, but I don't think it's strictly necessary to before talking about it next week.
The main article is about the desire for labeled singletons in the metatheory. There are some additional notes on tangential matters.
A written out form for "why proving kind analysis soundness is ugly w/o labeled singletons in the metatheory" is at the end.
It is very short.
The outstanding issue with holes and labeled singletons-- as pointed out by @cyrus- --, and in the future type constructors, is perturbing.

bkase · 2021-07-07T17:16:31Z

hazelgrove/hazel@45e180c uses higher-singletons and the S_{S_k(c)}(c') === S_k(c) rule to resolve the variable issue

hejohns · 2021-07-17T02:15:11Z

^force push was rollback from accidental push upstream (confused remotes/muscle memory)

@bkase , @cyrus- recommended making a new phi for the (wip) system w/ type constructors/Pi/Sigma-kinds, and updating this one to reflect the code as is.
https://raw.githubusercontent.com/hejohns/hazel-etc/trunk/9-type-aliases/kind-judgements.diff.pdf
is a latexdiff generated pdf diff of the updates. Should be as expected. Singleton labels are only for typvar propogation.
The bnf got cut off but it's just S(\htau) => S_{\hkappa}(\htau).

https://raw.githubusercontent.com/hejohns/hazel-etc/trunk/9-type-aliases/diff.patch (the full/binary patch; includes pdf)

bkase added 3 commits March 20, 2021 20:23

Initial draft

d5c4db2

Merges in content from PHI 5 (type variables) with latex judgements for bidirectional type elaboration and kind synthesis/analysis. Will follow up with content from the PHI 3 (type aliases) later.

Adds note about type holes

8b3f0dd

Delta supports htyp/varctx or kind/tyvarctx

aaa112a

cyrus- reviewed Mar 23, 2021

View reviewed changes

bkase added 5 commits March 23, 2021 20:39

Adds kind assignment, fixes a few bugs

696d9d9

Updated for kind-assignment and sane delta

41f5187

Uses cdot for both empty sets

f57dd56

Attempts to add Ana uvar rule

b14fc0c

Judgements and changes for singleton kinds

ecdcd5b

cyrus- reviewed Apr 11, 2021

View reviewed changes

cyrus- requested changes Apr 11, 2021

View reviewed changes

cyrus- reviewed Apr 11, 2021

View reviewed changes

bkase added 11 commits April 12, 2021 18:25

Requested changes

0d0dcb9

Fixes issues in PHI, adds theorems for reasoning

1506086

Unrecognition tweak

2759c7e

Fixes for broken handling of tyvars

c43241e

Made suggested changes

b2ea0f1

Latest changes

ed6b5e1

Moves to bidirectional kind assignment

ce7d4fe

Tweaks to design docs

3f6986b

Removes the extra recursive param in lines

f1f1ed1

Remove kind ascription on type equivalence

99db512

Synthesize self for tvars

4410cd5

hejohns force-pushed the 9-type-aliases-redux branch from f6fcfcc to 4410cd5 Compare July 17, 2021 01:40

bkase and others added 4 commits August 5, 2021 22:05

Tweaks to match code

5ee04fe

add some notes on the new tyoe system

21001a1

rename to 9-type-aliases and move KindSystem.md to here from hazel

7c87c49

add the diagram

4f52c67

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

PHI 9 - Type Variables and Type Aliases #10

PHI 9 - Type Variables and Type Aliases #10

bkase commented Mar 21, 2021

cyrus- Mar 23, 2021

cyrus- Mar 23, 2021

cyrus- Apr 11, 2021

cyrus- Apr 11, 2021

bkase Apr 12, 2021

cyrus- Apr 11, 2021

bkase Apr 11, 2021

cyrus- Apr 12, 2021

bkase Apr 12, 2021

cyrus- Apr 11, 2021

cyrus- Apr 11, 2021

bkase Apr 12, 2021

cyrus- Apr 11, 2021

bkase Apr 12, 2021

hejohns commented Jun 15, 2021

hejohns commented Jun 19, 2021

cyrus- commented Jun 20, 2021

hejohns commented Jun 22, 2021

hejohns commented Jun 25, 2021 •

edited

Loading

hejohns commented Jun 28, 2021

cyrus- commented Jun 29, 2021

bkase commented Jun 29, 2021

cyrus- commented Jun 29, 2021

hejohns commented Jun 30, 2021

hejohns commented Jul 4, 2021

bkase commented Jul 7, 2021

hejohns commented Jul 17, 2021


		So that we can still assign a type properly to the resulting `DExp.t` we add the following new syntax:

		`TyBindings(TyVarCtx.t, DHExp.t)` for abstract syntax

PHI 9 - Type Variables and Type Aliases #10

Are you sure you want to change the base?

PHI 9 - Type Variables and Type Aliases #10

Conversation

bkase commented Mar 21, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hejohns commented Jun 15, 2021

hejohns commented Jun 19, 2021

cyrus- commented Jun 20, 2021

hejohns commented Jun 22, 2021

hejohns commented Jun 25, 2021 • edited Loading

hejohns commented Jun 28, 2021

cyrus- commented Jun 29, 2021

bkase commented Jun 29, 2021

cyrus- commented Jun 29, 2021

hejohns commented Jun 30, 2021

hejohns commented Jul 4, 2021

bkase commented Jul 7, 2021

hejohns commented Jul 17, 2021

hejohns commented Jun 25, 2021 •

edited

Loading