I'm not Conor, but I'll have a go... On 31/08/12 20:14, Simon Peyton-Jones 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.
As Edward and others have recognised, the problem here is that FC coercions are not expressive enough to prove eta rules, that is forall x : (a, b) . x ~ (Fst x, Snd x) or more generally, that every element of a single-constructor (record) type is equal to the constructor applied to the projections. It seems like it should be perfectly fine to assert such a thing as an axiom, though: FC doesn't care what your equality proof is, provided it's consistent. Consistency of eta-laws follows from the fact that any inhabitant of the kind must be built with the sole constructor, unless you have Any (as Richard observed), in which case all bets are off. Why did you want Any again?
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 (:*)?
Here's my solution: irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x). (:*) i i i a (ax |> g1) (Nil i a) |> g2 where g1 : a x ~ a '(Fst x, Snd x) g1 = < a > (eta x) g2 : Thrist i a '(Fst x, Snd x) ~ Thrist i a x g2 = < Thrist i a > (sym (eta x)) are coercions derived from the eta axiom above. Hope this helps, now I should really go on holiday, Adam
*From:*Edward Kmett [mailto:ekmett@gmail.com] *Sent:* 31 August 2012 18:27 *To:* Simon Peyton-Jones *Cc:* glasgow-haskell-users@haskell.org mailto: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