I am nearly done with the main part of the project: constraint generation!
I have been testing the system and comparing it with GHC and the demo implementations of the two papers: Typing Haskell in Haskell and “Practical type inference for arbitrary-rank types”
This week has been full of surprises… everyday a new “strange” case arises that some Haskellers call it a bug and others call it an intended behavior! Despite the fun of hacking into the problem and reverse engineering the systems, it slowed down the process of the development and left us with the deadline stress.
For example, today I was checking my implementation if it “leaks” local-assumptions in pattern bindings and I was comparing the results with GHC. Here is minimal code to show the problem on GHC ( 7.4 ) :
data T a where
T1 :: (a ~ Bool) => a -> T a
T2 :: Bool -> T Bool
h1 y = let T1 n = y in n --h1 :: T t -> t ???
h2 y = let T2 n = y in n --h2 :: T t -> Bool
with some simplifications:
data T a where
T1 :: (a ~ Bool) => a -> T a
T2 :: Bool -> T Bool
f1 (T1 n) = n --f1 :: T t -> Bool
f2 (T2 n) = n --f2 :: T t -> Bool
g1 ~(T1 n) = n --g1 :: T t -> t ???
g2 ~(T2 n) = n --g2 :: T t -> Bool
Apparently, T2 is translated to T2 :: (a ~ Bool) => Bool -> T a not the type that we expect it to be: T2 :: (a ~ Bool) => a -> T a and the lazy pattern match cuts out the constraints so we end up with two different types.
I guess I have to leave the constraint generation part now (with all the bugs) and focus on the internals, mainly the constraint solver. It’s hard to estimate the timing, specially since the original typechecker didn’t have a complete constraint solver and there are no other (even demo) implementations at hand either. Moreover, there are two external parts that should be integrated to the system (in a long run): Haskell-Name-Exts for naming resolution and Haskell-Dependency-Exts for dependency analysis. Fortunately, I have full support of Niklas for the two (also for the constraint solver!).
I guess it is enough for now, I have few other technical points to share that I will in the weekend.
Shayan,
I am happy to hear about your progression! It makes me wonder though, do you have a public repo somewhere?
All the best,
Dan
In case you have not noticed:
http://cleantypecheck.wordpress.com/2012/09/05/hte-v-haskell-2010-at-github/
Hi Dan,
Not yet, there are so many dramatical refactorings / changes (I will explain soon in a new post) being applied to the code and I guess having a public repository would of no use, just misleading…
I am planning to share part by part (the actual code) here soon
/Shayan
Thanks for the update. How does your current implementation do with Haskell98, even without type classes? Can you say that your main problems are class and equality constraints? What’s your current goal for determining how complete the project is?
Hi Sean,
And thank you for following my work! In fact I have written multiple versions for typechecking Haskell 2010, RankN system and the constraint based system. The one for Haskell 2010 is fully functional (few parts are missing), i.e. you can pass HSE binding-groups to the checker and check/infer the types. Though, you need to pass the environments manually; it doesn’t work on HSE Module type yet. Niklas is working on the naming resolution package, so support for HSE Module is on its way.
I was talking about the constraint based system’s constraint solver yesterday which is incomplete at the moment. The main problem there is technically the implication constraint and scoping of untouchables.
The solver of Haskell 2010 version is complete; it also supports multi-parameter typeclasses.
My goal is much bigger than just a student summer project! working on this project spawned some other fun projects that I mentioned some in the blog (H?E s) . I will continue working on those projects and expand the typecheckers.
But officially, to call the GSoC project finished my mentor and mentoring organization should decide.
For the sake of Haskellers waiting to use outputs of this project, I guess releasing the Haskell 2010 checker (with few improvements) would be a good temporary solution. Then I have time to keep working on the constraint based system.
I will talk more in details soon in the blog.
/Shayan