[Agda] Strictly positivity of indexed families

[Anton Setzer]

On 03/11/10 17:38, Florent Balestrieri wrote:
> Hello, I'd like to know if there is a workaround for  defining the 
> following datatype which is rejected by the termination checker 
> although it seems reasonable to me.  If there is a theoretical 
> argument to rule out such definitions, I would welcome your explanations.
>
> -- This datatype is rejected by agda.
>
> data D : Nat -> Set where
>  z : {n : Nat} -> D n
>  s : {n : Nat} -> (D n -> Nat) -> D (suc n)

What about (not tested in Agda)

data F0 : Set where
    z : F0

data F1 (A : Set) : Set where
     z : F1 A
     s : (A -> Nat) -> F1 A

D : Nat -> Set
D 0 = F0
D (suc n) = F1 (D n)

Anton
>
> -- But we can expand the family as much as we want
> -- without getting into trouble.
>
> data D0 : Set where
>  z : D0
>
> data D1 : Set where
>  z : D1
>  s : (D0 -> Nat) -> D1
>
> data D2 : Set where
>  z : D2
>  s : (D1 -> Nat) -> D2
>
> data D3 : Set where
>  z : D3
>  s : (D2 -> Nat) -> D3
>
>
> -- Florent
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------