[Agda] Re: Builtins

[Kirill Elagin]

On Sat, Apr 25, 2015 at 1:19 PM N. Raghavendra <raghu at hri.res.in> wrote:

> Does it mean that if I don't use rewrite and
> primTrustMe, I don't need to put the instructions
>
> {-# BUILTIN EQUALITY _≡_ #-}
> {-# BUILTIN REFL refl #-}
>
> in my file?


Yes.


> Also, what's the relation between the "builtin equality"
> and "judgemental equality"?
>

“Judgmental equality” is the computational one, that is, two terms are
judgmentally equal iff they are equal up to reductions (which are built
into Agda or any other type system), or, to be more precise, they are in
the same equivalence class of the reflexive, symmetric, transitive closure
of all the reduction rules. Basically, this means, they have the same
normal form.

“Propositional equality” generally refers to the equality you define
yourself.

The `BUILTIN` pragma is a way to hook your definitions into Agda’s internal
mechanisms. E.g. the `rewrite` syntax rewrites goals relative to some
notion of equality and using the `EQUALITY` builtin you tell Agda which
notion of equality to use.
As you can see on the [page which gives examples of `rewrite`](
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching),
Agda basically expands the `rewrite` syntax into something boring and
tedious to write by hand, but it needs to use `refl` there. What is `refl`
in that case? The answer is that it is whatever you specify as the `REFL`
builtin.

Your notion of “equality” can be as absurd as you want. Unless you want to
use it with the `rewrite` syntax. The fact that the judgmental equality
implies a propositional one says exactly that the propositional equality in
question is reflexive (as _everything_ in type theory is up to judgmental
equality). Now, for the `EQUALITY` builtin you give a type constructor with
two arguments and Agda expects the `REFL` builtin to have one argument `a`
and to return a proof of `a == a` (where `_==_` is whatever you called
`EQUALITY`). So `REFL` has to be a proof that your equality is reflexive
or, which is the same, that it is implied by the judgmental equality.

I’m not really sure what will happen if you define `EQUALITY` to be
something non-symmetric or non-transitive but I believe this should be fine.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150425/21bc488e/attachment.html