[Haskell-cafe] Re: 6.4 -> 6.6, scoped type variables

[oleg at pobox.com]

I too miss the old way of handling local type variables. Previously,
local type annotations worked a lot like an additional constraint,
with type variables denoting some type. The same type variable denoted
the same type. Here's how it works in OCaml, for example:

# let pair x y = (x,y);;
val pair : 'a -> 'b -> 'a * 'b = <fun>
# let pair1 (x:'a) (y:'a) = (x,y);;
val pair1 : 'a -> 'a -> 'a * 'a = <fun>
# let pair2 x y = ((x:'a),(y:'a));;
val pair2 : 'a -> 'a -> 'a * 'a = <fun>
# let pair3 x (y:int) = ((x:'a),(y:'a));;
val pair3 : int -> int -> int * int = <fun>
# let pair4 x (y:int) = ((x:'a list),(y:'a));;
val pair4 : int list -> int -> int list * int = <fun>
# let pair5 (x:'a list) (y:int) = (x,(y:'a));;
val pair5 : int list -> int -> int list * int = <fun>

Which of the two occurrences of the type variable |'a| a binding one? Who
cares... It just works: within the same expression, the same type
variable stands for the same type.

> 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

It seems that with GCH 6.6, we are forced to go back to the fourth
method -- the one that was available back in Haskell98. Use useless
expressions to hint the typechecker.

> 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.

It seems that you wish that, for example, v0 and v1 be of the same
type. We have to be direct then and write
   where fn'' v1 = inj (lazyPrj v0 `op` lazyPrj (v1 `asTypeOf` v0)
or
   where fn'' v1 = inj (lazyPrj v0 `op` lazyPrj v1)
           where useless = if True then v0 else v1
or
   where fn'' v1 | const True [v0,v1] = inj (lazyPrj v0 `op` lazyPrj v1)

or something similar...