1 | | = Syntax for explicit type and kind application = |
| 1 | = Syntax for explicit kinds, new story = |
| 2 | |
| 3 | When working with kind polymorphism and promotion we often want to |
| 4 | specify kinds independently of types. In fact, we might not even be |
| 5 | interested in the types, only in kinds. This is fine in FC-pro, but |
| 6 | we need syntax to express it in source Haskell. We propose to allow |
| 7 | choosing at the definition site to either: |
| 8 | |
| 9 | a. give explicit kind parameters, or |
| 10 | b. infer kind parameters |
| 11 | |
| 12 | If you choose (a) you must always give explicit kind arguments. |
| 13 | If you choose (b) you cannot ever give explicit kind arguments. |
| 14 | |
| 15 | == Examples == |
| 16 | |
| 17 | (b) above is the current behaviour; you can only specify kinds by |
| 18 | annotating types: |
| 19 | {{{ |
| 20 | type family App (f :: k1 -> k2) (a :: k1) :: k2 |
| 21 | }}} |
| 22 | |
| 23 | We typically want to use (a) when we are not interested in types, only kinds. |
| 24 | For instance, in the `Sing` family of the |
| 25 | [https://github.com/ghc/packages-base/blob/master/GHC/TypeLits.hs type-level literals module]: |
| 26 | {{{ |
| 27 | data family Sing (k :: ☐) |
| 28 | |
| 29 | newtype instance Sing Nat = SNat Integer |
| 30 | newtype instance Sing Symbol = SSym String |
| 31 | }}} |
| 32 | |
| 33 | Note that `Nat` and `Symbol` above are '''kinds'''. |
| 34 | |
| 35 | Explicit kind arguments can also be used in type classes, and function type |
| 36 | signatures: |
| 37 | {{{ |
| 38 | class SingE (k :: ☐) where |
| 39 | type SingRep (k :: ☐) :: * |
| 40 | fromSing :: Sing (k :: ☐) -> SingRep (k :: ☐) |
| 41 | |
| 42 | instance SingE Nat where |
| 43 | type SingRep Nat = Integer |
| 44 | fromSing (SNat n) = n |
| 45 | |
| 46 | instance SingE Symbol where |
| 47 | type SingRep Symbol = String |
| 48 | fromSing (SSym s) = s |
| 49 | }}} |
| 50 | |
| 51 | '''Question: ''' do we want/need explicit kind arguments at the value level? |
| 52 | |
| 53 | == How to distinguish kind variables == |
| 54 | |
| 55 | In the examples above we have used the `k :: ☐` notation to indicate that `k` |
| 56 | is a kind variable. We do not want to require unicode usage for this, so we |
| 57 | propose either: |
| 58 | |
| 59 | 1. `k :: BOX`, or |
| 60 | 2. `@k` |
| 61 | |
| 62 | (1) makes `BOX` a reserved name. (2) does not require reserving any names, but |
| 63 | will not work on value-level patterns, since it can be confused with an |
| 64 | at-pattern. (However, see below for a possible solution to this problem.) |
| 65 | |
| 66 | = Syntax for explicit type and kind application, old story = |
| 67 | |
| 68 | We now describe a more general proposal that allows explicit type and kind application, but is better |
| 69 | suited for specifying arguments at the call site. This makes it easier to work with impredicative |
| 70 | polymorphism, but not with kind families, for instance. |