Summer school 2008:Typed arithmetic expressions with sums 2

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

Summer school 2008

Previous: Typed arithmetic expressions

Arithmetic expressions with pairs and sums. (This solution involves output factoring, but no identity types. Dan posted a solution involving identity types, and Chris posted a solution that avoids output factoring.)

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.

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.

For technical reasons, we bundle the branches of the case into a separate term with type cases; this makes the termination order more evident to Twelf. An element of "cases T U V" is the branches for a "sum T U" whose result has tp "V".

cases : tp -> tp -> tp -> type.
cases/i : (T val -> V exp) -> (U val -> V exp) -> cases T U V.
case : (sum T U) exp -> cases T U V -> V exp.

Add eval cases for case.

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

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

For "case" evaluation, we need an auxiliary relation "evalcase" to branch on inl vs. inr (output factoring).

evalcase : (sum T U) val -> cases T U S -> S val -> type.
%mode evalcase +V +Cases -A.

eval/case
  : eval (case E Cases) A
      <- eval E V
      <- evalcase V Cases A.

evalcase/inl
   : evalcase (inl V1) (cases/i ([x] F1 x) ([y] F2 y)) A
      <- eval (F1 V1) A.

evalcase/inr
   : evalcase (inr V2) (cases/i ([x] F1 x) ([y] F2 y)) A
      <- eval (F2 V2) A.

Then we use mutual induction to show evaluation total.

%worlds () (eval _ _) (evalcase _ _ _).
%total (E Cases) (eval E _) (evalcase _ Cases _).

Summer school 2008

Previous: Exercises 1