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

[Adam Gundry]

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 at gmail.com]
> *Sent:* 31 August 2012 18:27
> *To:* Simon Peyton-Jones
> *Cc:* glasgow-haskell-users at haskell.org
> <mailto: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
>