Merge pull request #47 from jonsterling/decalf

Add Decalf examples

src/Calf/Data/IsBounded.agda

@@ -31,7 +31,7 @@ bound/step : {A : tp⁺} (c : ℂ) {c' : ℂ} (e : cmp (F A)) →
   IsBounded A (step (F A) c e) (c + c')
 bound/step c {c'} e h = boundg/step c {b = step⋆ c'} e h
 
-bound/bind/const : ∀ {A B : tp⁺} {e : cmp (F A)} {f : val A → cmp (F B)}
+bound/bind/const : {e : cmp (F A)} {f : val A → cmp (F B)}
   (c d : ℂ) →
   IsBounded A e c →
   ((a : val A) → IsBounded B (f a) d) →

src/Calf/Directed.agda

@@ -85,25 +85,38 @@ postulate
 syntax ≤⁻-syntax {X} e e' = e ≤⁻[ X ] e'
 
 
-bind-mono-≤⁻ : {A : tp⁺} {X : tp⁻} {e e' : cmp (F A)} {f f' : val A → cmp X}
+bind-mono-≤⁻ : {e e' : cmp (F A)} {f f' : val A → cmp X}
   → e ≤⁻[ F A ] e'
   → f ≤⁻[ Π A (λ _ → X) ] f'
-  → _≤⁻_ {X} (bind {A} X e f) (bind {A} X e' f')
+  → (bind {A} X e f) ≤⁻[ X ] (bind {A} X e' f')
 bind-mono-≤⁻ {A} {X} {e' = e'} {f} {f'} e≤e' f≤f' =
   ≤⁻-trans
     (≤⁻-mono (λ e → bind {A} X e f) e≤e')
     (≤⁻-mono {Π A (λ _ → X)} {X} (bind {A} X e') {f} {f'} f≤f')
 
-bind-monoˡ-≤⁻ : {A : tp⁺} {X : tp⁻} {e e' : cmp (F A)} (f : val A → cmp X)
-  → _≤⁻_ {F A} e e'
-  → _≤⁻_ {X} (bind {A} X e f) (bind {A} X e' f)
+bind-monoˡ-≤⁻ : {e e' : cmp (F A)} (f : val A → cmp X)
+  → e ≤⁻[ F A ] e'
+  → (bind {A} X e f) ≤⁻[ X ] (bind {A} X e' f)
 bind-monoˡ-≤⁻ f e≤e' = bind-mono-≤⁻ e≤e' ≤⁻-refl
 
-bind-monoʳ-≤⁻ : {A : tp⁺} {X : tp⁻} (e : cmp (F A)) {f f' : val A → cmp X}
-  → ((a : val A) → _≤⁻_ {X} (f a) (f' a))
-  → _≤⁻_ {X} (bind {A} X e f) (bind {A} X e f')
+bind-monoʳ-≤⁻ : (e : cmp (F A)) {f f' : val A → cmp X}
+  → ((a : val A) → (f a) ≤⁻[ X ] (f' a))
+  → (bind {A} X e f) ≤⁻[ X ] (bind {A} X e f')
 bind-monoʳ-≤⁻ e f≤f' = bind-mono-≤⁻ (≤⁻-refl {x = e}) (λ-mono-≤⁻ f≤f')
 
+bind-irr-mono-≤⁻ : {e₁ e₁' : cmp (F A)} {e₂ e₂' : cmp X}
+  → e₁ ≤⁻[ F A ] e₁'
+  → e₂ ≤⁻[ X ] e₂'
+  → (bind {A} X e₁ λ _ → e₂) ≤⁻[ X ] (bind {A} X e₁' λ _ → e₂')
+bind-irr-mono-≤⁻ e₁≤e₁' e₂≤e₂' =
+  bind-mono-≤⁻ e₁≤e₁' (λ-mono-≤⁻ λ a → e₂≤e₂')
+
+bind-irr-monoˡ-≤⁻ : {e₁ e₁' : cmp (F A)} {e₂ : cmp X}
+  → e₁ ≤⁻[ F A ] e₁'
+  → (bind {A} X e₁ λ _ → e₂) ≤⁻[ X ] (bind {A} X e₁' λ _ → e₂)
+bind-irr-monoˡ-≤⁻ e₁≤e₁' =
+  bind-irr-mono-≤⁻ e₁≤e₁' ≤⁻-refl
+
 
 open import Relation.Binary.Structures
 

src/Examples.agda

@@ -15,3 +15,6 @@ import Examples.Exp2
 
 -- Amortized Analysis via Coinduction
 import Examples.Amortized
+
+-- Effectful
+import Examples.Decalf

src/Examples/Decalf.agda

@@ -0,0 +1,9 @@
+{-# OPTIONS --rewriting #-}
+
+module Examples.Decalf where
+
+import Examples.Decalf.Basic
+import Examples.Decalf.Nondeterminism
+import Examples.Decalf.ProbabilisticChoice
+import Examples.Decalf.GlobalState
+import Examples.Decalf.HigherOrderFunction

src/Examples/Decalf/Basic.agda

@@ -0,0 +1,56 @@
+{-# OPTIONS --rewriting #-}
+
+module Examples.Decalf.Basic where
+
+open import Algebra.Cost
+
+costMonoid = ℕ-CostMonoid
+open CostMonoid costMonoid using (ℂ)
+
+open import Calf costMonoid
+open import Calf.Data.Nat
+import Data.Nat.Properties as Nat
+open import Calf.Data.Equality as Eq using (_≡_; refl; module ≡-Reasoning)
+open import Function
+
+
+double : cmp $ Π nat λ _ → F nat
+double zero    = ret zero
+double (suc n) =
+  step (F nat) 1 $
+  bind (F nat) (double n) λ n' →
+  ret (suc (suc n'))
+
+double/bound : cmp $ Π nat λ _ → F nat
+double/bound n = step (F nat) n (ret (2 * n))
+
+double/has-cost : (n : val nat) → double n ≡ double/bound n
+double/has-cost zero    = refl
+double/has-cost (suc n) =
+  let open ≡-Reasoning in
+  begin
+    (step (F nat) 1 $
+    bind (F nat) (double n) λ n' →
+    ret (suc (suc n')))
+  ≡⟨
+    Eq.cong
+      (step (F nat) 1)
+      (begin
+        (bind (F nat) (double n) λ n' →
+        ret (suc (suc n')))
+      ≡⟨ Eq.cong (λ e → bind (F nat) e λ n' → ret (suc (suc n'))) (double/has-cost n) ⟩
+        (bind (F nat) (step (F nat) n (ret (2 * n))) λ n' →
+        ret (suc (suc n')))
+      ≡⟨⟩
+        step (F nat) n (ret (suc (suc (2 * n))))
+      ≡˘⟨ Eq.cong (step (F nat) n ∘ ret ∘ suc) (Nat.+-suc n (n + 0)) ⟩
+        step (F nat) n (ret (2 * suc n))
+      ∎)
+  ⟩
+    step (F nat) 1 (step (F nat) n (ret (2 * suc n)))
+  ≡⟨⟩
+    step (F nat) (suc n) (ret (2 * suc n))
+  ∎
+
+double/correct : ◯ ((n : val nat) → double n ≡ ret (2 * n))
+double/correct u n = Eq.trans (double/has-cost n) (step/ext (F nat) (ret (2 * n)) n u)

src/Examples/Decalf/GlobalState.agda

@@ -0,0 +1,82 @@
+{-# OPTIONS --rewriting #-}
+
+module Examples.Decalf.GlobalState where
+
+open import Algebra.Cost
+
+costMonoid = ℕ-CostMonoid
+open CostMonoid costMonoid using (ℂ)
+
+open import Calf costMonoid
+open import Calf.Data.Nat as Nat using (nat; _*_)
+open import Calf.Data.Equality as Eq using (_≡_; module ≡-Reasoning)
+open import Function
+
+
+S : tp⁺
+S = nat
+
+variable
+  s s₁ s₂ : val S
+
+postulate
+  get : (X : tp⁻) → (val S → cmp X) → cmp X
+  set : (X : tp⁻) → val S → cmp X → cmp X
+
+  get/get : {e : val S → val S → cmp X} →
+    (get X λ s₁ → get X λ s₂ → e s₁ s₂) ≡ (get X λ s → e s s)
+  get/set : {e : cmp X} →
+    (get X λ s → set X s e) ≡ e
+  set/get : {e : val S → cmp X} →
+    set X s (get X e) ≡ set X s (e s)
+  set/set : {e : cmp X} →
+    set X s₁ (set X s₂ e) ≡ set X s₂ e
+
+  get/step : (c : ℂ) {e : val S → cmp X} →
+    step X c (get X e) ≡ get X λ s → step X c (e s)
+  set/step : (c : ℂ) {e : cmp X} →
+    step X c (set X s e) ≡ set X s (step X c e)
+
+
+module StateDependentCost where
+  open import Examples.Decalf.Basic
+
+  e : cmp (F nat)
+  e =
+    get (F nat) λ n →
+    bind (F nat) (double n) λ n' →
+    set (F nat) n' $
+    ret n
+
+  e/bound : cmp (F nat)
+  e/bound =
+    get (F nat) λ n →
+    set (F nat) (2 * n) $
+    step (F nat) n $
+    ret n
+
+  e/has-cost : e ≡ e/bound
+  e/has-cost =
+    Eq.cong (get (F nat)) $ funext λ n →
+    let open ≡-Reasoning in
+    begin
+      ( bind (F nat) (double n) λ n' →
+        set (F nat) n' $
+        ret n
+      )
+    ≡⟨ Eq.cong (λ e₁ → bind (F nat) e₁ λ n' → set (F nat) n' (ret n)) (double/has-cost n) ⟩
+      ( bind (F nat) (step (F nat) n (ret (2 * n))) λ n' →
+        set (F nat) n' $
+        ret n
+      )
+    ≡⟨⟩
+      ( step (F nat) n $
+        set (F nat) (2 * n) $
+        ret n
+      )
+    ≡⟨ set/step n ⟩
+      ( set (F nat) (2 * n) $
+        step (F nat) n $
+        ret n
+      )
+    ∎

src/Examples/Decalf/HigherOrderFunction.agda

@@ -0,0 +1,92 @@
+{-# OPTIONS --rewriting #-}
+
+module Examples.Decalf.HigherOrderFunction where
+
+open import Algebra.Cost
+
+costMonoid = ℕ-CostMonoid
+open CostMonoid costMonoid using (ℂ)
+
+open import Calf costMonoid
+open import Calf.Data.Nat as Nat using (nat; zero; suc; _+_; _*_)
+import Data.Nat.Properties as Nat
+open import Data.Nat.Square
+open import Calf.Data.List using (list; []; _∷_; [_]; _++_; length)
+open import Calf.Data.Bool using (bool; if_then_else_)
+open import Calf.Data.Product using (unit)
+open import Calf.Data.Equality as Eq using (_≡_; refl; module ≡-Reasoning)
+open import Calf.Data.IsBoundedG costMonoid using (step⋆)
+open import Calf.Data.IsBounded costMonoid
+open import Function
+
+
+module Twice where
+  twice : cmp $ Π (U (F nat)) λ _ → F nat
+  twice e =
+    bind (F nat) e λ x₁ →
+    bind (F nat) e λ x₂ →
+    ret (x₁ + x₂)
+
+  twice/is-bounded : (e : cmp (F nat)) → IsBounded nat e 1 → IsBounded nat (twice e) 2
+  twice/is-bounded e e≤step⋆1 =
+    let open ≤⁻-Reasoning (F unit) in
+    begin
+      bind (F unit)
+        ( bind (F nat) e λ x₁ →
+          bind (F nat) e λ x₂ →
+          ret (x₁ + x₂)
+        )
+        (λ _ → ret triv)
+    ≡⟨⟩
+      ( bind (F unit) e λ _ →
+        bind (F unit) e λ _ →
+        ret triv
+      )
+    ≤⟨ ≤⁻-mono₂ (λ e₁ e₂ → bind (F _) e₁ λ _ → bind (F _) e₂ λ _ → ret triv) e≤step⋆1 e≤step⋆1 ⟩
+      ( bind (F unit) (step⋆ 1) λ _ →
+        bind (F unit) (step⋆ 1) λ _ →
+        ret triv
+      )
+    ≡⟨⟩
+      step⋆ 2
+    ∎
+
+module Map where
+  map : cmp $ Π (U (Π nat λ _ → F nat)) λ _ → Π (list nat) λ _ → F (list nat)
+  map f []       = ret []
+  map f (x ∷ xs) =
+    bind (F (list nat)) (f x) λ y →
+    bind (F (list nat)) (map f xs) λ ys →
+    ret (y ∷ ys)
+
+  map/is-bounded : (f : cmp (Π nat λ _ → F nat)) →
+    ((x : val nat) → IsBounded nat (f x) c) →
+    (l : val (list nat)) →
+    IsBounded (list nat) (map f l) (length l * c)
+  map/is-bounded     f f-bound []       = ≤⁻-refl
+  map/is-bounded {c} f f-bound (x ∷ xs) =
+    let open ≤⁻-Reasoning (F unit) in
+    begin
+      bind (F unit)
+        ( bind (F (list nat)) (f x) λ y →
+          bind (F (list nat)) (map f xs) λ ys →
+          ret (y ∷ ys)
+        )
+        (λ _ → ret triv)
+    ≡⟨⟩
+      ( bind (F unit) (f x) λ _ →
+        bind (F unit) (map f xs) λ _ →
+        ret triv
+      )
+    ≤⟨
+      ≤⁻-mono₂ (λ e₁ e₂ → bind (F unit) e₁ λ _ → bind (F unit) e₂ λ _ → ret triv)
+        (f-bound x)
+        (map/is-bounded f f-bound xs)
+    ⟩
+      ( bind (F unit) (step⋆ c) λ _ →
+        bind (F unit) (step⋆ (length xs * c)) λ _ →
+        ret triv
+      )
+    ≡⟨⟩
+      step⋆ (length (x ∷ xs) * c)
+    ∎