[Haskell-cafe] 6.4 -> 6.6, scoped type variables, prescribing poly-/mono-morphism

17 Oct 2006

      I've been writing some code that relies heavily on the type system.
Some of my polymorphic functions end up too polymorphic.

I'm looking for some tips and references regarding prescribing
poly-/mono-morphism. I know of three ways to do it:
 1) rely on the monomorphism-restriction -- kind of scary in that its
not explicitly obvious
 2) introducing scoped-type variables of interest -- explicit and modular
 3) introducing all type variables with a forall -- explicit but not modular

The rest of this email is a discussion of a particular problem I'm
having. Scoped-type variables worked in 6.4, but no longer in 6.6. I'm
sure there's good reasons for this (I think I found a Peyton-Jones
message regarding it in 6.4->6.5) I just didn't quite catch on to
them.

The problem is in the |bop| function:

class SubType a v where -- the lack of fundeps is required by design
  inj :: a -> v
  lazyPrj :: v -> Maybe a

bop :: forall x y z m c v .
       ( SubType x v, SubType y v, SubType z v
       , SubType (Fun m c v) v
       , Monad m, Comonad c
       ) => (x -> y -> z) -> Fun m c v
bop op = Fun fn
    where fn = wrap fn'
              where fn' v0 = (inj . Fun) (wrap fn'')
                        where fn'' v1 = inj (lazyPrj v0 `op` lazyPrj v1)
          wrap :: (v -> v) -> (c v -> m v)
          wrap = (return .) . (. counit)

If I leave the types to inference (i.e. drop the forall and the type
ascription for |wrap|), then I end up with this type

bop :: ( SubType x v2, SubType y v1, SubType z v1
         , SubType (Fun m c v1) v2
         , Monad m, Comonad c
         ) => (x -> y -> z) -> Fun m c v2

Note the multiple |v|s; they wreak havoc in the rest of my code. (The
monomorphism restriction still takes care of the |m| and |c|.)

I'd like to not have to introduce the forall, because with that comes
introducing the entire context of the type. Thus I have to maintain
any changes to the context, which I would prefer to leave to inference
for modularity's sake.

In 6.4 I was able to fix this without having to introduce the forall;
I could introduce scoped type-variables in patterns to get the job
done. That felt a bit like voodoo, especially when trying to get it
right for 6.6--which I gave up on doing. I can post the code that
works with 6.4 if anyone would like to see it (I just can't find it at
the moment).

I know there's some work on introducing partial signatures (fun pat |
False = ...), but I don't see how to prescribe monomorphism for
particular type variables in that way.

Any thoughts on how to get the preferred signature using scoped-type
variables in 6.6? I'd also welcome any references you might think are
relevant.

Thanks for your time,
Nick

[Haskell-cafe] 6.4 -> 6.6, scoped type variables, prescribing poly-/mono-morphism

Nicolas Frisby