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

[Edward Kmett]

Hrmm. This seems to work manually for getting product categories to work.
Perhaps I can do the same thing for thrists.

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-}
module Product where

import Prelude hiding (id,(.))

class Category k where
  id :: k a a
  (.) :: k b c -> k a b -> k a c

type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p

type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
  (:*) :: x (Fst a) (Fst b) -> y (Snd a) (Snd b) -> (x * y) a b

instance (Category x, Category y) => Category (x * y) where
  id = id :* id
  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)



On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett <ekmett at gmail.com> wrote:

> 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.
>
> Also, does it ever make sense for the kind of a kind variable mentioned in
> a type not to get a functional dependency on the type?
>
> e.g. should
>
> class Foo (m :: k -> *)
>
> always be
>
> class Foo (m :: k -> *) | m -> k
>
> ?
>
> Honest question. I can't come up with a scenario, but you might have one I
> don't know.
>
> -Edward
>
> On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones <simonpj at microsoft.com
> > wrote:
>
>>  With the code below, I get this error message with HEAD. And that looks
>> right to me, no?****
>>
>> The current 7.6 branch gives the same message printed less prettily.****
>>
>> ** **
>>
>> If I replace the defn of irt with****
>>
>> irt :: a '(i,j) -> Thrist a '(i,j)****
>>
>> irt ax = ax :- Nil****
>>
>> ** **
>>
>> then it typechecks.****
>>
>> ** **
>>
>> Simon****
>>
>> ** **
>>
>> ** **
>>
>> Knett.hs:20:10:****
>>
>>     Couldn't match type `x' with '(i0, k0)****
>>
>>       `x' is a rigid type variable bound by****
>>
>>           the type signature for irt :: a x -> Thrist k a x at
>> Knett.hs:19:8****
>>
>>     Expected type: Thrist k a x****
>>
>>       Actual type: Thrist k a '(i0, k0)****
>>
>>     In the expression: ax :- Nil****
>>
>>     In an equation for `irt': irt ax = ax :- Nil****
>>
>> simonpj at cam-05-unx:~/tmp$****
>>
>> ** **
>>
>> ** **
>>
>> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
>> MultiParamTypeClasses, PolyKinds, ****
>>
>>              RankNTypes, TypeOperators, DefaultSignatures, DataKinds, ***
>> *
>>
>>              FlexibleInstances, UndecidableInstances #-}****
>>
>> ** **
>>
>> module Knett where****
>>
>> ** **
>>
>> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ****
>>
>>   ireturn :: a x -> m a x****
>>
>> ** **
>>
>> infixr 5 :-****
>>
>> ** **
>>
>> data Thrist :: ((i,i) -> *) -> (i,i) -> * where****
>>
>>   Nil  :: Thrist a '(i,i)****
>>
>>   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)****
>>
>> ** **
>>
>> -- instance IMonad Thrist where****
>>
>> --  ireturn a = a :- Nil****
>>
>> ** **
>>
>> irt :: a x -> Thrist a x****
>>
>> irt ax = ax :- Nil****
>>
>> ** **
>>
>> ** **
>>
>> *From:* glasgow-haskell-users-bounces at haskell.org [mailto:
>> glasgow-haskell-users-bounces at haskell.org] *On Behalf Of *Edward Kmett
>> *Sent:* 31 August 2012 03:38
>> *To:* glasgow-haskell-users at haskell.org
>> *Subject:* PolyKind issue in GHC 7.6.1rc1: How to make a kind a
>> functional dependency?****
>>
>> ** **
>>
>> If I define the following****
>>
>> ** **
>>
>> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
>> MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
>> DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}
>> ****
>>
>> module Indexed.Test where****
>>
>> ** **
>>
>> class IMonad (m :: (k -> *) -> k -> *) where ****
>>
>>   ireturn :: a x -> m a x****
>>
>> ** **
>>
>> infixr 5 :-****
>>
>> data Thrist :: ((i,i) -> *) -> (i,i) -> * where****
>>
>>   Nil :: Thrist a '(i,i)****
>>
>>   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)****
>>
>> ** **
>>
>> instance IMonad Thrist where****
>>
>>   ireturn a = a :- Nil****
>>
>> ** **
>>
>> Then 'ireturn' complains (correctly) that it can't match the k with the
>> kind (i,i). The reason it can't is because when you look at the resulting
>> signature for the MPTC it generates it looks like****
>>
>> ** **
>>
>> class IMonad k m where****
>>
>>   ireturn :: a x -> m a x****
>>
>> ** **
>>
>> However, there doesn't appear to be a way to say that the kind k should
>> be determined by m. ****
>>
>> ** **
>>
>> I tried doing:****
>>
>> ** **
>>
>> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ****
>>
>>   ireturn :: a x -> m a x****
>>
>> ** **
>>
>> Surprisingly (to me) this compiles and generates the correct constraints
>> for IMonad:****
>>
>> ** **
>>
>> ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies
>> -XDataKinds -XGADTs****
>>
>> ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a
>> x -> m a x****
>>
>> ghci> :info IMonad****
>>
>> class IMonad k m | m -> k where****
>>
>>   ireturn :: a x -> m a x****
>>
>> ** **
>>
>> But when I add ****
>>
>> ** **
>>
>> ghci> :{****
>>
>> Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where****
>>
>> Prelude|   Nil :: Thrist a '(i,i)****
>>
>> Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)****
>>
>> Prelude| :}****
>>
>> ** **
>>
>> and attempt to introduce the instance, I crash:****
>>
>> ** **
>>
>> ghci> instance IMonad Thrist where ireturn a = a :- Nil****
>>
>> ghc: panic! (the 'impossible' happened)****
>>
>>   (GHC version 7.6.0.20120810 for x86_64-apple-darwin):****
>>
>>     lookupVarEnv_NF: Nothing****
>>
>> ** **
>>
>> Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug**
>> **
>>
>> ** **
>>
>> Moreover, attempting to compile them in separate modules leads to a
>> different issue. ****
>>
>> ** **
>>
>> Within the module, IMonad has a type that includes the kind k and the
>> constraint on it from m. But from the other module, :info shows no such
>> constraint, and the above code again fails to typecheck, but upon trying to
>> recompile, when GHC goes to load the IMonad instance from the core file, it
>> panicks again differently about references to a variable not present in the
>> core.****
>>
>> ** **
>>
>> Is there any way to make such a constraint that determines a kind from a
>> type parameter in GHC 7.6 at this time?****
>>
>> ** **
>>
>> I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be
>> applicable to this situation.****
>>
>> ** **
>>
>> -Edward****
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120831/6655ffd0/attachment-0001.htm>