Changes between Version 1 and Version 2 of GhcKinds/KindPolymorphism


Ignore:
Timestamp:
Aug 31, 2011 9:40:50 AM (3 years ago)
Author:
ia0
Comment:

type classes + data types

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds/KindPolymorphism

    v1 v2  
    11== Design of Kind Polymorphism == 
     2 
     3This is a simple proposal, that would allow us to do better later, but still allow us to go on step 3. 
    24 
    35Implicit foralls are added by the renamer. Kind generalization (adding more kind foralls) is done by the type checker. 
     
    4143g5 :: (forall f (a :: k). f a -> Int) -> Int   -- Not in scope: kind variable `k' 
    4244 
     45 
     46h :: forall k f (a :: k). f a -> Int 
     47h x = ...k...f a...  -- k, f, and a are in scope 
    4348}}} 
     49 
     50=== In kinds === 
     51 
     52The story is more complicated since we have several ways of talking about kinds: data types, type classes, type families, and type synonyms. 
     53 
     54We need a notion of large scoping, which means that a variable in the signature can bind in the where clause. 
     55 
     56==== Type classes ==== 
     57 
     58Rules: 
     59  * 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 
     62 
     63{{{ 
     64class C1 (f :: k1 -> *) (g :: k2 -> k1) where  -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> Constraint 
     65  foo :: f (g a) -> f b                        -- forall (a :: k2) (b :: k1). f (g a) -> f b 
     66 
     67-- C2 looks much easier with defaulting 
     68class C2 f g where                             -- (* -> *) -> (* -> *) -> Constraint 
     69  foo :: f (g a) -> f b                        -- forall (a :: *) (b :: *). f (g a) -> f b 
     70 
     71class C3 (f :: k1 -> *) g where                -- forall k1. (k1 -> *) -> (* -> k1) -> Constraint 
     72  foo :: f (g a) -> f b                        -- forall (a :: k1) (b :: *) -> f (g a) -> f b 
     73}}} 
     74 
     75==== Data types ==== 
     76 
     77Rules: 
     78  * No large scoping 
     79  * Any explicit kind variables are generalized over 
     80  * Defaulting for flexi meta kind variables 
     81 
     82{{{ 
     83data T1 s as where                         -- (* -> *) -> [*] -> * 
     84  Foo :: s a -> T1 s as -> T1 s (a ': as)  -- forall (s :: * -> *) (a :: *) (as :: [*]). the same 
     85 
     86data T1 s (as :: [k]) where                -- forall k. (k -> *) -> [k] -> * 
     87  Foo : s a -> T1 s as -> T1 s (a ': as)   -- forall k (s :: k -> *) (a :: k) (as :: [k]). the same where `T1' becomes `T1 k' 
     88}}} 
     89