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

[Edward Kmett]

This works, though it'll be all sorts of fun to try to scale up.


{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances,
TypeFamilies #-}
module Indexed.Test where

class IMonad (m :: (k -> *) -> k -> *) | m -> k
  where ireturn :: a x -> m a x

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

infixr 5 :-
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
  Nil :: Thrist a '(i,i)
  (:-) :: (Snd ij ~ Fst jk, Fst ij ~ Fst ik, Snd jk ~ Snd ik) => a ij ->
Thrist a jk -> Thrist a ik

instance IMonad Thrist where
  ireturn a = a :- Nil

I know Agda has to jump through some hoops to make the refinement work on
pairs when they do eta expansion. I wonder if this could be made less
painful.


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

> 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/08eaf27e/attachment-0001.htm>