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 ?
[EMAIL PROTECTED] (/\s. return@(ST s)@?a ([EMAIL PROTECTED])) 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
([EMAIL PROTECTED]) ([EMAIL PROTECTED]@?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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
