This week I’ve been working on the new constraint-based type-system for Roy. I’ve been working on it for a few months but got a bit stuck recently with typing algebraic data type definitions. I think I properly implemented that and I’m up to pattern matching.

I’m basing the work off Generalizing Hindley-Milner Type Inference Algorithms (PDF) - a way of achieving Hindley-Milner via constraints; rather than the environment in Algorithm W. The big benefit is that it delegates unification until the end of constraint generation. My understanding is that this will help with structural typing since I’ll be able to generate proper subtype constraints - instead of the hacky, buggy stuff I’ve done until now.

I’m probably a while away from finishing the core of the type-system but then I can move onto Rank-2 types, hopefully allowing me to implement Tony Morris’ lens-proposal work - allowing automatic lens generation from Roy types!