Closed Azure-Vani closed 7 years ago
@sdiehl Could you provide any information for this issue?
Simpler example
let id x = x
let foo x = let y = id x in y + 1
:type foo
return forall a. a -> Int
instead of Int -> Int
after let y = id x
, y
has type forall b. b
and when lookupEnv
for y
is used in y + 1
it uses instantiate
over this type so there is no connection between type b
and type Int
I use this approach in my language. Is there any simple way to fix it or it would be easier to rewrite it with poly
approach?
@user471 You can fix that by the algorithm described in Types and Programming Language
To avoid this re-typechecking, practical implementations of languages with let-polymorphism actually use a more clever (though formally equivalent) re-formulation of the typing rules. In outline, the typechecking of a term let x=t1 in t2 in a context Γ proceeds as follows:
- We use the constraint typing rules to calculate a type S1 and a set C1 of associated constraints for the right-hand side t1.
- We use unification to find a most general solution σ to the constraints C1 and apply σ to S1 (and Γ) to obtain t1’s principal type T1.
- We generalize any variables remaining in T1. If X1. . .Xn are the remaining variables, we write ∀X1...Xn.T1 for the principal type scheme of t1. 334 22 Type Reconstruction
One caveat is here that we need to be careful not to generalize variables T1 that are also mentioned in Γ , since these correspond to real constraints between t1 and its environment. For example, in λf:X→X. λx:X. let g=f in g(x); we should not generalize the variable X in the type X→X of g, since doing so would allow us to type wrong programs like this one: (λf:X→X. λx:X. let g=f in g(0)) (λx:Bool. if x then true else false) true; We extend the context to record the type scheme ∀X1...Xn.T1 for the bound variable x, and start typechecking the body t2. In general, the con- text now associates each free variable with a type scheme, not just a type. Each time we encounter an occurrence of x in t2, we look up its type scheme ∀X1...Xn.T1. We now generate fresh type variables Y1...Yn and use them to instantiate the type scheme, yielding [X1 Y1, . . . , Xn Yn]T1, which we use as the type of x.4
You can fix that by the algorithm described in Types and Programming Language
Do you know any Haskell implementation of this algorithm?
I am also struggling with this error and can't seem to crack it. Anyone here cracked it or have pointers to solutions?
@user471 @molysgaard you guys can refer to my repository Hkael which is a simple control flow analysis framework for Haskell. It implements a derivation of Hindley-Milner inference correctly and maybe you will find inspiration to solve the issue.
Fixed by #89
Consider following expressions:
The accurate type of
f
isBool -> Bool
butforall a . a -> Bool
was given by poly_constraints. The reason is that poly_constraints doesn't substitute type variables in constraints set when instantiate a type scheme with fresh variables. (i.e. there are still some constraints witha
althoughforall a . a -> a
has been instantiated by other fresh variables)