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

Edward Kmett ekmett at gmail.com
Fri Aug 31 19:26:49 CEST 2012


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

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

>  Same question.  Do you expect the code below to type-check?  I have
> stripped it down to essentials.  Currently it’s rejected with ****
>
> ** **
>
>     Couldn't match type `a' with '(,) k k1 b0 d0****
>
> ** **
>
> And that seems reasonable, doesn’t it?  After all, in the defn of bidStar,
> (:*) returns a value of type ****
>
>      Star x y ‘(a,c) ‘(b,d)****
>
> which is manifestly incompatible with the claimed, more polymorphic type.
> And this is precisely the same error as comes from your class/instance
> example below, and for precisely the same reason.  ****
>
> ** **
>
> I must be confused.****
>
> ** **
>
> Simon****
>
> ** **
>
>
> ****
>
> {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}****
>
> module Product where****
>
> ** **
>
> data Star :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where**
> **
>
>   (:*) :: x a b -> y c d -> Star x y '(a,c) '(b,d)****
>
> ** **
>
> bidStar :: Star T T a a****
>
> bidStar = bidT :* bidT****
>
> ** **
>
> data T a b = MkT****
>
> ** **
>
> bidT :: T a a****
>
> bidT = MkT****
>
> ** **
>
> ** **
>
> ** **
>
> *From:* Edward Kmett [mailto:ekmett at gmail.com]
> *Sent:* 31 August 2012 13:45
> *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?****
>
>  ** **
>
> Hrmm. This seems to render product kinds rather useless, as there is no
> way to refine the code to reflect the knowledge that they are inhabited by
> a single constructor. =( ****
>
> ** **
>
> For instance, there doesn't even seem to be a way to make the following
> code compile, either.****
>
> ** **
>
> ** **
>
> {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}****
>
> module Product where****
>
> ** **
>
> import Prelude hiding (id,(.))****
>
> ** **
>
> class Category k where****
>
>   id :: k a a****
>
>   (.) :: k b c -> k a b -> k a c****
>
> ** **
>
> data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where***
> *
>
>   (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)****
>
> ** **
>
> instance (Category x, Category y) => Category (x * y) where****
>
>   id = id :* id****
>
>   (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)****
>
> ** **
>
> This all works perfectly fine in Conor's SHE, (as does the thrist example)
> so I'm wondering where the impedence mismatch comes in and how to gain
> knowledge of this injectivity to make it work.****
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120831/2f834444/attachment.htm>


More information about the Glasgow-haskell-users mailing list