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