Undocumented concepts: "type", "enum", "struct", "union"

[ThinkOpenly]

• type There is no obvious documentation for the "type" keyword, although it appears early in the tutorial, then in "Usage :: Other options". In the tutorial, I see:

  type xlen : Int = 64

  Is Int (capital I) a built-in type? If not, that could be confusing. "type variables" is a term referenced in the first section under "The Sail Language", but this term is not defined.

• struct The first appearance of the struct keyword appears in "Matching on structs". There is no documentation on its form or purpose before or after.

• enum Similar story as struct.

• union Same. There are some isolated references in "Scattered definitions".

[Alasdair]

Is Int (capital I) a built-in type? If not, that could be confusing.

In a sense. To be precise it's a built in kind, which is the type of a type, so we might say:

• 5 : int "five has type int"
• int : Type "int has kind Type", or "int is a type"

For something like bitvector, that is a type constructor with kind Int -> Type, means that bitvector creates a type by taking a type-level integer as an argument.

Most mainstream languages just have a single kind for all types, so don't expose this in the syntax, and very few languages have any higher-kinded polymorphism like Haskell (Sail does not have this either though) that would require distinguishing Type and Type -> Type in the syntax. Sail has this because we distinguish between integers, constraints, and 'regular types' in types (using the kinds Int, Bool, and Type).

In theory we could make this more transparent with some better kind-inference, as it should be possible to always infer kinds. Not sure how best to present this in the manual without going to deep into type theory.

[Alasdair]

There is now documentation for enum and struct in the manual. I will add the others hopefully this week.

[Alasdair]

Documentation for union has been added.

There is also now kind-inference, so one can now write just type xlen = 64, which should allow some examples to be simplified.

[Alasdair]

I've now added a section on type synonyms and type kinds as well.