有效地抽象数据类型 arity

Question

众所周知，您可以轻松地从 2 元组构建 n 元组。

record Twople (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

n-ple : List Set -> Set
n-ple = foldr Twople Unit

（Agda 语法，但它可以在 Idris 中使用，并且可以在 Haskell、Scala 中使用...）

同样，您可以从二进制和构建 n 元和类型。

data Either (A B : Set) : Set where
  left : A -> Either A B
  right : B -> Either A B

OneOf : List Set -> Set
OneOf = foldr Either Void

简单、漂亮，但效率低下。从 n-ple 中提取最右边的项目需要 O(n) 时间，因为您必须在途中解压每个嵌套的 Twople。 n-ple 更像是一个异构列表而不是一个元组。同样，在最坏的情况下，OneOf 值存在于 n-1 rights 的末尾。

可以通过手动解包字段并内联数据类型的构造函数案例来缓解低效率问题：

record Threeple (A B C : Set) : Set where
  constructor _,_,_
  field
    fst : A
    snd : B
    thd : C

data Threeither (A B C : Set) : Set where
  left : A -> Threeither A B C
  middle : B -> Threeither A B C
  right : C -> Threeither A B C

从 Threeple 中挑选一个项目并对 Threeither 执行案例分析现在都是 O(1)。但是涉及到很多类型，而不是好的类型 - Fourple、Nineither、Hundredple 等等，必须都是单独定义的数据类型。

我必须在 O(1) 时间和 O(1) 行代码之间做出选择吗？或者依赖类型可以帮助我吗？可以有效地抽象数据类型元数吗？

Answer 1

对于使用 O(1) 代码的 O(1) 字段访问，我们需要一个 array 作为原始对象，或者仍然实现为一个异构或依赖泛化大批。 Agda 没有这样的东西。

对于 n 元求和，情况有点微妙，但也取决于机器的实现。在这里，O(1) 可能合理地意味着我们能够通过一个指针解引用和一个构造函数标记检查在任意构造函数上进行模式匹配，就像本地定义的求和类型一样。在 Agda 中，可以尝试：

open import Data.Nat
open import Data.Vec

record NSum {n}(ts : Vec Set n) : Set₁ where
  field
    ix  : Fin n
    dat : lookup ix ts

当然，这取决于 Data.Fin 被实现为机器（大）整数，据我所知，当前的 Agda 并非如此。我们应该尝试 Data.Nat，因为它的实施效率很高：

open import Data.Nat hiding (_<_)
open import Agda.Builtin.Nat using (_<_)
open import Data.Bool
open import Data.List

lookup : ∀ {α}{A : Set α}(as : List A) n → T (n < length as) → A
lookup [] zero ()
lookup [] (suc n) ()
lookup (a ∷ as) zero    p = a
lookup (a ∷ as) (suc n) p = lookup as n p

record NSum (ts : List Set) : Set₁ where
  constructor nsum
  field
    ix       : ℕ
    {bound}  : T (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

请注意，我们使用布尔值 _<_ 而不是默认值 _<_，因为涉及前者的证明占用 O(1) space。此外，对于大多数用例，lookup 仅在编译时运行，因此它不会破坏我们的 O(1)。

有效地抽象数据类型 arity

Efficiently abstracting over datatype arity

haskell

agda

dependent-type

idris