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)
The explicit forall is needed to introduce the scoped type variables
so that I can prescribe the type of |wrap|. After that, the
monomorphism restriction on |wrap| takes care of the rest of my
worries (that there is only one |m|, only one |c|, and only one |v|).
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 mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
