Summer school 2008:Alternate typed arithmetic expressions with sums

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.
Summer school 2008
Previous: Typed arithmetic expressions

Arithmetic expressions with pairs and sums. (There are two alternate solutions, one by William (involving output factoring) and one by Dan (involving output factoring and identity types).)

Numbers and strings are unchanged.

Typed expressions

Add a type for disjoint sums:

tp : type.				%name tp T.
number : tp.
string : tp.
prod   : tp -> tp -> tp.
sum    : tp -> tp -> tp.

Add injections as values, and case as an expression. Note that you can only case on a value. This makes evaluation slightly easier; for versions with expression-case as a primitive; see the above alternate solutions.

val : tp -> type.			%name val V.  %postfix 1 val.
num : nat -> number val.
lit : str -> string val.
pair : T val -> U val -> (prod T U) val.
inl : T val -> (sum T U) val.
inr : U val -> (sum T U) val.

exp : tp -> type.			%name exp E.  %postfix 1 exp.
ret : T val -> T exp.
plus : number exp -> number exp -> number exp.
append : string exp -> string exp -> string exp.
let : T exp -> (T val -> U exp) -> U exp.
fst : (prod T U) exp -> T exp.
snd : (prod T U) exp -> U exp.
case : (sum T U) val -> (T val -> V exp) -> (U val -> V exp) -> V exp.

Note that if we want to case on an expression, we can let-bind it:

ecase : (sum T U) exp -> (T val -> V exp) -> (U val -> V exp) -> V exp 
            = [esum] [e1] [e2] (let esum ([x] case x e1 e2)).

Add eval cases for case.

eval : T exp -> T val -> type.
%mode eval +E1 -E2.

   : eval (ret V) V.

   : eval (plus E1 E2) (num N)
      <- eval E1 (num N1)
      <- eval E2 (num N2)
      <- add N1 N2 N.

   : eval (append E1 E2) (lit S)
      <- eval E1 (lit S1)
      <- eval E2 (lit S2)
      <- cat S1 S2 S.

   : eval (let E1 ([x] E2 x)) A
      <- eval E1 V
      <- eval (E2 V) A.

   : eval (fst E) A
      <- eval E (pair A _).

   : eval (snd E) B
      <- eval E (pair _ B).

  : eval (case (inl A) ([x] E1 x) _) A1
      <- eval (E1 A) A1.

  : eval (case (inr A) _ ([x] E2 x)) A2
      <- eval (E2 A) A2.

%worlds () (eval _ _).
%total E (eval E _).
Summer school 2008
Previous: Exercises 1