chrisnevers / bidirectional-typechecking Goto Github PK

In section 2.1 Dunfield and Krishnaswami explain that sum, product and recursive types can be easily added to this type checker. I'm very new to type theory and it's not very clear how to do so, an example here would be very helpful.

Im trying to read this together with the paper to reimplement this type system in go. Although the interpreter is simple, there are some things (like acronyms) that are not instantaneous to understand.
If you added some explanations of the internals in comments/github page it would be easier to reimplement and associate concepts/types/functions with the paper. Also, if you specified which rules are being applied in typecheck.ml it would also be a lot easier to associate pattern matching cases with the judgments in the paper.

For example, how are recursive functions achieved?