[Agda] Future of Agda?

[Peter G. Hancock]

Catarina,

Thanks for the example of the class system.  It seems to make sense. 

One remark:

> To explicitly mark function that are recursive is fine, but I would
> like to have something also to say that a function is not recursive, I
> think it is a good principle to have both flags but one is default,
> just like the other flags in Agda.

If one had a way to say that a function is not recursive, that could
only mean that the "f" in the right hand-side refers to some prior 
definition and not to the "f" being defined.  While that makes
perfect sense (I think: cf "it"), I'm not sure that it's good practice,
and I can't see that it would be useful. 

A "rec" keyword would be like a "mutual" keyword where there is
allowed to be just one thing involved.  I am strongly in favour of it:
the default should be: no recursion (at all).  

But I have not thought about how to plug in different kinds of
type-checking or termination checking for recursion.  Wouldn't
a "rec" keyword be useful syntax for invoking these things?

It may be unHaskell-ic, but it is ML-ic. 

(Hic!)

Peter Hancock