You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Reading through the paper again, their main argument is related to problems with constraint based type systems.
Koka uses something closer to simple Hindley Milner so it does not have that problem.
Additionally they state that generalization is not used much and so only in a very slim number of cases do you need it.
In contrast I believe that the effect system of Koka makes this a much bigger issue here.
Let's take for example one of their examples of the issue:
dataSawhereMkS::Showa=>a->Safs::a->Sa->Bool
fs x y =let h z =show x
incase y ofMkS v ->show v ++ h ()
This does not type check in Haskell, but with let generalization it would (since the function h would be generalized to include a Show constraint).
Koka does not have the same problem, show instances do not get populated in datatypes and implicitly destructured, additionally generalizing lambdas does not add implicit arguments.
Instead this function would require a show instance, and be captured as a free variable in the lambda instead of propagated via constraints, and if you do want to add a show instance to a datatype it will be an explicit lambda that you would have to access from the datatype.
Currently Koka instantiates at lets, this causes issues with using a function at multiple different effects.
Making that small change would solve the following issues.
#401
#402
Daan has been concerned whether this will cause other issues, due to some issues mentioned in this paper:
Let should not be generalized
We should investigate whether Koka has the problems listed in the paper, and if not, let generalize, which would make the effect system a lot nicer.
The text was updated successfully, but these errors were encountered: