[Agda] how to type this?

[Anton Setzer]

Martin Escardo wrote:
> Dear Agda fans (and type theorists),
>
> I want to consider functions f that take infinite sequences x_0, x_1,
> x2_, .... to values in a result type R. So, at first sight, we have
> something like
>
> f : prod_i X_i -> R.
>
> But I want the type X_i to depend on the elements x_0, ... x_(i-1) in
> addition to i. That is, x_i is to have type (X_i x_0 ... x_(i-1)).
>
> If the sequence x_i were finite, I know how to do that.
>
> How can this be expressed in Agda (or in type theory) in the infinite
> case in a simple and mathematically elegant way? (I prefer to avoid
> co-induction if possible.)
>
> Thanks!
>
> MHE.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
The following uses codata but seems to me a possible solution:

> module testFunctionDependingOnManyArguments where
>
>
> open import Data.Nat
> open import Data.Fin hiding (_+_)
>
> codata MultiArgsType : Set₁ where
> _::_ : (X : Set) → (X → MultiArgsType) → MultiArgsType
>
>
> data Fam (C : Set₁) : Set₂ where
> p : (A : Set) → (A → C) → Fam C
>
> proj₁ : {C : Set₁} → Fam C → Set
> proj₁ (p A B) = A
>
> proj₂ : {C : Set₁} → (A : Fam C) → (proj₁ A) → C
> proj₂ (p A B) = B
>
>
>
> headtail : MultiArgsType → Fam MultiArgsType
> headtail (A :: B) = p A B
>
> head : MultiArgsType → Set
> head A = proj₁ (headtail A)
>
> tail : (A : MultiArgsType) → head A → MultiArgsType
> tail A = proj₂ (headtail A)
>
>
> {-
>
>
>
> tail : (A : MultiArgsType) → head A → Set
> tail (A :: B) = B
> -}
>
> Example : ℕ → MultiArgsType
> Example n = Fin n :: (\ k -> Example (n + toℕ k))
>
>
> codata MultiArgsTypeToSet ( A : MultiArgsType) : Set where
> cons' : (a : head A)
> -> (b : MultiArgsTypeToSet (tail A a))
> -> MultiArgsTypeToSet A
>
>
> example : (n : ℕ) → MultiArgsTypeToSet (Example (suc n))
> example n = cons' zero (example (n + 0))



-- 

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