search

sdiehl / write-you-a-haskell

Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
MIT License
3.34k stars 256 forks source link

make calc build and fix poly #33

Closed chsievers closed 9 years ago

chsievers commented 9 years ago

calc doesn't build (for me) without the first two commits. poly has some type inference bugs -- see commit message. However you fix it, the change should be mirrored in 006_hindley_milner.md. BTW, why does that correspond to code in chapter7/ ?

Thanks for your very nice work! You made me finally create a github account...

sdiehl commented 9 years ago

The chapter 3 stuff looks good. Only reason they weren't in sync is my fault.

The chapter 7 might have had some pathological cases. As far as I understand you fixed this by baking the ifthenelse and fix operators as typed "primops" in the language?

chsievers commented 9 years ago

Yes, kindof. I guess usually you do this at the parsing stage, but here it is only for type inference, so I use the same variable int#int->int for +, - and *. First I tried to fix the code by applying the substitutions where needed, which helped but I didn't get it completely right. Looking into Damas/Milner showed me that the code for the App case is correct and that one can't just apply every substitution everywhere. One could figure out what to do in the other cases, but I decided to let the computer do the work.

sdiehl commented 9 years ago

I did the equivalent of inlining the App calls. Think this should fix the cases you noticed. The original Milner Algorithm-W with explicit substitutions is kind of subtle. Thanks for noticing the problem.

Poly> (\x -> if x then x else (x+1))
Cannot unify types: 
    Int
with 
    Bool
Poly> (\x -> if x then 1 else (x+1))
Cannot unify types: 
    Int
with 
    Bool
Poly> (\x -> if x then (x+1) else 1)
Cannot unify types: 
    Int
with 
    Bool
Poly> :type (\x -> fix (x 0))
<<closure>> : forall a. (Int -> a -> a) -> a
chsievers commented 9 years ago

In the If case of infer, you are not using s1 at all. That can't be right.

Poly> let not x = if x then False else True
Poly> \x -> if (not x) then x else (x+1)
<<closure>> : Int -> Int

I think you have to type check tr and fl in extended environments, and return the composition of all substitutions.

There are still similar problems with the Op case:

Poly> let b2i x = if x then 1 else 0
Poly> \x -> (b2i x) + x
<<closure>> : Int -> Int
Poly> (\x -> (b2i x) + x) 0
poly: Pattern match failure in do expression at Eval.hs:58:5-12