Class and Object

Like most of programming languages, we use the class keyword to define classes.
After the definition, ABC is a Type.
Note that, the field b depends on the expression a from previous fields, this is called dependent record type,
A class is like a sigma type (dependent pair type), while a very important difference is that the names of fields are significant.
For example, the following class has similar field types as ABC, but since it has different field names, it is not the same type as ABC.
We can use { ... } to construct objects of a class.
  • Note that, when using { ... } to construct objects, the commas between fields is required, while when using class { ... } to construct classes, the commas are optional.
We can get the fields of an object by the dot notation.
Being a dependent record type means that the type of a field can depends on the values of the previous fields.
Here is another ABC, note how the type of b is different from my_abc.
An object can has extra fields not specified by the class.
When we claim an object is ABC, as long as the fields specified by the class all pass the type check, we know our claim is right.
A class can be nested.
An object can also be nested.
If we already defined the name a, b and c as the following,
Then, instead of repeating the same name twice for each fields,
We can use the following shorthand.
Another useful syntax about constructing object is called "spread".
If we have an object with b and c,
We can spread it out using ...bc.