Starting understanding of Unification and Type Inference

[CMCDragonkai]

http://dev.stephendiehl.com/fun/006_hindley_milner.html

We need to type check compatibility between QoS specs and Protocol Specs.

[CMCDragonkai]

@olligobber

[CMCDragonkai]

• https://winterkoninkje.dreamwidth.org/100478.html
• http://dev.stephendiehl.com/fun/006_hindley_milner.html#unification

There are example unification libraries here: https://hackage.haskell.org/package/unification-fd

@olligobber Please update your progress here.

[CMCDragonkai]

The article: http://dev.stephendiehl.com/fun/004_type_systems.html

Gives a starting point for how you translate type theory that is written in books like PFPL (https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf) to actual Haskell code.

Most of it is just writing a type checker and evaluator. The evaluator matches the evaluation rules (pattern matching the ADT), while the type checker matches the typing rules.

The language is just represented as an ADT.

Note that you would have wrappers around this core, that first lexes tokens and parses tokens into into the ADT.

The PFPL book goes through several foundational concepts and incrementally introduces languages from simple natural number + calculator expressions to more complex languages that involve new concepts. We have the Language E, Language T, Language F (System F)... etc separated by chapters.

[CMCDragonkai]

Not relevant anymore.