Skip to content

@jlouis /Fishy1 secret
Created

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Fishy!
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.