PHI 3 - Explicit Polymorphism #3
Conversation
|
|
||
| # Concrete Syntax / Representation | ||
|
|
||
| Forall's appear within types and look like: `forall a. ?`, where `a` is |
| a space in a type hole. This will add a Forall type with the cursor at the type | ||
| pattern hole and a hole as the body. | ||
|
|
||
| `Construct(STyArg)` will be triggered when the user types "type" followed by a |
There was a problem hiding this comment.
need a little more detail here -- what happens when there is an expression next to it? are things parenthesized?
| One character is removed from the type variable "a". If it's only one char, | ||
| we're left with `λ ?|:type. { body }` | ||
|
|
||
| * `λ a:|type. { body }` |
There was a problem hiding this comment.
this should probably just go to λ a.
There was a problem hiding this comment.
the trick here is we need to define a mapping from TPat to UHPat, and a partial mapping in the other direction too, if we want this to be maximally fluid.
|
|
||
| ## Type Lambdas | ||
|
|
||
| * `λ |a:type. { body }` or `λ ?|:type. { body }` or `λ a:type. { |body }` or `λ a:type. { body }|` |
There was a problem hiding this comment.
just say that we're reusing the lambda construct so the same logic applies
|
|
||
| The cursor is moved back to `λ a|:type. { body }`. | ||
|
|
||
| * `λ a:type|. { body }` |
There was a problem hiding this comment.
so we're basically adding the keyword "type" to the UHTyp grammar. can you add that to the syntax above?
There was a problem hiding this comment.
This isn't how I was thinking of it. I was thinking that we would have a completely separate type in the expression language: TyLambda, which would be constructed when you write "type" in the annotation field. I guess we could alternatively extend UHTyp --- what do you think?
There was a problem hiding this comment.
it seems syntactically easier to just add "type" to the UHTyp syntax and then interpret annotations containing "type" differently in "lam"...
| Similarly, typing "d" at this cursor position should render a normal lambda | ||
| with the type annotation "typed". | ||
|
|
||
| * `λ a:type. { body| }` |
There was a problem hiding this comment.
this is the zipper case, don't need to mention it in particular since we're reusing lambda
No description provided.