[Agda] The joys and sorrows of abstraction

[Philip Wadler]

Dear Agda mailing list,

I am defining substitution on possibly open terms, and therefore need a way
to generate fresh variable names. The operation

fresh x xs

returns a name that is similar to x but does not appear in the list xs,
where similar means that it may have extra primes at the end. For example,

fresh "x" [ "x" , "x′" , "x′′" , "y" ] ≡ "x′′′"

To define `fresh`, I start by defining operations on identifiers and
corresponding lemmas including the following:

make : Prefix → ℕ → Id
prefix : Id → Prefix
suffix : Id → ℕ

prefix-lemma : ∀ {p n} → prefix (make p n) ≡ p
suffix-lemma : ∀ {p n} → suffix (make p n) ≡ n
make-lemma : ∀ {x} → make (prefix x) (suffix x) ≡ x

Prefix is defined to be a String that does not end in a prime.

The definitions of make, prefix, and suffix are quite involved, so in order
to prevent them expanding to unreadable length in proofs I have made them
and the corresponding lemmas abstract. Doing so, the proof was fairly easy
to complete. However, because the definitions are abstract, Agda cannot
actually compute fresh variables as in the example above.

That's ok. Having completed the proofs with readable terms, I should be
able to now remove the abstract declaration. Since everything typechecked
before, revealing the definition bodies should preserve types. But in fact,
Agda now complains about one of the key proofs!

Is there any way to *both* be able to compute fresh names *and* retain my
related proofs, in particular, the proof that `fresh x xs` generates a name
not in `xs`?

The relevant files are attached, or can be found at

https://github.com/wenkokke/sf

Thank you for your help! Cheers, -- P


. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

[Wolfram Kahl]

Post by Philip Wadler
The definitions of make, prefix, and suffix are quite involved, so in order
to prevent them expanding to unreadable length in proofs I have made them
and the corresponding lemmas abstract.

You could try to make them module parameters instead,
and later supply the implementation where needed.


Wolfram

[Nils Anders Danielsson]

Post by Philip Wadler
Is there any way to *both* be able to compute fresh names *and* retain
my related proofs, in particular, the proof that `fresh x xs`
generates a name not in `xs`?

When normalising an expression you can make abstract definitions compute
by using C-u C-c C-n instead of C-c C-n. However, there is no way to
turn off abstract while type-checking (because this could lead to
problems with subject reduction).

There are other ways to control reduction. Wolfram suggested one.
Another is to match on a value of the unit type, and not supply a
concrete constructor until you want the code to compute.

[Philip Wadler]

Thank you to Wolfram and Nils!

Wolfram's suggestion worked!

Nils's suggestions C-u C-c C-n is great for testing, but doesn't help if I
want to document the results of the test in the file. I'm writing a
textbook, so including examples in the file is important! It would also be
important if one wanted to include tests for documentation and reliability.

Nils's suggestion to disable reduction with () is neat, but possibly not
the best pedagogy for a textbook.

However, there is no way to

Post by Nils Anders Danielsson
turn off abstract while type-checking (because this could lead to
problems with subject reduction).

So, I have an equality that is proved under abstraction, that fails when
the abstraction is removed. Isn't that also a failure of subject reduction,
or stability under substitution, or some other important property that we
care about?

Cheers, -- P




. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Nils Anders Danielsson

Post by Philip Wadler
Is there any way to *both* be able to compute fresh names *and* retain
my related proofs, in particular, the proof that `fresh x xs`
generates a name not in `xs`?

When normalising an expression you can make abstract definitions compute
by using C-u C-c C-n instead of C-c C-n. However, there is no way to
turn off abstract while type-checking (because this could lead to
problems with subject reduction).
There are other ways to control reduction. Wolfram suggested one.
Another is to match on a value of the unit type, and not supply a
concrete constructor until you want the code to compute.
--
/NAD

[Nils Anders Danielsson]

Post by Philip Wadler
So, I have an equality that is proved under abstraction, that fails
when the abstraction is removed. Isn't that also a failure of subject
reduction, or stability under substitution, or some other important
property that we care about?

Do you really have code of the form

abstract

<code>

that fails (ignoring resources) if abstract is removed?

I would not be surprised to see code of the following form fail when
abstract is removed:

abstract

<code>

<code>

However, this seems less problematic to me. Type-checking involves
computation, and when you remove abstract you change the computational
behaviour of the code.

[Philip Wadler]

Thanks for following up. It is the latter case. But I don't understand why
it should be ok for that to fail. Removing abstract should just replace
some abstract terms by their concretions, which have already been type
checked. Everything that was provably equal before should still be equal,
so why is it ok for the proof of equality to now fail? Doesn't this violate
stability under substitution? Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Nils Anders Danielsson

Post by Philip Wadler
So, I have an equality that is proved under abstraction, that fails
when the abstraction is removed. Isn't that also a failure of subject
reduction, or stability under substitution, or some other important
property that we care about?

Do you really have code of the form
abstract
<code>
that fails (ignoring resources) if abstract is removed?
I would not be surprised to see code of the following form fail when
abstract
<code>
<code>
However, this seems less problematic to me. Type-checking involves
computation, and when you remove abstract you change the computational
behaviour of the code.
--
/NAD

[Martin Escardo]

Post by Philip Wadler
Thanks for following up. It is the latter case. But I don't understand
why it should be ok for that to fail. Removing abstract should just
replace some abstract terms by their concretions, which have already
been type checked. Everything that was provably equal before should
still be equal, so why is it ok for the proof of equality to now fail?
Doesn't this violate stability under substitution? Cheers, -- P

It is because of things such as this that I prefer to restrict my usage
of Agda to a fragment corresponding to a well-understood type theory.

This may be limiting in terms of expressivity, conciseness, and
efficiency, but at least one can tell whether something is a bug or not,
rather than a bug or a feature.

:-)
Martin

[Philip Wadler]

Thanks, Martin. So which fragment do you recommend? Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Philip Wadler
Thanks for following up. It is the latter case. But I don't understand
why it should be ok for that to fail. Removing abstract should just replace
some abstract terms by their concretions, which have already been type
checked. Everything that was provably equal before should still be equal,
so why is it ok for the proof of equality to now fail? Doesn't this violate
stability under substitution? Cheers, -- P

It is because of things such as this that I prefer to restrict my usage of
Agda to a fragment corresponding to a well-understood type theory.
This may be limiting in terms of expressivity, conciseness, and
efficiency, but at least one can tell whether something is a bug or not,
rather than a bug or a feature.
:-)
Martin

[Ulf Norell]

In your case the reason the proof fails without `abstract` is that the
`rewrite` doesn't trigger.
Here's a simpler example exhibiting the same behaviour:

module _ where

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

module WithAbstract where

abstract
f : Nat → Nat
f zero = zero
f (suc n) = suc (f n)

lem : ∀ n → f n ≡ n
lem zero = refl
lem (suc n) rewrite lem n = refl

thm : ∀ m n → f (suc m) + n ≡ suc (m + n)
thm m n rewrite lem (suc m) = refl
-- Works.

module WithoutAbstract where

f : Nat → Nat
f zero = zero
f (suc n) = suc (f n)

lem : ∀ n → f n ≡ n
lem zero = refl
lem (suc n) rewrite lem n = refl

thm : ∀ m n → f (suc m) + n ≡ suc (m + n)
thm m n rewrite lem (suc m) = refl
-- Fails since rewrite doesn't trigger:
-- lem (suc m) : suc (f m) ≡ suc m
-- goal : suc (f m + n) ≡ suc (m + n)

In general I think it's optimistic to expect tactics (of which rewrite is
an example) to be stable under substitution.

/ Ulf

Post by Philip Wadler
Thanks, Martin. So which fragment do you recommend? Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Martin Escardo

Post by Philip Wadler
Thanks for following up. It is the latter case. But I don't understand
why it should be ok for that to fail. Removing abstract should just replace
some abstract terms by their concretions, which have already been type
checked. Everything that was provably equal before should still be equal,
so why is it ok for the proof of equality to now fail? Doesn't this violate
stability under substitution? Cheers, -- P

It is because of things such as this that I prefer to restrict my usage
of Agda to a fragment corresponding to a well-understood type theory.
This may be limiting in terms of expressivity, conciseness, and
efficiency, but at least one can tell whether something is a bug or not,
rather than a bug or a feature.
:-)
Martin

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Philip Wadler]

Ulf,

Thank you for taking the time to produce your simple example. Indeed, that
makes it clear why stability under substitution may be too much to hope for.

Martin,

Thank you for sketching your preferred subset. I must admit that 'with' and
implicits are two of my favourite features. In place of `with`, do you
simply use auxiliary functions? I thought that `with` and auxiliary
functions were meant to be equivalent?

Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Ulf Norell
In your case the reason the proof fails without `abstract` is that the
`rewrite` doesn't trigger.
module _ where
open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
module WithAbstract where
abstract
f : Nat → Nat
f zero = zero
f (suc n) = suc (f n)
lem : ∀ n → f n ≡ n
lem zero = refl
lem (suc n) rewrite lem n = refl
thm : ∀ m n → f (suc m) + n ≡ suc (m + n)
thm m n rewrite lem (suc m) = refl
-- Works.
module WithoutAbstract where
f : Nat → Nat
f zero = zero
f (suc n) = suc (f n)
lem : ∀ n → f n ≡ n
lem zero = refl
lem (suc n) rewrite lem n = refl
thm : ∀ m n → f (suc m) + n ≡ suc (m + n)
thm m n rewrite lem (suc m) = refl
-- lem (suc m) : suc (f m) ≡ suc m
-- goal : suc (f m + n) ≡ suc (m + n)
In general I think it's optimistic to expect tactics (of which rewrite is
an example) to be stable under substitution.
/ Ulf

Post by Philip Wadler
Thanks, Martin. So which fragment do you recommend? Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Martin Escardo

Post by Philip Wadler
Thanks for following up. It is the latter case. But I don't understand
why it should be ok for that to fail. Removing abstract should just replace
some abstract terms by their concretions, which have already been type
checked. Everything that was provably equal before should still be equal,
so why is it ok for the proof of equality to now fail? Doesn't this violate
stability under substitution? Cheers, -- P

It is because of things such as this that I prefer to restrict my usage
of Agda to a fragment corresponding to a well-understood type theory.
This may be limiting in terms of expressivity, conciseness, and
efficiency, but at least one can tell whether something is a bug or not,
rather than a bug or a feature.
:-)
Martin

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Martin Escardo]

Post by Jesper Cockx
Martin,
Thank you for sketching your preferred subset. I must admit that 'with'
and implicits are two of my favourite features. In place of `with`, do
you simply use auxiliary functions? I thought that `with` and auxiliary
functions were meant to be equivalent?

I forgot to say that I also use Agda to communicate mathematics to
fellow researchers that know type theory but not necessarily Agda.

Because the meaning of "with" is not obvious and self-explanatory, it
doesn't work for this purpose.

One good thing about Agda is that it can be very readable, if you write
well.

Martin

[Andreas Abel]

(The co-patterns of Andreas et al are also very good for making
readable definitions; I’m not so sure if they have firm foundations —
pardon my ignorance.)

Andy,

concerning foundations of copattern matching, there is a forthcoming
ICFP paper by Jesper Cockx and me

http://www.cse.chalmers.se/~abela/lhs-checking-submitted.pdf

that describes the transformation of dependent copattern matching into
case trees.

The second step, going from case trees to "introducers" for coinductive
types hasn't been formally described. This would require a description
of productivity checking without sized types. The foundational question
for sized types has not been fully settled for dependent types, but see
my work on non-dependent types...

Best,
Andreas

Post by Martin Escardo
One good thing about Agda is that it can be very readable, if you write
well.

For me this aspect of Agda is very important and why I have ended up
using it. Access to dependent pattern matching is a crucial part of
what makes it so nice. And even if Agda does not do it that way for
historical reasons, we do apparently have a good account of
elaborating such patterms to elimation combinators. (From what I
understand, this is used by Lean to translate code with patterns back
into its core type theory.)
(The co-patterns of Andreas et al are also very good for making
readable definitions; I’m not so sure if they have firm foundations —
pardon my ignorance.)
Andy
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Matthieu Sozeau]

Hi,

I know in Coq and Matita for example, equipping the core term
representation with general explicit substitutions was tried and found to
be a performance bottleneck, for conversion in particular, and not the
converse, sadly. But Coq does still use some explicit/delayed substitution
representation in its “efficient” reduction abstract machine.

Best,
— Matthieu

Or is there some reason why solid foundations and practical

implementations

should not coincide?

This is the right question.
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Apostolis Xekoukoulotakis]

This is really scary, for good reason. It seems that we are in a better
position now than a few years ago.

I do remember as an undergraduate, thinking that all I need is to start
from the fundamentals of Mathematics and then prove all of the rest.
Then , I found that the fundamentals were full of paradoxes.
https://en.wikipedia.org/wiki/Foundations_of_mathematics#Foundational_crisis

Post by Philip Wadler
Thanks, Martin. So which fragment do you recommend? Cheers, -- P

I can't recommend any fragment to you or anybody else. This is
because I don't know which type theories you understand well, and
because I don't know what you want to do with them (your research or
teaching interests).
I can tell you which fragments I work with, and why. I prefer to restrict
to fragments of Agda corresponding to well-understood Martin-Loef type
theories.
This is not for dogmatic reasons, but instead because my current research
involves them as the base for univalent mathematics, and I use Agda as tool
for this research.
I use Agda to write Martin-Loef type theory constructions (and usually for
spartan Martin-Loef type theories).
"With", instance arguments, "abstract", sized types, irrelevant fields,
among others, don't belong to the type theories I understand well, or that
people have precisely defined, or that have the blessing of the community
as finished things. So I don't use them, either because of ignorance or
lack of trust or lack of precise definition.
(I tried instance arguments, but then my code that compiled in one version
of Agda failed in the next, and because I never saw a convincing definition
of them, I decided to abandon them, as a non-reliable, non-stable feature.)
Moreover, I use the options --exact-split and --without-K. The former
because I would like to think that, even if I indulge in using
(well-founded) recursive definitions by pattern matching, my code should,
in principle, be automatically translatable to code that uses "Martin-Loef
combinators" only. The latter is because of my current particular field of
interest, which allows types that don't necessarily satisfy "uniqueness of
identity proofs".
As an exception, although I don't think implicit-argument resolution is
well defined (independently of the Agda implementation), I do use implicit
arguments, because they are very convenient. And I don't think they can
give rise to serious problems (although I faced a bug once). However, I
have observed, and reported, that sometimes new versions of Agda fail to
infer implicit arguments that were (correctly) inferred in previous
versions. It is a worry that 15000 lines of code may break in the future
because of changes in implicit argument resolution (that is, we are not
working in a well-defined, stable, type theory for implicit arguments).
I can say the same for pattern matching, as an exception, but this has
been ameliorated with the options --exact-split and --without-K, already
mentioned
Martin

Post by Philip Wadler
. \ Philip Wadler, Professor of Theoretical Computer Science, .
/\ School of Informatics, University of Edinburgh . / \ and Senior
Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/
Thanks for following up. It is the latter case. But I don't understand
why it should be ok for that to fail. Removing abstract
should just replace some abstract terms by their concretions, which
have already been type checked. Everything that was provably equal
before should still be equal, so why is it ok for the proof of
equality to now fail? Doesn't this violate stability under
substitution? Cheers, -- P
It is because of things such as this that I prefer to restrict my usage
of Agda to a fragment corresponding to a well-understood type theory.
This may be limiting in terms of expressivity, conciseness, and
efficiency, but at least one can tell whether something is a bug or not,
rather than a bug or a feature.
:-) Martin
The University of Edinburgh is a charitable body, registered in Scotland,
with registration number SC005336.

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Arseniy Alekseyev]

I'll point out that source-level stability under substitution is not even
compatible with implicit parameters if unsolved metavariables is also
something you care about.
For example the below program works with "abstract" and has unsolved
metavariables without "abstract".

data Bool : Set where
true false : Bool

abstract
or : Bool → Bool → Bool
or true _ = true
or false x = x

data Is-bool : Bool → Set where
is-bool : ∀ x → Is-bool x

contrived : ∀ {x} → Is-bool (or x true) → Bool
contrived {x} _ = x

z = contrived (is-bool (or false true))

Post by Apostolis Xekoukoulotakis
This is really scary, for good reason. It seems that we are in a better
position now than a few years ago.
I do remember as an undergraduate, thinking that all I need is to start
from the fundamentals of Mathematics and then prove all of the rest.
Then , I found that the fundamentals were full of paradoxes.
https://en.wikipedia.org/wiki/Foundations_of_mathematics#Fou
ndational_crisis

Agda is an incarnation of both established type theories and frontier
research on possible new type theories, and it is good that things are like
this, because researchers can use it for experimentation.
But some other researchers would like to use Agda to work with established
type theories.
It is good that Agda has some seat-belts such as --exact-split, --safe,
and --without-K, for that purpose.
Further seat-belts would be welcome.
The point I was making was not about scariness but about awareness. If you
use a feature beyond your type-theory expertise, consider whether this
feature is well established, but unknown to you, or something experimental
and perhaps not well-defined.
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Arseniy Alekseyev]

(and to be sure, [abstract] keyword is not the issue here: this manifests
no matter how you achieve abstraction: module parameter, lambda, whatever)

Post by Arseniy Alekseyev
I'll point out that source-level stability under substitution is not even
compatible with implicit parameters if unsolved metavariables is also
something you care about.
For example the below program works with "abstract" and has unsolved
metavariables without "abstract".
data Bool : Set where
true false : Bool
abstract
or : Bool → Bool → Bool
or true _ = true
or false x = x
data Is-bool : Bool → Set where
is-bool : ∀ x → Is-bool x
contrived : ∀ {x} → Is-bool (or x true) → Bool
contrived {x} _ = x
z = contrived (is-bool (or false true))

Post by Apostolis Xekoukoulotakis
This is really scary, for good reason. It seems that we are in a better
position now than a few years ago.
I do remember as an undergraduate, thinking that all I need is to start
from the fundamentals of Mathematics and then prove all of the rest.
Then , I found that the fundamentals were full of paradoxes.
https://en.wikipedia.org/wiki/Foundations_of_mathematics#Fou
ndational_crisis

Agda is an incarnation of both established type theories and frontier
research on possible new type theories, and it is good that things are like
this, because researchers can use it for experimentation.
But some other researchers would like to use Agda to work with
established type theories.
It is good that Agda has some seat-belts such as --exact-split, --safe,
and --without-K, for that purpose.
Further seat-belts would be welcome.
The point I was making was not about scariness but about awareness. If
you use a feature beyond your type-theory expertise, consider whether this
feature is well established, but unknown to you, or something experimental
and perhaps not well-defined.
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Jesper Cockx]

Hi Martin,

I can easily see why you'd want to limit yourself to such a subset of Agda,
and I hope we will be able to support this style of using Agda even better
in the future (e.g. having more flags to turn on/off specific features). At
the same time, I hope you also understand why we must keep pushing the
boundaries of what's possible in Agda, in the hope that one day these
'unsafe' features can also enter the divine realm of commonly accepted type
theory.

One thing I'm wondering is whether you make any use of mutual definitions
in your code, specifically inductive-recursive and inductive-inductive
definitions. These are often used for universe constructions and extend the
power of the type theory quite a bit, but Agda currently has no flags to
limit or disable them. Would people be interested in such a flag?

Also, if you have any other flags you would like to see, just let us know
and I promise we'll at least consider them seriously :)

-- Jesper

Post by Philip Wadler
Thanks, Martin. So which fragment do you recommend? Cheers, -- P

I can't recommend any fragment to you or anybody else. This is
because I don't know which type theories you understand well, and
because I don't know what you want to do with them (your research or
teaching interests).
I can tell you which fragments I work with, and why. I prefer to restrict
to fragments of Agda corresponding to well-understood Martin-Loef type
theories.
This is not for dogmatic reasons, but instead because my current research
involves them as the base for univalent mathematics, and I use Agda as tool
for this research.
I use Agda to write Martin-Loef type theory constructions (and usually for
spartan Martin-Loef type theories).
"With", instance arguments, "abstract", sized types, irrelevant fields,
among others, don't belong to the type theories I understand well, or that
people have precisely defined, or that have the blessing of the community
as finished things. So I don't use them, either because of ignorance or
lack of trust or lack of precise definition.
(I tried instance arguments, but then my code that compiled in one version
of Agda failed in the next, and because I never saw a convincing definition
of them, I decided to abandon them, as a non-reliable, non-stable feature.)
Moreover, I use the options --exact-split and --without-K. The former
because I would like to think that, even if I indulge in using
(well-founded) recursive definitions by pattern matching, my code should,
in principle, be automatically translatable to code that uses "Martin-Loef
combinators" only. The latter is because of my current particular field of
interest, which allows types that don't necessarily satisfy "uniqueness of
identity proofs".
As an exception, although I don't think implicit-argument resolution is
well defined (independently of the Agda implementation), I do use implicit
arguments, because they are very convenient. And I don't think they can
give rise to serious problems (although I faced a bug once). However, I
have observed, and reported, that sometimes new versions of Agda fail to
infer implicit arguments that were (correctly) inferred in previous
versions. It is a worry that 15000 lines of code may break in the future
because of changes in implicit argument resolution (that is, we are not
working in a well-defined, stable, type theory for implicit arguments).
I can say the same for pattern matching, as an exception, but this has
been ameliorated with the options --exact-split and --without-K, already
mentioned
Martin

Post by Philip Wadler
. \ Philip Wadler, Professor of Theoretical Computer Science, .
/\ School of Informatics, University of Edinburgh . / \ and Senior
Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/
Thanks for following up. It is the latter case. But I don't understand
why it should be ok for that to fail. Removing abstract
should just replace some abstract terms by their concretions, which
have already been type checked. Everything that was provably equal
before should still be equal, so why is it ok for the proof of
equality to now fail? Doesn't this violate stability under
substitution? Cheers, -- P
It is because of things such as this that I prefer to restrict my usage
of Agda to a fragment corresponding to a well-understood type theory.
This may be limiting in terms of expressivity, conciseness, and
efficiency, but at least one can tell whether something is a bug or not,
rather than a bug or a feature.
:-) Martin
The University of Edinburgh is a charitable body, registered in Scotland,
with registration number SC005336.

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Martin Escardo]

Post by Jesper Cockx
Hi Martin,
I can easily see why you'd want to limit yourself to such a subset of
Agda, and I hope we will be able to support this style of using Agda
even better in the future (e.g. having more flags to turn on/off
specific features). At the same time, I hope you also understand why we
must keep pushing the boundaries of what's possible in Agda, in the hope
that one day these 'unsafe' features can also enter the divine realm of
commonly accepted type theory.
One thing I'm wondering is whether you make any use of mutual
definitions in your code, specifically inductive-recursive and
inductive-inductive definitions. These are often used for universe
constructions and extend the power of the type theory quite a bit, but
Agda currently has no flags to limit or disable them. Would people be
interested in such a flag?
Also, if you have any other flags you would like to see, just let us
know and I promise we'll at least consider them seriously :)

Thanks, this is very kind of you. I have a lists of things I would like. :-)

But let me write this properly rather than as an immediate reaction now.

Martin

Post by Jesper Cockx
-- Jesper
On Wed, May 16, 2018 at 10:36 PM, Martin Escardo
Thanks, Martin. So which fragment do you recommend? Cheers, -- P
I can't recommend any fragment to you or anybody else. This is
because I don't know which type theories you understand well, and
because I don't know what you want to do with them (your research or
teaching interests).
I can tell you which fragments I work with, and why. I prefer to
restrict to fragments of Agda corresponding to well-understood
Martin-Loef type theories.
This is not for dogmatic reasons, but instead because my current
research involves them as the base for univalent mathematics, and I
use Agda as tool for this research.
I use Agda to write Martin-Loef type theory constructions (and
usually for spartan Martin-Loef type theories).
"With", instance arguments, "abstract", sized types, irrelevant
fields, among others, don't belong to the type theories I understand
well, or that people have precisely defined, or that have the
blessing of the community as finished things. So I don't use them,
either because of ignorance or lack of trust or lack of precise
definition.
(I tried instance arguments, but then my code that compiled in one
version of Agda failed in the next, and because I never saw a
convincing definition of them, I decided to abandon them, as a
non-reliable, non-stable feature.)
Moreover, I use the options --exact-split and --without-K. The
former because I would like to think that, even if I indulge in
using (well-founded) recursive definitions by pattern matching, my
code should, in principle, be automatically translatable to code
that uses "Martin-Loef combinators" only. The latter is because of
my current particular field of interest, which allows types that
don't necessarily satisfy "uniqueness of identity proofs".
As an exception, although I don't think implicit-argument resolution
is well defined (independently of the Agda implementation), I do use
implicit arguments, because they are very convenient. And I don't
think they can give rise to serious problems (although I faced a bug
once). However, I have observed, and reported, that sometimes new
versions of Agda fail to infer implicit arguments that were
(correctly) inferred in previous versions. It is a worry that 15000
lines of code may break in the future because of changes in implicit
argument resolution (that is, we are not working in a well-defined,
stable, type theory for implicit arguments).
I can say the same for pattern matching, as an exception, but this
has been ameliorated with the options --exact-split and --without-K,
already mentioned
Martin
.   \ Philip Wadler, Professor of Theoretical Computer Science, .
/\ School of Informatics, University of Edinburgh .  /  \ and Senior
Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/
<http://homepages.inf.ed.ac.uk/wadler/>
Thanks for following up. It is the latter case. But I don't
understand why it should be ok for that to fail. Removing abstract
should just replace some abstract terms by their concretions, which
have already been type checked. Everything that was provably equal
before should still be equal, so why is it ok for the proof of
equality to now fail? Doesn't this violate stability under
substitution? Cheers, -- P
It is because of things such as this that I prefer to restrict
my usage of Agda to a fragment corresponding to a
well-understood type theory.
This may be limiting in terms of expressivity, conciseness, and
efficiency, but at least one can tell whether something is a bug
or not, rather than a bug or a feature.
:-) Martin
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>