Re: Changes to Typeable

typo, I meant "Proxy :: (exists k . k) -> *" is isomorphic to "Proxy :: forall k . k -> *" John On Sat, Feb 11, 2012 at 6:02 PM, John Meacham wrote:

On Fri, Feb 10, 2012 at 2:24 PM, Ian Lynagh 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.

From the users perspective, the Proxy will behave the same as ghcs, the only difference is that I need the 'ANY' annotation when declaring the type as such kinds are never automatically infered at the moment. I may just support the 'exists k . k' syntax directly in kind annotations actually eventually, I support it for types and it is handy on occasion.

   John