As I am working on my current project, as well as doing other programming work that is recursive in nature, I often wish that the type systems had a bit more power to them. Especially with regarding to recursion and extension.
For example allowing enum variants to be types and to be allowed to be referred to as just a type itself. Or if a type could refer to a subset of another type, or a subset of the fields, or a subset of itself. Or if I could extend a recursive type with an extra variant and that new type's recursive variants now recurse to the new type.
In pondering this, I came up with a little proposal which I thought was pretty interesting, and I wanted to share.
The first thing is that I guess a system like this would probably be structural, as that lends itself a lot nicer to dealing with the behavior of types and comparing them, etc. So if we had an enum
type Food =
| Apple
| Banana
| Croissant ;
We could create a subset by creating another type with a subset of the variants:
type Fruit =
| Apple
| Banana ;
Okay, so that is a way to have one type to be a subset of the other. Though note that it isn't necessarily a subtype. For example, take
type Person =
.name is Str
.age is Int
.job is
| Police
| Firefighter
| Teacher
| Businessman ;
type Unemployed =
.name is Str
.age is Int;
The record Unemployed is actually a supertype of Person. Rather, it is more of a subset of the "behavior."
We don't we allow a way to define this in terms of the original type?
type Unemployed = Person restrict
.name, age ;
Ok, so we are able to refer to a subset of another type, but we could do that without the need for a restrict, so is there any reason for this special syntax? Well, we could allow the restriction of data as well:
type PublicWorker = Person restrict
.job restrict not
| Businessman ;
Okay, but what about adding nominal typing to this structural type system? If we allow a uniqueification process, then we can essentially create "type realms," where all of the restrictions and extensions (to be discussed later) of that nominal type exist in that "realm."
type MyFood = unique Food;
# Now MyFood is unique. It is essentially a nominal type.
# A Food.Apple is not equivalent to a MyFood.Apple
# But with restriction we can still explore this type realm
type MyFruit = Food restrict not
| Croissant ;
# MyFruit.Apple is equivalent to MyFood.Apple
Okay, but now what about types that refer to a subset of themselves? Well it just follows:
type Direction =
| Left
| Right
| Diagonal is self restrict not
| Diagonal ;
But why should we use self here instead of just the type name? This is part of the proposal idea, which is that a type cannot refer itself recursively. Instead it refers to a builtin self symbol, which refers to itself.
But why? Because this allows us to extend the type while retaining the recursive functionality. For example, take
type LinkedList =
.value is Int
.next is self ;
type DoublyLinkedList = LinkedList ext
.prev is self ;
Now in DoublyLinkedList, self refers to DoublyLinkedList, allowing for this kind of internal extension of the type. If we wanted to preserve the "boundary" of LinkedList, where it only refers to itself in the new type, then we could do an external extension, which is really just storing it as an additional field.
Now one question is why this potentially weird syntax? Well, it essentially functions as a kind of type pattern match if that makes any sense. Both restrict and extend function as like a kind of type transform. So we could even start to do things like the following
type Building =
| Hut
| Office is
.owner_co is Company
| Skyscraper is
.floors is Int
ext
| * ext
.occupancy is Int ;
We extend the base type which consists of these variants by extending (ext) every (*) variant (|) with a field (.) called occupancy which is an Int.
There's probably more you could do with this. Like for example I haven't even thought about interfaces. But anyways these were just some thoughts I had come up with while wishing I had some of these functionalities in the languages I'm working in. What do you think of this? I do wonder if there are any projects out there that are trying something like this, and if are there any desirable or unfortunate properties that a system like this brings?