Comments (6)
@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?
from write-you-a-haskell.
@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 ReconstructionOne 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
from write-you-a-haskell.
You can fix that by the algorithm described in Types and Programming Language
Do you know any Haskell implementation of this algorithm?
from write-you-a-haskell.
I am also struggling with this error and can't seem to crack it. Anyone here cracked it or have pointers to solutions?
from write-you-a-haskell.
@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.
from write-you-a-haskell.
Fixed by #89
from write-you-a-haskell.
Related Issues (20)
- Ebook & AZW3 (for kindle) versions of PDF HOT 3
- Cabal-simple_mPHDZzAJ_1.22.5.0_ghc-7.10.3: can't find source for Main in .
- includes.hs: createProcess: runInteractiveProcess: exec: does not exist (No such file or directory)
- Error in characterization of free theorem for functors
- Unification fail in type checker HOT 1
- Seems dead HOT 3
- Unable to compile with current toolchain HOT 1
- Addition does not work in poly
- Doesn't it unit in line 34?
- Liberate this proprietary work HOT 18
- Error in substitution algorithm HOT 1
- Inconsistency between poly/poly_constraints type inference HOT 1
- epub format HOT 12
- SKK /= I in chapter 4 HOT 2
- Cabal & Stack has nothing on Stack?
- Is this project dead? :( HOT 12
- HM chapter on website needs sync
- Error in T-Lam Rule in chapter 5
- Parser/Type error for + and - HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from write-you-a-haskell.