Recursive Type Families

Question

I am experimenting with an mtl-style class that allows me to lift Pipe composition over an outer monad. To do so, I must define which two variables of the type are the domain and codomain of Pipe composition.

I tried using an associated type family approach, but to no avail:

{-# LANGUAGE TypeFamilies #-}

import Control.Monad.Trans.Free
import Control.Monad.Trans.State
import Control.Pipe hiding (Pipe)

data Pipe a b m r = Pipe { unPipe :: FreeT (PipeF a b) m r }

class MonadPipe m where
    type C a b (m :: * -> *) :: * -> *
    idT :: C a a m r
    (<-<) :: C b c m r -> C a b m r -> C a c m r

instance (Monad m) => MonadPipe (Pipe i o m) where
    type C a b (Pipe i o m) = Pipe a b m
    idT = Pipe idP
    (Pipe p1) <-< (Pipe p2) = Pipe (p1 <+< p2)

instance (MonadPipe m) => MonadPipe (StateT s m) where
    type C a b (StateT s m) = StateT s (C a b m)
    idT = StateT $ \s -> idT
    (StateT f1) <-< (StateT f2) = StateT $ \s -> f1 s <-< f2 s

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

family.hs:23:15:
    Could not deduce (C a a m ~ 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 a a (StateT s m) 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 s m)'

family.hs:24:10:
    Could not deduce (C b c m ~ 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 b c (StateT s m) 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 s m)'

<<Two other errors for 'C a b m' and 'C a c m'>>

It's hard for me to understand why the types won't unify, especially for the idT definition, since I'd expect the inner idT to be universally quantified over a so it would match the outer one.

So my question is whether this is implementable with type families, and if not possible with type families, how could it be implemented?

Answer 1

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

Let me guess: leftovers?

Let me walk myself through the type error first, the a SOLUTION.

The class defines :
type C a0 b0 m  where a0 and b0 are fresh.
idT :: C a a m r, where a and r are fresh. 

The idT in the (Pipe i o m0) instance is okay by what I think is the logic:
LHS is idT :: C a0 a0 (Pipe i o 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 to make the Category instances probably works here if the type family becomes a data family.

EDIT: You alter the order of 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 m a b r = Pipe { unPipe :: FreeT (PipeF a b) m r }

newtype StatePipe s mp a b r = SP (StateT s (mp a b) r)

class MonadPipe mp where
    idT :: mp a a r
    (<-<) :: mp b c r -> mp a b r -> mp a c r

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

Though MonadTrans might now be sad. Another approach keeps the argument order by using a GADT to, perhaps, more cleanly 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 s a b m r where
  FPipe :: { unPipe :: FreeT (PipeF a b) m r } -> Pipe () a b m r
  LPipe :: StateT s1 (Pipe s2 a b m) r -> Pipe (s1,s2) a b m r

class MonadPipe s where
    idT :: Monad m => Pipe s a a m r
    (<-<) :: Monad m => Pipe s b c m r -> Pipe s a b m r -> Pipe s a c m r

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 I can translate this into a perhaps 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 () a b m r = Pipe { unPipe :: FreeT (PipeF a b) m r }
newtype instance GPipe (s1,s2) a b m r = LPipe ( StateT s1 (GPipe s2 a b m) r )

class MonadPipe s where
  idT :: Monad m => GPipe s a a m r
  (<-<) :: Monad m => GPipe s b c m r -> GPipe s a b m r -> GPipe s a c m r

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 inference is, by default, a guessing game. Haskell's surface syntax makes it rather awkward to be explicit about which types should instantiate a forall, even if you know what you want. This is a legacy from the good old days of Damas-Milner completeness, when ideas interesting enough to require explicit typing were simply forbidden.

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

idT = StateT $ \ s -> idT

is supposed to mean

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

so that the left has type C a a (StateT s m) r and the right has type StateT s (C a a m) r, which are equal by definition of the type family and joy radiates over the world. But that's not the meaning of what you wrote. The "variable-rule" for invoking polymorphic things requires that each forall is instantiated with a fresh existential type variable which is then solved by unification. So what your code means is

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

The available constraint, after computing the type family, is

C a a m ~ C a' a' m'

but that doesn't simplify, nor should it, because there is no reason to assume C is injective. And the maddening thing is that the machine cares more than you about the possibility of finding a most general solution. You have a suitable solution in mind already, but the problem is to achieve communication when the default assumption is guesswork.

There are a number of strategies which might help you out of this jam. One is to use data families instead. Pro: injectivity no problem. Con: structor. (Warning, untested speculation below.)

class MonadPipe m where
  data C a b (m :: * -> *) r
  idT :: C a a m r
  (<-<) :: C b c m r -> C a b m r -> C a c m r

instance (MonadPipe m) => MonadPipe (StateT s m) where
  data C a b (StateT s m) r = StateTPipe (StateT s (C a b m) r)
  idT = StateTPipe . StateT $ \ s -> idT
  StateTPipe (StateT f) <-< StateTPipe (StateT g) =
    StateTPipe . StateT $ \ s - f s <-< g s

Another con is that the resulting data family is not automatically monadic, nor is it so very easy to unwrap it or make it monadic in a uniform way.

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

newtype WrapC a b m r = WrapC {unwrapC :: C a b m r}

then use WrapC in the types of the operations to keep the typechecker on the right track. I don't know if that's a good strategy, but I plan to find out, one of these days.

A more direct strategy is to use proxies, phantom types, and scoped type variables (although this example shouldn't need them). (Again, speculation warning.)

data Proxy (a :: *) = Poxy
data ProxyF (a :: * -> *) = PoxyF

class MonadPipe m where
  data C a b (m :: * -> *) r
  idT :: (Proxy a, ProxyF m) -> C a a m r
  ...

instance (MonadPipe m) => MonadPipe (StateT s m) where
  data C a b (StateT s m) r = StateTPipe (StateT s (C a b m) r)
  idT pp = StateTPipe . StateT $ \ s -> idT pp

That's just a crummy way of making the type applications explicit. Note that some people use a itself instead of Proxy a and pass undefined as the argument, thus failing to mark the proxy as such in the type and relying on not accidentally evaluating it. Recent progress with PolyKinds may at least mean we can have just one kind-polymorphic phantom proxy type. Crucially, the Proxy type constructors are injective, so my code really is saying "same parameters here as there".

But there are times when I wish that I could drop to the System FC level in source code, or otherwise express a clear manual override for type inference. Such things are quite standard in the dependently typed community, where nobody imagines that the machine can figure everything out without a nudge here and there, or that hidden arguments carry no information worth inspecting. It's quite common that hidden arguments to a function can be suppressed at usage sites but need to be made explicit within the definition. The present situation in Haskell is based on a cultural assumption that "type inference is enough" which has been off the rails for a generation but still somehow persists.