Changes between Version 7 and Version 8 of PolymorphicKinds


Ignore:
Timestamp:
Oct 17, 2008 3:07:03 PM (7 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 }}}