Constant access n-Sums

Datatype.agda

module Datatype where

open import Data.Empty hiding (⊥-elim)
open import Data.Nat
open import Data.Bool
open import Data.List
open import Relation.Nullary

¬n<0 : {n : ℕ} → ¬ (n < 0)
¬n<0 ()

instance
  base : {n : ℕ} → 0 ≤ n
  base = z≤n

  step : {m n : ℕ} → {{pr : m ≤ n}} → suc m ≤ suc n
  step {{pr}} = s≤s pr
  
1+m≤1+n-inv : {m n : ℕ} → suc m ≤ suc n → m ≤ n
1+m≤1+n-inv (s≤s pr) = pr

⊥-elim : ∀ {α} {A : Set α} → .⊥ → A
⊥-elim ()

lookup : ∀ {α} {A : Set α} (as : List A) n → .(n < length as) → A
lookup []       n       pr = ⊥-elim (¬n<0 pr)
lookup (a ∷ as) zero    pr = a
lookup (a ∷ as) (suc n) pr = lookup as n (1+m≤1+n-inv pr)

record NSum (ts : List Set) : Set₁ where
  constructor nsum
  field
    ix         : ℕ
    .{{bound}} : ix < length ts
    dat        : lookup ts ix bound

foo : NSum (ℕ ∷ Bool ∷ ℕ ∷ Bool ∷ [])
foo = nsum 0 10

bar : NSum (ℕ ∷ Bool ∷ ℕ ∷ Bool ∷ []) → ℕ
bar (nsum 2 dat) = dat
bar _            = 3