Changes between Version 1 and Version 2 of GhcKinds/KindPolymorphism


Ignore:
Timestamp:
Aug 31, 2011 9:40:50 AM (4 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