[Haskell-cafe] Composing functions with runST

[Conor McBride]

Hi

Yitzchak Gale wrote:
> Can anyone explain the following behavior (GHCi 6.6):

I don't know if I can explain it entirely, or justify it properly, but I 
do have some idea what the issue is. Type inference with higher-ran 
types is weird. The primary reference is

  Practical type inference for arbitrary-rank types
  Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark 
Shields.
  To appear in the Journal of Functional Programming.

  http://research.microsoft.com/~simonpj/papers/higher-rank/index.htm

  'The paper is long, but is strongly tutorial in style.'

Back in the Hindley-Milner days, we knew exactly what polymorphism could 
happen where. All the free type variables were existential (hence 
specialisable); generalisation over free type variables happened at let. 
Unification was untroubled by issues of scope or skolem constants. The 
machine could always guess what your idea was because you weren't 
allowed to have interesting ideas.

Now you can ask for polymorphism in funny places by writing non-H-M 
types explicitly. As in

  runST :: (forall s. ST s a) -> a

When you apply runST, you create a non-let source of (compulsory) 
polymorphism. You get a new type variable a and a new type constant s, 
and the argument is checked against (ST s a). Let's look.

> Prelude Control.Monad.ST> runST (return 42)
> 42

Can (return 42) have type ST s a, for all s and some a? Yes! Instantiate 
return's monad to (ST s) and a to the type of 42 (some Num thing? an Int 
default?). In made up System F, labelling specialisable unknowns with ?

  runST@?a (/\s. return@(ST s)@?a (42@?a))   such that   Num ?a

Now what's happening here?

> Prelude Control.Monad.ST> (runST . return) 42

We're trying to type an application of (.)

  (.) :: (y -> z) -> (x -> y) -> (x -> z)

We get two candidates for y, namely what runST wants (forall s. ST s a) 
and what return delivers (m b) and these must unify if the functions are 
to compose. Oops, they don't.

The point, I guess, is that application in Haskell source code is no 
longer always translated exactly to application in System F. We don't 
just get

  (runST@?a) (return@?m@?b)   such that   (forall s. ST s ?a) = ?m ?b

we get that extra /\s. inserted for us, thanks to the explicit request 
for it in the type of runST. The type of (.) makes no such request. Same 
goes for type of ($), so runST behaves differently from (runST $).

It's a murky world.

Happy New Year

Conor