如何在agda中定义抽象类型

Question

如何在Agda中定义抽象类型.我们在Isabelle中使用typedecl这样做.

更准确地说,我想要Isabelle中以下代码的agda对应物:

typedecl A

谢谢

Answer 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

将此实例传递给模块,为我们提供相应的add/mult操作:

open import Relation.Binary.PropositionalEquality

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