Derived Forms

Example

Define unless

Concrete Syntax:

unless c e 
-- or
e unless c

Abstract Syntax:

Unless :: BBAE -> BBAE -> BBAE

Inference Rules:

UnlessF

\frac{c ⇓ False e ⇓ v}{unless c e ⇓ False}

UnlessT

\frac{c ⇓ True}{unless c e ⇓ False}

Evaluation:

eval (Unless c e) = do { (BoolV b) <- eval c;
                         if b then return (BoolV False) else eval e
                        }

Elaboration Function

elaboration function

host language - Target language for translation
embedded language - New language with extensions

Writing a type checker should be done for the embedded language not the host language

Note

This is useful because you can build a small core language, and build features around that language that transpile to the core language. If we can verify the core language, any wrapper around it will also not fail.