Recursive Type Families

Question

I am experimenting with the mtl style mtl , which allows me to raise the Pipe composition over the external monad. To do this, I have to determine which two type variables are the scope and the coding fan of the Pipe composition.

I tried using a sibling family type, but to no avail:

 {-# LANGUAGE TypeFamilies #-} import Control.Monad.Trans.Free import Control.Monad.Trans.State import Control.Pipe hiding (Pipe) data Pipe abmr = Pipe { unPipe :: FreeT (PipeF ab) mr } class MonadPipe m where type C ab (m :: * -> *) :: * -> * idT :: C aamr (<-<) :: C bcmr -> C abmr -> C acmr instance (Monad m) => MonadPipe (Pipe iom) where type C ab (Pipe iom) = Pipe abm idT = Pipe idP (Pipe p1) <-< (Pipe p2) = Pipe (p1 <+< p2) instance (MonadPipe m) => MonadPipe (StateT sm) where type C ab (StateT sm) = StateT s (C abm) idT = StateT $ \s -> idT (StateT f1) <-< (StateT f2) = StateT $ \s -> f1 s <-< f2 s 

However, the above code does not check the type. GHC gives the following errors:

 family.hs:23:15: Could not deduce (C aam ~ C a0 a0 m0) from the context (MonadPipe m) bound by the instance declaration at family.hs:21:14-52 NB: `C' is a type function, and may not be injective Expected type: C aa (StateT sm) r Actual type: StateT s (C a0 a0 m0) r In the expression: StateT $ \ s -> idT In an equation for `idT': idT = StateT $ \ s -> idT In the instance declaration for `MonadPipe (StateT sm)' family.hs:24:10: Could not deduce (C bcm ~ C b0 c0 m1) from the context (MonadPipe m) bound by the instance declaration at family.hs:21:14-52 NB: `C' is a type function, and may not be injective Expected type: C bc (StateT sm) r Actual type: StateT s (C b0 c0 m1) r In the pattern: StateT f1 In an equation for `<-<': (StateT f1) <-< (StateT f2) = StateT $ \ s -> f1 s <-< f2 s In the instance declaration for `MonadPipe (StateT sm)' <<Two other errors for 'C abm' and 'C ac m'>> 

It’s hard for me to understand why the types will not be unified, especially for determining idT , since I would expect the internal idT be evaluated on a whole scale greater than a , so that it matches the external.

So my question is, is this implemented with type families, and if this is not possible with type families, how can this be implemented?

Answer 1

EDITED Three times: see bottom for data family. And changed the version of GADT to remove m.

Let me guess: leftovers?

Let me first go through a type error, SOLUTION.

 The class defines : type C a0 b0 m where a0 and b0 are fresh. idT :: C aamr, where a and r are fresh. The idT in the (Pipe io m0) instance is okay by what I think is the logic: LHS is idT :: C a0 a0 (Pipe io m0) r0 which becomes Pipe a0 a0 m0 r0 RHS is Pipe idP :: Pipe a1 a1 m1 r1 starts fresh And then these unify because Pipe is a data constructor. The idT in the MonadPipe m0 => (StateT s0 m0) instance: LHS is idT :: C a0 a0 (StateT s0 m0) which becomes StateT s0 (C a0 a0 m0) RHS is StateT (\s -> idT) :: StateT s1 m1 r1 Some unification seems to happen... RHS is StateT (\s -> idT) :: StateT s1 (C a0 a0 m0) r1 where expression idT :: MonadPipe m1 => (C a2 a2 m2) r2 starts fresh context of idT :: (C a0 a0 m0) (a1, s1) And then (C a0 a0 m0) does not unify with (C a1 a2 m2) because C is a type constructor. 

Your previous newtype way of making instances of a category probably works here if the type family becomes a data family.

EDIT: you change the order of the parameters and newtype StateT to solve it:

 {-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-} import Control.Monad.Trans.Free import Control.Monad.Trans.State import Control.Pipe hiding (Pipe) data Pipe mabr = Pipe { unPipe :: FreeT (PipeF ab) mr } newtype StatePipe s mp abr = SP (StateT s (mp ab) r) class MonadPipe mp where idT :: mp aar (<-<) :: mp bcr -> mp abr -> mp acr instance (Monad m) => MonadPipe (Pipe m) where idT = Pipe idP (Pipe p1) <-< (Pipe p2) = Pipe (p1 <+< p2) instance (MonadPipe mp) => MonadPipe (StatePipe s mp) where idT = SP . StateT $ \s -> idT (SP (StateT f1)) <-< (SP (StateT f2)) = SP . StateT $ \s -> f1 s <-< f2 s 

Although MonadTrans can now be sad. Another approach maintains the order of the arguments, using GADT, to perhaps more clearly express what you are trying to build:

 {-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleInstances #-} import Control.Monad.Trans.Free import Control.Monad.Trans.State import Control.Pipe hiding (Pipe) data Pipe sabmr where FPipe :: { unPipe :: FreeT (PipeF ab) mr } -> Pipe () abmr LPipe :: StateT s1 (Pipe s2 abm) r -> Pipe (s1,s2) abmr class MonadPipe s where idT :: Monad m => Pipe saamr (<-<) :: Monad m => Pipe sbcmr -> Pipe sabmr -> Pipe sacmr instance MonadPipe () where idT = FPipe idP (FPipe p1) <-< (FPipe p2) = FPipe (p1 <+< p2) instance MonadPipe s2 => MonadPipe (s1,s2) where idT = LPipe (StateT $ \s -> idT) (LPipe (StateT f1)) <-< (LPipe (StateT f2)) = LPipe (StateT $ \s1 -> (f1 s1 <-< f2 s1)) 

And can I translate this into a possibly even nicer data family?

 {-# LANGUAGE TypeFamilies #-} import Control.Monad.Trans.Free import Control.Monad.Trans.State import Control.Pipe hiding (Pipe) data family GPipe s :: * -> * -> (* -> *) -> * -> * newtype instance GPipe () abmr = Pipe { unPipe :: FreeT (PipeF ab) mr } newtype instance GPipe (s1,s2) abmr = LPipe ( StateT s1 (GPipe s2 abm) r ) class MonadPipe s where idT :: Monad m => GPipe saamr (<-<) :: Monad m => GPipe sbcmr -> GPipe sabmr -> GPipe sacmr instance MonadPipe () where idT = Pipe idP (Pipe p1) <-< (Pipe p2) = Pipe (p1 <+< p2) instance MonadPipe s2 => MonadPipe (s1,s2) where idT = LPipe (StateT (\s -> idT)) (LPipe (StateT f1)) <-< (LPipe (StateT f2)) = LPipe (StateT (\s -> f1 s <-< f2 s)) 

Answer 2

Type input is, by default, a guessing game. Haskell's surface syntax makes it rather inconvenient to explicitly know what types an forall instance should create, even if you know what you want. This is a legacy from the good old days of the fullness of Damas-Milner, when ideas interesting enough to require explicit typing were simply forbidden.

Suppose we are allowed to make an application of a type explicit in patterns and expressions using the Agda-style f {a = x} notation, selectively accessing the type parameter corresponding to a in a signature of type f . Your

 idT = StateT $ \ s -> idT 

supposed to

 idT {a = a}{m = m} = StateT $ \ s -> idT {a = a}{m = m} 

so the left one is of type C aa (StateT sm) r , and the right one is of type StateT s (C aam) r , which is equal by definition to the type family, and joy radiates around the world. But that is not the point of what you wrote. A “variable rule” for calling polymorphic things requires that each forall be created with a new variable of the existential type type, which is then solved by unification. So what your code means

 idT {a = a}{m = m} = StateT $ \ s -> idT {a = a'}{m = m'} -- for a suitably chosen a', m' 

The available restriction after computing a type family is

 C aam ~ C a' a' m' 

but this does not simplify and should not, because there is no reason to assume that C is injective. And the madness is that the car cares more about the opportunity to find the most common solution. You already have a suitable solution, but the problem is reaching the connection when the default assumption is a hunch.

There are many strategies that can help you with this common cold. One of them is to use data families. Pro: injectivity is not a problem. Con: structor. (Warning, unverified spec below.)

 class MonadPipe m where data C ab (m :: * -> *) r idT :: C aamr (<-<) :: C bcmr -> C abmr -> C acmr instance (MonadPipe m) => MonadPipe (StateT sm) where data C ab (StateT sm) r = StateTPipe (StateT s (C abm) r) idT = StateTPipe . StateT $ \ s -> idT StateTPipe (StateT f) <-< StateTPipe (StateT g) = StateTPipe . StateT $ \ s - fs <-< gs 

Another convention is that the resulting data family is not automatically monadic, and it is very easy to deploy or make it a monadic uniform way.

I'm thinking of trying a template for these things where you keep your type family, but define a newtype wrapper for it

 newtype WrapC abmr = WrapC {unwrapC :: C abmr} 

then use WrapC in operation types to keep typechecker in the right way. I do not know if a good strategy, but I plan to find out the other day.

A more direct strategy is to use proxies, phantom types, and type variables (although they don't need this example). (Again, a warning about speculation.)

 data Proxy (a :: *) = Poxy data ProxyF (a :: * -> *) = PoxyF class MonadPipe m where data C ab (m :: * -> *) r idT :: (Proxy a, ProxyF m) -> C aamr ... instance (MonadPipe m) => MonadPipe (StateT sm) where data C ab (StateT sm) r = StateTPipe (StateT s (C abm) r) idT pp = StateTPipe . StateT $ \ s -> idT pp 

This is just a tricky way to make type applications explicit. Please note that some people use a their own instead of Proxy a and pass undefined as an argument, thereby not specifying the proxy server as such in the type and relying on its random evaluation. Recent progress with PolyKinds may at least mean that we can only have one type-polymorphic phantom proxy type. Basically, constructors like Proxy are injective, so my code really says "the same parameters as there."

But there are times when I want me to be able to go to the System FC level in the source code or otherwise express a clear manual override for type inference. Such things are completely standardized, depending on a typed community, where no one imagines that a machine can understand everything without a jerk here and there, or that hidden arguments do not contain any information that is worth checking. It is very common that hidden function arguments can be suppressed on usage sites, but must be clearly defined in the definition. Haskell’s current situation is based on the cultural assumption that the “type of inference is enough,” which has been off the rails for a generation but is still somehow preserved.