Changes between Version 11 and Version 12 of ExplicitTypeApplication

May 15, 2012 9:29:26 AM (5 years ago)

New story for explicit kinds


  • ExplicitTypeApplication

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