Changes between Version 2 and Version 3 of GhcKinds/KindPolymorphism


Ignore:
Timestamp:
Aug 31, 2011 9:54:35 AM (4 years ago)
Author:
ia0
Comment:

type families + type synonyms

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds/KindPolymorphism

    v2 v3  
    5050=== In kinds === 
    5151 
    52 The story is more complicated since we have several ways of talking about kinds: data types, type classes, type families, and type synonyms. 
     52Rules: 
     53  * Any explicit kind variables are generalized over 
     54  * Defaulting for flexi meta kind variables 
    5355 
    54 We need a notion of large scoping, which means that a variable in the signature can bind in the where clause. 
     56We need a notion of large scoping, which means that a variable in the signature can bind in the where clause. Only type classes have large scoping. 
    5557 
    5658==== Type classes ==== 
    5759 
    58 Rules: 
     60Additionnal rules: 
    5961  * Large scoping: any type or kind variables appearing on left or right side of a `::` in the signature is brought into scope 
    60   * Any explicit kind variables are generalized over 
    61   * Defaulting for flexi meta kind variables 
    6262 
    6363{{{ 
     
    7575==== Data types ==== 
    7676 
    77 Rules: 
    78   * No large scoping 
    79   * Any explicit kind variables are generalized over 
    80   * Defaulting for flexi meta kind variables 
    81  
    8277{{{ 
    8378data T1 s as where                         -- (* -> *) -> [*] -> * 
     
    8883}}} 
    8984 
     85==== Type families ==== 
     86 
     87Last rule becomes: Any missing kind signature defaults to `*` 
     88 
     89{{{ 
     90-- Note (nothing to do with kind polymorphism): we might want to say that only the Bool is an index. 
     91type family F1 (b :: Bool) (true :: k) (false :: k) :: k  -- F1 :: forall k. Bool -> k -> k -> k 
     92 
     93type family F2 b true false                               -- F2 :: * -> * -> * -> * 
     94 
     95type family F3 b (true :: k) false                        -- F3 :: forall k. * -> k -> * -> * 
     96}}} 
     97 
     98For type families it just doesn't make any sense to not write the whole kind signature, since there is no inference at all. 
     99 
     100==== Type synonyms ==== 
     101 
     102{{{ 
     103type S1 f g                             -- (* -> *) -> (* -> *) -> * 
     104  = forall a. f (g a)                   -- = forall (a :: *). f (g a) 
     105 
     106type S2 (f :: k1 -> *) g                -- forall k1. (k1 -> *) -> (* -> k1) -> * 
     107  = forall a. f (g a)                   -- = forall (a :: *). f (g a) 
     108 
     109type S3 (f :: k1 -> *) (g :: k2 -> k1)  -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> * 
     110  = forall a. f (g a)                   -- = forall (a :: k2). f (g a) 
     111 
     112type S4 f (g :: k2 -> k1)               -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> * 
     113  = forall a. f (g a)                   -- = forall (a :: k2). f (g a) 
     114}}} 
     115