Dependent Pattern Matching, Without Green Slime

Disclaimer: This is basically a blog post. I should start hosting my own website so I can write real blog posts...

Motivation

A classic pain point in proof assistants based on ITT is problems with "green slime" ¹.

foo : (x y : ℕ) → Fin (x + y) → ⊤
foo x y fz = {!!}
foo x y (fs _) = {!!}

I'm not sure if there should be a case for the constructor fz,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  suc n ≟ x + y
when checking that the pattern fz has type Fin (x + y)

These arise from how dependent pattern matching requires patterns to definitionally have the type of the scrutinee variable (so it is safe to substitute the variable for the pattern everywhere in the context).

As we'll see next, if the "inferred" (i.e. from the signature of the constructor) and "expected" (i.e. from the type of variable being matched on) indices can be unified to produce a single solution, we can easily elaborate this into a match where the indices coincide, and the pattern has the desired type (and if they anti-unify, we know the branch is impossible and can be elided); however, oftentimes, unification problems can yield multiple solutions, or worse, are undecidable.

Unification between patterns² and variables is easy: all we need to do is perform a substitution, which is what allows

foo : (x : ℕ) → Fin x → ⊤
foo x fz = {!!}
foo x (fs _) = {!!}

to be painlessly elaborated into

foo : (x : ℕ) → Fin x → ⊤
foo x@.(suc _) fz = {!!}
foo x@.(suc _) (fs \_) = {!!}

We could attempt a similar translation for more complicated indices, using a with-abstraction³

foo : (x y : ℕ) → Fin (x + y) → ⊤
foo x y n with x + y
foo x y fz | x+y = {!!}
foo x y (fs n) | x+y = {!!}

which, behind-the-scenes, can be elaborated into

foo : (x y : ℕ) → Fin (x + y) → ⊤
foo x y n with x + y
foo x y fz | x+y@.(suc _) = {!!}
foo x y (fs n) | x+y@.(suc _) = {!!}

This typechecks, but we have lost all connection between the index of the Fin and x + y. Such a with abstraction only works by indiscriminately replacing all occurences of x + y in the context with a new variable, so this is an inherent limitation.

Luckily, using Agda's with ... in ... syntax (or the inspect idiom) ⁴ we can retain propositional evidence of this connection

foo : (x y : ℕ) → Fin (x + y) → ⊤
foo x y n with x + y in p
foo x y fz | .(suc _) = {!!} -- Here, p : x + y ≡ suc n
foo x y (fs n) | .(suc _) = {!!}

But this is still inconvenient in two ways:

1. Propositional equality forces the user to manually coerce when necessary. It would be nice to have all x + ys which arise later rewrite to suc n automatically.
2. We were forced to manually write out the index to abstract over it. If we wanted to pattern match on multiple Fins, would would have to abstract over the index of each. We are doing a program translation by hand.

There is also a third, more subtle issue:

3. Sometimes, with-abstractions in Agda become "ill-typed". In the case of foo, this can happen if some expression in the context relies on the Fin being indexed by x + y definitionally to typecheck.

Pred : ∀ x y → Fin (x + y) → Set

foo : (x y : ℕ) (n : Fin (x + y)) → Pred x y n → ⊤
foo x y n p with x + y
foo x y fz p | .(suc _) = {!!}
foo x y (fs n) p | .(suc _) = {!!}

w != x + y of type ℕ
when checking that the type
(x y w : ℕ) (n : Fin w) (p : Pred x y n) → ⊤ of the generated with
function is well-formed
(https://agda.readthedocs.io/en/v2.6.4.2/language/with-abstraction.html#ill-typed-with-abstractions)

Solution 1: Transport-Patterns

To resolve these last two points, I propose a new syntax, which I call "transport-patterns". Simply put: we allow a built-in transport operator to appear in patterns, allowing us to match without fear of "green slime" while also binding propositional equality of the indices.

foo : (x y : ℕ) → Fin (x + y) → ⊤
-- I use a coercion operator inspired by Cubical Agda's transpX here because
-- ideally we would like to be able to refer to a transport operator specific to
-- the inductive family (so we can bind p to suc n ≡ x + y rather than
-- Fin (suc n) ≡ Fin (x + y))
foo x y (Fin.coeX p fz) = {!!} -- Here, p : suc n ≡ x + y
foo x y (Fin.coeX p (fs n)) = {!!}

In contrast to with-abstractions, we don't try to replace the index expression in the context. Instead, we just replace the variable we matched on with a transported value.

Personally, I think this feature alone is already a huge ergonomic improvement on the status quo. Of course the user could always resort to doing their own fording transformations, but this often infects many other parts of the development with unnecessary clutter (passing and matching on refls), i.e. in the cases where unification would have worked out.

Fixing the first bullet is harder - we must increase the power of definitional equality. Note this problem might sound less important (it certainly did to me at first), but in larger examples, having rewrites apply only once, immediately, can end up giving rise to so-called "with-jenga"⁵ where the order of with abstractions needs to be chosen extremely carefully to have the types work out (i.e. without resorting to copious amounts of manual coercing). Again, in my opinion, time spent finding solutions to puzzles like these is time wasted (even if solving puzzles can sometimes be fun).

Before I proceed to the proposal, I must give credit where it is due. I originally heard this idea from Ollef on the r/ProgrammingLanguages Discord, and worked through a lot of the tricky details with Iurii - thanks for the interesting discussions!

Solution 2: Neutral -> Value Mappings

Without further ado, the core idea is thus: Make it possible for the context to contain local rewrite rules (from neutrals to values), subject to an occurs check to prevent loops. We can then define dependent pattern matching where the scrutinee is a neutral as a process which adds such rewrite rules to the context (i.e. as opposed to the usual one-time-substitutions-of-variables-for-patterns).

An important note: the solution here is not "complete". I believe this is by necessity (a perfect solution would give arbitrary equality reflection and naturally make typechecking undecidable). It is simply designed to handle a majority of easy cases, with the fall-back of transport-patterns (or manual fording I suppose) always in reach.

TODO: Add paragraph on the occurs check and why it is necessary

Of course, the scrutinee of a pattern match may not always be a neutral or variable. It could be a canonical value. More severely, what might have started as a mapping from a neutral might become not so if some later pattern match causes the neutral to unblock. Our proposed scheme for handling such cases is as follows:

• First check if the RHS is a value.
• RHS is a neutral: Invert the direction of the rewrite rule and continue (TODO: justify why this shouldn't lead to loops)
• RHS is a value: Attempt to unify LHS and RHS
  • LHS and RHS unify: Safely discard the rewrite rule. It is redundant.
  • LHS and RHS anti-unify: Report the most recent match as impossible and refuse to typecheck the branch.
  • Typechecker cannot make a decision (e.g: LHS and RHS are functions): (*)

The final case, (*), is tricky situation. In the case that this was a new rewrite rule which we just attempted to add, we are probably screwed (the context is very likely reliant on this rewrite to typecheck, but adding a definitional rewrite between potentially not-equal values is BAD ⁶).

However, if we have reached this case by reducing the LHS of a previously valid rewrite, then we might hope that applying the rewrite eagerly to everything in the context will mean that we might discard the rewrite rule and everything will continue to typecheck (even if prior definitional equalities might no longer hold equal - which is odd, but not the end of the world).

However, recall the subtlety highlighted above as problem (3.):

Pred : ∀ x y → Fin (x + y) → Set

foo : (x y : ℕ) (n : Fin (x + y)) → Pred x y n → ⊤
foo x y n p with x + y
foo x y fz p | .(suc _) = {!!}
foo x y (fs n) p | .(suc _) = {!!}

w != x + y of type ℕ
when checking that the type
(x y w : ℕ) (n : Fin w) (p : Pred x y n) → ⊤ of the generated with
function is well-formed
(https://agda.readthedocs.io/en/v2.6.4.2/language/with-abstraction.html#ill-typed-with-abstractions)

The neutral -> value mapping idea is powerful enough to resolve many of these sorts of cases. To see how, note that Pred x y : Fin (x + y) → Set, so in the fz branch, we will check fz against Fin (x + y). As long as we apply our x + y -> suc n rewrite to the goal type, this will succeed!

But of course Pred x y is not a variable, and therefore we cannot record the rewritten type in our context (hence why Agda's with-abstraction immediate one-off rewrites don't work here). Therefore, if we later match on x and y, revealing them to both be zero, we will have a problem on our hands. Discarding the rewrite (which now would have the form zero -> suc n) will result in Pred x y fz no longer typechecking! Of course, checking zero and suc _ anti-unify is trivial, so we can report an impossible match, BUT if the problem was just slightly more subtle (perhaps we used Church numerals instead of ℕs) then we would be truly screwed.

So, how do we resolve these cases? I think this has to be some sort of type error, but exactly where to error and what to blame is somewhat debatable. I can think of three different reasonable-ish perspectives:

• The culprit was that the rewrite rule related values whos type can yield undecidable unification problems. Therefore error much earlier, at the original match which introduced the rewrite.
• The culprit is that an expression in the context relied on the rewrite rule but the match made it invalid. Therefore blame the p : Pred x y n and the match on x and y.
• The culprit was that the match on x and y unblocked the LHS of the rewrite rule which forced it to be discarded (i.e. the problem is unrelated to whether such a rewrite rule was necessary for validity for the context). Therefore blame the x + y -> suc n rewrite rule and the match on x and y.

I'll admit that I am partial to the latter here: I think erroring for any type that could possibly yield an undecidable unification puzzle is too conservative, given this must include not just functions, but also any inductive datatype which might contain a function, and also general QITs/HITs (which are pretty exotic constructions, but are also very exciting features which I would like a modern proof assistant to support well). I also don't like the idea that adding stuff to your context could trigger an error when there was none previously (validity of typechecking being stable under weakening seems highly desirable).

Now to actually try and implement such a feature! (just kidding, I'm a type theorist, I would never write code)

Introduction

WTy2 is a pure, strict, functional programming language based on extrinsic dependent types.

It is being designed with a few goals in mind:

• Aim for there to be exactly one "best" way to design every abstraction. If there has to be multiple, the relative trade-offs for each should be obvious and small in number.
• Allow extremely strong compile-time guarantees (via dependent types), but optionally. It should be possible to start with a program that relies heavily on run-time assertions and bit-by-bit introduce more and more static checks without major refactoring.
• To support this, breaking from common philosophy on dependent types, WTy2 does NOT encourage creating many separate datatypes to maintain invariants (correct-by-construction). For example, the idiomatic WTy2 encoding a vector (length-indexed list) is to pass a list and a constraint holding a runtime irrelevant proof that it's length is equal to n, NOT to define a new inductive datatype. The style of invariant-capturing WTy2 encourages is therefore more similar to languages with refinement-type systems. To make this feasible in a dependently typed setting, WTy2 supports subtyping, takes the notion of a kind of singly inhabited types ("Constraint"s) from Haskell and combines this with the concept of "implicit proofs", enabling powerful inference.
• WTy2 is also designed to be (eventually) blazing fast. Implementing the type system as-is will be more than enough work for the forseable future, but to avoid shooting itself in the foot if/when focus shifts to performance, some effort is being put into mechanisms for providing the programmer opt-in guarantees about data representation, memory layout, specialisation, compile-time code execution etc... (predominantly via "modes").

Summary

Core Types

Any

Any is the supertype of all types.

Type (Type)

Type is the supertype of all "types". This includes anything which can appear on the RHS of a : binding.

An automatic instance of Type is derived for every type declaration.

Constraint (Constraint)

Constraint represents "constraints". These can look syntactically similar to bindings (the constraint-versions of binding operators contain an extra : to disambiguate), but instead of bringing variables into scope, they constrain existing values.

Constraints can be created with the built-in ~, :: and <| operators.

Functions (Fun)

In WTy2, functions are defined as variables which implement the (Open) Fun type, which includes methods arg and res (which return the argument and return types of the function respectively).

Normally, functions in WTy2 are uncurried. The exception is operators, which are always of the form a -> b -> c.

See Core Type Operators for the definition of the (->) type operator in terms of the built-in Fun type.

Tuples/Records/Dependent Pairs/Lists and Telescopes

In WTy2, the built-in tuples, records, dependent pairs, lists etc... all desugar down to the same datatype - a dependent inductively-defined tuple:

datatype DepTup(tele: Tele) where
  (:.) : [ty, rest] (head: ty) -> (tail: rest(head))
       -> DepTup(ty .- rest)
  Nil  : DepTup(NilTele);

Where Tele is another built-in datatype, a telescope:

datatype Tele
  = (.-)    : (ty: Type) -> (rest: t -> Type) -> Tele
  | NilTele : Tele;

Ordinary lists and tuples can be defined from DepTup pretty trivially:

type List(ty: Type)
  = [head: ty, tail: List(ty)]
    '(head :. tail)
  | 'Nil;

type Tuple(tys: List(ty))
  = [ty, rest, head: ty, tail: Tuple(rest)]
    '(head :. tail) <<= { tys ~ ty :. rest }
  | 'Nil;

More convenient list/tuple syntax and records are implemented as syntax-sugar on top of these datatypes (i.e: (0, 1, 2) becomes 0 :. 1 :. 2 :. Nil). Following the structure of how DepTup is defined, fields in dependent records can only depend on fields to the left of them.

Unit (())

The unit type is also defined in terms of DepTup, with () parsed as an ordinary identifier:

() = Nil;
type Unit = '();

Design Note: Singleton Tuples

WTy2 also supports singleton tuples. The parsing ambiguity of expression in parens vs a singleton tuple is resolved as follows: (E) where E is an expression - parenthesised expression (E,) where E is an expression - singleton tuple (i: E) where i is an identifer and E is an expression - named value (t <: (i: t)) (i: E,) where i is an identifier and E is an expression - named singleton tuple/singleton record

Design Note: Bindings

In WTy2, the types of records can look syntactically identical to bindings (LHS of assignments). However, bindings are NOT first-class. return (x: Int) returns a Type which is equal to the record type (x: Int). do {x: Int} = 4 (perhaps intending the LHS expression to reduce down to x: Int) is nonsense.

Void

Void is the subtype of all types. It contains no inhabitants.

Common Type Operators

WTy2 quite a few common type operators (mostly arrows), they are summarised here.

Function (->)

(->): (t: Type) -> (t -> Type) -> Type
a -> b = (f: Fun) <<= { a <: arg(f) /\ res(f) <: b }

Dependent function arrow.

In the source language, braces are implicitly added around RHS if necessary.

Such That (<<=)

(<<=): (t: Type) -> (t -> Constraint) -> Type

Narrows a type, requiring the constraint to be satisfiable for all member values. When pattern matching on values of the type, the constraint is brought into scope.

Constructor (~>)

(~>): (t: Type) -> (t -> Type) -> Type
a ~> b = (a -> b) & Con

Similar to function arrow, but must be "matchable". i.e:

a ~> b = (f: a -> b) <<= {
    for(x: a, y: a, g: a ~> b) { f(x) ~ g(x) => f ~ g /\ x ~ y }
  }

In the source language, braces are implicitly added around RHS if necessary.

Design Question: Is Generativity Necessary?

Haskell assumes type constructors are both injective, and generative, and the work on unsaturated type families still separates functions into those that are both injective and generative, and those that are not necessarily either. However, the benefit of injectivity (for unification) is generally much more useful than generativity, and furthermore, it could be argued that injectivity meshes better with a notion of constructing/matchability anyway (given pattern synonyms are clearly not generative!). Of course, an arbitrary function paired with a proof of injectivity does not provide a strategy to invert it (which is what is really required for pattern matching) but perhaps that just justifies for two types: injective functions, and matchable constructors (the inference and checking of the latter being built-in to the compiler).

Subtype (<:)

(<:): Type -> Type -> Constraint
t <: u = for(x: t) { x :: u }

Values of the LHS type can be upcast into ones of the RHS type.

Implies (=>)

(=>): Constraint -> Constraint -> Constraint

The RHS constraint can be obtained from the LHS constraint.

Forall (for) / Derivable (|-)

for : (t: Type, c: t -> Constraint) -> Constraint
(|-): (t: Type, c: t -> Constraint) -> Constraint

The constraint c(t) is derivable from the typing context t - i.e: quantified constraints. The operator version (|-) exists predominately to allow use of (<<=) on the quantified-over type without requiring additional parenthesis.

In the source language, braces are implicitly added around RHS of (|-) if necessary.

Functions

WTy2 is a functional programming language, and as such, functions are first-class. Any variable that implements Fun is a function.

Lambda-Blocks

In WTy2, braces ({}) are used to denote a lambda. Inside the braces, there can be:

• Just an expression. In this case the argument type is inferred, and can be referred to in the expression as it. The really powerful part here is that variables varName are attempted to be resolved as fields of it first (as in it.varName). This is similar to this being in scope allowing access to fields and methods of the class without needing to specify the receiver in OOP languages.
• A "\" followed by an irrefutable pattern which is bound to by the argument, a "|->", and the return expression.
• Multiple |s, each followed by a pattern, a |-> and a return expression for if that match succeeds.

Function Definitions

WTy2 is a functional programming language, meaning functions are first class and can be bound to variables. Using only existing introduced syntax, a function that adds three integers can be defined like so:

addTriple: Tuple(Int, Int, Int) -> Int = { \(x, y, z) |-> x + y + z };

Using record syntax (and implicit it scoping), we can achieve this in a slightly cleaner way as

addTriple: (x: Int, y: Int, z: Int) -> Int = { x + y + z };

WTy2 introduces an additional way to define functions, which looks closer to imperative programming languages:

addTriple(x: Int, y: Int, z: Int): Int = x + y + z;

In general f(t): u can be thought of as equivalent to...

• If t is a type (including record types), f: t -> u
• If t is a list of types, f: Tuple(t) -> u ¹

With one extra special case: if the syntax is used as the LHS of an assignment (like above) then the braces around the RHS expression are implicit.

Recursion

TODO

¹ This rule is specifically intended to make signatures of higher-order functions easier to write.

Records

Records in WTy2 are internally compiled down to ordinary dependent tuples, but have a few extra features.

Construction

Records in WTy2 can be constructed similarly tuples but with each expression prefixed the field name and an = symbol: (field1=expr1, field2=expr2, ..., fieldN=exprN) to create a record of type (field1: type1, field2: type2, ..., type3).

Subtyping

Records are covariant in types of fields.

There is also one subtyping rule between records and tuples to allow for passing functions that take named arguments to higher order functions cleanly (recall functions are contravariant in argument type).

(Ty1, Ty2, ..., TyN) <: (field1: Ty1, field2: Ty2, ..., fieldN, TyN);

Shuffling

WTy2 defines a primitive shuffle to work with records with different orders of field names:

shuffle: [a](x: a, b: Type) <<= { a: permutation(b) } -> b;

Where permutation is a type family that produces a type containing all record types that are permuations of the fields of the argument record.

Partial Application ("?")

WTy2 supports a nominal ¹ partial application syntax based on records, which leverages yet another primitive:

partialise: (f: a -> b) -> [a1] a0 <<= { concat(a0, a1): permutation(b) }
           -> if(isUnit(a1)) { b }.else { a1 -> b };

Where concat is a type family which concatenates two records in the obvious way and isUnit is a function on (record) types which decides if the type is () (one implementation would be isUnit(a: Rec) = a.size() == 0).

One way to view this primitive is as a generalised curry which infers desired argument order based on record field names.

As syntax sugar, WTy2 allows (?) = partialise to be used a primitive operator which binds tighter than function application, allowing use like:

f: (x: Int, y: Char, z: Bool) -> Int;

g: (y: Char) -> Int = ?f(x=3, z=True);

In the case a0: permutation(b), we have a1 :: () => isUnit(a1) ~ True. We special-case this situation in the type signature to allow for convenient passing of records with shuffled field order to functions:

w: Int = ?f(y='a', z=False, x=3);

It is likely inference for this primitive will need to be handled specifically in the typechecker (i.e: to take advantage how a1 can be inferred by removing fields of b that occur in a0).

¹ As opposed to positional, which is the usual approach in languages supporting partial application, such as Haskell. For example, given the Haskell function foo a b = a / b we can easily partially apply foo to a numerator, n, with foo n, but partially applying to a denominator, d, requires more clunky syntax such as (`foo` a) or a combinator like flip or (&). This problem gets worse as the arity of functions increases.

Declarations

WTy2 supports top-level bindings in the form of "declarations".

All named declarations can be prefixed with visibility annotations.

Type Declarations

Type declarations create new types or type constructors. Types formed with constructors declared via type declarations are irreducible terms of type Type.

Unlike many other formal type systems, user-defined types in WTy2 can be "open", meaning we can, in a distinct module, declare more sets of terms as members of the original type.

Open types can have a number of associated members (specifically, functions) that must be defined for all implementors of that type. The type signatures of these functions can refer to the implementor of the type: self. Indeed, each of these functions must take at least one explicit (i.e: runtime relevant) argument (the "receiver") of type self, impl(self) or 'self (a practical limitation to make type inference and compiling to VTables possible).

Super-constraints that all implementors must obey can also be declared using <<= followed by an function of type (self: DeclaredType) -> Constraint. This introduces for(self: DeclaredType) { f(self) } (where f is the super-constraint function) into the context, which is applied eagerly during typechecking, so care must be taken by the user to avoid writing super-constraints that loop. Requiring laws without the eager-expansion behaviour can be done through requiring function members of appropriate type (e.g: fmap_id(f: self): Proof(fmap?(f: id) ~ id))

As an example, here is the ParMonad type, which is similar to a Monad in functional languages like Haskell but does not require the type constructor to be total (meaning it can support data structures like sets and hashmaps).

type ParMonad where {

    fmap[a: arg(self), b: arg(self)](x: self(a), f: a -> b): self(b)

    pure[a: arg(self)](m: 'self, x: a): self(a)

    (>>=)[a: arg(self), b: arg(self)](x: self(a), f: a -> self(b)): self(b)

} <<= { [domain: Type] self :: domain ~> Type };

¹

Type Synonyms

Sometimes a type is desired that is simply a synonym for some other more elaborate type. As types are first class, this can be implemented in WTy2 just with ordinary terms; however, term definitions have slightly different semantics to created types (terms reduce, while types do not) which can impact typechecking and inference.

Type synonyms can be alternatively written by declaring a type with the appropriate super-constraint and then writing instances to cover every value (if the type being aliased is open type, the instance head can be impl(OpenType)).

datatype Foo
  | MkFoo
  ;

type Alias {} <<= { self <| Foo };

inst Alias for MkFoo;

This pattern is quite clunky (especially for closed types with many constructors), so WTy2 provides syntax sugar for it:

type Alias = Foo;

As coherence rules enforce that instances where the instance head is an open type prevent any other instances being written, it is suggested that ideal practice when writing an open-head instance is to instead write a type alias. Implementations may wish to warn the programmer in when this is not done.

Instance Declarations

Instance declarations in WTy2 are denoted with the inst keyword followed by the open, inst-able type and the instance head (separated with for). Every instance adds Head :: InstableType to the context.

The instance head type must not have any stuck terms and must not overlap with other instance types (the conditions of overlap are given fully in Coherence).

Data Declarations

Data declarations define "variants" or "tags". These are similar to functions but instead of producing arbitrary values after executing some computation, they create tagged versions of whatever type they are declared to take as parameter.

The suggested implementation is for tags to all share the same 32-bit space of values. As an optimisation, it is suggested that this tag is elided in cases where it is known at compile-time.

I.e: In the below program

data Foo(Bar)

x: Bar = ...
y: Foo = Foo(x)

Both Foo and Bar should have equivalent runtime representations.

Handling variance while ensuring unnecessary tag information is not stored at runtime is not a trivial problem: for how this is solved specifically with regards to recursive types, see the dedicated section.

Datatype Declarations

Unfortunately, some types might need many variants that would quickly fill up a 32-bit space of values (for example: int32s). A datatype declaration looks a bit closer to an inductive type declaration in other functional languages, and is implemented by having an outer tag which takes one slot of the 32-bit space, then allowing the variants all make use of a separate space of values.

Datatype declarations are also just convenient in allowing the user to simultaneously define a type and set of variants.

datatype Bool
  | True
  | False
  ;

Function/Constant Declarations

Ordinary terms like functions or constants can also be defined as top level bindings. They do not need to be prefixed with any keyword.

Proof Declarations

However, functions can be optionally be prefixed with the proof keyword. This changes the semantics of the binding, allowing calls to the function to be inserted automatically to aid typechecking. proofs my also be anonymous. See the dedicated section on proofs for more information.

Erasure and Visibility

Runtime Relevance of Types and Constraints

In Haskell, runtime relevance can effectively be summarised as: types are erased, constraints are not. Even equality constraints like a ~ b which don't contain any fields often do not get fully optimised away as Constraint is lifted and so could point to a bottoming value (see discussion at https://github.com/ghc-proposals/ghc-proposals/pull/547).

In WTy2, we take the opposite approach: constraints are erased but types are not. To perform dispatch, implementations will in all likelyhood need to implement some sort of runtime.

Erasure and Visibility in Types and Values

Even though values and types must in general be kept around at runtime, in many specific cases, this is not necessary (consider a generic function which takes both a type t :|=> Animal and an argument a: t - t can be recovered entirely from a). The key observation made here is that arguments we would like the typechecker infer for convenience generally correspond with ones recover.

A type surrounded in parenthesis can be prefixed with something that looks similar to a record type but the bindings are placed inside brackets ([]) instead of parenthesis.

A variable can be bound in the erased elements of a record only if:

• It occurs by itself in a matchable function application (i.e: as an argument or the function itself) to the right of a member constraint and the type (i.e: RHS object of member constraint) is Closed (the Closed constraint is inferred if the use of []s require it, similar to definedness constraints which arise from function applications in types). ¹
• It is on the RHS of an equality constraint with a non-erased element (unclear if this is actually useful).

An example of erasure being useful is when working with length-indexed vectors:

vecLen[t: Type, n: Nat](v: Vec(t, n)): Nat <<= { it ~ n }

returnsVecOfUnknownLen(...): [n: Nat] Vec[Bool, n]

In vecLen, binding t and n in the []s allows them to be inferred, and makes it so there is no runtime cost of having to pass the type or length. Note if we had to pass the length explicitly, then the function would be entirely useless: we would need to know the length to calculate it!

This combines nicely with functions like returnsVecOfUnknownLen. If we ever do actually need to know the length (perhaps to pattern match on it), then we can call vecLen on the result, and this all works out because we still have an erased n: Nat in scope.

To be concrete, a term being erased means that it cannot be pattern matched on, or passed as an argument to somewhere where a non-erased term is expected.

Unlike constraints in <<=, erased terms in records can be manually specified at construction or bound when matching.

[erasedLen=n] vec = returnsVecOfUnknownLen(...);
len = vecLen[Bool, erasedLen](vec);

// From the signature of 'vecLen', `erasedLen ~ len` is in the context
_: () <<= { erasedLen ~ len } = ();

Bidirectional Type Inference

One unfortunate consequence of handling inference in this way is that setting up constraints based on the desired return type (bidirectional type inference) is not really possible. This can be a useful feature - for example, in languages like Haskell, numeric expressions can stay entirely in terms of Num a => a until finally being instantiated to a specific numeric type at call-site, but it also leads to many cases of potential ambiguity and arguably makes code harder to reason about.

¹ Note this is less restrictive than it might initially sound. If we have x: Animal and a function id[t: Type](x: t): t, id(x) does indeed typecheck, with t instantiated to x.head(Animal).

Coherence

WTy2 has a number of rules on instance declarations to guarantee instances do not overlap. Note "overlap" has a slightly stronger meaning in WTy2 than in other languages with typeclasses given the ubiquity of subtyping: treated as sets, there should exist no value that is a member of both types.

Rules around instances and overlap can get tricky, and luckily, a lot of prior work has been done investigating them in languages such as Rust and Haskell. As such, I will repeatedly refer to the decisions those languages have taken to compare and contrast.

Detecting Errors Early

A goal of WTy2 is that adding a valid instance (i.e: no error is detected at the site of the instance) should never break existing code.

Note that Haskell does not actually meet this criteria due to overlap only being checked lazily (when trying to solve the constraint), see:

class C a

instance C (Char, a)

-- This instance appears to be fine, but causes an error at the
-- call to `bar` due to the instance of `C` becoming ambiguous
{-
instance C (a, Bool)
-}

foo :: ()
foo = bar ('a', True)

bar :: C a => a -> ()
bar _ = ()

Following this rule doesn't just lead to a theoretically cleaner language, it has a direct practical benefit: adding new valid instances to a library can never be a breaking change and so does not require a semantic version bump.

Outermost Constructors

Given WTy2 is dependently typed with types effectively modelling arbitrary sets, checking if an arbitrary two types overlap is obviously undecidable. We can trivially encode Fermat's last theorem as a type overlap problem.

type C { };
inst C for (x: Int, y: Int, z: Int) { };
inst C for [n: Int] (x: Int, y: Int, z: Int) <<= { x ^ n + y ^ n ~ z ^ n } { };

We take the conservative approach of only considering the outermost constructor(s)¹. For example, the two below instances will always be treated as overlapping (regardless of whether Foo and Bar overlap):

data Mk[a: Type](x: a);

type Foo : Type = ...

type Bar : Type = ...

type C { };

inst C for [x: Foo] 'Mk(x) { };
inst C for [x: Bar] 'Mk(x) { };

The check for overlap between closed types then becomes quite simple. The instance head types are reduced into form [...] 'C0(...) | [...] 'C1(...) | ... and the sets of outermost constructors are compared.

As well as making overlap rules MUCH simpler, this has a really poweful benefit for implementation. (I believe that) with it, we can fully erase constraints (instead keeping tags around at runtime, and dispatching based off the outer tag).

I further argue (though more loosely) that this has a further advantage in program reasoning, similar to parametricity. Consider defining a Num instance for lists. Haskell would allow defining a Num instance for List Int which operates with zipWith and List SomethingElse which concatenates lists with (+), removes elements from the first list on (-) etc... I personally believe the solution mandated by WTy2 of defining a separate list datatype to correspond with each of the instances behaviours (or at the very least a newtype wrapper) leads to clearer code.

Open/Closed Rules

Types can either be open or closed. These properties interact with the (|) and (&) type operators like so:

for(t: Closed, u: Closed) { t | u :: Closed }
for(t: Open, u: Type)     { t | u :: Open   }
for(t: Closed, u: Type)   { t & u :: Closed }
for(t: Open, u: Open)     { t & u :: Open   }

Types are closed iff their supertype is closed. Recall that

type T = U;

...is translated into:

type T { } <<= { self <| impl(U) };
inst T for impl(U); // Or an instance for every value if `U` is not open.

So for type-alias syntax, the defined type is closed iff the RHS type is closed.

A type may have exactly one "open" instance, or many "closed" instances.

If the equivalent of a WTy2 "open" type in Rust is considered to be a blanket impl (as opposed to an impl for a concrete type), then the rules Rust uses are actually a bit more flexible. It allows:

struct S1;
struct S2;
struct S3;

trait T1 {}
trait T2 {}
trait T3 {}

impl <T: T2> T1 for T {}

impl T1 for S1 {}

impl T1 for S2 {}

// This impl, if uncommented, will cause an overlap with the blanket impl, but
// only indirectly - the error message will not point to this line!
//impl T2 for S2 {}

In my opinion, this is a mistake: the error message not highlighting the correct line is confusing to the programmer, the rules which allow this are necessarily more complicated and I would argue this pattern has very limited utility (OOP has proven that default instances for a type in terms of another are useful, but this can be achieved through much more principled means like Haskell's deriving via).

Orphan Rules

To avoid overlap even when multiple modules are involved, WTy2 disallows "orphan instances". The gist is that, either the instance-d type and or every outer constructor of the instance head must be defined in the same module as the instance declaration.

Haskell only reports a warning on orphan instances rather than an outright error. I believe this is a mistake - orphan instances can trivially lead to overlap and overlap can lead to incoherence.

Modules

WTy2 programs are organised into modules, similar to Haskell (so modules are not first-class/intended as a method of abstraction - open types suit that purpose well already).

Imports/Exports

The public exports of a module are written in parens after the module declaration. Imports of a module are written in parens after the name of the imported module. Publically exported members are considered part of the public API of a module and breaking changes to them reflect semantic version changes for the module.

If and only if the exact version of the dependended-upon module is specified in the package file is the programmer given the freedom to import members that are not publically exported (still with a warning).

Requirement: Non-semantic version changes of upstream modules should never cause compile errors in downstream modules.

Module Members

Module members include top-level variables, types, tags, instances and proofs.

• Variables, v : t = e, and their types (v : t) can be exported/imported via their identifer. The RHS of their definition (v ~ e) can be exported/imported with (..).
• Closed types, type t = u, can be exported/imported via their identifiers. The RHS (t <: u /\ u <: t) can be exported/imported with (..).
• Open types, type t { m0: t0; m1: t1; }, can be exported/imported via their identifiers. Members of the type can be exported/imported in parens. Instances can only be made if all members are in scope via (..).
• Instances,impl t for u { m0 := e0; m1 := e1; } , are exported/imported implicitly. How to signal intent for whether to export the definition of members of the instance (m0 ~ e0) can be done by writing the special syntax m0(..) for u.
• Tags can be exported via their identifers. Modifying the type of arguments to a tag is always a breaking change.
• proofs proof p := e are exported/imported as functions via their identifiers and imported as unnamed proofs with proof(p) (they are always exported as unnamed proofs). A named proof can be imported as both a function and an unnamed proof by a downstream module. All proofs can be imported as unnamed at once with proof(..).

Summary

Utilities

WTy2's syntax is designed for allowing defining functions that appear similar to built-in language constructsof other languages. Below are a few examples:

Do

Inspired by Haskell

do(f: () -> t): t = f()

This is primarily useful when defining functions in f(x: t): u = ...-style where you still want to use a block to define locals or use do-notation sugar ¹. E.g:

foo(x: Int, y: Int): Int = do {
    z := x * 3;
    w := y - 2;
    (z * z + w) / (x + w)
}

If-Elif-Else

Inspired by oh-so-many programming languages, maybe Algol 60 was first?

if[t: Type](c: Bool, e: () -> t): Maybe(t) = with(c) {
| True  -> Just(e()),
| False -> Nothing
}

elif[t: Type](x: Maybe(t), c: Bool, e: () -> t): Maybe(t) = with(x, c) {
| (Just(y), _)     |-> x,
| (Nothing, True)  |-> Just(e()),
| (Nothing, False) |-> Nothing,
}

else[t: Type](x: Maybe(t), e: () -> t): t = with(x) {
| Just(y) |-> y,
| Nothing |-> e()
}

E.g:

_ := if(True) {
  "Case one!"
}.elif(False) {
  "Case two!"
}.else {
  "Case three!"
}

Fun

Inspired by Kotlin

fun[r: Type](t: Type, f: t -> r): t -> r = f

In WTy2, serves to annotate the argument type of a function without having to use arrow-lambda syntax.

Lazy

Inspired by Scala

lazy[t: Type](f: () -> t): () -> t = f

Note this does not perform any memoisation (call-by-need). This would require some form of mutability to implement.

The

Inspired by Idris

the(t: Type, x: t): t = x

Annotates the type of x.

With and Also

Inspired by Kotlin

with[t: Type, r: Type](x: t, f: t -> r): r = f(x)

also[t: Type, m: Applicative](x: t, f: t -> m()): m(t) = f(x) $> x

with combines well with lambda-case syntax as a way to pattern match on a variable. E.g:

_ := with(x) {
| 0 |-> "Zero!",
| 1 |-> "One!",
| _ |-> "Other!"
}

Tagged

tagged[a: Type](f: a ~> Any): Type = [x: a] 'f(x)

Returns the set of all values tagged with the constructor.

Impl

impl(t: Type): Type = [u: t] u

The union of all types which implement an open type.

¹ Of course in WTy2, do-notation is not really related to the do utility defined here; it can be used in any block. "Braces-notation" doesn't quite roll of the tongue though...

Summary

Constraints

Constraints (Constraint) in WTy2 are used to pass evidence of equality or type membership, inspired by Haskell's Constraint kind. Unlike Haskell, WTy2 retaining tags at runtime means that dictionary-passing is not the only sensible implementation strategy (we can instead just dispatch on tags) but viewing Constraint as the set of types which are guaranteed to only have one value (i.e, if we were allowed to name members of constraints in WTy2, we would have for(c: Constraint, x: c, y: c) { x ~ y }), with appropriate inference rules, is still sensible.

Constraint Operators:

• x :: t = Dual to the binding operator :. Variable x is a member of the type t.
• t <| u = Dual to the binding operator <:. Type t is a subtype of u. This is actually not built-in. We can define it as t <| u := for(x: t) { x :: u }
• x ~ y = Variable x is equal to y. Specifically, reduces to the same normal form, or if a function, is extensionally equal.
• c /\ d = A constraint conjunction. Both constraint c and constraint d are derivable.
• c => d = A constraint implication. Constraint d is derivable if constraint c is assumed.
• for(t, f) = A quantified constraint. Function taking argument of type t and returning a constraint, f returns a derivable constraint for every value of type t. Example usage: for(x: Int, y: Int) { x + y ~ y + x } represents the constraint that (+) on Ints is commutative.
• Constraints, like types, are first-class. The type of constraints is Constraint and so arbitrary expressions of this type can also appear inside constraints.

Such That (<<=)

WTy2 features a built-in dependent operator that places additional constraints on values of a type. When used on the argument and return type of a function, this has the interpretation of defining requires and ensures contracts, respectively.

The <<= operator has the following type signature:

(<<=) : (a: Type, f: a -> Constraint) -> Type

To construct a value of type a <<= b from a value x of type a, b(x) must be in the context. Matching on a value of type (x: a) <<= b is equivalent in syntax to matching on a value of type a, but b(x) is implicitly added to the typing context.

Another interpretation of this operator that might be more intuitive for programmers who have used languages with dependent types before is as a dependent pair, where the second element must be a constraint dictionary.

An approximation of this operator in Idris2 could be defined like so (using boolean predicates lifted to the type level instead of Haskell-style constraints, which Idris2 does not really have https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.So.html):

data (<<=) : (a: Type) -> (p: a -> Bool) -> Type where
  Mk : forall a, p. (x: a) -> { auto f: So (p x) } -> ((<<=) a p)

infix 4 <<=

An example use would be to restrict the integers received by a function: ¹

total
foo : (Nat <<= \x => 1 <= x && x <= 3) -> ()
foo (Mk 1) = ()
foo (Mk 2) = ()
foo (Mk 3) = ()

We can see that although foo only matches on the natural number being 1, 2 or 3, the function is still correctly checked as total, as we must also pass a proof that the Nat is in the range [1-3].

The equivalent WTy2 declaration of foo is:

foo(x: Nat) <<= { (1 <= x && x <= 3) ~ True }

Note in this signature, foo is declared as a function which takes an argument of type (x: Nat) <<= { (1 <= x && x <= 3) ~ True }. This idea extends, we could define a type synonym and use that instead:

type NatBetween(min: Nat, max: Nat)
    = Nat <<= { min <= it && it <= max ~ True }

foo(x: NatBetween(1, 3))

Design Note: Equivalent Constraints

You may notice that given constraints can contain arbitrary expressions, we could formulate semantically-equivalent constraints in many different ways. For example, we could write { contains([1, 2, 3], it) ~ True }, or even { max(1, min(3, it)) ~ it }. That these constraints do indeed imply each other is not always obvious (especially to the typechecker).

This is arguably the main pain-point with dependent types. Proving that one constraint implies another can be tiresome and can clutter up code significantly. Refinement type systems solve this through restricting constraints to those that can be dispatched with an SMT solver, but this is often limiting. WTy2 attempts to provide some of the ergonomics of refinement types without the restrictions through the ability to write and use implicit proofs.

¹ As a side note, on the current Idris2 version (0.6.0), if x <= 3 is replaced with x < 4, the example breaks, with the compiler protesting that case foo (Mk (S (S (S (S _)))) _) is not covered. I suspect this is a bug.

Proofs

In many dependently typed language, an unfortunate side effect of needing to translate between different constraints is that code must be cluttered with calls to functions that do effectively nothing except prove that some constraint implies another.

WTy2 attempts to separate out these "proof" functions from the code that requires them through the mechanism of implicit proofs.

Syntax

The proof keyword can be written before a variable definition, with the name of the variable optionally elided. Named proofs can be called just like normal functions.

Variables annotated as proofs must be functions that return something of type Proof(c) for some c: Constraint.

Semantics

During WTy2 typechecking, all constraints which could not be satisfied are collected (along with their associated local typing contexts). For each of these constraints, we iterate through every in-scope proof and attempt to apply it (i.e: trying to match result/head of the proofs up with the desired constraint, via a similar mechanism to how superclass constraints are applied).

If introducing a call to the proof function immediately before the offending expression (concretely, for expression e and proof function p, replacing e with do { Refl := p(...); e }) allows the expression to typecheck, then we are done, and move on to the next stuck constraint. If there is still an error, there might still be a more suitable proof in scope and so we undo changes (revert to just e), and try to apply the next proof. If all in-scope proofs are exhausted, then the type error is outputted as normal.

Importantly, inserted proofs are limited to single function calls. If there is a proof that A => B and a proof that B => C, and a proof of A => C is required, the programmer must explicitly write a new proof of A => C. This is to prevent typechecking from looping.

proof(Proof(A)): Proof(B)

proof(Proof(B)): Proof(C)

proof(Proof(A)): Proof(C) = do {
    _: Proof(B) = QED;
    QED
}

Design Note: Transitive Closure of Proofs

While needing to write transitive proofs might seem slightly painful, note it is NOT intended that every single possible valid proof function is written. First of all, this is likely impossible (for the same reason typechecking would loop: infinite valid proofs can be obtained while starting from a finite number), but also, it is unnecessary! Why prove anything that isn't helpful?

Instead, it is hoped that the WTy2 programmer writes code assuming all obvious implications are known to the typechecker, and then if a type error is encountered, the programmer writes the proof that fixes that specific error. The benefit is that now all future times that same error would appear, the in-scope proof is implicitly reused.

Design Note: Provisional Definitions

Idris has a feature with a similar goal (that of splitting proofs and code relying on them) known as "Provisional Definitions" https://docs.idris-lang.org/en/latest/tutorial/provisional.html. The main disadvantage is that you do not get the reuse of proofs that comes from WTy2 (i.e: proofs must be specifically named based on the function they are required in).

The obvious benefit here is that the Idris compiler does not have to search through all possible implicit proofs, meaning the impact on typechecking performance is lessened. Right now, it is somewhat unclear how often implicit proofs will be able to be reused, but it is hoped that this will be a significant quality-of-life benefit for ordinary programs, perhaps even near the scale of much more heavyweight features, say, tactics (the convenience of not needing any explicit user-interaction when relying on properties like m + n ~ n + m, I think should not be understated).

Implementation Note: Typechecking Performance

A naive implementation of the implicit proof searching algorithm will have a pretty devastating impact on typechecking performance. Hopefully some good method of pruning the search space can be found. It is also suggested that when proofs are successfully found, that information is cached somehow so on future compilation it does not need to be rediscovered.

Note the process of searching in-scope terms to find something that will allow the program to typecheck is not at all a new idea. Idris, for example, allows for writing explicit "holes" in programs https://docs.idris-lang.org/en/latest/elaboratorReflection/holes.html, where the compiler can automatically search for expressions that fit the desired type signature using functions labelled with #hint pragmas. Compared to this, WTy2 holes are relatively modest: the expressions are limited to single function calls.

Implementation Note: Runtime Performance

WTy2 does not assume totality of functions. This includes proofs, and so it is entirely possible for a proof to typecheck, but then at runtime loop infinitely or crash.

For this reason, to preserve safety, running these proofs is unfortunately necessary. Execution these proofs can have severe performance impacts however (to the point of changing the time complexity of many algorithms). It is therefore suggested that WTy2 implementations allow compiling with an option that skips over calls to proofs, assuming totality. This has the consequence of ,aking infinite loops/runtime crashes in proofs undefined behaviour.

Modules/Imports

It would be nice if importing proofs operated similarly to importing instances: just having them always be implicitly imported from modules.

However, it is unfortunately possible to write buggy/even malicious proofs (given they are not checked for totality) and so users should probably have some control over which proofs are brought into scope.

Importing a function and it's proof-y nature separately might be desirable, and so importing a named proof can be done as if it was an ordinary function, while importing it as an unnamed proof can be done with the specific syntax: proof(proofFun1, proofFun2). All proofs in a module can be imported as proof(..).

Dependent Types

WTy2 features dependent record and function types.

TODO (should start with low level definitions of dependent cons/telescopes and dependent function arrow)

Summary

Low-level Semantics

WTy2 is a programming language (read: language for writing programs). Programs are usually written with the intention of executing them on a computer, and so some thought should probably be put into how that might be achieved.

Original goals for WTy2 included having it be a suitable language for systems programming, with predictable compilation and blazing-fast performance. These are noble goals, but the reality of making a programming language is that there is only so much time and so I must admit: while I think (hope) that I have come up with novel and interesting ideas in the realm of abstraction, I have not been able to crack how to place those in a systems-programming-appropriate type system, and I do not believe I am likely to anytime soon.

Specifically, the state-of-the-art right now in this area seems generally to focus on linear/uniqueness typing, borrowing, monomorphisation and allowing unboxed types with suitable restrictions. Let's address each in turn:

• Linearity/Uniqueness Typing - A very powerful type system feature, useful for expressing contracts with types (i.e: safe resource usage) on top of benefits for memory management implementation. However, it is also hard to combine with dependent types. Idris2 has managed the linearity half via QTT, but suffers from a lack of quantity polymorphism that requires code be duplicated to handle the different quantities, which is unnacceptable in an abstraction-driven language IMO.

• Borrowing - Linearity/uniqueness typing also has an additional problem: it is very restrictive (especially if it is the default). Lending a temporary reference (with the caller afterwards still free to drop or move the referenced value safely) becomes pretty necessary when using these typing features in practice. Unfortunately, these guarantees about how long referenced values live for are hard to track, requiring (lifetime) annotations and/or very restricted use. Further, when references become pervasive in a language with subtyping, considerations must be made over whether that subtyping relation is coercive - effectively a decision between variance and efficient/flexible runtime representation. Both would be nice!

• Monomorphisation - Noticing how typeclasses, invented merely as a tool for abstraction in Haskell fit so perfectly with a low-level compilation strategy of compiling distinct versions of functions for each type is in my opinion the coolest thing by far about Rust. It's so clean that I spent quite a few months obsessed with the idea, looking at ways to enhance it ¹.

  Simultaneously, when types are viewed as sets of values, monomorphisation starts to look insane - it's entirely predicated on the idea that the number of sets of values considered by a program is vastly smaller than the number of values it deals with (for one, the number of those sets must be finite or your executable must become infinitely large). This simply isn't the case when subtyping, fancy-typing, let alone dependent typing are added to the mix. Plus as a dual to the predictability you get as a programmer, the compilation strategy reveals implementation details, requiring consideration on whether to suffer executable bloat or dynamic dispatch cost.

• Unboxed Types - I already rejected the duplication of code associated with linearity-without-polymorphism so that I similarly reject it in the context of (un)boxing should come as no surprise - and polymorphism over unboxed values relies on full monomorphisation. Further, giving control over exactly the representation of data inherently leaks implementation details (e.g: the decision of whether to pass by reference or value based on the size a type vs a pointer) to the programmer.

  It is unfortunate that this is probably the feature least compatible with WTy2 and yet is one with potentially the highest impact (zero-cost FP via unboxed closures is very enticing). My hope is that a compiler doing extensive cross-module specialisation might be able to automatically unbox, but this is something that should be explored far down the line.

I argue there are really two main aspects of implementation that these features are focussed on: memory management and runtime representation of values/dispatch strategy. For the former, WTy2 will take inspiration from Lean and Koka (similarly functional, pure, strict programming languages with rich type systems) and adopt a form of reference counting. What's especially nice about this approach is that it combines well with the lower-level type system features that might be added later (in-place updates for values with a refcount of one is just a runtime version of in-place updating of uniques, borrows can skip the refcount increment/decrement etc...). For the latter, in the best case specialising functions for specific sets of values is likely to be a significant optimisation, but the baseline strategy must support WTy2's infinitely large types, existential types etc... - a uniform runtime representation of values is required. See the dedicated section for the current design.

• Extend rust-style impl returns to allow returning values of potentially different types. This can be implemented by monomorphising all code following the call-site and statically dispatching at the return statement.
• Allow variables to be generic (take a type parameter), allowing first-class higher-rank polymorphic functions, and also, perhaps more interestingly, super efficient heterogeneous unordered collections (data-oriented programming without the hassle).

Runtime Representation

Note that there is likely a ton of flexibility here, and I know very little about writing efficient language runtimes/low-level performance optimisation. The design I layout here is just a suggestion, that will probably be changed significantly over time ¹.

WTy2 values are linked lists ¹ of tags, where each tag is 32-bits. The starting point for this idea is that these lists of tags are just the natural serialisations of the values (i.e: the data constructors). All tags are associated with some source-code identifier, and so to illustrate below, I will denote all tags as T_<Ident> where <Ident> is the associated identifier.

The first obvious issue with this is how to fit all the tags into 32-bits. For example, 32-bit integers alone would fill the space of tags. This is fixed by giving datatype declarations slightly unique semantics. A datatype defines one tag for the type, and then all variants are placed in a separate tag-space (and so are free to overlap with other tags in other datatypes).

To clarify, after the below two declarations:

datatype Bool0 where
  True  : Bool0
  False : Bool0

data True0
data False0
type Bool1 = True1 | False1

x: Bool0 = True0 and y: Bool1 = True1 (in the absense of other optimisations) will have differently lengthed tag lists at runtime - x will have a tag list of length two (T_Bool0 and T_True0), while y will just be a single tag (T_True1).

In order to "be not stupid" ¹, tags which are known to be fixed at compile time really should be elided. Achieving this is subtle though. Consider that WTy2 allows writing extensional proofs about functions like for(x: Int) { foo(x) :: Int } - does this mean we must elide the T_Int0 tag from foo-returned values? Achieving this consistently in general is catastrophically undecidable (for the same reason WTy2 bounds the number of automatic proof insertions to one per goal constraint).

TODO - Come up with some tag-elision system that actually works, and supports aliasing (HARD).

Core Language

Implementing a typechecker and compiler for the entire WTy2 language at once is likely to prove somewhat challenging. Here, a design for an intermediate, typed core language (inspired by efforts on GHC) is outlined.

Core-Lang Constructs:

• Lambda case expressions (covers lambdas, matches and let bindings)
• Telescopes: A single built-in datatype covering (dependent) tuples and lists
• Dependent function arrows
• Constraints (equality coercions, type membership, quantified constraints)
• Data declarations
• Type declarations, with associated methods and supertype constraints
• Default instance declarations

Desugaring:

• WTy2 core does not feature named tuples/records. These are instead desugared into telescopes like ordinary tuples and lists.
• In WTy2 core, all function arrows are dependent, meaning a function that takes and returns an integer would be represented as Int -> { Int }

Unanswered Questions:

• How to represent recursion? Could either use recursive binders or a dedicated fixpoint operator.

Specialisation

WTy2 does NOT currently feature "specialisation" as a high-level language feature (à la Rust ¹), being able to override typeclass instances for specific types. Instead, specialisation in the context of WTy2 refers to an optimisation strategy that is key to get highly polymorphic WTy2 programs to perform well¹.

Specialisation can be thought of a bit like a "lite" version of monomorphisation. Types can be arbitrarily large in WTy2, so full monomorphisation as a compilation strategy is infeasible; however, where possible, compiling separate versions of functions for specific argument values (or sets of argument values) and dispatching to those specialised versions can get most of the benefits (the main downside being the compiler now has to decide on a strategy for deciding when to specialise).

Some possible heuristics for deciding when specialisation is a good idea might include:

• One of the function's arguments has a small set of inhabiting values. For example, if a function takes a Bool argument, specialisations for when the Bool is True and False are probably a good idea.
• A function is explicitly called somewhere in the program with an argument of more constrained type than the function could accept. For example, if a function takes an arbitrary Num and is called somewhere with an Int, a specialisation for Ints should probably be generated. If the function is called with a constant 23, then a specialisation for this exact integer could be generated (effectively constant-folding).
• Note after one function is specialised, function calls in that function's body may now also become candidates for specialisation by the rule above. This transitive specialisation is very powerful, as it can eliminate what might otherwise be a large number of repeated matches.

Specialisation is similar to inlining, but generated specialised code can be reused, reducing executable bloat. Prioritising specialisation over inlining seems like a reasonable goal.

Dispatching to Specialised Functions

Dispatching to specialised functions at runtime rather than compile time would greatly increase the power of this optimisation. i.e: suppose there is a function foo : impl(Num) -> Bool with a much faster specialisation for n ~ Int. We would like to ensure that even code like x: Int = 0; y: Num = x; z = foo(y); uses the specialiased version of foo, using the type information (in the form of variant tags) that is kept around at runtime to dispatch appropriately (assuming the savings from running the specialised version are worth it over the cost of dispatching appropriately).

Exactly how feasible this is will likely have to be reassessed after the design for open types/instances is finalised, but this potentially could be implemented very simply as just a compiler pass which adds seemingly redundant pattern matches before various function calls that appear to be good candidates for specialisation ¹.

Summary

Soundness

WTy2 is a programming language with dependent types first and foremost, NOT a theorem prover.

In fact, viewed as a logic, WTy2 as it currently exists is highly inconsistent. It is trivial to prove bottom and from there anything. The only guarantee making this somewhat palatable is that these are all cases where the program will loop or crash at runtime. WTy2 (when programs are ran in debug mode without optimisations) will never actually create values of bottom type.

This is useful for programming (proving termination is tiresome and sometimes even impossible) but makes WTy2 effectively useless for theorem proving. In the far future if these holes were to be closed (likely opt-in with some sort of compiler pragma or flag, safe), then this would no longer be the case, and hence these holes are documented below:

Non-terminating Recursive Functions

foo() := foo()

Type in Type

Similar to Haskell, WTy2 has the axiom Type : Type. Girard's paradox ¹ is almost certainly derivable from this.

Russel's Paradox, Directly

WTy2's expressivity and subtyping allows for a much more direct encoding of Russel's paradox (treating types as sets).

type Russel = (t: Type) <<= { t :: t => Bottom };

The additional danger here is that a suffiently advanced constraint solver could derive bottom entirely on it's own just from this definition being in-scope.

An informal sketch of how this might happen is outlined is below:

Constraints are written in similar syntax to WTy2 source, but we elide types of for bound variables, instead prefering to write them as implications.

# From definition of Russel

[G1] for(t) { t :: Russel /\ t :: t => Bottom }
[G2] for(t) { (t :: t => Bottom) => t :: Russel }

[W1] Russel :: Russel

# Head of G2 matches, so instantiate t = Russel

[W2] Russel :: Russel => Bottom

# Need to show an implication, so assume LHS to reach RHS

[G3] Russel :: Russel
[W3] Bottom

# Head of G1 matches, so instantiate t = Russel

[W4] Russel :: Russel /\ Russel :: Russel

# Simplify

[W5] Russel :: Russel

# Solve with G3

And so we conclude by deriving Russel :: Russel (from which, we can trivially obtain Bottom via G1).

That this is a real danger is illustrated by how we can encode exactly problem with Haskell typeclasses:

main :: IO ()
main = case veryBad of MkDict -> no @(IO ())

class Bottom where
  no :: a

data Dict c where
  MkDict :: c => Dict c

data Set = Russel

type In :: Set -> Set -> Constraint
class ((a ~ b, In b Russel) => Bottom) => In a b

instance (In s s => Bottom) => In s Russel

bad :: Dict (In Russel Russel)
bad = MkDict

veryBad :: Dict Bottom
veryBad = case bad of MkDict -> MkDict

Indeed, Haskell runtime loops when executing this program, despite there being no explicit recursion in the code¹.

IMO it is pretty important we avoid this. Mathematicians might argue the cause of the problem here is the typeclass declaration itself, but ruling it out would require a drastic reduction of WTy2's expressivity (e.g: removing an entire feature, like the (<<=) operator) or adding type universes.

Luckily, there is a much easier fix: not giving the solver access to an implication-introduction rule. Instead implications should only be brought into scope via superclass constraints, instances and explicitly written proofs. We could of course write a proof of Russel :: Russel => Bottom, but that this would loop at runtime is fine - we at least have source code we can point to in a stack trace (proofs are not totality-checked in WTy2).

¹ See http://liamoc.net/posts/2015-09-10-girards-paradox.html for a nice walkthrough of how to derive this in Agda.

¹ Though do note that the loop in Haskell can be encoded much more simply (and arguably arises from using superclass constraints when checking instances):

class (ImpliesBottom => Bottom) => ImpliesBottom

instance ImpliesBottom

Syntax Debates

https://wiki.haskell.org/Wadler's_Law

Syntax is hard, and discussions about it tends to go nowhere...

...so let's discuss syntax!

Enforced Capitalisation Convention

In functional languages, it is easy to have an ambiguity with irrefutable pattern matches vs variable bindings. Consider in Haskell:

foo = ...
  where
    {- Function or Constructor -} i = ...

Haskell gets around the ambiguity here by enforcing a simple capitalisation convention: constructors must start with a capital letter, and variables must start with a lowercase one.

foo = ...
  where
    Bar i = ... -- Pattern match
    bar i = ... -- Local function definition

As long as, the language allows nullary data constructors data constructors this does not just apply to functions, and the ambiguity in WTy2 specifically is even more prevalent, given the rule that f: t -> u can be written as f(t): u.

One obvious solution is to copy Haskell's homework: data constructors are capitalised and variables are not. This rule fits well with WTy2's style in general: types should be capitalised, and this makes sense because types, like data constructors, are matchable.

However, there are downsides. The most compelling from my perspective is how non-latin alphabets do not necessarily contain capital letters. I do not believe this is quite as significant of an issue as sometimes presented (a convention for code written in those alphabets could easily be created where data constructors/types must start with a latin-alphabet capital letter, say M for matchable) but even so, it is not ideal.

The alternative is to use some dedicated keyword/symbol to disambuate. Perhaps def prefixing all variable bindings or match prefixing all irrefutable pattern matches.

Using def keyword on functions

def takesFunctionAndMatches(def foo(Int): Int, MkFoo(x): Foo) := do {
    def bar(y: Int) := foo(y);
    MkBar(z) := x;
}

Using match keyword on matches

takesFunctionAndMatches(foo(Int): Int, match MkFoo(x): Foo) := do {
    bar(y: Int) := foo(y);
    match MkBar(z) := x;
}

Neither alternative feels great though coming from Haskell. There is no reward for following the capitalisation convention! My current plan is therefore a compromise: capitalised = assume match, lowercase = assume variable, but the programmer can also use either keyword to override. This might be an overkill solution, but it seems promising (and actually quite easy to parse!).

Binding/Constraint Operators

Currently, I am liking:

But there are a few possible alternatives and questions:

• Use keywords/infix functions instead of operators. E.g: x is t/x in t instead of x :: t.
• Make the common pattern for constraint (except for (~)) be to add a second colon. E.g: (<::) instead of (<|).
• Add a dedicated binding operator for (~), such as (~:).
• Instead of (::), all types could implement Any -> Constraint so instead of x :: Int you would write Int(x) (a bit Verse-like).
• With (:), (::), and (<:) taken, what should cons be? (:>) could very easily be misinterpreted as a flipped version of (<:). Perhaps (:;) or (:.)?

Implicit Braces

WTy2 contains a few built-in dependent type operators ((->), (~>)) which automatically add braces to the RHS if the type expression does not type-check without. The advantage is obvious: cleaner syntax. All non-dependent functions requiring braces around the result type (e.g: Int -> { Int }) (or using a different arrow) is ugly.

That said, this is clearly a special case, and special cases generally do not lead to a cleaner and easier-to-learn language. It might be worth considering if this implicit lambda-abstraction functionality is something that should be possible to opt into with other operators.

Unicode

TODO

• ∀ should be parsed as a letter to allow ∀ := for.

Lambda/Pattern Match Syntax

Currently, for lambdas that bind variables, I like the look of the following syntax: { \Pat -> ...} for irrefutable patterns and { | Pat1 -> ..., | Pat2 -> ... } for lambda-case expressions.

However, this does overload the meaning of -> somewhat. Lambda-calculus gives us an alternative separator . as in { \Pat. ... } which I don't hate, but I find { | Pat1. ..., | Pat2. ... } very ugly. { \Pat1. ..., \Pat2. ... } is better but now no longer really looks like a pattern match.

Yet another alternative is to use an arrow with a bar |->. This is justified via numerous FP papers which use the LaTeX equivalent of this symbol, but of course transliterated into ASCII, it does look somewhat ugly.

"Such That" Operator

There appears to not really be a standard operator for "such that" in mathematics (except in set comprehensions, but (:) and (|) are already taken), and the most common, (∋)¹, does not have a reasonable ASCII approximation (at least that I can think of).

(<<=) I think has some advantages in that it is very clearly not symmetrical (IMO symmetrical-looking glyphs as operators should really only identify associative, if not commutative operations) and it is vaguely reminiscent of (=>) which in Haskell is used to represent the curried version of a similar concept. On the other hand, it (surprisingly) doesn't appear to have a unicode equivalent (there are double-headed arrows, and double-lined arrows, but apparently no double-headed-double-lined arrows...).

On the other hand, a very common operator being three-characters long is a bit unfortunate. (-<) is IMO quite aesthetically nice and I do also quite like ($) given how (if you squint) it looks a bit like an S and a T overlaid.

Type Aware Allocators

A goal of WTy2 is to allow for good performance (especially with regards to memory locality) without much additional work on the part of the programmer/enforcing closed-world assumptions on written code.

A major part of this is the concept of a type-aware-allocator. WTy2 makes extensive use of allocators (array based and recursive data structures in WTy2 should ideally be generic over the allocation scheme) so by providing tools to create good ones, almost all data structures should benefit.

As an example for the sort of properties we would like to achieve, suppose our program had a large list of Ints, this was then upcasted into a list of Nums and then many other opaque Nums got added to the list. We then calculate a total sum (note that this operation does not care about the order in which we iterate over the values). Ideally therefore (for cache and memory locality reasons) we should somehow keep all the Ints in their own region of memory and sum these first.

The rules for performing specialisation with these allocators should use similar (perhaps the same) rules as ordinary function specialisation. i.e: a good heuristic is if we allocate any value with known concrete type, we should specialise for that type.

It would be ideal if WTy2 could provide some sort of language interface to create custom type-aware alloactors. I do not currently have a good model for how to design this. Difficulties I can currently forsee include prevent the number of specialisations from being observable (to prevent UB - the compiler is free to specialise as much or as little as it wants), and more generally just challenges of writing low-level mutability-based code in a pure functional language.

Recursive Data Types

Elsewhere in this spec (I may go back and fix it up later), I have been relatively loose with defining types like:

data Cons(head: t, tail: List(t))
data Nil

type List(t: Type) = [head: t, tail: List(t)]
                     Is(Cons(head, tail))
                   | Is(Nil)

Unfortunately, there is a bit of an issue with values of this type - they have unbounded size! Specifically, if a function takes a List(Int), the actual list it could receive when called could contain any number of Cons nodes.

Furthermore, it is not clear how to implement variance for this type. If we have a List(Int), then ideally at each node we would not store any information informing us that the item is indeed an Int (we can know that it could be nothing else from the type signature). However, we would like to be able to pass this into functions accepting say List(Num). This would seemingly require creating an entirely new list with the Int tag attached to every node.

One potential solution is to simply not use recursive data types. An array list-based data structure would help to avoid these problems and would also provide great memory locality. In functional languages like Haskell and Closure, however, the utility of being able to create large linked structures that utilise sharing cannot really be understated. WTy2 should be able to achieve something similar.

The solution is references, but with perhaps a slightly different flavour to what you might imagine coming from languages like Rust.

data Cons[r: Ref](head: t, tail: List(r, t))
data Nil
type List(r: Ref, t: Type) = r(
    [head, tail: List(r, t)] Is(Cons(head, tail))
                           | Is(Nil)
    )

The main interesting thing about this definition is that r, the type variable that will be instantiated to some sort of reference that will break up the infinite structure, is generic. We could instantiate r to some owning reference type like Box and get a definition similar to what we would achieve in Rust, but we can also do better.

The problem with Box or any other global allocator is poor memory locality. If the elements are added to the list randomly over time, then they will be placed in effectively random locations in memory. What we would like is for every element of the same list (not just same type!) to be placed in more-or-less the same location (note this idea is similar to that of arenas in Rust).

type Alloc = ...
type RefTo(a: Alloc, t: Type) = ...

// Get the allocator of a reference
allocOf[a: Alloc, t: Type](r: RefTo(a, t)): Alloc <== { it ~ a }

// Would be a method of the 'Alloc' type
alloc(a: Alloc, t: Type): RefTo(a, t)

// Create a new allocator and allocate an expression using it
new[t](x: t): [a] RefTo(a, t)

// Function application, but wrap in the allocator at the end
build[a: Alloc, t: Type](x: RefTo(a, t), f: RefTo(a, t) -> t)
    : RefTo(a, t) = alloc(allocOf(x), f(x))

// We take advantage of partial signatures to not need to specify the allocator
// in the signatures of 'x' or 'y'
x: List(t=Int) = new(Nil)
y: List(t=Int) = build(x) { Cons(3, it) }


// Alternate style, arguably neater but requires some extra busywork

type ConsLike(r, t) = [head: t, tail: List(r, t)] Is(Cons(head, tail))

// Would likely be a method of some type
// '(,..)' denotes partial application
// (i.e: will fill in the other arguments later)
allocOfCons[a: Alloc, r: RefTo(a,..), t: Type]
    (x: ConsLike(r, t)): Alloc <== { it ~ a  }
    = match(x) case(Cons(_, tail)) -> allocOf(tail)


altBuild[a: Alloc, r: RefTo(a,..), t: Type]
    (x: ConsLike(r, t)): List(r, t)
    = alloc(allocOfCons(x), x)


z: List(t=Int) = altBuild(Cons(3, x))

There are some interesting consequences of enforcing code like this. For example, if you have two different lists, potentially created with different allocators, the elements from one allocator must be all copied into the other. Because of this, it is recommended that if an algorithm involves a lot of merging of linked data structures, there a single allocator is created at the start and all sub-structures are built up with it.

Note that having the allocator responsible for storing all nodes also helps with the variance problem as mentioned above. Allocators in WTy2 must provide a way of recovering full type information for every value that is stored by them, but to ensure memory is not wasted, a good allocator would store elements with common type prefixes together and avoid duplicating said prefix. The exact mechanism for how these prefixes are represented is WIP and would be dependent on the allocator in question, but one could imagine, for instance, a binary tree which is traversed based on the reference and stores the common prefixes at the leaves.

The main downside is arguably the unfortunate amount of syntactic noise (for instance, compared to similar linked data structures in Haskell). Still, this is somewhat to be expected in a more low-level programming language - with the clutter comes flexibility.

A very nice side-effect is that in simple cases, as r is not restricted to be matchable (it uses the ordinary function arrow), references can be omitted for known finitely sized structures.

x: List(r={it}, t=Int) = Cons(1, Cons(2, Cons(3, Nil)))

Note this works because the type of x is elaborated with the constraint x ~ Cons(1, Cons(2, Cons(3, Nil))) which fixes the size of x.

In theory, this means lists with constraints that ensure finite length should also be allowed. In practise, compilers may want to try and detect these cases by iterating through potential inhabiting values. If iterating through all potential inhabiting values takes too long, it is likely that the structure is large enough that it would benefit from being heap allocated anyway. Perhaps it could be made possible (via dependent types) to allow the programmer to write proofs that a constraint implies that the size of the type is bounded.