TM011 Types in Core

Additions for types:

type: alias for types. ie,

type Foo = Number + String
type Bar<A> = List<A>
type Prim = Number(is-prime)

newtype: a way of constructing new types.

syntax:

newtype TypeName with Constructor [of Type]

semantics:

creates a type with name TypeName (this is a tag), and a constructor that has type: Type -> TypeName (ie, it adds the tag TypeName, assuming that the value has type Type). If [of Type] is missing, the constructor has type Any -> TypeName example: (note that this reflects the semantics of how we build lists currently)

newtype List<A> with mkList of Empty<A> + Link<A>
newtype Empty<A> with mkEmpty
newtype Link<A> with mkLink of {first :: A, rest :: List<A>}
fun<A> empty() -> Empty<A>:
  mkList(mkEmpty({}))
end
fun<A> link(f :: A, r :: List<A>) -> Link<A>:
  mkList(mkLink({first: f, rest: r}))
end

The point of the from clause is it allows the compiler to reason statically about structural (or other) properties of values with TypeName.

typecase: dispatching on types.

syntax:

typecase(Type) expr:
  | Type1 => expr1
  | Type2 => expr2
  ...
end

semantics: expr should be a subtype on Type, and Type1 + Type2... should be equal to Type. This will evaluate to expr1 if expr is a subtype of Type1, and within expr1, expr will have type Type1, if not, the same check will happen for Type2...

example (an obvious goal is to infer the parameters):

typecase(List<Number>) l:
  | Empty<Number> => 0
  | Link<Number> => l.first
end

One side note, implementation-wise: to handle match (ie, cases as it stands, reformulated slightly), we can type check our double dispatch in a straightforward way:

match(List<Number>) l:
  | Empty => 0
  | Link(f, rest) => f
  | else => -1 # never reached, but here for sake of example
end

Can be compiled to:

typecase(Any) l:
  | List<Number> => l._match({Empty: fun(): 0 end, Link: fun(f, rest): f end, else: fun(): -1 end})
  | else => error
end

Which will type check, because l has type List<Number> ie Link<Number> + Empty<Number>, and Link<Number> was created from the structural type: {first :: A, rest :: List<A>, _match :: (self, {Link :: (A, List<A>) -> B} + {else: () -> B}) -> B} and Empty was created from the structural type: {first :: A, rest :: List<A>, _match :: (self, {Empty :: () -> B} + {else: () -> B}) -> B} Which means that the value passed to _match above (which has Empty, Link, and else fields) will be a proper subtype of _match for Link and _match for Empty.

Then the body of the _match methods are straightforward - here is Link:

_match: fun(self, dispatch):
  typecase({Link: (A,List<A>) -> B} + {else: () -> B}) dispatch:
    | {Link :: (A,List<A>) -> B} => dispatch.Link(self.first, self.rest)
    | {else :: () -> B) => dispatch.else()
  end
end

Finally, we have have one more addition to the language: wrap(T, expr). This expression has type T and will probably fail at runtime if expr is not a T (it could fail immediately, it could fail later, and possibly, not at all, in the case of a function that is wrapped but never called).

Note that this enforces a (useful) constraint:

All types must have a corresponding way to check them at runtime. There are (at least) four categories of types we have envisioned thus far, and three of them have this property: structural types (ie {f :: Number}), nominal types (ie, Empty), and refinement types (which are a nominal test and a runtime predicate, ie Number(odd)). The checks are:

structural: we can check that the fields exist in the object, and recursively check that the types match.

nominal: we can do runtime tag tests. Any value that matches a nominal value must have been constructed by a constructor function, which added the tag.

refinement: we run the predicate!

The fourth category are (recursive) constructed types, ie List<Number>. One possible runtime wrapping is to add proxies to the fields of the object, enforcing invariants and adding further wrapping to the recursive members. We don't have proxies, but might need to add them for this purpose.

Polymorphism may affect this: type parameters should create locally scoped nominality, but there is the question of how those types are applied (ie, where are the constructors run?). Again, proxies may be needed.