Summer school 2008:Typed arithmetic expressions

This is Literate Twelf Code: here Status: %% OK %% Output: here.

Summer school 2008

Previous: Arithmetic expressions with let-binding (hypothetical evaluation)

Next: Typed arithmetic expressions (extrinsic encoding)

Next, we add another base type besides numbers.

Numbers and addition

Natural numbers and addition are the same as before:

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

add : nat -> nat -> nat -> type.
%mode add +M +N -P.

add/z : add z N N.
add/s : add (s M) N (s P) <- add M N P.

%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.

Answers are typed as well:

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)
      <- add N1 N2 N.

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)).

Summer school 2008

Previous: Arithmetic expressions with let-binding (hypothetical evaluation)

Next: Typed arithmetic expressions (extrinsic encoding)