Changes to Typeable
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
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
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