candid

Dependently typed programming language with timeless referential transparently.

We functional programming language aficionados enjoy our referential transparency. We point to our functions and say "here, I know that whenever I see this expression it will always return the same value". Then you want to use some package that requires a newer version of some other package, and suddenly your code doesn't even type check much less return the same value. Or there's a new version of the programming language, and old code doesn't compile on it anymore.

This is an attempt to fix all of that, by reworking a number of assumptions that we make about the mechanics of programming.

Inspirations

Morte

Morte is a minimalist implementation of the calculus of constructions. Every type checked program is total, and thus will terminate in finite time. Morte uses this property to optimise it's input by evaluating it to the extent possible. Morte doesn't do any type inference, just type checking and that is complete, so any complete set of code that compiles now will always compile.

Unfortunately, Morte cannot be implemented in itself, not being total. Morte is also based on the traditional text file full of names in the write-parse-type check-compile loop.

Unison

Unison is much more of a traditional functional programming language is some respects, with unbounded recursion and type inference. However, it's purpose is to ease distributed computation, and it needs to be able to send functions to other nodes to evaluate, and know that they have all the same pieces.

To this end, Unison identifies functions by a hash if it's content. If you have a x = x b and you make a new version of b, the system will need to make a new version of a also. However, if you have the hash of a, there's no changing it. The hash will always point to the same function.

To this end, Unison strives to do away with the notion of textual source code. Instead of editing a text file, the goal is to be editing abstract syntax trees directly. This introduces quite a shift from the traditional programming process, there is no more parsing of source code.

Candid

Both these systems have a level of timeless referential transparency. Morte with it's check-only type system, and Unison with it's immutable hash-tree codebase. Yet if you have a Morte URL reference, you can't be sure it's the same data without keeping extra information. And how strong is the guarantee that Unison's type inference won't ever change?

Candid strives to do both, given a hash, it will always expand to the same code, and if that code type checked before, it will type check to at least the same degree later, and it will evaluate to the same result (given the same inputs of course). There are no circumstances where the compiler is guessing at what the programmer means, so there's no leeway to change what assumptions the language makes.

The Calculus

One might represent Candid's (and Morte's) inner calculus something like this:

data Expr
  = Lam (inType : Expr) (body : Expr)    -- inType ⇒ body
  | Ref (n : Nat)                        -- n
  | App (func : Expr) (arg : Expr)       -- func arg
  | Pi (inType : Expr) (outType : Expr)  -- inType → outType
  | Star                                 -- *

• Lam encloses a function, apply an argument (type inType) and it returns body with references to it replaced by that argument.

• Ref refers back n arrows, to a Lam or a Pi, to take the place of an argument on function application.

• App applies the argument arg to the function func.

• Pi is the type of Lam, where inTypes match and outType is the derived type of the body.

• Star represents a type, informally this includes the type of Star and a Pi with an output of Star - though reality is more complicated.

With these one may define functions:

id      = * ⇒ 0 ⇒ 0

id is the simplest function, it simply returns it's argument. However, as every Lam requires a input type, it takes an additional argument first that specifies the type. Candid replaces polymorphism with specialization. Notice also how the two 0s refer to different arguments, the first one refers the first argument (which is a type) and the second to the second (which is a value of that type).

Unit    = * → 0 → 1

Unit is the type of id, so named because id is the only one function of that type. Here both 0 and 1 refer to the first argument, the type of the value given to and returned by id.

Boolean = * → 0 → 1 → 2
True    = * ⇒ 0 ⇒ 1 ⇒ 1
False   = * ⇒ 0 ⇒ 1 ⇒ 0

Boolean has exactly two inhabitants, True and False, which one is which is purely arbitrary, but, for our purposes, True returns the first value and False returns the second, and thus function application:

or     = Boolean ⇒ Boolean ⇒ 1 Boolean True 0
and    = Boolean ⇒ Boolean ⇒ 1 Boolean 0 False

or takes two Booleans uses the first one to choose between True and the second. Sugaring this to something more familiar:

or : Bool -> Bool -> Bool
or a b = case a of
              True -> True
              False -> b

and could be sugared in exactly the same way.

Both are of the type Boolean → Boolean → Boolean. Note that above we don't make any allowances to refer to things by name in the data structure up above. Boolean here is just a placeholder for * → 0 → 1 → 2.

For more examples of what you can do with this sort of minimal calculus of constructions, albeit with names instead of numbers, see the Morte Tutorial.

Hashes

  | Hash (hash : Vect 8 Bits32)

This is the first thing (other using natural number indices rather than names) that differentiates Candid from Morte. Boolean can also be represented by the 256-bit hash 941ad446211f88e385d2b95be6336328b1708e77a11dca3e783a240d9dfadca5. Hashes replace well-typed closed sub-expressions, and indeed, introduce no semantic differences what-so-ever, but are like a provable form of Morte's URL references. Hashes are the basis of Candid "source code" as a pure immutable data structure, a directed acyclic graph (albeit representing a cyclic one).

With just the above Expr type, we can only represent total functions, and only total functions at that. This is by design, and is very helpful in writing correct code. However, this also means we can't implement Candid in Candid.

Recursion

  | Rec (n : Nat)                        -- @n
  | Type (outType : Expr) (body : Expr)  -- outType | body

So we get primitive recursion. Rec is a lot like Ref, but instead of being replaced with the argument, it is replaced with the function. Type is here to assist the type checker, so it can calculate the output types of a Rec.

Nat = * → 0 → (@1 → 2) → 2
Zero = * ⇒ 0 ⇒ (Nat → 2) ⇒ 1
Succ = Nat ⇒ * ⇒ 0 ⇒ (Nat → 2) ⇒ 0 3
add = Nat ⇒ Nat ⇒ Nat | 0 Nat 1 (@1 (Succ 1))

This is the recursive version of Nat, which sugars to:

data Nat = Zero | Succ Nat
add : Nat -> Nat -> Nat
add n m = case m of
               Zero -> n
               Succ p -> add (Succ n) p

Now all (or nearly all) the interesting things to do with Nats can be done without this sort of recursion using Nat = * → 0 → (1 → 2) → 2 on which operations are provably total by dint of type checking. So consider...

Expr = * →
       0 →
       1 →
       (Nat → 3) →
       (Nat → 4) →
       (@4 → @5 → 6) →
       (@5 → @6 → 7) →
       (@6 → @7 → 8) →
       (@7 → @8 → 9) →
       8

Editor

Notice that there're a lot of handy features missing here. No variable names or function names, just numbers and hashes! No type inference, type classes, or implicit arguments! All that bookkeeping overhead passing all these types around! Are you sure this isn't one of those esoteric languages? Well, that's where the editor comes in.

Presented above is the data structure, how code in stored inside the compiler, the interpreter, the code store, and the editor. It is, at the same time, quite verbose and yet terse and inscrutable. Therefore editors also store names to give functions and arguments, comments, presentation data, everything they need to transform that data structure into something humans can work with.

Editors can hide any type annotation that is normally implicit and inferred, they can infer that type information to start with. They can present numbers with digits instead of as functions, gave names to your functions and arguments, expand and collapse expressions, pretty print the math, and automatically derive sufficiently constrained functions by their type.

By editing directed acyclic graphs rather than blobs of text, there are no syntax errors, no reformatting, type checking may be done at edit time, compilation can be done incrementally at edit time, all valid type checked expressions are efficiently saved in the code store until garbage collection - long term undo history at the granularity of functional changes.

And we can still have all the magic that comes of parsing and syntactic sugar, of type inference and implicit arguments, but it'll be magic you can look at, magic you can change by tweaking your editor, not the compiler, transparent magic, magic revealed, candid magic.

Structurally Equivalent Types

One of the boons of using de Bruijn indices is that we get α-equivalence for free. That is, checking whether two expressions have the same structure, disregarding names. This also means that:

data Ordering = LT | EQ | GT

is exactly the same as

data Axis = X | Y | Z

and any other enumerated type with three values:

Ternary = * → 0 → 1 → 2 → 3
Zero = * ⇒ 0 ⇒ 1 ⇒ 2 ⇒ 2
One = * ⇒ 0 ⇒ 1 ⇒ 2 ⇒ 1
Two = * ⇒ 0 ⇒ 1 ⇒ 2 ⇒ 0

This means that our type checker loses the power to distinguish between Axis and Ordering. There are a number of ways to regain this power, and one requires nothing extra from the language, introducing a singleton into the type.

There are an infinite number of singleton types. * → 0 → 1 is the simplest and most obvious, but * → * → 1 → 2 is much the same. While one could go on forever just adding intermediate type arguments, consider the type:

* → * → * → * → (4 → 3 → 2 → 4 → 6) → 1 → 2

So long as the arguments to the function and the value argument are not all of the same type, there is obviously only one possible function with that type, in this case:

* ⇒ * ⇒ * ⇒ * ⇒ (4 → 3 → 2 → 4 → 6) ⇒ 1 ⇒ 0

With $n$ type arguments and $m$ arguments to the function, this yields $n^{m+2}-n$ unique singleton types, 4092 for the model above.

So to make a type unique, one simply prepends a unique singleton type.

Axis = (* → * → * → * → (4 → 3 → 2 → 4 → 6) → 1 → 2) → * → 0 → 1 → 2 → 3
X = (* → * → * → * → (4 → 3 → 2 → 4 → 6) → 1 → 2) ⇒ * ⇒ 0 ⇒ 1 ⇒ 2 ⇒ 2

As there is only one possible value for the singleton type, it can be filled in automatically (and hidden) by a sufficiently smart editor. During type checking this will ensure that X isn't used in place of LT or vice versa, and it will be optimized away with partial evaluation during compilation, producing the exact same code as Axis = * → 0 → 1 → 2 → 3.

Note this also allows one to specify a function:

(* → 0 → 1 → 2 → 2) ⇒ (* → * → * → * → (4 → 3 → 2 → 4 → 6) → 1 → 2) ⇒ 1

which turns an Ordering into an Axis, much like the lone constructor in Haskell's newtype.

Type Inference

If there is a hole in the expression, it is helpful to be able to infer the type of the expressions that fit in the hole. Though we call this type inference, it takes place in the editor rather than the complier and charges or improvements do not change any already written programs.

We start with an expression and a path to the sub-expression which we want to infer the type of, and an expected output type. In general we follow the path, changing the expected output type based on the root of our current expression.

• Pi expects a type for both arguments.
• Lam expects a type for it's type and anything for the body.
• Type expects a type for it's type and that type for it's body.
• App is a little more complicated. The type of the function must be a Pi from the type of the argument to the expected type. So if we're looking for that we need to figure out the type of the argument first. Conversely to infer the type of the argument we need to determine the type of the function, and we expect that function's input type.

When we reach the end of the path we simply return the expected type. Thus our result can be anything, any type, a value of some type, or a Pi from one of those to another. with this type pattern we can match or generate expression to fit in the hole.

What to do about Universes

Informally, ★ is the type of ★ and ★ → ★ and the like. In reality, stars are paramaterized over natural numbers, such that the type of ★ₙ is ★ₙ₊₁. This is to prevent inconsistancy due to Girard's Paradox.

In the current implementations, ★ is either of type □ or (paradoxically) of type ★. Eventually there will be universe inference, which will result in some ultimately invalid programs that currently type check fail to type check. This is the sole exception to Candid's forward compatibility guarentee - if there is a bug in Candid that results in an inconsistant logic, programs that depend on that bug will not work in future versions.

The problem with ★ is having of type □ is that one cannot use the conventional definition of Bool as a dependant type, and cannot even convert a value Bool to a type-level Bool:

Bool = t:★ → true:t → false:t → t
True = t:★ ⇒ true:t ⇒ false:t ⇒ true
False = t:★ ⇒ true:t ⇒ false:t ⇒ false

<s>x:Bool → x ★ Bool Nat</s>

Bool★ = true:★ → false:★ → ★
True★ = true:★ ⇒ false:★ ⇒ true
False★ = true:★ ⇒ false:★ ⇒ false

<s>Bool★fromBool = bool:Bool ⇒ bool Bool★ True★ False★</s>

With universe inference it just looks like this:

Boolₙ = t:★ₙ → true:t → false:t → t
Trueₙ = t:★ₙ ⇒ true:t ⇒ false:t ⇒ true
Falseₙ = t:★ₙ ⇒ true:t ⇒ false:t ⇒ false

x:Boolₙ₊₊ → x ★ₙ Boolₙ Natₙ

Programs for Free

Consider the type Map, which is the type of a map function for the type m:

Map = m:(★ → ★) ⇒ t:★ → s:★ → fun:(t → s) → val:(m t) → m s

For each type m there will be a few possible programs that satisfy that type. For instance given the type Maybe and it's constructors Nothing and Just:

Maybe = t:★ ⇒ ★
	s:★ → nothing:s → just:(t → s) → s
Nothing = t:★ ⇒ Maybe t
	s:★ ⇒ nothing:s ⇒ just:(t → s) ⇒ nothing
Just = t:★ ⇒ x:t ⇒ Maybe t
	s:★ ⇒ nothing:s ⇒ just:(t → s) ⇒ just x

Our map function will have the type Map Maybe:

Map Maybe = ★
	t:★ → s:★ → fun:(t → s) → val:(Maybe t) → Maybe s

We need a Maybe s, which we can get via Nothing s and Just s y, where y is of type s. so one obvious (and wrong) option is:

map' = t:★ ⇒ s:★ ⇒ fun:(t → s) ⇒ val:(Maybe t) ⇒ Maybe s
	Nothing s

However we also have fun:(t → s) and val:(Maybe t). Either val is a Nothing t, in which case our only option is to use Nothing s, or it is a Just t x, in which case we have have two options, Nothing s and (x:t ⇒ Just s (fun x)). This points to the actual map function between Maybes:

map = t:★ ⇒ s:★ ⇒ fun:(t → s) ⇒ val:(Maybe t) ⇒ Maybe s
	val (Maybe s) (Nothing s) (x:t ⇒ Just s (fun x))

The heuristic here is to prefer solutions that use more arguments. If the type specifies that we take an argument, we probably want to use it in our program. Note that, as all of this takes place in the editor, it is just as easy to present the user with ten suggestions as one. The heuristic can just be used to order the suggestions. On the other hand, if there is only one possible program with a particular type, the editor could just fill it in.

Sometimes though, there are more than just a few options.

List = t:★ ⇒ ★
	r:★ → nil:r → cons:(r → t → r) → r
Nil = t:★ ⇒ List t
	r:★ ⇒ nil:r ⇒ cons:(r → t → r) ⇒ nil
Cons = t:★ ⇒ a:t ⇒ list:(List t) ⇒ List t
	r:★ ⇒ nil:r ⇒ cons:(r → t → r) ⇒ cons (list r nil cons) a

The type t:★ → xs:(List t) → List t has countably infinite different inhabitants. At the simplest there are Nil t and xs, for a little more effort any other duplication and/or permutation of xs works too. Thus we cannot present every solution - rather we must take the first few results of a breadth first search for solutions.

Note that if there are infinite inhabitants of List t → List t than there are likewise infinite inhabitants of List t → List s. Note also that there are infinite programs equivalent to any other program, simply by encapsulating the program in an id. A properly defined breadth first search will relegate those solutions to later on, where they will usually not even be enumerated.

Complier

• partial evaluation / specialization
• automatic source fetching
• extendible core data types
• automatic core data types

Runtime

• type system enforced capabilities
• forward (and limited backward) compatibility via translation layer specialization

Unlicensed

This is free and unencumbered software released into the public domain.