Changes between Version 8 and Version 9 of GhcKinds/KindPolymorphism
 Timestamp:
 Aug 31, 2011 1:55:53 PM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

GhcKinds/KindPolymorphism
v8 v9 1 1 == 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.4 2 5 3 Implicit foralls are added by the renamer. Kind generalization (adding more kind foralls) is done by the type checker. … … 8 6 9 7 Rules: 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: 11 9 * no implicit foralls even for kind variables 12 10 * no kind generalization, which means defaulting flexi meta kind variables to `*` … … 33 31  forall k (f :: * > *) (a :: *). f a > Int 34 32 35 f7 :: forall k f (a :: k). f a > Int  forall k (f :: k > *) (a :: k). f a > Int 33 f7 :: forall k f (a :: k). f a > Int  forall k (f :: k > *) (a :: k). f a > Int 34 36 35 f8 :: forall k. forall f (a :: k). f a > Int  forall k (f :: k > *) (a :: k). f a > Int 36 37 37 38 38 g1 :: (f a > Int) > Int  forall (f :: k > *) (a :: k). (f a > Int) > Int … … 55 55 Rules: 56 56 * Any explicit kind variables are generalized over 57 * Defaulting for flexi meta kind variables57 * We kind generalize flexi meta kind variables when possible 58 58 59 59 We 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. … … 66 66 {{{ 67 67 class 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 b68 foo1 :: f (g a) > (f :: k1 > *) b  forall (a :: k2) (b :: k1). f (g a) > f b 69 69  Note that k1 and k2 scope over the type signatures 70 70  just as f and g do. 71 71 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 72 class C2 f g where  Same as C1 73 foo2 :: f (g a) > f b  Same as foo1 75 74 76 class C3 (f :: k1 > *) g where  forall k1. (k1 > *) > (* > k1) > Constraint77 foo :: f (g a) > f b  forall (a :: k1) (b :: *) > f (g a) > f b75 class C3 (f :: k1 > *) g where  Same as C1 76 foo3 :: f (g a) > f b  Same as foo1 78 77 }}} 79 78 … … 84 83 Foo1 :: s a > T1 s as > T1 s (a ': as)  forall k (s :: k > *) (a :: k) (as :: [k]). 85 84  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 87 86 88 87 data T2 s (as :: [k]) where  Same as T1 89 88 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 91 data 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 91 95 }}} 92 96 … … 96 100 97 101 {{{ 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. 99 103 type family F1 (b :: Bool) (true :: k) (false :: k) :: k  F1 :: forall k. Bool > k > k > k 100 104 … … 109 113 110 114 {{{ 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) > * 115 type S1 f g  forall k1 k2. (k1 > *) > (k2 > k1) > * 118 116 = forall a. f (g a)  = forall (a :: k2). f (g a) 119 117 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) 118 type S2 (f :: k1 > *) g  Same as S1 119 = forall a. f (g a)  Same as S1 120 121 type S3 (f :: k1 > *) (g :: k2 > k1)  Same as S1 122 = forall a. f (g a)  Same as S1 123 124 type S4 f (g :: * > *)  (* > *) > (* > *) > * 125 = forall a. f (g a)  = forall (a :: *). f (g a) 122 126 }}} 123 127