[Agda] Type declaration might lead to non-termination?

[Lionel Elie Mamane]

On Tue, Jun 14, 2005 at 12:30:03PM +0900, takeyama wrote:

>> 1)
>> ...
>> Hmm... What should I understand from this message? It is a type
>> declaration! What can be unsafe about it?

> Probably nothing is wrong in the type declaration.   The error message

>    At: XXX
>    The call: f
>    might lead to non-termination.

> should have been written

>    At: XXX
>    The function f [whose definition starts at XXX] might not
>    terminate.

Ah, OK, I see. Is there a description somewhere of what exactly the
termination checker will accept and what it won't? I'd like to
investigate why my definition is believed to maybe not terminate and
try to massage it into a form that is checked to terminate. But for
that I have to understand what it accepts. Is there something - maybe
a paper? - I can read for this?

>> 2) Given this definition:
>> ...
>>  1) I couldn't find the right syntax to do that. A suggestion?

> If you mean some sort of let-definition, it is not recommended.

I was trying things along the lines of 

P(X::PASet) :: Set =
 data
  P_cons((xi::(case X of (PASet_cons I f N)-> I))-> P((case X of (PASet_cons I f N)-> f) xi))

but they didn't work out.

>>  2) This would make the definition of P much less readable; is there
>>     another solution?

> How about this?

> P_CONS(F::Set)::Set = data P_cons(f::F)
> mutual
>   PASet::Type = data
>     PASet_cons (I::Set)(f::I->PASet)(N::(i::I)-> (P (f i)))
>   P(X::PASet) :: Set =
>     case X of (PASet_cons I f N)-> P_CONS((xi::I)-> P(f xi))

Yeah, this works and after some reflection I've been able to
generalise it to the case of more than one constructor, etc. I don't
understand what's going on, though.

> (The reason P_CONS is defined separately is that "data expression"
> should always be explicitly named.)

That's probably the same as my "don't understand what's going on"
before, but I don't understand this remark. What is "data expression"?

Thanks for your help,

-- 
Lionel