Introduction to Formality (Part 1)

First, because it keeps the language simple, obviously.

After all, this can be easily solved with macros outside the “official spec”.

But there is more than that: lambda encodings give you much more control over the runtime representations (i.

e.

, interaction nets) of your structures and algorithms.

In Formality, you can express, for example, functions that undergo runtime fusion, something that is, simply, not possible with Haskell’s or Agda’s native datatypes.

4a.

Simple types (Bool, Pair)To start with a simple example, let’s start with booleans:data Bool : Set where true : Bool false : Boolif : (b : Bool) (P : Bool -> Set) -> P true -> P false -> P bif true P t f = tif false P t f = fnot : Bool -> Boolnot a = if a (λ x → Bool) false trueand : Bool -> Bool -> Booland a b = if a (λ a → Bool) b falseor : Bool -> Bool -> Boolor a b = if a (λ a → Bool) true bThis Agda program declares: 1.

a new datatype, Bool; 2.

its elimination principle, if; 3.

a function using it.

Here is how the same program is translated to Formality:.

Bool: Type= $self {-P : {:Bool} Type} {true : (P true)} {false : (P false)} (P self).

true: Bool= @Bool [-P] [t] [f] t.

false: Bool= @Bool [-P] [t] [f] f.

if: {a : Bool} {-P : {:Bool} Type} {:(P true)} {:(P false)} (P a)= [a] ~a.

not: {a : Bool} Bool= [a] (if a -[a]Bool false true).

or : {a : Bool} {b : Bool} Bool= [a] [b] (if a -[a]Bool true b).

and : {a : Bool} {b : Bool} Bool= [a] [b] (if a -[a]Bool b false).

main (not true)The first thing to note is that, instead of defining Bool, true and false in a terse, 3-line data statement, we needed to define each one separately, in a total of 13 non-empty lines of code.

The first thing we did here is define the type Bool.

Notice how similar it is to Agda’s if?.That’s because Formality datatypes are simply Agda’s elimination principles for that datatype, except with self used on the first and last lines!.I could elaborate on this, but I honestly think studying this example is the best way to grasp it.

So, spend some time on it until this makes sense to you!.Things worth noting:The lambda binding -P is erased to avoid unnecessary runtime costs.

Both true and false must be declared explicitly because, unlike Agda’s native data syntax, our Bool definition won’t automatically define them.

$self … is used to define an inductive datatype T, and @T .

is used to instantiate each of its constructors.

The type of Bool refers to true, which refers to Bool, in a “mutually recursive” fashion.

This is clearly necessary, because inductive datatypes are defined as their own elimination principles, which refer to their constructors, which are members of those types, and so on!.Yet, this kind of type-level recursion isn’t capable of causing infinite loops because, remember, Formality’s termination proof doesn’t rely on types.

We give an explicit annotation to all the terms because, due to the cyclic dependency above, Formality wouldn’t be able to infer their types.

Once that makes sense to you, the rest is straightforward.

Since datatypes are encoded as their elimination principles, in order to get them you must just eliminate their self types with a ~, which can be seen on the body of if.

After the bureaucracy of defining a new datatype is complete, functions that operate on them are basically direct, syntactical translation of their Agda counterparts!.You can test this program with formality -inN main:Type:BoolNorm (interpreted):[t] [f] fThe fact it display no error messages means our program is well-typed.

Try replacing (not true) by, for example, (not not) and see what happens.

For completion sake, here is how a dependent pair type looks like:data Sigma (A : Set) (B : A → Set) : Set where sigma : (a : A) (b : B a) → Sigma A BBecomes:.

Sigma [A : Type] [B : {a : A} Type]: Type= $self {-P : {:(Sigma A B)} Type} {pair : {a : A} {b : (B a)} (P (sigma -A -B a b))} (P self).

sigma [-A : Type] [-B : {a : A} Type]: {a : A} {b : (B a)} (Sigma A B)= [a] [b] @(Sigma A B) [-P] [pair] (pair a b)While this looks complex, it isn’t.

Again, the Formality version is exactly the elimination principle of the Agda’s counterpart, except with self used on the first and last line, and refl defined explicitly.

We can easily get the Formality version by writing down Agda’s elim and manually porting it!4b.

Simple proofs (DeMorgan’s theorem)The coolest thing about proof languages is that their type systems are capable of enforcing and checking static invariants about their programs.

Let’s translate Agda’s propositional equality type to Formality:data Eq (T : Set) (a : T) : (b : T) → Set where refl : Eq T a aBecomes:.

Eq: {T : Type} {a : T} {b : T} Type= [T] [a] [b] $self {-Prop : {b : T} {self : (Eq T a b)} Type} {refl : (Prop a (refl -T -a))} (Prop b self).

refl: {-T : Type} {-a : T} (Eq T a a)= [-T] [-a] @(Eq T a a) [-Prop] [refl] reflThis can be ported using the same technique as above.

But what about proofs?.Can we also easily port them too?.Of course!.Here is DeMorgan’s theorem:DeMorgan : (a : Bool) (b : Bool) → SetDeMorgan a b = Eq Bool (not (and a b)) (or (not a) (not b))de-morgan : (a : Bool) (b : Bool) → DeMorgan a bde-morgan a b = if a (λ a → DeMorgan a b) (refl {T = Bool} {a = if b (λ _ → Bool) false true}) (refl {T = Bool} {a = true})Translating to Formality, we get:.

DeMorgan: {a : Bool} {b : Bool} Type= [a] [b] (Eq Bool (not (and a b)) (or (not a) (not b))).

de_morgan: {a : Bool} {b : Bool} (DeMorgan a b)= [a] [b] (~a -[a](DeMorgan a b) (refl -Bool -(not b)) (refl -Bool -true)).

main de_morganOf course, I wrote the Agda proof in a shape that simplified the manual translation, but, other than that, the translation was straightforward.

You can test this program with formality -inN main, which outputs:Type:{a : Bool} {b : Bool} (DeMorgan a b)Norm (interpreted):[a] [b] (a [refl] refl [refl] refl)Once again, the fact we see no type errors means our program is well-typed an, in this case, that our theorem is correct!.As an exercise, try proving something incorrect such as Eq Bool (and a b) (or (not a) (not b)).

But wait, if all I’ve done in Formality so far was port Agda proofs, what is the point?.The point is, once again, all of that is checked in an extremely portable language that is itself implemented in ~1000 LOC, and designed in a way that is suitable for efficient, parallel compilations.

That is the magic of Formality!Now, for what kind of programs this works?.Can we port absolutely any Agda proof to Formality just like that?. More details

Leave a Reply