Monomorphism restriction strikes again

A while ago I blogged about monomorphsim restriction. I thought I understood most of it, but just yesterday I was surprisingly hit by it. I was working my way through chapter 9 of Real World Haskell. In this chapter authors present a case study of a library that is designed for searching the file system. The central point in the design of this library are predicates that are used to perform queries. A predicate function is given some information about the file system entry: path, permissions (they allow to determine if the entry is a file or a directory), size and modification time. Based on that information a predicate function can return some information, e.g. name of the file or Bool value stating if the file meets some given criteria. To save a bit of typing RWH authors introduce a type synonym:

import System.Directory (Permissions(..))
import System.Time (ClockTime(..))
 
type InfoP a =  FilePath
             -> Permissions
             -> Maybe Integer
             -> ClockTime
             -> a

‘P’ at the end of name stands for ‘predicate’. As you can see this type defines a function type with polymorphic return value acting as type parameter. Here’s an example of usage:

pathP :: InfoP FilePath
pathP path _ _ _ = path
 
sizeP :: InfoP Integer
sizeP _ _ (Just size) _ = size
sizeP _ _ Nothing _ = -1

These functions retrieve path to a file and its size, respectively. We’d certainly would like to do something with those information. We might want to know if the file is larger than some specified size. We might also want to join predicates using logical AND and OR. Here’s an example:

equalP :: (Eq a) => InfoP a -> a -> InfoP Bool
equalP f k = \w x y z -> f w x y z == k

This function takes a predicate and a value and compares them for equality, e.g. equalP sizeP 1024. This can be generalized to any comparison operator by introducing additional parameter1 :

liftP :: (a -> b -> c) -> InfoP a -> b -> InfoP c
liftP q f k = \w x y z -> f w x y z `q` k
 
equalP :: (Eq a) => InfoP a -> a -> InfoP Bool
equalP = liftP (==)

So liftP takes an operator q (infix notation is used to show that explicitly) and applies it to the result of f and k. Note that both liftP and previous version of equalP return anonymous functions that require four more parameters to yield a result. So far so good. We can easily define other predicates like lesserP and greaterP only by passing different comparison operator to liftP. The liftP function can be further generalized to allow logical operators:

liftP2 :: (a -> b -> c) -> InfoP a -> InfoP b -> InfoP c
liftP2 q f g = \w x y z -> f w x y z `q` g w x y z
 
andP = liftP2 (&&)
orPĀ  = liftP2 (||)

As you can see liftP and liftP2 are very similar and in fact the former one can be written in the terms of the latter:

constP :: a -> InfoP a
constP k _ _ _ _ = k
 
liftP :: (a -> b -> c) -> InfoP a -> b -> InfoP c
liftP q f k = liftP2 q f (constP k)

This part was very confusing to me at first, but it becomes clear when you replace the InfoP type synonym in constP type declaration with actual type:

constP :: a -> FilePath -> Permissions -> Maybe Integer -> ClockTime -> a
constP k _ _ _ _ = k

Now it becomes clear that constP takes a constant and four other parameters for the predicate, discards these parameters four and returns the constant.

Now comes the key part. Notice that logical predicates andP and orP were written without type signature. That’s perfectly fine. However, omitting type signature for equalP function causes an error:

Ambiguous type variable `b0' in the constraint:
  (Eq b0) arising from a use of `=='
Possible cause: the monomorphism restriction applied to the following:
  equalP :: InfoP b0 -> b0 -> InfoP Bool (bound at rwh9.hs:20:1)
Probable fix: give these definition(s) an explicit type signature
              or use -XNoMonomorphismRestriction
In the first argument of `liftP', namely `(==)'
In the expression: liftP (==)
In an equation for `equalP': equalP = liftP (==)

I’m not sure why this happens when we try to lift (==), but doesn’t happen when (&&) is lifted in same manner. It seems that this happens because (==) operator introduces additional type class constraints (Eq type class), but I don’t see why these constraints would cause monomorphsim restriction to kick in. These mystery is yet to be solved.

  1. My code slightly differs from what you’ll find in RWH []

5 Responses to “Monomorphism restriction strikes again”

  1. Dan Burton says:

    I’ve been playing with pipes code recently, and I’ve noticed the same thing: the monomorphism restriction will sometimes kick in when a typeclass constraint is involved. In my case, it was the Show typeclass that caused the same “Ambiguous type variable” error.

  2. Andrea Vezzosi says:

    There are exactly 3 conditions needed for the MR to trigger:

    1. you have what is called a pattern binding, i.e. a definition like x = ..; in which x could be a complex pattern or just a variable, but importantly there are no explicit arguments on the left of =.

    2. no type signature for it

    3. its inferred type contains a typeclass constraint

    This is because with these conditions you have something ‘x’, that at the source level syntax looks like its computation will be shared among multiple uses but in a typical haskell implementation won’t. The reason it won’t is the typeclass constraint, since at the implementation level it gets translated into an additional argument, so what at the source level is (x , x), underlying becomes (x a0 , x a1) or even (x a0 , x a0) and that, unless some other optimization kicks in, computes x a0 twice.

    If instead we force x to be monomorphic, then a0 is never passed as an argument at the site of use of x but it’s instead used within x’s definition, because which ‘a’ to use depends only on the type.

    On the other hand without the typeclass constraint x remains x and there’s no sharing lost by being polymorphic, which shows why andP and orP are fine.

    These aN i’ve been talking about are usually called typeclass dictionaries, because they are a record containing the implementations of the typeclass methods for a specific type.

    I hope this helps.

  3. Mikhail Glushenkov says:

    Both `(&&)` and `(||)` have type `Bool -> Bool -> Bool`, so the monomorphism restriction can’t kick in, since the term `liftP (&&)` is already monomorphic (of type `InfoP Bool -> InfoP Bool -> InfoP Bool`).

  4. Jan Stolarek says:

    Andrea, thanks for detailed explanation. I still have to think about it, since not everything is yet clear to me, but I think now I’ll manage to understand what’s going on.

  5. Lalaine says:

    There’s at least one big exception to this being a good rule: cleasss with somehow mutually definable methods. For instance, Ordclass Ord a where compare :: a -> a -> Ordering ( a -> Bool …It actually has a lot of methods, and sensibly so, because any one of several works as the default (although, the defaulting facilities could be buffed as well: let me specify all possible defaults, with implementations in terms of each, instead of working out an implicit graph with one or two possible nodes like now).Another I want is:class … => Monad m where (>>=) :: m a -> (a -> m b) -> m b join :: m (m a) -> m aI should be able to pick which I want to define. Or both if I want. And allowing me to override some more specific combinators isn’t a bad idea either, like the new Functor:class Functor f where fmap :: (a -> b) -> f a -> f b ( f b -> f aApplicative and Monad are likely to have similar possible, this could be significantly more efficient for some implementations, methods. People seem averse to this sort of thing (and often suggest RULEs instead, which are unportable), but I don’t really see the problem with indulging a bit (you can obviously go overboard).As an additional aside: I’m not sure we can blame the various kinds of failure’ mess on multiple methods specifically. It’s a combination of factors.1. fail exists for dubious reasons that don’t have to do with a separate class. Failure was specifically intended to be possible for every Monad in H98.2. Alternative exists separately from MonadPlus because the latter predates Applicative, but there’s no reason to require all MonadPlusses to be a Monad. So it’s a hierarchical (and legacy code) issue.3. Monoid exists apart from the others (at least) because you cannot write a constraint like (forall a. Monoid (m a)). So it’s a type system issue.Anyhow, I don’t see anything wrong with one-function-per-class as a basic guideline, but I wouldn’t want it to be enforced by the language for instance (like it used to be in Clean).

Leave a Reply

(required)

Staypressed theme by Themocracy