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

Fri Aug 31 15:37:58 CEST 2012

I ran into this same issue in my own experimentation: if a type variable x has a kind with only one constructor K, GHC does not supply the equality x ~ K y for some fresh type variable y. Perhaps it should. I too had to use similar workarounds to what you have come up with.

One potential problem is the existence of the Any type, which inhabits every kind. Say x gets unified with Any. Then, we would have Any ~ K y, which is an inconsistent coercion (equating two types with distinct ground head types). However, because the RHS is a promoted datatype, we know that this coercion can never be applied to a term. Because equality is homogeneous (i.e. ~ can relate only two types of the same kind), I'm not convinced the existence of Any ~ K y is so bad. (Even with heterogeneous equality, it might work out, given that there is more than one type constructor that results in *...)

Regarding the m -> k fundep: my experiments suggest that this dependency is implied when you have (m :: k), but I guess not when you have k appear in the kind of m in a more complicated way. Currently, there are no kind-level functions, so it appears that m -> k could be implied whenever k appears anywhere in the kind of m. If (when!) there are kind-level functions, we'll have to be more careful.

Richard

On Aug 31, 2012, at 9:06 AM, Edward Kmett wrote:

> 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
> 
> 
> 
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120831/6821f802/attachment-0001.htm>