=Paper=
{{Paper
|id=Vol-1454/ramics15-st_15-22
|storemode=property
|title=Relational Equality in the Intensional Theory of Types
|pdfUrl=https://ceur-ws.org/Vol-1454/ramics15-st_15-22.pdf
|volume=Vol-1454
}}
==Relational Equality in the Intensional Theory of Types==
https://ceur-ws.org/Vol-1454/ramics15-st_15-22.pdf
Relational Equality in the Intensional Theory of
Types
Victor Cacciari Miraldo
University of Minho
University of Utrecht
1 Introduction
Relational Algebra [BdM97] has already proven to be a very expressive for-
malism for calculating with programs. In particular, relational shrinking can be
used to derive a program as an optimization of its specification [MO12]. Nev-
ertheless, there is still lack of computer support for relational calculus. Our ap-
proach is basically piggybacking on Agda[Nor09], an emerging language with a
dependent type system, instead of building such a support system from scratch.
Agda has a series of features that make it a very interesting target for such sys-
tem. One such feature is being able to define mix-fix operators, from where
its Equational Reasoning framework arises. This framework can be modified to
closely resemble what a squiggolist would write on paper.
The task of encoding Relational Algebra in Martin-Löf’s theory of types
[ML84], however, is not as straightforward as one might think. There exists
two separate efforts in such a direction. One is due to Mu et al., where a library
targeted at program refinement is presented [MKJ09]; the other, more general
approach, is due to Kahl [Kah14] and provides a complete categorical library
for Agda, where the category of relations arises as a specific instantiation. Our
goal is somewhat different, making both approaches unsuitable for us.
This student-track paper will focus on the difficulties we encountered when
encoding relational equality in Agda in way suitable for (automatic) rewriting.
We start with a (very) small introduction to Agda, section 2, aimed at readers
without any Agda background whatsoever. We, then, explain how to perform
syntactical rewrites in Agda, section 3. This should give a fair understanding of
whats going to happen on sections 4, 5 and 6. Where we explain the encoding
of relations, more specifically relational equality, in Agda and introduces some
concepts from Homotopy Type Theory that allows one to fully formalize our
model. We conclude on section 7 providing a summary of what was done and
an example that illustrates the application of the tool we developed.
2 Agda Basics
In languages such as Haskell or ML, where a Hindley-Milner based algorithm
is used for type-checking, values and types are clearly separated. Values are the
objects being computed and types are simply tags to categorize them. In Agda,
16 V.C. Miraldo
however, this story changes. There is no distinction between types and values,
which gives a whole new level of expressiveness to the programmer.
The Agda language is based on the intensional theory of types by Martin-
Löf [ML84]. Great advantages arise from doing so, more specifically in the
programs-as-proofs mindset. Within the Intensional Theory of Types, we gain
the ability to formally state the meaning of quantifiers in a type. We refer the
interested reader to [NPS90].
Datatype definitions in Agda resemble Haskell’s GADTs syntax [VWPJ06].
Let us illustrate the language by defining fixed-size Vectors. For this, we need
natural numbers and a notion of sum first.
data Nat : Set where + : Nat → Nat → Nat
Z : Nat Z +n = n
S : Nat → Nat (S m) + n = S (m + n)
The Nat : Set statement is read as Nat is of kind ∗, for the Haskell enthusiast.
In a nutshell, Set, or, Set0 , is the first universe, the type of small types. For
consistency reasons, Agda has an infinite number of non-cumulative universes
inside one another. That is, Seti * Seti but Seti ⊆ Seti+1 .
The underscores in the definition of + indicate where each parameter goes.
This is how we define mix-fix operators. We can use underscores virtually any-
where in a declaration, as long as the number of underscores coincide with the
number of parameters the function expects.
Leaving details aside, and jumping to Vectors, the following a possible dec-
laration of fixed-size vectors in Agda.
data Vec (A : Set) : Nat → Set where
Nil : Vec Z
Cons : A → Vec A n → Vec A (S n)
Here we can already see something different from Nat. The type Vec takes
one parameter, which must be a small type, we called it A and it is indexed by
a natural number. Given an A : Set, Vec A has kind N at → ∗. This correctly
models the idea of an inductive type family. For every natural number n, there
is one type Vec A n.
Intuitively, if we concatenate a Vec A n to a Vec A m, we will obtain a
Vec A (n + m). This is exactly how vector concatenation goes in Agda.
++ : {A : Set } {n m : Nat } → Vec A n → Vec A m → Vec A (n + m)
Nil ++ v = v
(Cons a as) +
+ v = Cons a (as + + v)
The parameters enclosed in curly brackets are known as implicit parameters.
These are values that the compiler can figure out during type-checking, so we
need not to worry.
Relational Equality in the Intensional Theory of Types 17
3 Rewriting in Agda
The steps of mathematical reasoning one usually writes on a paper have a fair
amount of implicit rewrites. Yet, we cannot skip these steps in a proof assistant.
We need to really convince Agda that two things are equal, by Agda’s equality
notion, before it can rewrite.
In Agda, writing x ≡ y means that x and y evaluate to the same value. This
can be seen from the definition of propositional equality, where we only allow
one to construct an equality type using reflexivity:
data ≡ {A : Set } (x : A) : A → Set where
refl : x ≡ x
Having a proof p : x ≡ y convinces Agda that x and y will evaluate to the
same value. Whenever this is the case, we can rewrite x for y in a predicate. The
canonical way to do so is using the subst function:
subst : {A : Set } (P : A → Set) {x y : A} → x ≡ y → P x → P y
subst P refl p = p
Here, the predicate P can be seen as a context where the rewrite will hap-
pen. From a programming point of view, Agda’s equality notion makes perfect
sense! Yet, whenever we are working with more abstract concepts, we might
need a finer notion of equality. However, this new equality must agree with
Agda’s equality if we wish to perform syntactical rewrites. As we will see in
the next section, this is not always the case.
It is worth mentioning a subtle detail on the definition of subst. Note that, on
the left hand side, the pattern p has type P x , according to the type signature.
Still, Agda accepts this same p to finish up the proof of P y. What happens
here is that upon pattern matching on refl , Agda knows that x and y evaluate
to the same value. Therefore it basically substitutes, in the current goal, every y
for x . As we can see here, pattern-matching in Agda actually allows it to infer
additional information during type-checking.
4 Relations and Equality in Agda
In order to have a Relational Reasoning framework, we first need to have rela-
tions. We follow the same powerset encoding of [MKJ09], and encode a subset
of a given set by:
P : Set → Set1
P A = A → Set
18 V.C. Miraldo
In Agda, Set is the type of types, which allows us to encode a subset of a set
A as a function f : P A. Such subset is defined by {a ∈ A | f a is inhabited}.
R
A simple calculation will let one infer B ← − A = B → A → Set from
P (A × B ). The subrelation notion is intuitively defined by:
R S
⊆ : {A B : Set } → (B ←
− A) → (B ←
− A) → Set
R ⊆ S = ∀ab → Rba → S ba
R
This makes sense because we are saying that B ←
− A is a subrelation of
S
B← − A whenever the set R b a being inhabited implies that the set S b a is also
inhabited, for all b a. For this matter, a set S being inhabited means that there
exist some s : S. This follows from the inclusion of (mathematical) sets.
The relation ⊆ is an order: it is reflexive, transitive and anti-symmetric. Re-
flexivity and transitivity are straight-forward to prove, but there is a catch in
anti-symmetry. Remember that relational equality is defined by mutual inclu-
sion:
R S
≡r : {A B : Set } → (B ←
− A) → (B ←
− A) → Set
R ≡r S = R ⊆ S × S ⊆ R
On paper, anti-symmetry follows by construction. But for rewriting purposes
in Agda, we need to find a way to prove R ≡ S from R ≡r S . Unfortunately,
this is not possible without additional machinery. We would like to have:
∀ab → Rba → S ba
∀ab → S ba → Rba ≡r promote
R ≡ S
We could postulate function extensionality1 and, if the functions are isomor-
phisms, this would finish the proof. But this is somewhat cheating. By pin-
pointing the problem one can give a better shot at solving it.
Well, if R ≡ S , then R b a ≡ S b a at least propositionally. On the other
hand, if R ≡r S then we might have propositionally different relations. Con-
sider the following relations (where 1 is the unit type and + is the coproduct).
Top : Rel N N Top 0 : Rel N N
Top = 1 Top 0 = 1+1
Although they are equivalent, it is clear that Top b a = 1 6≡ 1 + 1 =
Top 0 b a. To prove propositional equality from relational equality we depend
1
Function extensionality is expressed by point-wise equality. It is known not to intro-
duce any inconsistency and it is considered to be a safe postulate. In short, given
f , g : A → B , f ≡ g only if ∀ x → f x ≡ g x .
Relational Equality in the Intensional Theory of Types 19
on the user not making stupid decisions. We are thus facing a subtle encoding
problem.
5 Homotopy Type Theory
Luckily people from the Univalent Foundations have thought of this problem.
In this section we will borrow a few concepts from Homotopy Type Theory
[Uni13] (HoTT) and discuss how these concepts can contribute to a solution for
our encoding. There is no final solution, though, since they will boil down to
design decisions.
Recalling our problem, given R ≡r S , R b a and S b a might evaluate to
different types. But we do not care to which values they evaluate to, as long as
one is inhabited iff the other is so. This notion is called proof-irrelevance in HoTT
jargon, and the sets which are proof irrelevant are called mere propositions.
isProp : Set → Set
isProp P = (p1 p1 : P ) → p1 ≡ p2
Let us denote the set of all proof irrelevant types, or (Σ Set isP rop), by MP.
Should we have defined our relations as B → A → MP, our problem
would be almost done. The drawback of such a decision is the evident loss of
expressiveness, for instance, coproducts are already not proof-irrelevant. Not
to mention that users would have to be familiar with such notions before en-
coding their relations. We chose to encode this as a typeclass and, for using a
fully formal definition of anti-symmetry, both relations must belong into that
typeclass.
There is a very useful result we exploit. Given P a mere proposition. If we
find an inhabitant p : P , then P ≈ 1. If we find a contradiction P → ⊥,
then P ≈ ⊥, where ≈ means univalence. For the unfamiliar reader, univalence
can be thought of as some sort of isomorphism. The concept is too deep to be
introduced in detail here. We refer the reader to [Uni13].
6 Anti-Symmetry of Relational Inclusion
Being a mere proposition is of no interest if we cannot compute the set R a b,
for a given R , a and b. Yet, we can also make this explicit in Agda, by means of
another typeclass. We require our relations to be decidable.
R
isDec : {A B : Set } (B ←
− A) → Set
isDec R = (a : A) (b : B ) → (R b a) + (R b a → ⊥)
On these terms, together with function extensionality, we are able to provide
a proof of anti-symmetry in Agda’s terms. The type2 is:
2
The double braces {{ }} work almost like Haskell’s type context syntax (F a) ⇒.
20 V.C. Miraldo
⊆ −antisym : {A B : Set } {R S : Rel A B }
{{decr : IsDec R }} {{decs : IsDec S }}
{{prpr : IsProp R }} {{prps : IsProp S }}
→ R ⊆ S → S ⊆ R → R ≡ S
Yet, this model of anti-symmetry is too restrictive for the user. During de-
velopment, base relations might change, which will trigger changes in all of
their instances. For this reason, we provide a postulate of the ≡r -promote rule
introduced in section 4. Note, however, that this postulate allows for a contra-
diction. It is easy to see why. Take the Top and Top 0 relations defined in section
4. It is easy to prove Top ≡r Top 0 , therefore, through ≡r -promote we have
Top ≡ Top 0 , but 1 6≡ 1 + 1, and, through cong (const ◦ const), we have
λ → 1 6≡ λ → 1 + 1. Therefore, Top 6≡ Top 0 . The actual Agda code
for this is trickier than one thinks, hence it is omitted here.
This is not inconsistent with our model, however. Since the definition of a
relation is basically the encoding of its defining predicate in Agda, one should
not need to use Sets which are not mere propositions. The ≡r -promote pos-
tulate is there to speed up development. As we proved in this section (more
details on [Mir15]), if we use decidable mere-propositions in the domain of our
relations, no inconsistency arises. The coproduct is not a mere-proposition.
7 Summary and Conclusions
On this very short paper we presented the problem of encoding relational equal-
ity in Agda, and gave a few pointers on how to tackle it. This is just a short
summary of [Mir15], where we present our library in full. We provide standard
relational constructs, including a prototype of catamorphisms, generic on their
functor. Our encoding uses W-types and is built on top of [AAG04]. We had to
build all of these constructs from scratch, since we had the goal of also provid-
ing automatic inference of rewriting context for them, which we accomplished.
The full Agda code of our relational algebra library, together with the author’s
master dissertation is available on GitHub.
https://github.com/VictorCMiraldo/msc-agda-tactics
It is arguable that we did not really solve the problem, since our final so-
lution still relies on the univalence axiom (a ≈ b → a ≡ b [Uni13]). We
reiterate that there is no final solution to this problem, since different options
will lead to libraries with different designs, fit for different purposes.
Here we give a small example of the final product of this project, and how
we use the lifting of relational equality to perform generic (automatic) rewrites
in Agda. Note that Agda’s mix-fix feature allows one to define operators such
as the squiggol environment. The example below is one branch of the proof that
Lists are functors. The by function was also developed by us, and it uses the
Relational Equality in the Intensional Theory of Types 21
Reflection mechanism of Agda (similar to Template Haskell) to infer the substi-
tution to be performed.
The rewrites we perform are just substs, as explained in section 3. The au-
tomation happens on compile time. The tactic keyword gives us the meta-representation
of the relevant terms, our engine then generates a meta-representation of the
subst that justifies the rewrite step, which is then plugged back in before the
compiler resumes type-checking. It is very relevant to state that, although the
lemmas justifying the rewrite steps have a ≡r as their type, this is then con-
verted to Agda’s ≡ in order for us to use subst. Relational equality is not substi-
tutive, in general.
Let us imagine we are in doubt whether lists are a functor or not. A good
start is if they distribute over composition, that is,
L (f · g) ≡ L f · L g
The proof itself is simple to complete with the universal law for coproducts. We
illustrate the i2 branch in Agda, using our library.
ex : (Id + (Id × R) ◦ Id + (Id × S )) ◦ i2 ≡r i2 ◦ Id × (R ◦ S )
ex = begin
(Id + (Id × R) ◦ Id + (Id × S )) ◦ i2
≡r { tactic (by (quote +-bi-functor)) }
(Id ◦ Id ) + (Id × R ◦ Id × S ) ◦ i2
≡r { tactic (by (quote i2 -natural)) }
i2 ◦ Id × R ◦ Id × S
≡r { tactic (by (quote ×-bi-functor)) }
i2 ◦ (Id ◦ Id ) × (R ◦ S )
≡r { tactic (by (quote ◦-id-r)) }
i2 ◦ Id × (R ◦ S )
References
[AAG04] Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Representing nested
inductive types using w-types. In In Automata, Languages and Programming,
31st International Colloqium (ICALP), pages 59 71, pages 59–71, 2004.
[BdM97] R. Bird and O. de Moor. Algebra of Programming. Prentice-Hall international
series in computer science. Prentice Hall, 1997.
[Kah14] W. Kahl. Rath-agda, relational algebraic theories in agda, Dez 2014.
[Mir15] Victor Cacciari Miraldo. Proofs by rewriting in Agda. Master’s thesis, Utrecht
University and University of Minho, 2015. Submitted.
22 V.C. Miraldo
[MKJ09] S-C. Mu, H-S. Ko, and P. Jansson. Algebra of programming in agda. Journal of
Functional Programming, 2009.
[ML84] P. Martin-Löf. Intuitionistic type theory, 1984.
[MO12] Shin-Cheng Mu and Jos Nuno Oliveira. Programming from galois connec-
tions. The Journal of Logic and Algebraic Programming, 81(6):680 – 704, 2012. 12th
International Conference on Relational and Algebraic Methods in Computer
Science (RAMiCS 2011).
[Nor09] Ulf Norell. Dependently typed programming in agda. In Proceedings of the 4th
International Workshop on Types in Language Design and Implementation, TLDI
’09, pages 1–2, New York, NY, USA, 2009. ACM.
[NPS90] Bengt Nordström, Kent Petersson, and Jan Smith. Programming in Martin-Löf’s
Type Theory. Oxford University Press, 1990.
[Uni13] The Univalent Foundations Program. Homotopy Type Theory: Univalent Founda-
tions of Mathematics. http://homotopytypetheory.org/book, Institute for Ad-
vanced Study, 2013.
[VWPJ06] Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Boxy types:
Inference for higher-rank types and impredicativity. SIGPLAN Not., 41(9):251–
262, September 2006.