Как определять абстрактные типы в agda

Как можно определять абстрактные типы в Agda. Для этого мы используем typedecl в Isabelle.

Точнее, мне нужен аналог agda приведенного ниже кода в Isabelle:

typedecl A

Спасибо


agda isabelle
person qartal    schedule 12.11.2014    source источник
comment
На самом деле, я почти никогда не видел, чтобы typedecl использовался в производственном коде Изабель. Я бы предпочел использовать классы типов или локали, чтобы оставаться абстрактными.   -  person chris    schedule 12.11.2014

Ответы (1)


arrow_upward
7
arrow_downward

Вы можете использовать параметризованные модули. Давайте посмотрим на пример: мы начнем с введения записи 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
person gallais    schedule 12.11.2014