TypeSafeEval.elm

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