如何在agda中定义抽象类型答案

【问题标题】：How to define abstract types in agda如何在agda中定义抽象类型
【发布时间】：2014-11-12 13:46:44
【问题描述】：

如何在 Agda 中定义抽象类型。我们在 Isabelle 中使用 typedecl 来做到这一点。

更准确地说，我想要 Isabelle 中以下代码的 agda 对应项：

typedecl A

谢谢

【问题讨论】：

实际上，我几乎没见过 typedecl 在 Isabelle 的生产代码中使用。我宁愿建议使用类型类或语言环境来保持抽象。

标签： isabelle agda

【解决方案1】：

您可以使用参数化模块。我们来看一个例子：我们首先引入一条记录Nats，将Set与对它的操作打包在一起。

record Nats : Set₁ where
  field
    Nat     : Set
    zero    : Nat
    succ    : Nat → Nat
    primrec : {B : Set} (z : B) (s : Nat → B → B) → Nat → B

然后我们可以定义一个由这种结构参数化的模块。加法和乘法可以用原始递归、零和后继来定义。

open import Function
module AbstractType (nats : Nats) where

  open Nats nats

  add : Nat → Nat → Nat
  add m n = primrec n (const succ) m

  mult : Nat → Nat → Nat
  mult m n = primrec zero (const (add n)) m

最后我们可以提供Nats 的实例。这里我重用了标准库中定义的自然数，但也可以使用二进制数。

open Nats
Natsℕ : Nats
Natsℕ = record { Nat     = ℕ
               ; zero    = 0
               ; succ    = suc
               ; primrec = primrecℕ }
  where
    open import Data.Nat
    primrecℕ : {B : Set} (z : B) (s : ℕ → B → B) → ℕ → B
    primrecℕ z s zero    = z
    primrecℕ z s (suc n) = s n $ primrecℕ z s n

将此实例传递给模块，为我们提供相应的加/多操作：

open import Relation.Binary.PropositionalEquality

example :
  let open AbstractType Natsℕ
  in mult (add 0 3) 3 ≡ 9
example = refl

【讨论】：