Code of Dependently typed programming in Agda

Views.agda

module Views where

open import Data.Nat renaming (ℕ to Nat)
--open import AgdaBasics

data Parity : Nat → Set where
  even : (k : Nat) → Parity (k * 2)
  odd  : (k : Nat) → Parity (1 + k * 2)

-- zero  + m = m
-- suc n + m = suc m
-- 
-- 3                      + 1
-- (suc (suc (suc zero))) + (suc zero)
--
-- = suc ( (suc (suc zero)) + (suc zero) )
-- = suc ( suc ( (suc zero) + (suc zero) ) )
-- = suc ( suc ( suc ( zero + (suc zero) ) ) )
-- = suc ( suc ( suc ( (suc zero) ) ) )
-- = 4

parity : (n : Nat) → Parity n
parity zero    = even zero
parity (suc n) with parity n
parity (suc .(k * 2))     | even k = odd k
parity (suc .(1 + k * 2)) | odd  k = even (suc k)

open import Data.List
open import Function using (_∘_)
open import Data.Bool renaming (T to isTrue)
open import Data.Unit -- for tt

-- isEven : Nat → Bool
-- isEven n with parity n
-- ... | x = {!!}
--
-- with を用いる時は，上記のように書いてから，x で場合分け(Ctr-c, Ctr-c)する．

isEven : Nat → Bool
isEven n with parity n
isEven .(k * 2)       | even k = true
isEven .(suc (k * 2)) | odd  k = false

isOdd : Nat → Bool
isOdd n = not (isEven n)


infixr 30 _:all:_
data All {A : Set} (P : A → Set) : List A → Set where
  all[]   : All P []
  _:all:_ : ∀ {x xs} → P x → All P xs → All P (x ∷ xs)

sampleList : List Nat
sampleList = 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []

<6 : Nat → Bool
<6 0 = true
<6 1 = true
<6 2 = true
<6 3 = true
<6 4 = true
<6 5 = true
<6 _ = false

p : Nat → Set
p x = isTrue (<6 x)

-- isTrue true  = ⊤
-- データ型 "⊤" のコンストラクタは "tt" のみ

AllSample : All p sampleList
AllSample = tt :all: (tt :all: (tt :all: (tt :all: (tt :all: all[]))))

satisfies : {A : Set} → (A → Bool) → A → Set
satisfies p x = isTrue (p x)

data Find {A : Set} (p : A → Bool) : List A → Set where
  found     : (xs : List A) (y : A) → satisfies p y → (ys : List A) → Find p (xs ++ y ∷ ys)
              -- p を満たすかどうかは関係のない List xs
              -- p を満たす要素 y
              -- 与えられたリストから xs と y 取り除いた残りであるリスト ys
  not-found : ∀ {xs} → All (satisfies (not ∘ p)) xs → Find p xs

data _==_ {A : Set} (x : A) : A → Set where
  refl : x == x

-- y が Inspect x 型であるとは，y は A 型の値で，x と y が等しいということである．
data Inspect {A : Set} (x : A) : Set where
  it : (y : A) → x == y → Inspect x

InspectExa : Inspect 3
InspectExa = it 3 refl

inspect : {A : Set} (x : A) → Inspect x
inspect x = it x refl

InspectExa' : Inspect 3
InspectExa' = inspect 3

trueIsTrue : {x : Bool} → x == true → isTrue x -- (⊤)
trueIsTrue refl = tt

isFalse : Bool → Set
isFalse x = isTrue (not x)

falseIsFalse : {x : Bool} → x == false → isFalse x  -- isFalse x
falseIsFalse refl = tt                              -- isFalse false
                                                    -- isTrue (not false)
                                                    -- isTrue true
                                                    -- ⊤

find : {A : Set} (p : A → Bool) (xs : List A) → Find p xs
find p [] = not-found all[]
find p (x ∷ xs) with inspect (p x)
... | it true  prf = found [] x (trueIsTrue prf) xs
... | it false prf with find p xs
find p (x ∷ .(xs ++ y ∷ ys)) | it false prf | found xs y py ys = found (x ∷ xs) y py ys
find p (x ∷ xs) | it false prf | not-found npxs = not-found (falseIsFalse prf :all: npxs)

-- 二つ目の with での場合分けについて．最初のリストの x が条件 p を満たさないとき，
-- リストの残りの xs 中に p を満たすものがあるかどうかを, "with find p xs" によって
-- 場合分けしている．
-- ここで， "find p xs" が
--   found xs y py ys
-- ならば（残りの xs 中に p を満たす要素があるならば），条件 p を満たす要素 y の前
-- の，何も意味しないリスト xs の先頭に付け加える．
-- もう一つの場合，"find p xs" が
--   not-found npxs
-- ならば（残りの xs 中に p を満たす要素が存在しないならば），上記の様に構成すれば
-- 良い（分からなくなったら，"not-found" の後を消して，Ctr-c．Ctr-t でゴールを確認
-- すれば分かる．はず...）

data _∈_ {A : Set} (x : A) : List A → Set where
  hd : ∀ {xs}   → x ∈ (x ∷ xs)
  tl : ∀ {y xs} → x ∈ xs → x ∈ (y ∷ xs)

-- tl は hoge ∈ (hoge ∷ haha) の証明をもらうと
-- hoge ∈ (hehe ∷ haha) の形の "hehe" という hoge
-- hoge でない要素を追加した証明を返す．

index : ∀ {A} {x : A} {xs} → x ∈ xs → Nat
index hd     = 0
index (tl p) = suc (index p)

∈sample : 0 ∈ (4 ∷ 3 ∷ 0 ∷ 1 ∷ 2 ∷ [])
∈sample = tl (tl hd)

indexSample : Nat
indexSample = index ∈sample

data Lookup {A : Set} (xs : List A) : Nat → Set where
  inside  : (x : A) (p : x ∈ xs) → Lookup xs (index p)
  outside : (m : Nat) → Lookup xs (length xs + m)

_!_ : {A : Set} (xs : List A) (n : Nat) → Lookup xs n
[] ! n           = outside n
(x ∷ xs) ! 0     = inside x hd
(x ∷ xs) ! suc n with xs ! n
(x ∷ xs) ! suc .(index p)       | inside y p = inside y (tl p)
(x ∷ xs) ! suc .(length xs + n) | outside n  = outside n

infixr 30 _⇒_
data Type : Set where
  ı    : Type
  _⇒_ : Type → Type → Type

data Equal? : Type → Type → Set where
  yes : ∀ {τ}    → Equal? τ τ
  no  : ∀ {σ τ} → Equal? σ τ

_=?=_ : (σ τ : Type) → Equal? σ τ
ı =?= ı      = yes
ı =?= _ ⇒ _ = no
_ ⇒ _ =?= ı = no
(σ ⇒ τ) =?= (σ₁ ⇒ τ₁) with σ =?= σ₁ | τ =?= τ₁
σ ⇒ τ =?= .σ ⇒ .τ | yes | yes = yes
σ ⇒ τ =?= σ₁ ⇒ τ₁  | _   | _   = no

-- with P(x) | Q(y) と場合わけしたい時は，
--
-- with P(x) | Q(y)
-- ... | a | b = ?
--
-- として，a, b でスプリットすると良い．

infixl 80 _$_
data Raw : Set where
  var : Nat → Raw
  _$_ : Raw → Raw → Raw
  lam : Type → Raw → Raw

Cxt = List Type

data Term (Γ : Cxt) : Type → Set where
  var : ∀ {τ} → τ ∈ Γ → Term Γ τ
  _$_ : ∀ {σ τ} → Term Γ (σ ⇒ τ) → Term Γ σ → Term Γ τ
  lam : ∀ σ {τ} → Term (σ ∷ Γ) τ → Term Γ (σ ⇒ τ)

erase : ∀ {Γ τ} → Term Γ τ → Raw
erase (var x)    = var (index x)
erase (t $ u)    = erase t $ erase u
erase (lam σ t) = lam σ (erase t)

data Infer (Γ : Cxt) : Raw → Set where
  ok  : (τ : Type) (t : Term Γ τ) → Infer Γ (erase t)
  bad : {e : Raw} → Infer Γ e

infer : (Γ : Cxt) (e : Raw) → Infer Γ e

infer Γ (var n) with Γ ! n
infer Γ (var .(index x))      | inside σ x = ok σ (var x)
infer Γ (var .(length Γ + n)) | outside n  = bad

infer Γ (e₁ $ e₂) with infer Γ e₁ | infer Γ e₂
infer Γ (.(erase t) $ e₂) | ok τ t | bad = bad
infer Γ (e₁ $ e₂) | bad | _ = bad
infer Γ (.(erase t) $ .(erase t₁)) | ok ı t | ok τ₁ t₁ = bad
infer Γ (.(erase t) $ .(erase t₁)) | ok (τ ⇒ τ₁) t | ok τ₂ t₁
  with τ =?= τ₂
infer Γ (.(erase t) $ .(erase t₁)) | ok (τ ⇒ τ₁) t | ok τ₂ t₁ | no = bad
infer Γ (.(erase t) $ .(erase t₁)) | ok (τ ⇒ τ₁) t | ok .τ t₁ | yes = ok τ₁ (t $ t₁)

infer Γ (lam σ e) with infer (σ ∷ Γ) e
infer Γ (lam σ .(erase t)) | ok τ t = ok (σ ⇒ τ) (lam σ t)
infer Γ (lam σ e)          | bad = bad

c0 : Raw -- Church Numeral 0 (λf.λx.x) λ λ 0
c0 = lam (ı ⇒ ı) (lam ı (var 0))

c1 : Raw -- Church Numeral 1 (λf.λx.f x) λ λ 10
c1 = lam (ı ⇒ ı) (lam ı (var 1 $ var 0))

church : Cxt
church = (ı ⇒ ı) ⇒ ı ⇒ ı ∷ (((ı ⇒ ı) ⇒ (ı ⇒ ı)) ⇒ ((ı ⇒ ı) ⇒ (ı ⇒ ı))) ∷ []

c0' : {Γ : Cxt} → Term Γ ((ı ⇒ ı) ⇒ (ı ⇒ ı))
c0' = lam (ı ⇒ ı) (lam ı (var hd))

c1' : Term church ((ı ⇒ ı) ⇒ ı ⇒ ı)
--c1' : {Γ : Cxt} → Term Γ ((ı ⇒ ı) ⇒ ı ⇒ ı)
c1' = lam (ı ⇒ ı) (lam ı (var (tl hd) $ var hd))

--succ : Raw  -- λ λ λ 1 2 1 0
--succ = lam {!!} (lam {!!} (lam {!!} (var 1 $ (var 2 $ var 1 $ var 0))))

succ' : {Γ : Cxt} → Term Γ (((ı ⇒ ı) ⇒ (ı ⇒ ı)) ⇒ ((ı ⇒ ı) ⇒ (ı ⇒ ı)))
succ' = lam ((ı ⇒ ı) ⇒ (ı ⇒ ı)) (lam (ı ⇒ ı) (lam ı (var (tl hd) $ (var (tl (tl hd)) $ var (tl hd) $ var hd))))

-- input tips: ⇒ (\r=)
-- C-u C-x = <ret>