[Agda] Termination problems with "with" and recursion
abela at chalmers.se
Mon Dec 2 11:41:52 CET 2013
On 02.12.2013 09:43, Jan Stolarek wrote:
>> My suggestion is to use --sized-types
> Yes, I'm aware of that possibility, but it feels like a lot of
> boilerplate to get something other languages offer out-of-the-box. As
> a user I'd just like to see a better termination checker :-)
It is some overhead, but not a lot. Did you check my examples? Look
for "Size" and "Size<"!
The main focus of Agda is providing the programmer with a language where
he can express the properties of his programs. Sized types are a
language to express termination arguments.
We should not bloat the language to much with heuristics only "to get
something other languages offer out-of-the-box". Here is something
other languages do for you, but Agda does not: type inference.
-- Agda is so stupid,
-- cannot even infer the type of this trivial function:
plus zero n = n
plus (suc m) n = suc (plus m n)
-- What is so difficult about that? Bitch!
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
More information about the Agda