Add syntax for type-related facilities

[j-hui]

We need the following:

• syntax for ADTs (@EmilySillars)
• syntax for type classes definitions, instance definitions, and type class constraints (@leoqiao18)
• syntax for type variables (@XijiaoLi)
• syntax for record type getters and setters

I tagged some relevant authors here since they will likely find this syntax useful for constructing test cases as they continue to work on the implementation, but @hmontero1205 and I can also help out.

---

For the first cut, we should just use syntax similar to what Haskell uses, without idiosyncratic keywords like data, newtype, etc., and with support from our lexer's layoutNL system:

type Option a =
  Some a
  None

class Eq a
  eq : a -> a -> Bool

inst Eq Bool
  eq a b = // definition

not (a: a) (b: b): Bool where (Eq a, Eq b) = // definition

Something like that (perhaps people have thoughts?)

---

As for the record types, we do need to think a little more carefully about how the field accessors are designed to be used, and how that plays with the assignment operation. OCaml and Haskell set an example of constructing functions out of the field names which access the variable, but they each make talking about deeply nested fields awkward in different circumstances. I'd like to avoid this awkwardness from the get-go and try to have something like Haskell's lenses baked into the language syntax (rather than relying on typeclass wizardry to achieve readable syntax).

[sedwards-lab]

This is exactly what I have in mind for type declarations. "type" is a keyword that introduces a new data type, typically algebraic. Do we need two keywords like Haskell done, one for creating type aliases and one for creating new types, or can get away with "type" for both?

Let's decide whether we want to call these classes or something else, but the syntax here is also what I had in mind.

For definitions with typeclass constraints, first, we should define a "type literal" syntax. Using "where" should work:

a -> b -> Bool where { Eq a ; Eq b }

so we can make where another layout keyword, e.g.,

a-> b -> Bool where
     Eq a
     Eq b

For the "name the arguments" style, we can probably do something similar, e.g.,

not (x : a) (y : b) -> Bool where { Eq a; Eq b } =

but it's important to understand these are slightly different.

[j-hui]

Do we need two keywords like Haskell done, one for creating type aliases and one for creating new types, or can get away with "type" for both?

I think we should stick with one for now, and just not support type aliases for now. And once we do get around to supporting them, I still think type should mean "define a new type", rather than its meaining in Haskell (which I find confusing). Perhaps for type alises we could do like type alias or just alias or something.

[j-hui]

I also like the idea of making where a layoutNL keyword