Type conjunctions

In the code above, the form A * B * ... is a type conjunction and is equivalent to both an intersection of A, B, etc, when the terms are sets (eg: when a type is the set of all values of that type); and a logical conjunction of A, B, etc when the terms are predicates (eg: when a type is a predicate that tells you when a value is a member of that type). For this prototype I use the logical model, and the guard tests are the defining predicates for the corresponding types

So the (theoretical) form let x: Positive * Integer means the value x is a member of both Positive and Integer. Logically, that means both types’ defining predicates return true when given x, ie: member(Positive * Integer, x) = member(Positive, x) && member(Integer, x). Setwise, it means x is a member of the intersection of the two types’ sets: x ∈ Positive ∩ Integer, which means x must be in both sets x ∈ Positive ∧ x ∈ Integer

At a higher level of abstraction, certain terms in a type conjunction can be interpreted like adjectives. Consider: Fox * Brown, this is the type for all foxes that are brown. When interpreted as a set, Brown would have to contain all the brown foxes, plus all the brown dogs, and all the brown houses, and so on. The logical interpretation means the test for Brown is true whenever the value is brown, which is a more obvious interpretation

Type conjunctions can be used to refine types in a composable way without having to make new type definitions. For instance in Integer * Positive, the type Positive refines Integer. We could define a new type PositiveInteger, which refines and subtypes Integer. But now say we also wanted to also add a type definition PositiveRealNumber equivalent to RealNumber * Positive: we would have to copy the contribution of Positive from our PositiveInteger and paste it in PositiveRealNumber because the contribution would be the same. Instead, we can equivalently express these two definitions as Integer * Positive and RealNumber * Positive

Theoretically, we could use type conjunctions for composing interfaces. Consider this pseudocode:

interface Fooable { void foo(x: X); }
interface Gooable { void goo(x: X); }
interface FooableAndGooable extends Fooable, Gooable { }

The last definition, which is entirely nominal, can be expressed equivalently with Fooable * Gooable, but this type expression can be used without a definition

Similarly, all composite types can be expressed as type conjunctions whose terms are composite types with only one member:

class Vector2D {
  x: RealNumber * XDimension
  y: RealNumber * YDimension
}
class Vector3D {
  x: RealNumber * XDimension
  y: RealNumber * YDimension
  z: RealNumber * ZDimension
}
// equivalent to:
class XRealDim { x: RealNumber * XDimension }
class YRealDim { y: RealNumber * YDimension }
class ZRealDim { Z: RealNumber * ZDimension }
Vector2D = XRealDim * YRealDim
Vector3D = XRealDim * YRealDim * ZRealDim

Where the XDimension, etc are tag types (see below). Notice that the XRealDim, YRealDim, and ZRealDim definitions are essentially nominal as well. One of my original goals for developing the idea of type conjunctions and tag types was determining if something analogous to tacit programming for types is possible. Since the XRealDim, etc are distinguished by their XDimension tag types, a composite vector type might be expressed like:

Vector2D = {RealNumber * XDimension} * {RealNumber * YDimension}
// and you could then create a value of this type:
let v: Vector2D
v[XDimension] = 5
v[YDimension] = 15

Of course, the XDimension, etc tag types are equivalent to names like x, y, etc as distinguishers, but since XDimension is a type and can have definitions, the system is aware of it and can reason about it to some degree, whereas it can’t with a name like x

Along these lines, consider a variable name like truncatedBufferLength. This name means nothing to a compiler, but to a human programmer they can sort of understand what its for: its the length of a buffer that’s been truncated, or there is a buffer and that buffer has been truncated to this length, or something. We ideally want to reproduce the mental model we have of the program inside the program’s code so it can be validated and analyzed more fully by the compiler, but if we’re modeling elements of a program to some degree via their names, then the compiler won’t be aware of that model

Now consider a variable like x: Integer * Positive * LengthOf(Buffer) * For(truncatedBuffer). It conveys the same meaning to the programmer as the truncatedBufferLength above, but is presumably comprehensible by the compiler. This is pseudocode and likely not of a consistent form, but it hopefully conveys the idea: type conjunctions are equivalent to nominal definitions, and might allow programmers to more fully model their program in a compiler-aware way without the chilling effect and pollution of those nominal definitions

Tag types

A tag type (especially in a type conjunction) is a type without a definition. These are solely to help the compiler distinguish between alternates, and to aid the programmer as a form of metadata

Consider this code:

function foo(x: Integer) { print('A') }
function foo(x: Integer * MyTagType) { print('B') }
let a: Integer = 5
foo(a) // prints A
let b: Integer * MyTagType = 5
foo(b) // prints B

This necessitates the dispatcher chooses the most exclusive conjunctions first (see limitations below) by testing whether one type conjunction is a subset of another type conjunction by comparing their terms. This is possible even when they both include tag types, but to make that work meaningfully you have to assume its true that A * B is a proper subset of A when B is a tag type. That isn’t necessarily universally true in reality though, for example consider Integer * RealNumber. Even if RealNumber is a tag type (it has no definition), presumably Integer is a subset of RealNumber, so Integer * RealNumber == Integer and Integer * RealNumber isn’t a proper subset of Integer

But tag types in type conjunctions, when treated solely as a method for choosing which alternates to use, are apparently very powerful. In some sense, tag types are a way to automatically choose function names. Consider: when B is a tag type, function foo(x: A * B) is equivalent to function foo_B(x: A) because there is otherwise no defined test for which x values foo_B can take that distinguishes between a x: A * B and x: A

Tag types can also work on their own, and don’t have to be included in type conjunctions. For instance, a function function foo(x: MyVariable) to only be used on a particular variable whose type is also the sole tag type MyVariable

Limitations of this translator

Its undefined behavior for one function overload to be a superset of another function overload. So all the overloads have to be disjoint

function foo(x: A) { ... }
function foo(x: A * B) { ... }

This isn’t allowed because A is a superset of A * B. The reason for this is the order guard tests are applied in isn’t defined, so if two tests A and A * B would pass for a particular value, then which is actually applied is undefined

~~~

All functions are mangled and have a dispatcher added, even when it doesn’t make any sense (eg: when the function isn’t overloaded, and has no parameters). The reason for this is because I’m lazy

~~~

It uses regex to find forms like guard someGuard(xyz) and function foo(x, ...), and edge cases that match these regexs but shouldn’t (or should match but don't) are probably very likely

~~~

Parameterized types aren’t supported. A theoretical example of a conjunction type including a parameterized type is: Integer * GreaterThan(5). It would probably be very difficult to modify the current system to accomodate this

~~~

Dispatcher functions are added only at the top level, and only for functions using the form function NAME(PARAMETERS), so nested functions aren’t supported, and anonymous functions aren’t supported. Classes are also not supported in any way

~~~

Probably many other limitations as well

Future work

This program could be made significantly less brittle by: taking an already-written grammar for a parser generator (eg: ANTLR, treesitter, etc), modifying the grammar to recognize guard statements, write a transformation function to turn the parse tree into an equivalent vanilla javascript parse tree, and deparse the tree. This is probably a lot of work, though, and for not much better a result

~~~

Ideally, for a dynamic language like javascript, the dispatcher functions’ behaviors would be a part of the runtime, so the extra dispatcher functions would be unnecessary, and perhaps even name mangling would be unnecessary. Of course, statically typed languages could do static dispatching when possible. Note though that using only static dispatching eliminates a very broad category of dispatching that’s only possible at runtime

~~~

I hope that at least one statically-typed language’s developers implement a version of conjunctive typing with tag types into their language. Hell, maybe I’m an idiot and someone already has. I run into so many cases on an almost daily basis where I want conjunctive typing and/or tag typing, that I have to imagine it would be that useful for many people and so nobody has properly implemented it yet

~~~

My original plan was to implement conjunctive typing into a language with static typing then integrate an Automatic Function Composer (AFC) into it. The AFC I was envisioning searches through function signatures, solving for a new function composition whose signature matches a given unrecognized signature. This essentially necessitated conjunctive typing (which I used to call set typing) because you need some way to add more information about registered functions’ parameters without writing a bunch of new definitions (which potentiallys defeats the purpose of the AFC). Incidentally, you can also use function conjunction types to add information about functions (eg: foo is a member of DoesX * DoesntThrow * ...). Anyway, I wrote an AFC directed hypergraph-based solver (see here), but it turned out to be really hard to use the type conjunctions to guide the AFC, at least in its current language-nonattached form, and its really hard to distinguish good solutions from useless ones. In the near future, I will likely make an effort to solve the AFC’s solution order problem and integrate it into a language to really determine if its practical and useful to use

~~~

Constant parameters make a sort of sense in predicate-based logical typing:

function foo(x: 5) { print('A') }
function foo(x: 10) { print('B') }
foo(5) // prints A
foo(10) // prints B

Where the guard test would be like valueToTest == theConstant, and could be probably more or less easily added to this system

~~~

Since guard tests are type invariants, typed variables’ values can be checked for proper form by the runtime using their types' guard tests. Consider the following code:

let x: Positive * Integer = 5
x -= 10 // runtime should throw an error

Dynamic dispatching via type conjunctions prototype

Type conjunctions

Tag types

Limitations of this translator

Future work