Changes between Version 7 and Version 8 of PolymorphicKinds


Ignore:
Timestamp:
Oct 17, 2008 3:07:03 PM (6 years ago)
Author:
TristanAllwood
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • PolymorphicKinds

    v7 v8  
    11= Polymorphic Kinds for Haskell = 
    22 
    3 Currently thinking about adding '''Polymorphic Kinds''' to GHC... 
    4 (Currently very WIP) 
     3Currently thinking about adding '''Polymorphic Kinds''' to GHC ... this document is a WIP 
     4 
     5This is strongly motivated by wanting to add a new KindSystem, but does not require it.   
     6See KindSystem for a discussion of the syntax of sorts (which classify kinds). 
    57 
    68== Example: At the term level == 
     
    5456instance (Typeable (t1 :: (* -> *),  
    5557          Typeable (t2 :: *))) => Typeable (t1 t2) where 
    56   typeOf _ = (typeOf (undefined :: t1)) `mkAppTy` (typeOf (undefined :: t2)) 
     58  typeOf _ = (typeOf (undefined :: Proxy t1)) `mkAppTy` (typeOf (undefined :: Proxy t2)) 
    5759}}} 
    5860 
     
    156158 
    157159{{{ 
    158 class Blah :: forall k . (k -> *) -> ??? where 
     160class Blah :: forall k . (k -> *) -> CLASS where 
    159161}}} 
    160  
    161  
    162 == Type functions == 
    163  
    164 Follow as per type classes 
    165  
    166  
    167 == Syntax of Kinds == 
    168  
    169 {{{ 
    170 kind ::=  * | # | ? | (kind) | kind -> kind |  
    171           ty :=: ty | forall var . kind | var 
    172 }}} 
    173  
    174 == Syntax of Types == 
    175  
    176 Type syntax needs to be extended with a new binder. 
    177  
    178  
    179 == Implementation route == 
    180  
    181 Places that would be hit (TODO): 
    182  
    183 * Parser 
    184   * New Language Flag {-# PolymorphicKinds #-} ? 
    185   * Syntax of kinds 
    186   * Possibly syntax of function types 
    187  
    188 * Type checker 
    189  
    190 * Core / Core Lint 
    191  
    192 * Module interfaces 
    193   * To expose kind-quantified variables (does this drop out of any other change) 
    194  
    195 * Test cases 
    196  
    197  
    198 == To classify == 
    199  
    200 Other 'issues' (probably non-issues).  Kinds in rank-n types? 
    201 foobar :: forall k1 (b :: k1) (c :: k1 -> *) . (forall k2 (e :: k2 -> *) (f :: k) . e f -> Int ) -> b c -> Int 
    202  
    203 Impredicativity 
    204  
    205 {{{ 
    206 #!text/x-haskell 
    207 data Proxy :: forall k . k -> * 
    208  
    209 foo :: forall (m :: forall k . k -> *) . m Int -> m Maybe -> Int -- This is ok 
    210  
    211 bar = foo Proxy Proxy 
    212 }}} 
    213  
    214 {{{ 
    215 #!text/x-haskell 
    216 data Foo :: forall k . k -> * 
    217  
    218 foo :: forall (m :: (forall k . k -> *) -> *) . m Proxy -> Int -- This line is ok 
    219                                                                -- has a higher 
    220                                                                -- ranked kind, but 
    221                                                                -- that's not an 
    222                                                                -- issue as we 
    223                                                                -- have to be 
    224                                                                -- explicit 
    225  
    226 bar = foo Foo -- This is impredicative (and rejected) as it requires instantiating  
    227               -- Foo's k to (forall k .  k -> *) 
    228 }}}