Changes to Typeable

John Meacham john at repetae.net
Sun Feb 12 03:02:45 CET 2012


On Fri, Feb 10, 2012 at 2:24 PM, Ian Lynagh <igloo at earth.li> wrote:
> But it would be better if they could use the new definition. Is
> PolyKinds sufficiently well-defined and simple that it is feasible for
> other Haskell implementations to implement it?

There is actually a much simpler extension I have in jhc called
'existential kinds' that can
express this.

Existential kinds grew from the need to express the kind of the
function type constructcor

data (->) :: * -> * -> *

is fine for haskell 98, but breaks when you have unboxed values, so
jhc used the same solution of ghc, making it

data (->) :: ?? -> ? -> *

where ?? means * or #, and ? means *, #, or (#), I will call these
quasi-kinds for the moment.

all you need to express the typeable class is an additional quasi-kind
'ANY' that means, well, any kind.

then you can declare proxy as

data Proxy (a :: ANY) = Proxy

and it will act identially to the ghc version.

So why existential?

because ANY is just short for 'exists k. k'

so Proxy ends up with

Proxy :: (exists k . k) -> *

which is isomorphic to

forall k . Proxy :: k -> *

? expands to (exists k . FunRet k => k) and ?? expands to (exists k .
FunArg k => k)  where FunRet and FunArg are appropriate constraints on
the type.

so the quasi-kinds are not any sort of magic hackery, just simple
synonyms for existential kinds.

The implemention is dead simple for any unification based kind
checker, normally when you find a constructor application, you unify
each of the arguments kinds with the kinds given by the constructor,
the only difference is that if the kind of the constructor is 'ANY'
you skip unifying it with anything, or create a fresh kind variable
with a constraint if you need to support ?,and ?? too and unify it
with that. about a 2 line change to your kind inference code.



More information about the Glasgow-haskell-users mailing list