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

[Simon Peyton-Jones]

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]
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120831/664ca0ee/attachment.htm>