# Summer school 2008:Alternate typed arithmetic expressions with sums

 This is Literate TwelfCode: hereStatus: %% 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)).```

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

eval/val
: eval (ret V) V.

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

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

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

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

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

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

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

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