PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Edward Kmett ekmett at gmail.com
Fri Aug 31 21:24:25 CEST 2012


I'm going to defer to Conor on this one, as it is one of the examples from
his Kleisli Arrows of Outrageous fortune that I'm translating here. ;)

-Edward

On Fri, Aug 31, 2012 at 3:14 PM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

>  Try translating into System FC!  It’s not just a question of what the
> type checker will pass; we also have to produce a well-typed FC program.**
> **
>
> ** **
>
> Remember that (putting in all the kind abstractions and applications:****
>
>   Thrist :: forall i.  ((i,i) -> *) -> (i,i) -> *****
>
>   (:*) :: forall i j k. forall (a: (i,j) -> *). ****
>
>             a '(i,j) -> Thrist (j,k) a '(j,k) -> Thrist (i,k) a '(i,k)****
>
> ** **
>
> So consider ‘irt’:****
>
> ** **
>
> irt :: forall i. forall (a : (i,i) -> *). forall (x : (i,i)).****
>
>         a x -> Thrist i a x         ****
>
> irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x).****
>
>        (:*) ? ? ? ? ax (Nil ...)****
>
> ** **
>
> So, what are the three kind args, and the type arg, to (:*)?  ****
>
> ** **
>
> It doesn’t seem to make sense... in the body of irt, (:*) produces a
> result of type****
>
>   Thrist (i,k) a ‘(i,k)****
>
> but irt’s signature claims to produce a result of type ****
>
>   Thrist i a x****
>
> So irt’s signature is more polymorphic than its body.  ****
>
> ** **
>
> If we give irt a less polymorphic type signature, all is well****
>
> ** **
>
> irt :: forall p,q. forall (a : ((p,q),(p,q)) -> *). forall (x :
> ((p,q),(p,q))).****
>
>         a x -> Thrist (p,q) a x         ****
>
> ** **
>
> ** **
>
> Maybe you can explain what you want in System FC? Type inference and the
> surface language come after that.  If it can’t be expressed in FC it’s out
> of court.  Of course we can always beef up System FC.****
>
> ** **
>
> I’m copying Stephanie and Conor who may have light to shed.****
>
> ** **
>
> Simon****
>
> ** **
>
> *From:* Edward Kmett [mailto:ekmett at gmail.com <ekmett at gmail.com>]
> *Sent:* 31 August 2012 18:27
>
> *To:* Simon Peyton-Jones
> *Cc:* glasgow-haskell-users at haskell.org
> *Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
> functional dependency?****
>
> ** **
>
> It is both perfectly reasonable and unfortunately useless. :(****
>
> ** **
>
> The problem is that the "more polymorphic" type isn't any more
> polymorphic, since (ideally) the product kind (a,b) is only inhabited by
> things of the form '(x,y).****
>
> ** **
>
> The product kind has a single constructor. But there is no way to express
> this at present that is safe.****
>
> ** **
>
> As it stands, I can fake this to an extent in one direction, by writing***
> *
>
> ** **
>
> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
> MultiParamTypeClasses, PolyKinds, TypeFamilies,****
>
>              RankNTypes, TypeOperators, DefaultSignatures, DataKinds,****
>
>              FlexibleInstances, UndecidableInstances #-}****
>
> ** **
>
> module Kmett where****
>
> ** **
>
> type family Fst (p :: (a,b)) :: a****
>
> type instance Fst '(a,b) = a****
>
> ** **
>
> type family Snd (p :: (a,b)) :: b****
>
> type instance Snd '(a,b) = b****
>
> ** **
>
> data Thrist :: ((i,i) -> *) -> (i,i) -> * where****
>
>   Nil  :: Thrist a '(i,i)****
>
>   (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =>****
>
>           a ij -> Thrist a '(j,k) -> Thrist a ik****
>
> ** **
>
> irt :: a x -> Thrist a x****
>
> irt ax = ax :- Nil****
>
> ** **
>
> and this compiles, but it just pushes the problem down the road, because
> with that I can show that given ij :: (x,y), I can build up a tuple '(Fst
> ij, Snd ij) :: (x,y)****
>
> ** **
>
> But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
> when you go to define an indexed bind, and type families are insufficient
> to the task. Right now to get this property I'm forced to fake it with
> unsafeCoerce.****
>
> ** **
>
> -Edward****
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120831/5569d430/attachment-0001.htm>


More information about the Glasgow-haskell-users mailing list