Changes between Version 1 and Version 2 of PolymorphicKinds


Ignore:
Timestamp:
Oct 16, 2008 1:04:07 PM (7 years ago)
Author:
guest
Comment:

a bit more on type classes

Legend:

Unmodified
Added
Removed
Modified
  • PolymorphicKinds

    v1 v2  
    102102== Type Classes ==
    103103
     104Declaration options:
    104105
     106=== Option 1: Implicit kind variables ===
    105107
    106108{{{
     
    109111
    110112class Bar (a :: k -> *) => Baz (a :: * -> k) where -- superclass, explicit name (shared)
    111 class Bar a => Baz (a :: * -> k) where             -- superclass, implicit or new name?
     113class Bar a => Baz (a :: * -> k) where             -- superclass, new k?
    112114
    113115instance Bang (a :: k -> *) => Bar (a :: k -> *)   -- instance implication, explic
     116instance Bang a => Bar (a :: k -> *)   -- instance implication, explic
     117
     118class Foo (a :: k -> *) (b :: k -> *) where        -- MPTC name shared
    114119}}}
     120
     121=== Option 2: Explicit kind variables ===
     122
     123Here reusing {{{forall}} is probably safe, although possibly inconsistent if we go for {{{forall_kind}}} (or other) as a term level quantifier...
    115124
    116125{{{
    117126#!text/x-haskell
    118 class forall k . Blah (a :: k -> *) where
     127class forall k . Blah (a :: k -> *) where                     -- standalone
     128class forall k . Baz (a :: k -> *) => Bar (a :: * -> k) where -- superclass, shared k
     129class forall k . Baz a => Bar (a :: * -> k) where             -- superclass, new k
     130
     131instance forall k . Bang (a :: k -> *) => Bar (a :: k -> *)   -- instance implication, shared k
     132instance forall k . Bang a => Bar (a :: k -> *)               -- instance implication, new k
     133
     134class forall k . Foo (a :: k -> *) (b :: k -> *) where        -- MPTC name shared
    119135}}}
    120136
     137Again, this doesn't seem to add much now, however if we ever want to constrain the kind variables to particular sorts in the future, we will probably need binders for them.
     138
     139=== Option 3: Explicit kind signatures for type classes ===
     140
     141Can't do this in general, as you need to name the variables that index the type class for use in member functions.  Although for type classes with no member functions this may be a viable option.  The question is what is the result of a type class?
     142
    121143{{{
    122 #!text/x-haskell
    123 class forall k . Baz (a :: k -> *) => Bar (a :: * -> k) where
     144class Blah :: forall k . (k -> *) -> ??? where
    124145}}}
     146
     147
     148== Type functions ==
     149
     150Follow as per type classes
     151
    125152
    126153== Syntax of Kinds ==
     
    133160== Syntax of Types ==
    134161
    135 Type syntax need to be extended with a new binder TODO
     162Type syntax need to be extended with a new binder.
    136163
    137164
    138 == Type Classes ==
     165== Implementation route ==
     166...
    139167
    140 TODO
    141168
    142169== To classify ==