open import 1Lab.Path
open import 1Lab.Type

module Data.Product.NAry where

n-Ary productsπŸ”—

This is an alternative definition of the type of n-ary products, which, unlike Vec, is defined by recursion on the length.

Vecβ‚“ : βˆ€ {β„“} β†’ Type β„“ β†’ Nat β†’ Type β„“
Vecβ‚“ A 0             = Lift _ ⊀
Vecβ‚“ A 1             = A
Vecβ‚“ A (suc (suc n)) = A Γ— Vecβ‚“ A (suc n)

The point of having the type Vecβ‚“ around is that its inhabitants can be written using the usual tuple syntax, so that we can define a From-product β€œtype class” for those type constructors (possibly indexed by the length) which can be built as a sequence of arguments.

_ : Vecβ‚“ Nat 3
_ = 1 , 2 , 3

record From-product {β„“} (A : Type β„“) (T : Nat β†’ Type β„“) : Type β„“ where
  field from-prod : βˆ€ n β†’ Vecβ‚“ A n β†’ T n

Shuffling the arguments to from-prod slightly, we arrive at the β€œlist syntax” construction:

[_] : βˆ€ {β„“} {A : Type β„“} {T : Nat β†’ Type β„“} {n} ⦃ fp : From-product A T ⦄
    β†’ Vecβ‚“ A n β†’ T n
[_] ⦃ fp = fp ⦄ = fp .From-product.from-prod _