lang: add inductive data types

[zerbina]

Add inductive data types to the source language, which are what some other programming languages call enum types, or just data types.

This is a work in progress. At the moment, there only exist tests, showcasing how the feature is intended to work.

---

To-Do

• make a separate PR for placing types into a separate namespace
• add the abstract syntax
• add the static and dynamic semantics
• implement the feature in source2il
• extend the set of tests
• write a commit message

[zerbina]

A Q&A intended to describe the thought process behind the current design and to answer some questions one may have:

Q: What's the type of a constructor?
A: A ProcTy, meaning that it can be used as a first-class procedure value itself. When called directly, the compiler simply inlines the call.

Q: Why do constructors also introduce a type?
A: Because it's useful to be able to refer to all values of a kind. For example, it allows writing procedures that easily and statically enforce that their input is of a certain kind. Without the type, something like run-time assertions would have to be used.

Q: How does the identifier overloading work? Don't types and values/variables share a namespace?
A: Yes, at present they do, but the plan is to separate the namespaces.

Q: Having to (Constr x) for nullary constructor matching is cumbersome. Why not allow just the identifier?
A: Because patterns are meant to only refer to types, and the nullary constructor defines a value. That said, having nullary constructors also introduce a type (which could then be used in patterns) seems like a good idea.

Q: How do inductive data types relate to NimSkull's enum types?
A: NimSkull's enum types are largely the same as inductive data types with only nullary constructors.

Q: Should there be a dedicated enum type?
A: I tend towards "no", but I'm not sure. It would allow for better communicating the intention behind the type, giving a name to the concept of "inductive data type with only nullary constructors (i.e. values)". Some form of pragma/attribute/annotation might work just as well, however.

Q: Why is inductive data type recursion disallowed?
A: For two reasons:

1. the type IR for source2il doesn't support any form of recursive type
2. how recursive types should behave in the type system (isorecursive vs. equirecursive) is not yet clear, and therefore it's also not clear how the actual storage should (e.g., implicit heap allocation)

Recursion for inductive data types is definitely going to be revisited in the future. At the very least, the same form of recursion as is possible in NimSkull should also be possible in the source language.

Q: Should inductive data types be allowed to extend existing inductive data types?
A: Yes! My plan is for every inductive data type definition to include an (optional) inductive data type reference. The extending type becomes a super type of the extended type, meaning that all values of the extended type can be used (with implicit widening) where the extending type is expected. This is possible without the types having to be part of the same module.

Q: How will inductive data types be represented in memory?
A: As a tagged union, most likely.