Gagallium

My PhD thesis manuscript is sent for review and I finally have some time to write a blog post about it! It presents a framework of coercions to describe and unify existing type systems. In particular, all erasable type system features (such as coherent polymorphism) are expressed as coercions, which can be seen as a subtyping relation between erasable typings.

A few days ago Kate Deplaix came to ask me this question: when using the include trick to override some definition in a module, how can we also override some definition in a submodule? The answer is short – just scroll to the last code block – and may be of interest to some readers.