[Agda] Termination problems with "with" and recursion

[Andreas Abel]

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!

;-)

Cheers,
Andreas

-- 
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
http://www2.tcs.ifi.lmu.de/~abel/