How to define abstract types in agda

Question

How is it possible to define abstract types in Agda. We use typedecl in Isabelle to do so.

More precisely, I would like the agda counterpart of the below code in Isabelle:

Click to copy

typedecl A

Thanks

Answer 1

You could use parametrized modules. Let's have a look at an example: we start by introducing a record Nats packing a Set together with operations on it.

Click to copy

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

We can then define a module parametrized by such a structure. Addition and multiplication can be defined in terms of primitive recursion, zero and successor.

Click to copy

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

Finally we can provide instances of Nats. Here I reuse the natural numbers as defined in the standard library but one could use binary numbers for instance.

Click to copy

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

Passing this instance to the module, gives us the corresponding add / mult operations:

Click to copy

open import Relation.Binary.PropositionalEquality

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