Closed VitorCBSB closed 7 years ago
I'll take a look at this.
I am certainly no expert, so take this comment with a grain of salt, but I took a glance at this, and it looks right to me. I think it might be possible to implement it more nicely, though, by keeping the use of RWS
and using listen
from MonadWriter
instead of manually threading the results around.
I know this is several years late, but there is indeed a better solution, which I found while trying to build my own compiler as a learning exercise, using the code here as a starting point.
in particular, the code
infer expr = case expr of
...
Let x e1 e2 -> do
env <- ask
t1 <- infer e1
let sc = generalize env t1
...
should be
infer expr = case expr of -- < I would also use LambdaCase here
...
Let x e1 e2 -> do
env <- ask
(t0, constraints) <- listen $ infer e1
subst <- liftEither $ runSolve constraints
let t1 = apply subst t0
sc = generalize env t1
...
The issue, as I'm sure is well known, is that we generate constraints for the type variable in the scheme bound to x
, which are never solved because each use of x
causes instantiation of its scheme. This is not a problem if x's type should truly be universal, but this is rarely the case. My simplest breaking example was \y -> let x = y + 1 in x
. We generate the type y :: a
and the scheme x :: forall b. b
. We also generate the constraints a ~ Int
and b ~ Int
, where the latter will never be used. In the body of the let
, we instantiate x
to x :: c
. Then we solve our constraints and produce the incorrect type forall a. Int -> a
.
This can be fixed simply by listening to the constraint generation while inferring the RHS of the binding, solving the constraints, and applying the substitution to to the type of e1
before generalizing it. Now we correctly generate the type y :: a
and the scheme x :: forall . Int
.
The algorithm referenced in #82 warns of a caveat with generalization, but the existing logic seems to already handle it; the given example:
(\f x -> let g = f in g 0) (\x -> if x then True else False) True
fails the type checker.
Attempts to fix issues #72 and #82 regarding let polymorphism. Inference works correctly for the functions provided in them and they have been added to the test.ml file. Big thanks to @Azure-Vani for the pointer to his / her implementation as well as providing the algorithm described in TAPL.
For this fix, I had to radically change the
infer
function's interface, and alter the Infer monad to being a simpleState
+Reader
+Except
instead ofRWS
(theWriter
part was not being used). This might not be good for readability, but it's the solution I could come up with.Additionally, this is going to need to be reflected in the text, but I'm not confident enough to submit changes to it.