# Summer school 2008:Typed arithmetic expressions

 This is Literate TwelfCode: hereStatus: %% OK %% Output: here.

Next, we add another base type besides numbers.

Natural numbers and addition are the same as before:

```nat : type.             %name nat M.
z : nat.
s : nat -> nat.

add : nat -> nat -> nat -> type.

%worlds () (add _ _ _).
%total M (add M _ _).```

## Strings and append

Strings and append are analogous

```char : type.				%name char X.
a : char.
b : char.

str : type.				%name str S.
emp : str.
cons : char -> str -> str.

cat : str -> str -> str -> type.
%mode cat +S1 +S2 -S3.

cat/e : cat emp S S.
cat/c : cat (cons X S1) S2 (cons X S3) <- cat S1 S2 S3.

%worlds () (cat _ _ _).
%total S (cat S _ _).```

## Typed expressions

There are two types:

```tp : type.				%name tp T.
number : tp.
string : tp.```

We use an intrinsic encoding, where only well-typed terms are represented. Another way of looking at this is that we skip raw syntax and work directly with typing derivations. This works well for simply-typed languages, where the raw syntax for well-typed terms is isomorphic to its typing derivations.

```val : tp -> type.			%name val V.  %postfix 1 val.
num : nat -> number val.
lit : str -> string 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.```

```ans : tp -> type.			%name ans A.  %postfix 1 ans.
anum : nat -> number ans.
astr : str -> string ans.```

Evaluation relates an expression to an answer of the same type, guaranteeing type preservation.

Because of Twelf's implicit argument mechanism, the cases for numbers and let-binding are unchanged.

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

eval/val/num
: eval (ret (num N)) (anum N).

eval/val/str
: eval (ret (lit S)) (astr S).

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

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

eval/let/num
: eval (let E1 ([x] E2 x)) A
<- eval E1 (anum N)
<- eval (E2 (num N)) A.

eval/let/str
: eval (let E1 ([x] E2 x)) A
<- eval E1 (astr S)
<- eval (E2 (lit S)) A.

%worlds () (eval _ _).
%total E (eval E _).```

Note: in this example ans is isomorphic to val, so we can simplify things slightly by not making the distinction. (See Typed arithmetic expressions (value)).