[Agda] Strictly positivity of indexed families

[Dan Licata]

Hi Florent,

To see that this datatype makes sense, Agda would have to notice that
you are using the indices in a special way: D(suc n) is defined in terms
of D n, but not any higher numbers.  E.g. if the argument to s were
(D(suc n) -> D(suc n)) then you could write a loop.  Agda doesn't look
at the indices when checking positivity.  The workaround is to define
the datatype recursively instead:

  data Nat : Set where
    zero : Nat
    suc : Nat -> Nat

  record Unit : Set where
    constructor <>

  data Either (A B : Set) : Set where
    Inl : A -> Either A B
    Inr : B -> Either A B

  D : Nat -> Set
  D zero = Unit
  D (suc n) = Either Unit (D n -> Nat)

Now D is defined by recursion on the index, which explains why it makes
sense.  

You can then use your original datatype as a view:

  data D' : Nat -> Set where
   z : {n : Nat} -> D' n
   s : {n : Nat} -> (D n -> Nat) -> D' (suc n)

  show : ∀ {n} -> D n -> D' n
  show {zero} <> = z
  show {suc n} (Inl <>) = z
  show {suc n} (Inr f) = s f

  z' : ∀ {n} -> D n
  z' {zero} = <>
  z' {suc n} = Inl <>

  hide : ∀ {n} -> D' n -> D n
  hide z = z'
  hide (s f) = Inr f

-Dan

On Nov03, 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)
> 
> -- 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
>