Changes to Typeable

John Meacham john at repetae.net
Sun Feb 12 03:05:31 CET 2012


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 <john at repetae.net> wrote:
> 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.
>
> 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



More information about the Glasgow-haskell-users mailing list