record type in Agda
Menu Menudata 型の復習
record-ex.agda record type に相当するものは Haskell にはありません。なので、使い方と data との使い分けを意識する必要があります。
data _∨_ (A B : Set) : Set where
or1 : A -> A ∨ B
or2 : B -> A ∨ B
この or1、or2 は Constructor つまり、∨ introduction として使われます。
A
----------- or1
A ∨ B
λ式としては、 or1 b のように呼び出します。data _∨_ は、or1 か or2 であり、パターンマッチとして使うことができます。
f (or1 a) = ...
f (or2 b) = ...
これによって、中身を取り出しますことができます。
data _∨_ (A B : Set) : Set where
or1 : A -> A ∨ B
or2 : B -> A ∨ B
postulate A B C : Set
postulate a1 a2 a3 : A
postulate b1 b2 b3 : B
x : ( A ∨ B )
x = or1 a1
y : ( A ∨ B )
y = or2 b1
f : ( A ∨ B ) -> A
f (or1 a) = a
f (or2 b) = a1
or1 と or2 は射であって、
or1 or2
A -----> A ∨ B <------ B
となっています。
record 型の復習
record は、
record _∧_ (A B : Set) : Set where
field
and1 : A
and2 : B
record { and1 = hoge; and2 = fuga } が Constructor になります。and1, and2 は accessor に相当します。 推論規則では _∧_ elimmination です。
A ∧ B
----------- _∧_.and1
A
実際、
z : A ∧ B
z = record { and1 = a1 ; and2 = b2 }
xa : A
xa = _∧_.and1 z
xb : B
xb = _∧_.and2 z
となります。 and1 と and2 は射であって、
and1 and2
A <----- A ∧ B ------> B
となっています。open _∧_ すると、_∧_. は省略できます。
open _∧_
ya : A
ya = and1 z
ある性質を満たすものを表す record
Mod 3 を考えましょう。3で割った余りが等しければ等しいとします。record Mod3 の要素 x の field に、この性質を記述すると、mod3 x は、その性質の型を持ちます。つまり、その性質を公理としていつでも呼び出せます。例えば、4 ≡ 1 ならば以下のように証明できます。
open import Relation.Binary.PropositionalEquality
data Nat : Set where
zero : Nat
suc : Nat -> Nat
record Mod3 (m : Nat) : Set where
field
mod3 : (suc (suc (suc m ))) ≡ m
n : Nat
n = m
open Mod3
Lemma1 : ( x : Mod3 ( suc (suc (suc (suc zero))))) ( y : Mod3 ( suc zero ) ) -> n x ≡ n y
Lemma1 x y = mod3 y
ここでは、パターンとしての型に data を使い、その data が満たす公理を recod に記述しています。