Changes between Version 2 and Version 3 of GhcKinds/KindPolymorphism
 Timestamp:
 Aug 31, 2011 9:54:35 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

GhcKinds/KindPolymorphism
v2 v3 50 50 === In kinds === 51 51 52 The story is more complicated since we have several ways of talking about kinds: data types, type classes, type families, and type synonyms. 52 Rules: 53 * Any explicit kind variables are generalized over 54 * Defaulting for flexi meta kind variables 53 55 54 We need a notion of large scoping, which means that a variable in the signature can bind in the where clause. 56 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. 55 57 56 58 ==== Type classes ==== 57 59 58 Rules:60 Additionnal rules: 59 61 * 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 over61 * Defaulting for flexi meta kind variables62 62 63 63 {{{ … … 75 75 ==== Data types ==== 76 76 77 Rules:78 * No large scoping79 * Any explicit kind variables are generalized over80 * Defaulting for flexi meta kind variables81 82 77 {{{ 83 78 data T1 s as where  (* > *) > [*] > * … … 88 83 }}} 89 84 85 ==== Type families ==== 86 87 Last rule becomes: Any missing kind signature defaults to `*` 88 89 {{{ 90  Note (nothing to do with kind polymorphism): we might want to say that only the Bool is an index. 91 type family F1 (b :: Bool) (true :: k) (false :: k) :: k  F1 :: forall k. Bool > k > k > k 92 93 type family F2 b true false  F2 :: * > * > * > * 94 95 type family F3 b (true :: k) false  F3 :: forall k. * > k > * > * 96 }}} 97 98 For type families it just doesn't make any sense to not write the whole kind signature, since there is no inference at all. 99 100 ==== Type synonyms ==== 101 102 {{{ 103 type S1 f g  (* > *) > (* > *) > * 104 = forall a. f (g a)  = forall (a :: *). f (g a) 105 106 type S2 (f :: k1 > *) g  forall k1. (k1 > *) > (* > k1) > * 107 = forall a. f (g a)  = forall (a :: *). f (g a) 108 109 type S3 (f :: k1 > *) (g :: k2 > k1)  forall k1 k2. (k1 > *) > (k2 > k1) > * 110 = forall a. f (g a)  = forall (a :: k2). f (g a) 111 112 type S4 f (g :: k2 > k1)  forall k1 k2. (k1 > *) > (k2 > k1) > * 113 = forall a. f (g a)  = forall (a :: k2). f (g a) 114 }}} 115