Changes between Version 8 and Version 9 of GhcKinds/KindPolymorphism


Ignore:
Timestamp:
Aug 31, 2011 1:55:53 PM (4 years ago)
Author:
ia0
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds/KindPolymorphism

    v8 v9  
    11== Design of Kind Polymorphism ==
    2 
    3 This is a simple proposal, that would allow us to do better later, but still allow us to go on step 3.
    42
    53Implicit foralls are added by the renamer. Kind generalization (adding more kind foralls) is done by the type checker.
     
    86
    97Rules:
    10   * When there is an explicit forall, we don't add any foralls, which means:
     8  * When there is an explicit `forall`, we don't add any foralls, which means:
    119    * no implicit foralls even for kind variables
    1210    * no kind generalization, which means defaulting flexi meta kind variables to `*`
     
    3331                                       -- forall k (f :: * -> *) (a :: *). f a -> Int
    3432
    35 f7 :: forall k f (a :: k). f a -> Int           -- forall k (f :: k -> *) (a :: k). f a -> Int
     33f7 :: forall k f (a :: k). f a -> Int          -- forall k (f :: k -> *) (a :: k). f a -> Int
     34
    3635f8 :: forall k. forall f (a :: k). f a -> Int  -- forall k (f :: k -> *) (a :: k). f a -> Int
     36
    3737
    3838g1 :: (f a -> Int) -> Int                      -- forall (f :: k -> *) (a :: k). (f a -> Int) -> Int
     
    5555Rules:
    5656  * Any explicit kind variables are generalized over
    57   * Defaulting for flexi meta kind variables
     57  * We kind generalize flexi meta kind variables when possible
    5858
    5959We 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.
     
    6666{{{
    6767class C1 (f :: k1 -> *) (g :: k2 -> k1) where  -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> Constraint
    68   foo :: f (g a) -> (f :: k1 -> *) b           -- forall (a :: k2) (b :: k1). f (g a) -> f b
     68  foo1 :: f (g a) -> (f :: k1 -> *) b          -- forall (a :: k2) (b :: k1). f (g a) -> f b
    6969          -- Note that k1 and k2 scope over the type signatures
    7070          -- just as f and g do.
    7171
    72 -- C2 looks much easier with defaulting
    73 class C2 f g where                             -- (* -> *) -> (* -> *) -> Constraint
    74   foo :: f (g a) -> f b                        -- forall (a :: *) (b :: *). f (g a) -> f b
     72class C2 f g where                             -- Same as C1
     73  foo2 :: f (g a) -> f b                       -- Same as foo1
    7574
    76 class C3 (f :: k1 -> *) g where                -- forall k1. (k1 -> *) -> (* -> k1) -> Constraint
    77   foo :: f (g a) -> f b                        -- forall (a :: k1) (b :: *) -> f (g a) -> f b
     75class C3 (f :: k1 -> *) g where                -- Same as C1
     76  foo3 :: f (g a) -> f b                       -- Same as foo1
    7877}}}
    7978
     
    8483  Foo1 :: s a -> T1 s as -> T1 s (a ': as)  -- forall k (s :: k -> *) (a :: k) (as :: [k]).
    8584                                            --   s a -> T1 k s as -> T1 k s ((':) k a as)
    86     -- Note that s,a do not scope over the declaration of Foo
     85    -- Note that s,a do not scope over the declaration of Foo1
    8786
    8887data T2 s (as :: [k]) where                 -- Same as T1
    8988  Foo2 : s a -> T1 s as -> T1 s (a ': as)   -- Same as Foo1
    90     -- Note that s,as,k do not scope over the declaration of Foo
     89    -- Note that s,as,k do not scope over the declaration of Foo2
     90
     91data T3 s (as :: [*]) where                 -- (* -> *) -> [*] -> *
     92  Foo3 : s a -> T1 s as -> T1 s (a ': as)   -- forall (s :: * -> *) (a :: *) (as :: [*]).
     93                                            --   s a -> T1 s as -> T1 s ((':) * a as)
     94    -- Note that s,as do not scope over the declaration of Foo2
    9195}}}
    9296
     
    96100
    97101{{{
    98 -- Note (nothing to do with kind polymorphism): we might want to say that only the Bool is an index.
     102-- Note (nothing to do with kind polymorphism) that we might want to say that only the Bool is an index.
    99103type family F1 (b :: Bool) (true :: k) (false :: k) :: k  -- F1 :: forall k. Bool -> k -> k -> k
    100104
     
    109113
    110114{{{
    111 type S1 f g                             -- (* -> *) -> (* -> *) -> *
    112   = forall a. f (g a)                   -- = forall (a :: *). f (g a)
    113 
    114 type S2 (f :: k1 -> *) g                -- forall k1. (k1 -> *) -> (* -> k1) -> *
    115   = forall a. f (g a)                   -- = forall (a :: *). f (g a)
    116 
    117 type S3 (f :: k1 -> *) (g :: k2 -> k1)  -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> *
     115type S1 f g                             -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> *
    118116  = forall a. f (g a)                   -- = forall (a :: k2). f (g a)
    119117
    120 type S4 f (g :: k2 -> k1)               -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> *
    121   = forall a. f (g a)                   -- = forall (a :: k2). f (g a)
     118type S2 (f :: k1 -> *) g                -- Same as S1
     119  = forall a. f (g a)                   -- Same as S1
     120
     121type S3 (f :: k1 -> *) (g :: k2 -> k1)  -- Same as S1
     122  = forall a. f (g a)                   -- Same as S1
     123
     124type S4 f (g :: * -> *)                 -- (* -> *) -> (* -> *) -> *
     125  = forall a. f (g a)                   -- = forall (a :: *). f (g a)
    122126}}}
    123127