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