[Agda] Re: [Coq-Club] Positivity condition and nested recursion

[Andreas Abel]

Hello Robert,

MiniAgda also accepts your definition:

data Nat
{ zero
; suc (pred : Nat)
}

data Lt : Nat -> Nat -> Set
{ ltZ (   y : Nat)              : Lt zero    (suc y)
; ltS (x, y : Nat)(lt : Lt x y) : Lt (suc x) (suc y)
}

data List ++(A : Set)
{ nil
; cons (head : A) (tail : List A)
}

fun length : [A : Set] -> List A -> Nat
{ length A nil         = zero
; length A (cons a as) = suc (length A as)
}

data Val
{ vnat   (nat : Nat)
; varray (list : List Val) (nonEmpty : Lt zero (length Val list))
}

In fact, it is not difficult to see this.  One just needs the right 
concepts. ;-)

The length function is constant in the type argument A, this is 
indicated by the [A : Set] notation (as opposed to (A : Set)).  To check 
that Val is a valid inductive type, you need to check for varray that

1) List is strictly positive in its first argument.
    Yes, we have List : ++Set -> Set.

2) Lt zero (length _ list)  is strictly positive in _.
    Yes, because length is constant in _.

That's it!

I think Agda does essentially the same, only that it is inferred 
automagically, as opposed to just checking as in MiniAgda.

Cheers,
Andreas

On 10.05.12 1:23 AM, Robbert Krebbers wrote:
> Hello Cédric and Stéphane,
>
> thanks for the answers!
>
> On 05/09/2012 04:19 PM, AUGER Cédric wrote:
>> Do you not see why the strict positivity condition does not hold, or do
>> you not see why the strict positivity condition is not fit to allow what
>> you wrote and should be refined to allow it ?
>
> Initially both. But after Stéphane's answer, I was clear that the
> definition in the reference manual disallows it due to the implicit
> argument of length.
>
>> For the second point, things are less obvious, and I know there are
>> cases where it could be allowed without breaking consistency.
>
> Russell O’Connor's example at #coq
>
> Inductive val : Type := bad : ((fun X : Type => X -> X) val) -> val
>
> clearly showed me why functions in constructor arguments are unsafe in
> general.
>
> However, Agda allows my definition! But apparently it is non-trivial to
> type check, see [1].
>
> Robbert
>
> [1] https://lists.chalmers.se/pipermail/agda/2012/003992.html
>

-- 
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/