[Haskell-cafe] Composing functions with runST

Simon Peyton-Jones simonpj at microsoft.com
Mon Jan 1 12:26:27 EST 2007

Conor and others are right; it's all to do with type inference.  There is nothing wrong with the program you are writing, but it's hard to design a type inference algorithm that can figure out what you are doing.

The culprit is that you want to instantiate a polymorphic function (here (.) or ($) in your examples) with a higer-rank polymorphic type (the type of runST, in this case).  That requires impredicative polymorphism and while GHC now allows that, it only allows it when it's pretty obvious what is going on --- and sadly this case is not obvious enough.

The system GHC uses is described in our paper


| -----Original Message-----
| From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-bounces at haskell.org] On Behalf Of
| Conor McBride
| Sent: 01 January 2007 13:49
| To: haskell-cafe at haskell.org
| Subject: Re: [Haskell-cafe] Composing functions with runST
| 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
| _______________________________________________
| Haskell-Cafe mailing list
| Haskell-Cafe at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe

More information about the Haskell-Cafe mailing list