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 <j...@repetae.net> wrote: > On Fri, Feb 10, 2012 at 2:24 PM, Ian Lynagh <ig...@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. > > 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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
