... | ... | @@ -6,15 +6,35 @@ This page is to track the design of a plan, originally Simon PJ's idea, to get r |
|
|
|
|
|
Right now, there are several "base" kinds:
|
|
|
|
|
|
`*`: The kind of lifted, boxed types. That is, types of kind `*` are represented with a pointer and capable of being bottom.
|
|
|
- `*`: The kind of lifted, boxed types. That is, types of kind `*` are represented with a pointer and capable of being bottom.
|
|
|
|
|
|
`#`: The kind of unlifted types. Types of this kind cannot be bottom. (Some \[arrays\] are still represented with a pointer.)
|
|
|
- `#`: The kind of unlifted types. Types of this kind cannot be bottom. Most unlifted types are unboxed, e.g. `Int#`, `Double#`; but some are boxed (represented with a heap pointer), e.g. `Array#`.
|
|
|
|
|
|
`Constraint`: The kind of Haskell constraints. Rather annoyingly, it is important that Core treat `Constraint` and `*` as indistinguishable. So, `tcEqType` considers `Constraint` and `*` distinct (as they are distinct in Haskell) but `eqType` considers them to be equal.
|
|
|
- `Constraint`: The kind of Haskell constraints. Rather annoyingly,
|
|
|
|
|
|
`OpenKind`: The superkind of `*` and `#`. The existence of `OpenKind` is necessary to give a kind to `(->)`, which is `OpenKind -> OpenKind -> *`. It also classifies `error :: forall (a :: OpenKind). String -> a` and `undefined :: forall (a :: OpenKind). a`.
|
|
|
- During type checking `*` and `Constraint` must be distinct kinds; so that a signature `f :: Int => Int` is rejected.
|
|
|
- In Core, it is important to treat `Constraint` and `*` as indistinguishable. **SLPJ** why? It used to be the case because GND cast dictionaries, but we don't do that any more.
|
|
|
|
|
|
`BOX`: This classifies kinds. Thus, we have `* :: BOX` and `# :: BOX`. Somewhat cheekily, `BOX :: BOX`.
|
|
|
>
|
|
|
> So, `tcEqType` considers `Constraint` and `*` distinct (as they are distinct in Haskell) but `eqType` considers them to be equal.
|
|
|
|
|
|
- `OpenKind`: The superkind of `*` and `#`. The existence of `OpenKind` is necessary for several reasons
|
|
|
|
|
|
- To give a kind to `(->)`, which is `OpenKind -> OpenKind -> *`. **SLPJ** False. We actually give `(->)` kind `*->*->*`, but have a special kinding rule for saturated applications of `(->)`.
|
|
|
- To give a type to `error :: forall (a :: OpenKind). String -> a` and `undefined :: forall (a :: OpenKind). a`. We need to allow `error Int# "foo" :: Int#`.
|
|
|
- During inference, to give a kind to lambda-bound variables. E.g. `\x -> 3# +# x`. When we encounter the lambda we give it a type of `alpha`, a unification variable. But what kind does `alpha` have? Not `*`, else this lambda would be rejected. So we give it `OpenKind`.
|
|
|
|
|
|
- `BOX`: This classifies kinds. Thus, we have `* :: BOX` and `# :: BOX`. Somewhat cheekily, `BOX :: BOX`.
|
|
|
|
|
|
|
|
|
The entire handling of `OpenKind` is unsatisfactory. For example, it is not abstractable:
|
|
|
|
|
|
```wiki
|
|
|
myError s = error ("Blah" ++ s)
|
|
|
```
|
|
|
|
|
|
|
|
|
Currently `myError` cannot be used at type `Int#`.
|
|
|
|
|
|
## Down with kinds
|
|
|
|
... | ... | @@ -39,8 +59,8 @@ Then, we create a new magical constant `TYPE`, of type `Levity -> TYPE Lifted`. |
|
|
|
|
|
```wiki
|
|
|
(->) :: forall (l1 :: Levity) (l2 :: Levity). TYPE l1 -> TYPE l2 -> TYPE Lifted
|
|
|
error :: forall (l :: Levity). String -> TYPE l
|
|
|
undefined :: forall (l :: Levity). TYPE l
|
|
|
error :: forall (l :: Levity) (a :: TYPE l). String -> a
|
|
|
undefined :: forall (l :: Levity) (a :: TYPE l). a
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -55,4 +75,14 @@ type # = TYPE Unlifted |
|
|
and hope that GHC's existing preserve-type-synonyms-wherever-possible machinery keeps messages reasonable.
|
|
|
|
|
|
|
|
|
Note that `myError` would get a natural inferred type
|
|
|
|
|
|
```wiki
|
|
|
myError :: forall (l :: Levity) (a :: TYPE l). String -> a
|
|
|
```
|
|
|
|
|
|
|
|
|
Whether users could write down such a signature is another matter. (They probably should be able to.)
|
|
|
|
|
|
|
|
|
Note that this proposal does not address the `Constraint` / `*` infelicity -- that is a separate problem. |