secret
Last active

Fishy!

  • Download Gist
Fishy1
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
module Fish where
 
open import Function hiding (const)
open import Data.Bool
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality
 
data Exp : Set where
Const : ℕ -> Exp
Plus : Exp -> Exp -> Exp
Exit : Exp -> Exp
 
----------------------------------------------------------------------
-- Direct style
 
R = ℕ ⊎ ℕ
 
const : ℕ -> R
const i = inj₁ i
 
add : R -> R -> R
add (inj₁ x) (inj₁ x') = inj₁ (x + x')
add (inj₁ x) (inj₂ y) = inj₂ y
add (inj₂ y) y' = inj₂ y
 
exit : R -> R
exit (inj₁ x) = inj₂ x
exit (inj₂ y) = inj₂ y
 
eval : Exp -> R
eval (Const y) = const y
eval (Plus y y') = add (eval y) (eval y')
eval (Exit e) = exit (eval e)
 
-- Funny, how this stuff is immediate :)
thm-determ : ∀ {e : Exp}{v1 v2 : R} -> eval e ≡ v1 -> eval e ≡ v2 -> v1 ≡ v2
thm-determ refl refl = refl
 
-- This is immediate by normalisation of Agda terms as well :)
thm-terminates : ∀ (e : Exp) -> ∃ (\v -> eval e ≡ v)
thm-terminates e = eval e, refl
 
----------------------------------------------------------------------
-- Continuations, take 1, naive translation.
 
module Naive where
constK : ℕ -> (R -> R) -> R
constK i k = k (const i)
 
exitK : R -> (R -> R) -> R
exitK v k = k (exit v)
 
addK : R -> R -> (R -> R) -> R
addK v1 v2 k = k (add v1 v2)
 
evalK : Exp -> (R -> R) -> R
evalK (Const y) k = constK y k
evalK (Plus y y') k = evalK y (\v1 ->
evalK y' (\v2 -> addK v1 v2 k))
evalK (Exit y) k = evalK y (\v1 -> exitK v1 k)
 
run1 : Exp -> R
run1 e = Naive.evalK e id
 
-- I so much love me dependent type checker :)
thm-determ-naive : ∀ {e : Exp}{v1 v2 : R} -> run1 e ≡ v1 -> run1 e ≡ v2 ->
v1 ≡ v2
thm-determ-naive refl refl = refl
 
-- This so much feels like cheating. The ∃ is a Σ-type with two components:
-- * The value in question: By definition the evalK on the identity
-- * A proof that the output of the Σ-proj₁ is ≡ to run1 e.
-- The proof is immediate by normalisation in Agda :)
thm-run1-terminates : ∀ (e : Exp) -> ∃ (\v -> run1 e ≡ v)
thm-run1-terminates e = Naive.evalK e id , refl
 
----------------------------------------------------------------------
-- Continuations, take 2, exploit continuations
 
module NotNaive where
-- As before
constK : ℕ -> (ℕ -> ℕ) -> ℕ
constK i k = k i
 
-- Exit circumventing the 'rest-of-the-program' by not invoking the
-- continuation
exitK : ℕ -> (ℕ -> ℕ) -> ℕ
exitK i k = i
 
addK : ℕ -> ℕ -> (ℕ -> ℕ) -> ℕ
addK v1 v2 k = k (v1 + v2)
 
evalK : Exp -> (ℕ -> ℕ) -> ℕ
evalK (Const y) k = constK y k
evalK (Plus y y') k = evalK y (\v1 -> evalK y' (\v2 -> addK v1 v2 k))
evalK (Exit y) k = evalK y (\v1 -> exitK v1 k)
 
run2 : Exp -> ℕ
run2 e = NotNaive.evalK e id
 
thm-determ-2 : ∀ {e : Exp}{v1 v2 : ℕ} -> run2 e ≡ v1 -> run2 e ≡ v2 ->
v1 ≡ v2
thm-determ-2 refl refl = refl
 
thm-run2-terminates : ∀ (e : Exp) -> ∃ (\v -> run2 e ≡ v)
thm-run2-terminates e = NotNaive.evalK e id , refl
 
t1 = Plus (Const 20) (Const 22)
t2 = Plus (Exit (Const 88)) (Const 22)
 
----------------------------------------------------------------------
-- Dependent analysis :)
 
module DepAnalysis where
 
data E : Bool -> Set where
Const : ℕ -> E true
Plus : ∀ {c1 c2} -> E c1 -> E c2 -> E (c1 ∧ c2)
Exit : ∀ {c} -> E c -> E false
 
pure : {b : Bool} -> E b -> Bool
pure {x} e = x

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.