Skip to content

Instantly share code, notes, and snippets.

@szabba
Created September 6, 2016 04:03
Show Gist options
  • Save szabba/00cd20fc2968337830323a63b685d3dd to your computer and use it in GitHub Desktop.
Save szabba/00cd20fc2968337830323a63b685d3dd to your computer and use it in GitHub Desktop.
import Html
-- EQUIVALENCE OF TYPES
type Equiv a b = Equiv (a -> b) (b -> a)
refl : Equiv a a
refl =
Equiv identity identity
sym : Equiv a b -> Equiv b a
sym (Equiv to from) =
Equiv from to
trans : Equiv a b -> Equiv b c -> Equiv a c
trans (Equiv a2b b2a) (Equiv b2c c2b) =
Equiv (a2b >> b2c) (c2b >> b2a)
-- TYPE-SAFE EXPRESSIONS
type Expr a
= I (Equiv Int a) a
| B (Equiv Bool a) a
| Add (Equiv Int a) (Expr a) (Expr a)
| Mul (Equiv Int a) (Expr a) (Expr a)
| Eq (Equiv Bool a) (Expr Int) (Expr Int)
| Not (Equiv Bool a) (Expr a)
| And (Equiv Bool a) (Expr a) (Expr a)
| Or (Equiv Bool a) (Expr a) (Expr a)
| Cond (Expr Bool) (Expr a) (Expr a)
-- EVALUATOR(S)
evalBool : Expr Bool -> Bool
evalBool expr =
case expr of
B _ x ->
x
Eq _ left right ->
evalInt left == evalInt right
Not _ x ->
not <| evalBool x
And _ left right ->
evalBool left && evalBool right
Or _ left right ->
evalBool left || evalBool right
Cond cond left right ->
if evalBool cond then
evalBool left
else
evalBool right
_ ->
evalBool expr
evalInt : Expr Int -> Int
evalInt expr =
case expr of
I _ x ->
x
Add _ left right ->
evalInt left + evalInt right
Mul _ left right ->
evalInt left * evalInt right
Cond cond left right ->
if evalBool cond then
evalInt left
else
evalInt right
_ ->
evalInt expr
-- NICE CONSTRUCTORS
num : Int -> Expr Int
num = I refl
bool : Bool -> Expr Bool
bool = B refl
add : Expr Int -> Expr Int -> Expr Int
add = Add refl
mul : Expr Int -> Expr Int -> Expr Int
mul = Mul refl
eq : Expr Int -> Expr Int -> Expr Bool
eq = Eq refl
not' : Expr Bool -> Expr Bool
not' = Not refl
and : Expr Bool -> Expr Bool -> Expr Bool
and = And refl
or : Expr Bool -> Expr Bool -> Expr Bool
or = Or refl
cond : Expr Bool -> Expr a -> Expr a -> Expr a
cond = Cond
-- PROGRAMS
t : Expr Bool
t =
bool True
f : Expr Bool
f =
bool False
zero : Expr Int
zero =
I refl 0
one : Expr Int
one =
I refl 1
big : Expr Int
big =
add
(cond (eq (num 3) (add (num 1) (num 2)))
(mul (num 3) (num 2))
(num 12)
)
(num 1)
-- EVALUATE ME BABY!
main = Html.text <| toString <| evalInt big
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment