On Fri, Feb 10, 2012 at 2:24 PM, Ian Lynagh
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?
From the users perspective, the Proxy will behave the same as ghcs,
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. 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