When it comes to typecheckers, the expectations are high. We expect them to be defect free and function exactly as expected. Earlier, I argued that it cannot easily be achieved without translations to a more solid and accepted setting. For the very same purpose, to make the typechecker as solid as possible I developed a version (v.Haskell 2010) based on the standard and accepted methods.
Firstly, the core part of the typechecker is nearly identical to the one (THIH) developed (and extended) by Mark P. Jones. The desugaring system is carefully coded to follow translations defined in Haskell 2010 language report. Kind inference is done by the typechecker itself; it employs the demotion schemes described earlier. Finally, the layered architecture of the project keeps each part separated.
The system is composed of the following components:
- HSE – Parser
:: (User input – Haskell 2010 :: String) -> AST - Desugaring System
:: AST -> Desugared AST - ToTHIH
:: Desugared AST -> Surface THIH Syntax (implicitly kinded) - Kind Inference
:: Surface THIH Syntax -> Original THIH Syntax (explictly kinded)- Demotion
:: Types of Surface THIH Syntax -> THIH Expressions - Typeinference (THIH)
:: THIH Expressions (implicitly typed) -> Inferred Types - Promotion
:: Inferred Types -> Inferred Kinds - Syntax Conversion
:: (Surface THIH Syntax, Kinds) -> Original THIH Syntax
- Demotion
- Loading
:: Module Headers / Top-level declarations -> Environment - THIH
:: Original THIH Syntax -> Environment -> THIH Assumptions - FromTHIH
:: THIH Assumptions -> Pretty Assumptions
Is the code available yet?
In case, you have not noticed:
https://github.com/shayan-najd/HTE
Yes, soon I will put a snapshot (08/20) of it for public access. And thanks for your interest.