Changes between Version 11 and Version 12 of ExplicitTypeApplication


Ignore:
Timestamp:
May 15, 2012 9:29:26 AM (3 years ago)
Author:
dreixel
Comment:

New story for explicit kinds

Legend:

Unmodified
Added
Removed
Modified
  • ExplicitTypeApplication

    v11 v12  
    1 = Syntax for explicit type and kind application = 
     1= Syntax for explicit kinds, new story = 
     2 
     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: 
     8 
     9 a. give explicit kind parameters, or 
     10 b. infer kind parameters 
     11 
     12If you choose (a) you must always give explicit kind arguments. 
     13If 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 
     18annotating types: 
     19{{{ 
     20type family App (f :: k1 -> k2) (a :: k1) :: k2 
     21}}} 
     22 
     23We typically want to use (a) when we are not interested in types, only kinds. 
     24For instance, in the `Sing` family of the 
     25[https://github.com/ghc/packages-base/blob/master/GHC/TypeLits.hs type-level literals module]: 
     26{{{ 
     27data family Sing (k :: ☐) 
     28 
     29newtype instance Sing Nat    = SNat Integer 
     30newtype instance Sing Symbol = SSym String 
     31}}} 
     32 
     33Note that `Nat` and `Symbol` above are '''kinds'''. 
     34 
     35Explicit kind arguments can also be used in type classes, and function type 
     36signatures: 
     37{{{ 
     38class SingE (k :: ☐) where 
     39  type SingRep (k :: ☐) :: * 
     40  fromSing :: Sing (k :: ☐) -> SingRep (k :: ☐) 
     41 
     42instance SingE Nat where 
     43  type SingRep Nat = Integer 
     44  fromSing (SNat n) = n 
     45 
     46instance 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 
     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: 
     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 
     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.)  
     65 
     66= Syntax for explicit type and kind application, old story = 
     67 
     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. 
    271 
    372We propose a replacement and generalisation of [http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#scoped-type-variables lexically-scoped type variables] (and pattern signatures) that is