From f9eca7a621b24d177c64df75f45d0b152a5c3452 Mon Sep 17 00:00:00 2001 From: Charles Chamberlain Date: Tue, 5 May 2020 21:58:05 -0400 Subject: [PATCH 1/4] Add first draft of PHI for explicit polymorphism --- .../2-explicit-polymorphism.md | 147 ++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 2-explicit-polymorphism/2-explicit-polymorphism.md diff --git a/2-explicit-polymorphism/2-explicit-polymorphism.md b/2-explicit-polymorphism/2-explicit-polymorphism.md new file mode 100644 index 0000000..af1602e --- /dev/null +++ b/2-explicit-polymorphism/2-explicit-polymorphism.md @@ -0,0 +1,147 @@ +# Introduction + +Currently in Hazel every function has to be assigned a monomorphic type. +This makes it impossible to write code that operates on more than one type +of data. We currently have an example that implements `map : (Num -> Num) +-> [Num] -> [Num]`. By adopting this proposal, Hazel's map function can +have the type `forall a. (a -> a) -> [a] -> [a]`, and thereby be useful for +a larger set of values. + +Specifically, we propose extending Hazel with two type constructs +and two expression constructs, bringing Hazel's type system up to +a System F with holes than a Simply Typed Lambda Calculus with holes. + +# Type Language + +We'd have to extend UHTyp.t with `TyVar` and `Forall` cases: + +```reason +/* UHTyp.re */ + +type operand = +... +| Forall(TPat.t, t); +| TyVar(VarErrStatus.t, Var.t) + ``` + + A type pattern is the part of the language between the `forall` and the `.` + in `forall a. `. Type patterns will be very simple to begin with: + + ```reason + /* TPat.t */ + type t = + | Hole(MetaVar.t) +| Var(Var.t) + ``` + + + +# Expression Language + + ```reason + /* UHExp.t */ + type operand = + ... + | TyLam(TPat.t, block) +| TyVar(TPat.t) + ``` + +# Construct actions + + We'll be adding the following to `Construct(shape)`: + + ``` + type shape = + ... + | SForall + | SType + ``` + + `Construct(SForall)` will be triggered when the user types "forall" followed by + 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(SType)` will be triggered when the user types "type" followed by a + space in an expression hole. This will add a `TyVar.t` in the expression with a + type pattern hole. + +# Concrete Syntax / Representation + + Forall's appear within types and look like: `forall a. ?`, where `a` is + a TyVar.t. + + There are Type Vars types and expressions. Type Vars in types appear as a + string of lowercase letter without any prefix or constructor. Type Vars in + expressions appear as `(type a)` where `a` is also a string of lowercase + letters. + + Type Lambdas are written like a lambda: you start with `\`. Then you write + "type" followed by a space which will construct a type lambda. If however, you + type `type` into an existing lambda that has a non-empty type + annotation, the pattern of the lambda will be put into an error state until + either you delete the space following "type" or the type annotation. The final + representation is `λ(type a).{ }. + +# Backspace actions + + What happens when you press backspace at the following positions? (`|` + represents the cursor.) I don't fully understand how this works visual + indicators. Any backspace that does not change the tree or the cursor + but only changes the visual indicator is not taken into account here. + +## Forall + + * `forall| a. body` or `forall a.| body` + + Either of these remove the `forall a.` prefix and leave just the body. + + * `forall a|. type + + If the type variable is a single character, replace the type variable with a TyPat.Hole, + otherwise remove the last character of the type variable. + + * `forall a. type|` + + If the body is not a type hole, this forwards the backspace action onto the + body, leaving the forall untouched. However, if the body is a type hole, this + removes the whole type, leaving only a type hole. + +## Type Vars + + * `(type| a)` or `(type a)|` + + The entire expression is replaced with a hole. + + * `(type |a)` + + The cursor is moved to `(type| a)`. + + * `(type a|)` + + If the type variable is a single character, replace the type variable with a TyPat.Hole, + otherwise remove the last character of the type variable. + +## Type Lambdas + + * `λ.|(type a) { body }` or `λ(|type a) { body }` or `λ(type a)| { body }` + + The lambda is removed, leaving just `|body`. + + * `λ(type| a) { body }` + + The type lambda is reverted to a normal lambda with a type hole: `λ(? : ?) + + * `λ(type |a) { body }` + + + The cursor is moved back to `λ(type| a) { body }` + + * `λ(type a|) { body }` + * `λ(type a|) { body }` + +# Movement actions + + The semantics of MoveRight and MoveLeft should be clear based on the cursor + positions mentioned in the "Backspace actions" section above. + + From 988cb65c737003275a67ead237dff5fdef0df473 Mon Sep 17 00:00:00 2001 From: Charles Chamberlain Date: Sat, 9 May 2020 17:40:17 -0400 Subject: [PATCH 2/4] Rename to 3 and address some comments --- .../3-explicit-polymorphism.md | 64 +++++++++++-------- 1 file changed, 37 insertions(+), 27 deletions(-) rename 2-explicit-polymorphism/2-explicit-polymorphism.md => 3-explicit-polymorphism/3-explicit-polymorphism.md (69%) diff --git a/2-explicit-polymorphism/2-explicit-polymorphism.md b/3-explicit-polymorphism/3-explicit-polymorphism.md similarity index 69% rename from 2-explicit-polymorphism/2-explicit-polymorphism.md rename to 3-explicit-polymorphism/3-explicit-polymorphism.md index af1602e..4ce0d40 100644 --- a/2-explicit-polymorphism/2-explicit-polymorphism.md +++ b/3-explicit-polymorphism/3-explicit-polymorphism.md @@ -4,7 +4,7 @@ Currently in Hazel every function has to be assigned a monomorphic type. This makes it impossible to write code that operates on more than one type of data. We currently have an example that implements `map : (Num -> Num) -> [Num] -> [Num]`. By adopting this proposal, Hazel's map function can -have the type `forall a. (a -> a) -> [a] -> [a]`, and thereby be useful for +have the type `forall a. forall b. (a -> b) -> [a] -> [b]`, and thereby be useful for a larger set of values. Specifically, we propose extending Hazel with two type constructs @@ -15,13 +15,13 @@ a System F with holes than a Simply Typed Lambda Calculus with holes. We'd have to extend UHTyp.t with `TyVar` and `Forall` cases: -```reason -/* UHTyp.re */ - -type operand = -... -| Forall(TPat.t, t); -| TyVar(VarErrStatus.t, Var.t) + ```reason + /* UHTyp.re */ + + type operand = + ... + | Forall(TPat.t, t); + | TyVar(VarErrStatus.t, Var.t) ``` A type pattern is the part of the language between the `forall` and the `.` @@ -31,7 +31,7 @@ type operand = /* TPat.t */ type t = | Hole(MetaVar.t) -| Var(Var.t) + | Var(Var.t) ``` @@ -43,26 +43,26 @@ type operand = type operand = ... | TyLam(TPat.t, block) -| TyVar(TPat.t) + | TyArg(UHTyp.t) ``` # Construct actions We'll be adding the following to `Construct(shape)`: - ``` + ```reason type shape = ... | SForall - | SType + | STyArg ``` `Construct(SForall)` will be triggered when the user types "forall" followed by 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(SType)` will be triggered when the user types "type" followed by a - space in an expression hole. This will add a `TyVar.t` in the expression with a + `Construct(STyArg)` will be triggered when the user types "type" followed by a + space in an expression hole. This will add a `STyArg.t` in the expression with a type pattern hole. # Concrete Syntax / Representation @@ -70,17 +70,18 @@ type operand = Forall's appear within types and look like: `forall a. ?`, where `a` is a TyVar.t. - There are Type Vars types and expressions. Type Vars in types appear as a - string of lowercase letter without any prefix or constructor. Type Vars in - expressions appear as `(type a)` where `a` is also a string of lowercase - letters. + Type vars in types appear as a string of lowercase letter without any prefix + or constructor. + + Type Vars in expressions appear as `(type a)` where `a` is also a string of + lowercase letters. Type Lambdas are written like a lambda: you start with `\`. Then you write "type" followed by a space which will construct a type lambda. If however, you type `type` into an existing lambda that has a non-empty type annotation, the pattern of the lambda will be put into an error state until either you delete the space following "type" or the type annotation. The final - representation is `λ(type a).{ }. + representation is `λ a:type.{ }`. # Backspace actions @@ -123,21 +124,30 @@ type operand = ## Type Lambdas - * `λ.|(type a) { body }` or `λ(|type a) { body }` or `λ(type a)| { body }` + * `λ |a:type. { body }` or `λ ?|:type. { body }` or `λ a:type. { |body }` or `λ a:type. { body }|` + + + The type lambda is removed, leaving just `|body` + + * `λ a|:type. { body }` - The lambda is removed, leaving just `|body`. + One character is removed from the type variable "a". If it's only one char, + we're left with `λ ?|:type. { body }` - * `λ(type| a) { body }` + * `λ a:|type. { body }` - The type lambda is reverted to a normal lambda with a type hole: `λ(? : ?) + The cursor is moved back to `λ a|:type. { body }`. - * `λ(type |a) { body }` + * `λ a:type|. { body }` + The type lambda is converted to the normal lambda `λ a:typ|. { body }`. + Similarly, typing "d" at this cursor position should render a normal lambda + with the type annotation "typed". - The cursor is moved back to `λ(type| a) { body }` + * `λ a:type. { body| }` - * `λ(type a|) { body }` - * `λ(type a|) { body }` + Any backspaces here are forwarded the body unless the body is a hole, in + which case, backspace deletes the whole expression, leaving just a hole. # Movement actions From c0b7f8fa62bd39941c33fdb60fe3c133a1fbdd30 Mon Sep 17 00:00:00 2001 From: Charles Chamberlain Date: Sat, 9 May 2020 17:45:17 -0400 Subject: [PATCH 3/4] Describe type arg accurately --- 3-explicit-polymorphism/3-explicit-polymorphism.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/3-explicit-polymorphism/3-explicit-polymorphism.md b/3-explicit-polymorphism/3-explicit-polymorphism.md index 4ce0d40..83d3ab4 100644 --- a/3-explicit-polymorphism/3-explicit-polymorphism.md +++ b/3-explicit-polymorphism/3-explicit-polymorphism.md @@ -17,7 +17,7 @@ We'd have to extend UHTyp.t with `TyVar` and `Forall` cases: ```reason /* UHTyp.re */ - + type operand = ... | Forall(TPat.t, t); @@ -73,8 +73,7 @@ We'd have to extend UHTyp.t with `TyVar` and `Forall` cases: Type vars in types appear as a string of lowercase letter without any prefix or constructor. - Type Vars in expressions appear as `(type a)` where `a` is also a string of - lowercase letters. + Type Arg expressions appear as `(type TYPE)`, where TYPE is any type. Type Lambdas are written like a lambda: you start with `\`. Then you write "type" followed by a space which will construct a type lambda. If however, you @@ -126,7 +125,7 @@ We'd have to extend UHTyp.t with `TyVar` and `Forall` cases: * `λ |a:type. { body }` or `λ ?|:type. { body }` or `λ a:type. { |body }` or `λ a:type. { body }|` - + The type lambda is removed, leaving just `|body` * `λ a|:type. { body }` From 2f9fe026cd0dc4e9ca8931ffe8961a1873a6e3b8 Mon Sep 17 00:00:00 2001 From: Charles Chamberlain Date: Sat, 9 May 2020 17:47:20 -0400 Subject: [PATCH 4/4] Reword backspace on a type argument --- 3-explicit-polymorphism/3-explicit-polymorphism.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/3-explicit-polymorphism/3-explicit-polymorphism.md b/3-explicit-polymorphism/3-explicit-polymorphism.md index 83d3ab4..3b53b7f 100644 --- a/3-explicit-polymorphism/3-explicit-polymorphism.md +++ b/3-explicit-polymorphism/3-explicit-polymorphism.md @@ -106,7 +106,7 @@ We'd have to extend UHTyp.t with `TyVar` and `Forall` cases: body, leaving the forall untouched. However, if the body is a type hole, this removes the whole type, leaving only a type hole. -## Type Vars +## Type Args * `(type| a)` or `(type a)|` @@ -118,8 +118,8 @@ We'd have to extend UHTyp.t with `TyVar` and `Forall` cases: * `(type a|)` - If the type variable is a single character, replace the type variable with a TyPat.Hole, - otherwise remove the last character of the type variable. + Any backspace is treated as a backspace on the HTyp.t, represented by `a` here. + It's possible to get a TPat.Hole as a result of this backspace. ## Type Lambdas