[Haskellcafe] Composing functions with runST
Simon PeytonJones
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 higerrank 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
http://research.microsoft.com/~simonpj/papers/boxy
Simon
 Original Message
 From: haskellcafebounces at haskell.org [mailto:haskellcafebounces at haskell.org] On Behalf Of
 Conor McBride
 Sent: 01 January 2007 13:49
 To: haskellcafe at haskell.org
 Subject: Re: [Haskellcafe] 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 higherran
 types is weird. The primary reference is

 Practical type inference for arbitraryrank 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/higherrank/index.htm

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

 Back in the HindleyMilner 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 nonHM
 types explicitly. As in

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

 When you apply runST, you create a nonlet 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

 _______________________________________________
 HaskellCafe mailing list
 HaskellCafe at haskell.org
 http://www.haskell.org/mailman/listinfo/haskellcafe
More information about the HaskellCafe
mailing list