C++ Interpreter: Type System

[mason-bially]

Thoughts on the type system listed here (Subsumes #8, this is the second try).

• Types are just instances. They implement PType.
• Let's try to "host" the craft::types system.

References

• This thesis: https://github.com/JeffBezanson/phdthesis/blob/master/main.pdf

[mason-bially]

PType

Not yet sure how to write this one. A lot of these methods will be bidirectional (e.g. Tuple{Union{A,B},C}= Union{Tuple{A,C},Tuple{B,C}} from the paper above.

Here are my tentative methods:

• bool isConcrete(): Describes that type is concrete (e.g. only itself and bottom are subtypes of it ?). Implies this has a memory layout.
• bool isSubtypingSimple(): Describes types that have simple checks for sub-typing.
• bool isSubtype(instance<Environment>, instance<> left, instance<SubtypeAlgorithm> = instance<>()): Performs simple check to see if the left hand type is a sub type of this type.

Objects

Types are used to describe the kind of a value. At runtime the program knows the concrete type tag and the location in memory of every value (although the compiler may elide these if they are not necessary). For use in data flow analysis the system can perform computations on types.

CraftType

Wraps TypeId, describes a concrete craft type to the lisp.

Backport to craft::types?

AbstractTag

Describes an abstract tag.

Tuple

A sequence of types. Used to describe things like function signatures, and (ordered) collections of values.

Support variadic? or a separate type?

Union

A union of two types, meaning the value can be one or the other.

(?) Exists

An existential query over a type. Comes in three parts:

Called UnionAll in Julia. Could probably use a better name.

TypeVar

A variable in an existential query.

SpecialType

Used for Any and Bottom, uses std::function to implement PType.

Dispatch

Dispatch is done by finding the first method

Multi

Implemented with: Any, Bottom, concrete types, AbstractTag, and Union.

Diagonal

Triangular

[mason-bially]

Type Algorithm Notes:

• An option to the SubtypeAlgorithm to restrict type vars to concrete types (return false if lower bound is not concrete).

Type Hierarchy Notes:

• Need a way to represent (Type Param Param) as well as (AbstractTag Param Param).
  • Solution Make the description of a generic type a new node.
    • Calling it will construct it with the given parameters.
    • Otherwise the un-called version is a type which obeys (subtype (Ex A B) Ex).
    • Since the CraftType system does not yet support generics it is unnecessary for these until it does.
    • Will be needed for AbstractTags.
    • Will be needed for any in-lisp-datatypes.

[mason-bially]

We should consider whether we want to be able to mark type constructor arguments as contravariant, covariant or invariant, like in C#. Or simply assume invariance with covariance being a specialized exception (which Julia does). We may not have the choice. Page 67 of the thesis implies the lack of contravariant constructors is key to the decideability of the sub-typing system.

The rules in the second row appear asymmetric. This is a result of exploiting the lack of contravariant constructors. No contravariance means that every time a right-side variable appears on the left side of a comparison, it must be because it occurs in invariant position, and the steps outlined in the first paragraph of this section have “flipped” the order (comparing both B ≤ C and C ≤ B). This explains the odd rule for comparing two right-side variables: this case can only occur with differently nested UnionAlls and invariant constructors, in which case the relation holds only if all involved bounds are equal. By symmetry, one would expect the rule in row 3, column 2 to update X’s upper bound to B ∩ T. But because of invariance, T ≤ B has already been checked by rule in row 3, column 1. Therefore B∩T = T. This is the reason the “forward” direction of the comparison needs to be checked first: otherwise, we would have updated B to equal T already and the T ≤ B comparison would become vacuous. Alternatively, we could actually compute B ∩T. However there is reason to suspect that trouble lies that way. We would need to either add intersection types to the system, or compute a meet without them. Either way, the algorithm would become much more complex and, judging by past results, likely undecidable.

I believe it should be possible to express contra- and co- variant existential bindings through the use of extra bounds which represent upper, co, contra, and lower bounds. This should only increase the complexity of bounds recalculation, without introducing intersections. It's also an expansion of an existing special edge case for tuples, which is why I believe it should be possible.