When are two types equal? Consider these two declarations:
Student = { name: String, address: Int };
Code_Module = { name: String, address: Int };
Should these be considered two different types, or two names for the same type?
Should the compiler let us store values of one type in variables declared with the other type?
There are two schools of thought on this subject. Neither is right or wrong; each has advantages and disadvantages, and each has been used successfully in both theory and practice.
One school of thought focusses on structure. If two types have the same basic structure, if mathematically there can be no problem in using them interchangably, then they are equivalent.
According to this school of thought, the above two types are both records, they both have fields of the same name, and those fields have the same elementary types. Substituting a value of one type for a value of another type cannot possibly make any mathematical difference in the course of the computation. Therefore, the two types are the same, just different names for the same thing.
The other school of thought focusses on names. The clear intent of the coder is that Student records represent humans, giving their name and room number (or some such), whereas Code_Module records represent bits of executable code, giving their declared name and their current location in memory. Treating a room number as a memory address cannot possibly give rational results, nor is adding the name of a code module to a class enrollment list likely to accomplish anything useful.
According to this school of thought, the above two declarations were written for entirely different purposes, and the compiler should definitely do its best to prevent inadvertent mixing of the two types of values.
As a matter of practice, the name-oriented approach to typing has tended to dominate in programming languages developed by working programmers for industrial use — languages like C. It is very simple to implement and understand.
The structure-oriented approach, by contrast, has tended to dominate in programming languages developed by computer science theoreticians for research purposes. It has very clean mathematical semantics.
The Mythryl type system belongs to the structure-oriented school. If it were not, almost none of the machinery we have covered in these tutorials would be workable. For example, almost every call to a function implicitly defines an anonymous tuple type. Lacking names, a name-oriented compiler would be unable to decide whether that function call made sense from a type point of view. The structure-oriented approach, by contrast, has no problem doing type analysis of such masses of anonymous tuple types.
One major exception is that every sumtype declaration creates a new type:
package a { Color = RED | GREEN | BLUE; };
package b { Color = RED | GREEN | BLUE; };
The two types a::Color and b::Color are different even though their definitions are identical. If you want them to be equal, you should have one package borrow its definition from the other:
package a { Color = RED | GREEN | BLUE; };
package b { Color = a::Color; };
Still, that far from exhausts the discussion.
What does one do if one definitely wants to create a new type distinct from all others? What happens when a type is exported but its definition is not? Are two such types exported from different modules equivalent or not?
Theoreticians can and do spend entire careers exploring such questions and the consequences of different policy choices. Grab a copy of Pierce’s Types and Programming Languages if you’re interested. Here we are just going to summarize the basics of what Mythryl does and how to take advantage of it in practical programming.
First a bit of nomenclature. A type is opaque if it is exported from a package without exposing its underlying structure. It is transparent otherwise. For example:
api Silly {
My_Opaque_Color;
My_Transparent_Color = RED | GREEN | BLUE;
};
package silly: Silly {
My_Opaque_Color = RED | GREEN | BLUE;
My_Transparent_Color = RED | GREEN | BLUE;
};
Here the colors My_Opaque_Color and My_Transparent_Color are exactly identical within package silly. But due to package silly being cast to api Silly which hides the definition of My_Opaque_Color, the external world knows exactly what the definition is of My_Transparent_Color, but has absolutely no clue about the definition of My_Opaque_Color.
The critical Mythryl typing rules are thus three:
One practical consequence of this is that if, as a programmer, you wish to create a type which is distinct from all other types in the system, the way to do so is to export it as an opaque type from a package.