[Agda] Totality checking in Agda

[Henning Basold]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Hi Marko,

On 23/01/2019 09:02, Marko Dimjašević wrote:
> Hi Nils,
> 
> On Wed, 2019-01-23 at 08:49 +0100, Nils Anders Danielsson wrote:
>> 
>> I don't think there is a single text (other than the source
>> code) that describes everything in detail. What kind of
>> information are you looking for?
> 
> 
> There are several things I am looking for. I am interested in:
> 
> 1) What form of recursion is allowed in Agda for terminating
> functions?
> 

Agda has two mechanisms: The Foetus productivity checker that is
described here:
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Termin
ationChecker
and in the there linked publication by Andreas Abel. The other
mechanism are sized types, which have been described in various
places, check
https://agda.readthedocs.io/en/latest/language/sized-types.html and
http://www.cse.chalmers.se/~abela/rairo04.pdf

> 2) How does Agda check for productivity?
> 

Productivity is ensured by termination checking if you use the
copattern-style coinductive types. The reason is that elements of
coinductive types only unfold upon observation and the termination
checker ensures that all the terms in Agda remain terminating under
all observations. This is the idea underlying the strong normalisation
proof in
https://perso.ens-lyon.fr/henning.basold/publications/DepIndCoindTypes.p
df,
and I provide in Chapter 4 of my thesis
(http://perso.ens-lyon.fr/henning.basold/thesis/) a characterisation
of the largest class of inductive-coinductive programs that a
terminating and thus productive.

> 3) How to write a main program, which should be of type IO (), and
> if this is possible at all if partial functions are not allowed in
> Agda?
> 

Within Agda, there is no such thing as non-terminating functions and
impure IO. You can implement the IO monad in Agda (Interactive
Programs and Weakly Final Coalgebras in Dependent Type Theory by Anton
Setzer and Peter Hancock), or otherwise you postpone the IO
interaction to extracted code (check again Setzer's work, this time on
GUIs in Agda).

> 4) In Idris, one can annotate a function as partial; I found no way
> of writing partial functions in Agda. I read lecture notes from
> the International LerNetALFA Summer School 2008 and in particular
> chapter 2 titled "Dependent Types at Work" that has a section
> "General Recursion and Partial Functions", but I still don't see
> how to write partial functions in Agda; what is given there and in
> the Agda wiki doesn't look to me like partial functions, but total
> functions instead because those examples are defined on their whole
> domain.
> 

You can declare functions to be non-terminating or ignored by the
termination checker
(https://agda.readthedocs.io/en/latest/language/pragmas.html). If you
do this this in places where Agda has to compute with a
non-terminating function in, e.g., a dependent type, then things will
go wrong of course. For modelling non-terminating computations using
coinductive types, check Capretta (http://arxiv.org/abs/cs/0505037)
and https://perso.ens-lyon.fr/henning.basold/code/Partial/PComp.html
for the correctness of μ-recursion in Agda implemented through the
definition of partiality proposed by Capretta. Also have a look at
https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf

> 5) How to write productive programs in Agda that use fuel to
> ensure their totality?

I have to admit that I'm not very familiar with this, but is this not
about total functions ℕ → Maybe A?

Cheers,
Henning
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlxITWYACgkQatBsEc2x
Mm5vnw//Yuzk1b9P52HsgUxp14ZP16aDtWELqvklsG23tVz9U1Io8S2FwvnKVwrM
Ejkfyn7PCJ2yLwVJipbe7gRxUr1OvU7H5uMBazE1UynGW1Z7uNoGhVgk0w+ETDRE
By5FRudCmInaZBgvjKZCDcoPVbAFuR/TGBFEZue+sJOHjHWWVokpLjE3URkT/cvF
YMcIuAD8rg0RUGUYWsWSjYvZcxWEKTdj8ye7iH3M36LQCZc713fnsDZQ62BNI5Jp
AvqhLW/eMCH29wvpKO0nxa+V6U6/+dfkpluWr4n7kdBFsg/oApYOT69ZyO0LSq+m
1xHeOkGQyGR8Y+6V3Sj7YxlU47LVNEwU5y9HUDNjD85/o8UOWYp3LlaDcRilXHw/
ceveiPatlh23lkCBYMplp3OGpKEkPV5+zB3TTf8mmzwLTipFYtjcobMfsW4mFj3Z
oF8HHtpAjWcaoqoff9V3/nFD5beCWzzk4oIbklayn4siHwPHsB6tky835P7q2Rdu
aoUek01q0qI9N9i5HsPxs4kpkIXPwN+YIOZYXw2iUwVEutFgByNt4FjXNF7B9xU/
LYY9EU6TBItbhgwhZ3jfDULfYR00c5i/sceeh0VDdMx+ZjILLAnqQWW5duiDZJ+W
xY3O1pHTEAoMAXD+zVZUaQIdD0mRMuS+EzyYZcJwzhDGvgOdHss=
=MCYJ
-----END PGP SIGNATURE-----