A simple language with sums and products

sumprod.rkt

#lang plait

(define-type Type
  [TNum]
  [TProd (t1 : Type) (t2 : Type)]
  [TSum (t1 : Type) (t2 : Type)])

(define-type Exp
  [let1E (x : Symbol) (e1 : Exp) (e2 : Exp)]
  [varE (x : Symbol)]
  [numE (n : Number)]
  [fstE (e : Exp)]
  [sndE (e : Exp)]
  [pairE (e1 : Exp) (e2 : Exp)]
  [leftE (t : Type) (e : Exp)]
  [rightE (t : Type) (e : Exp)]
  [matchE (x : Symbol) (e : Exp) (left : Exp) (right : Exp)])

(define-type Value
  [numV (n : Number)]
  [pairV (fst : Value) (snd : Value)]
  ; tag is #t if left, #f if right
  [sumV (tag : Boolean) (v : Value)])

(define-type-alias Env (Hashof Symbol Value))
(define mt-env (hash empty)) ;; "empty environment"

(define (lookup (n : Env) (s : Symbol))
  (type-case (Optionof Value) (hash-ref n s)
             [(none) (error 'runtime "not bound")]
             [(some v) v]))

(extend : (Env Symbol Value -> Env))
(define (extend old-env new-name value)
  (hash-set old-env new-name value))

(interp : (Env Exp -> Value))
(define (interp env e)
  (type-case Exp e
             [(let1E x e1 e2)
              (interp (extend env x (interp env e1)) e2)]
             [(varE s) (lookup env s)]
             [(numE n) (numV n)]
             [(fstE e1)
              (type-case Value (interp env e1)
                         [(pairV fst snd) fst]
                         [else (error 'runtime "invalid")])]
             [(sndE e1)
              (type-case Value (interp env e1)
                         [(pairV fst snd) snd]
                         [else (error 'runtime "invalid")])]
             [(pairE e1 e2) (pairV (interp env e1) (interp env e2))]
             [(leftE t e) (sumV #t (interp env e))]
             [(rightE t e) (sumV #f (interp env e))]
             [(matchE x e1 leftE rightE)
              (type-case Value (interp env e1)
                         [(sumV tag v)
                          (if tag
                              (interp (extend env x v) leftE)
                              (interp (extend env x v) rightE))]
                         [else (error 'runtime "invalid")])]))

(test (interp mt-env (let1E 'x (pairE (numE 10) (numE 20))
                            (sndE (varE 'x)))) (numV 20))
(test (interp mt-env (let1E 'x (leftE (TSum (TNum) (TNum)) (numE 10))
                            (matchE 'match (varE 'x) (numE 0) (numE 3)))) (numV 0))



(define-type-alias TEnv (Hashof Symbol Type))
(define mt-tenv (hash empty)) ;; "empty environment"

(define (tlookup (n : TEnv) (s : Symbol))
  (type-case (Optionof Type) (hash-ref n s)
             [(none) (error 'type-error "unrecognized symbol")]
             [(some v) v]))

(textend : (TEnv Symbol Type -> TEnv))
(define (textend old-env new-name value)
  (hash-set old-env new-name value))


(define (type-of env e)
  (type-case Exp e
             [(varE s) (tlookup env s)]
             [(numE n) (TNum)]
             [(let1E x e1 e2)
              (type-of (textend env x (type-of env e1)) e2)]
             [(fstE e) (type-case Type (type-of env e)
                                  [(TProd t1 t2) t1]
                                  [else (error 'type-error "invalid prod")])]
             [(sndE e) (type-case Type (type-of env e)
                                  [(TProd t1 t2) t2]
                                  [else (error 'type-error "invalid prod")])]
             [(pairE e1 e2) (TProd (type-of env e1) (type-of env e2))]
             [(leftE t e)
              (type-case Type t
                         [(TSum l r)
                          (if (equal? (type-of env e) l)
                              t
                              (error 'type-error "invalid sum"))]
                         [else (error 'type-error "invalid sum")])]
             [(rightE t e)
              (type-case Type t
                         [(TSum l r)
                          (if (equal? (type-of env e) r)
                              t
                              (error 'type-error "invalid sum"))]
                         [else (error 'type-error "invalid sum")])]
             [(matchE x e eL eR)
              (type-case Type (type-of env e)
                         [(TSum tl tr)
                          (let [(t-left (type-of (extend env x tl) eL))
                                (t-right (type-of (extend env x tr) eR))]
                            (if (equal? t-left t-right)
                                t-left
                                (error 'type-error "match arms not same type")))]
                         [else (error 'type-error "invalid match")])]))