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 <ekm...@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 <ekm...@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 < >> simo...@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@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-boun...@haskell.org [mailto: >>> glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Edward Kmett >>> *Sent:* 31 August 2012 03:38 >>> *To:* glasgow-haskell-users@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@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users