← Microwave meringues | Monument →

Type Synonym Families

Posted on Sunday, 11 January 2009 at 20:11.

Update: removed incorrect type synonym example. Thanks to Ryan Ingram for pointing that out!

I think I’m getting the hang of type families, through what for me is the best way to learn a new concept: running into a problem to which that new concept turns out to be a solution.

First I will explain the problem I ran into and how type families came to the rescue; then I’ll play around with type families some more with a different example.

Type parameter order

Consider this alternative definition of MonadState from the mtl package:

class MonadState m where
  get :: m s s
  set :: s -> m s ()

With the accompanying instance for the State data type:

newtype State s a = State { runState :: s -> (a, s) }

instance MonadState State where
  get   = State $ \s -> (s, s)
  set s = State $ \_ -> ((), s)

This definition of MonadState has the advantage that it is valid Haskell98: no multi-parameter type classes and no functional dependencies required. It also has a very serious disadvantage: its one parameter m now has kind * -> * -> *, and the state type parameter s must be the last-but-one type parameter (the first * in the kind signature) of any type instance of MonadState.

This immediately poses a problem for the state transformer monad StateT, which is defined as:

newtype StateT s m a = StateT { runStateT :: s -> m (a,s) }

Here the last-but-one type parameter is the type of the underlying monad, and so there is no way to make StateT an instance of MonadState. We cannot even try and ignore the problem and write instance MonadState (StateT s), because then the compiler complains:

Kind mis-match
Expected kind `* -> * -> *',
but `StateT s' has kind `(* -> *) -> * -> *'
In the instance declaration for `MonadState (StateT s)'

Several solutions come to mind:

We could reorder StateT’s type parameters to StateT m s a, but this is bad in the general case: there might be other type classes that impose yet again different orderings on the type parameters, and these might be incompatible. In fact, the monad transformer class MonadTrans is such a type class:

class MonadTrans t where
  lift :: Monad m => m a -> t m a

instance MonadTrans StateT requires the type of the underlying monad to be the last-but-one type argument of the monad transformer, and so reordering StateT’s type arguments won’t do in this case.

We could wrap StateT in a newtype and write:

newtype StateT' m s a = StateT' { unStateT' :: StateT s m a }

instance MonadState (StateT' m) where
  ...

However, this introduces StateT' and unStateT' (de)constructors all over, which I don’t like much.

mtl solves this problem by introducing a second type parameter to the type class:

class Monad m => MonadState s m | m -> s where
  get :: m s
  put :: s -> m ()

Here the class parameters s and m seem totally unrelated to each other until the instance for State comes along:

instance MonadState (State s) s where
  get   = State $ \s -> (s, s)
  set s = State $ \_ -> ((), s)

This is where type families come in. mtl’s definition of MonadState can also be written as a type class with one type parameter, no functional dependencies and a type synonym family:

class MonadState m where
  type StateOf m :: *
  get :: m (StateOf m)
  set :: StateOf m -> m ()

Here StateOf :: (* -> *) -> * is a function on types. It tells given a type what the state type component of that type is. The function has no implementation yet. Instead, one case is added for each instance declaration of MonadState:

instance MonadState (State s) where
  type StateOf (State s) = s
  ...

instance MonadState (StateT s m) where
  type StateOf (StateT s m) = s
  ...

This is awesome, because now it doesn’t matter anymore what the state type argument’s position is! And get and set still automatically specialise to the types you would expect in the context of State and StateT.

We can improve MonadTrans in a similar fashion:

class MonadTrans m where
  type UnderlyingMonadOf m :: * -> *
  lift :: UnderlyingMonadOf m a -> m a

instance Monad m => MonadTrans (StateT s m) where
  type UnderlyingMonadOf (StateT s m) = m
  lift action = StateT $ \s -> do
    v <- action
    return (v, s)

Now that we're getting the hang of these type families, let's try another example.

The Parser class

We start with a simple backtracking parser based on a list of successes:

-- Input type s, result type a.
newtype SucParser s a = SucParser (StateT [s] [] a)
  deriving (Functor, Monad)

-- Recognise a symbol matching the predicate.
sucSatisfy :: (s -> Bool) -> SucParser s s
sucSatisfy p = SucParser $ do
  x : xs <- get
  if p x
    then do put xs; return x
    else fail "parse error"

-- Produce result on a valid sentence.
sucRunParser :: SucParser s a -> [s] -> Maybe a
sucRunParser (SucParser p) input =
  listToMaybe [ v | (v, []) <- runStateT p input ]

-- Recognise a specific symbol.
sucSymbol :: Eq s => s -> SucParser s s
sucSymbol = sucSatisfy . (==)

-- Recognise a string of symbols.
sucToken :: Eq s => [s] -> SucParser s [s]
sucToken = sequence . map sucSymbol

Together with instances for MonadPlus, Applicative and Alternative, this makes for an inefficient but powerful parser library which will do nicely as an example for now.

Let's extract a Parser type class and make SucParser an instance of it. We have a choice to make: do we let the class fix the positions of the symbol and result types, or do we use type families to allow flexible positions? Let's try and make both the input and output types flexible first:

class Parser p where
  type Input p  :: *
  type Output p :: *
  satisfy :: Input p ~ Output p => (Input p -> Bool) -> p
  runParser :: p -> [Input p] -> Maybe (Output p)

Here Input p ~ Output p is an equality constraint which says that the parser's input type should equal the parser's output type. Compare this with sucSatisfy above, which produced a SucParser s s.

For some reason GHC complained about this particular equality constraint:

All of the type variables in the constraint `Input p ~ Output p'
are already in scope (at least one must be universally quantified here)
  (Use -XFlexibleContexts to lift this restriction)
When checking the class method:
  satisfy :: (Input p ~ Output p) => (Input p -> Bool) -> p

I'm not sure what this means exactly, let alone why it is a problem, but enabling -XFlexibleContexts worked fine.

Let's make SucParser an instance:

instance Parser (SucParser s a) where
  type Input  (SucParser s a) = s
  type Output (SucParser s a) = a
  satisfy   = sucSatisfy
  runParser = sucRunParser

Generalising sucSymbol and sucToken to work with any Parser type produces some pretty intimidating types:

symbol :: (Input p ~ Output p, Parser p, Eq (Input p)) => Input p -> p
symbol = satisfy . (==)

token :: (Monad m, Parser (m a), Input (m a) ~ Output (m a),
           Eq (Input (m a))) => [Input (m a)] -> m [a]
token = sequence . map symbol

symbol's type makes sense enough, but I couldn't come up with token's type on my own. Simply leaving the type away won't do, because then GHC complains about missing contexts. GHCi however happily inferred sequence . map symbol's type for me.

Interestingly, using ~ we can create local type aliases. The following type signature, for example, is equivalent to the one above and works equally well:

token :: (p ~ m a, Monad m, Parser p, Input p ~ Output p,
           Eq (Input p)) => [Input p] -> m [a]

As for the other design choices for class Parser, I won't try fixing both type parameters, because as we saw above this is bad, and it doesn't require type families either. But there is still the option of fixing just one: the result type. Let's see what that will do to the type signatures:

class Parser p where
  type Input p :: *
  satisfy :: (Input p -> Bool) -> p (Input p)
  runParser :: p a -> [Input p] -> Maybe a

instance Parser (SucParser s) where
  type Input (SucParser s) = s
  satisfy   = sucSatisfy
  runParser = sucRunParser

symbol :: (Parser p, Eq (Input p)) => Input p -> p (Input p)
symbol = satisfy . (==)

token :: (Parser p, Monad p, Eq (Input p)) => [Input p] -> p [Input p]
token = sequence . map symbol

I think this is the best solution in this case. Fixing the result type to be the last argument resonates nicely with Functor and Monad. So nicely, in fact, that we don't need any equality constraints anymore.

I'm sure there's a lot more to these type families than I've seen so far. Reading through the Haskell Wiki entry on type families reveals that type synonym families can also appear outside of type classes, and that there's also such a thing as a data family which allows each class instance to define a new constructor of some associated data type. I hope I'll run into another problem some time to which these concepts are the solutions.

Comments

By Massimiliano Gubinelli on Saturday, 17 January 2009 at 10:05:

Hi, I come across another use of type families looking for a generic curry/uncurry. Here the implementation

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}

– uncurryG converts a function of the form a -> b -> c -> d to the uniform
– representation (a,(b,(c,()))) -> d
– curryG converts the uniform representation (a,(b,(c,()))) -> d to a function
– of the form a -> b -> c -> d

class Fn a c where
type Fnq a c :: *
uncurryG :: Fnq a c -> a -> c
curryG :: (a -> c) -> Fnq a c

instance Fn () c where
type Fnq () c = c
uncurryG f () = f
curryG f = f ()

instance (Fn b c) => Fn (a,b) c where
type Fnq (a,b) c = a -> Fnq b c
uncurryG f (a,b) = uncurryG (f a) b
curryG f = \a -> curryG (\b -> f (a,b))

By Martijn on Saturday, 17 January 2009 at 10:22:

Very nice. :-) Thanks for sharing!

Leave a comment!

Martijn loves to receive comments! Add yours by filling out the fields below.