[Agda] Agda "trusted core".

[Pierre Hyvernat]

> I have felt it would be a good idea to delimit the scopes in which
> recursion is to be allowed with an explicit "rec/mutual" keyword.
>
I totally agree.
This becomes almost necessary if we want to extend Agda with some notion
of guarded co-inductive definitions.
(Which I really would like to see and understand one day...)



> There is something extremely dangerous about recursion, and ideally
> there should be just a few instances of recursive definitions in an
> Agda program.  The recursion-free fragment of Agda would be a kind of
> trusted core.
>
I might also simplify some things a bit since we do not need any
termination check for such non-recursive definitions.


For the rest:

(1) we could allow "explicit" inductive definitions where the user
actually gives the decreasing argument. (Like in coq...)
Those should be really easy to check, and the use should be allowed to
write non-terminating functions. (Termination check during type
checking.)


(2) but we definitely want something more general to write recursive
functions. (Those who have used Coq know how painful it can be to use
only structurally inductive definitions...)
For those, we need to go through the whole termination check(s).


So, the question is whether we want to differentiate between the two
levels?
(ie, do we want to have both (1) and (2), or only (2)?)



> [In the editor, ideally sirens should go off and red lights flash when
> one enters the scope of a rec.]
>
ie in the scope of a (2)...



Another related question is whether we want to allow non-terminating
definitions. Right now, you can write anything; but it needs not pass
termination check?
Is it a Good thing or a Bad thing?



Pierre Hyvernat
--