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 <simo...@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:ekm...@gmail.com <ekm...@gmail.com>] > *Sent:* 31 August 2012 18:27 > > *To:* Simon Peyton-Jones > *Cc:* glasgow-haskell-users@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**** >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
