typed-ite.rkt

#lang racket
(require rackunit)

;;; type expr =
;;;   | eadd of expr * expr
;;;   | enum of number
;;;   | ebool of boolean
;;;   | eite of expr * expr * expr
(struct eadd (e1 e2) #:transparent)
(struct enum (n) #:transparent)
(struct ebool (b) #:transparent)
(struct eite (grd thn els) #:transparent)

;;; type value =
;;;    | vbool of bool
;;;    | vnum of num
(struct vbool (b) #:transparent)
(struct vnum (n) #:transparent)

;;; type itetyp =
;;;  | tnum
;;;  | tbool
(struct tnum () #:transparent)
(struct tbool () #:transparent)

;;; value->number : value -> number
(define (value->number v)
  (match v
    [(vnum n) n]
    [_ (error "not a number")]))


;;; value->bool : value -> bool
(define (value->bool v)
  (match v
    [(vbool b) b]
    [_ (error "not a number")]))


;;; interp : expr -> value
;;; evaluates an expression to a number
(define (interp e)
  (match e
    [(eadd e1 e2) (vnum (+ (value->number (interp e1)) ((value->number (interp e2)))))]
    [(enum n) (vnum n)]
    [(ebool b) (vbool b)]
    [(eite g thn els)
     (if (value->bool (interp g))
                      (interp thn)
                      (interp els))]))


;;; declare a type exception that is a subtype of exn:fail
(struct exn:type exn:fail ())
(define (raise-type-error)
  (raise (exn:type
          "type error"
          (current-continuation-marks))))

(define (type-of e)
  (match e
    [(enum n) (tnum)]
    [(ebool b) (tbool)]
    [(eadd e1 e2)
     (if (and (equal? (type-of e1) (tnum))
              (equal? (type-of e2) (tnum)))
         (tnum)
         (raise-type-error))]
    [(eite g thn els)
     (if (and (equal? (type-of g) (tbool))
              (equal? (type-of thn) (type-of els)))
         (type-of thn)
         (raise-type-error))]))


;;; returns #t if e is well-typed, #f otherwise
(define (type-check? e)
  (with-handlers ([exn:type? (lambda _ #f)])
    (let [(_ (type-of e))]
      #t)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; tests

;;; test for expressivity
(check-equal? (type-check? (eite (ebool #t) (enum 10) (enum 20))) #t)
(check-equal? (type-check? (eite (eite (ebool #t) (ebool #f) (ebool #t)) (enum 10) (enum 20))) #t)

;;; test for soundness
(check-equal? (type-check? (eite (enum 10) (ebool #t) (ebool #f))) #f)
(check-equal? (type-check? (eite (eite (ebool #t) (enum 10) (enum 30)) (ebool #t) (ebool #f))) #f)
(check-equal? (type-check? (eite (ebool #t) (ebool #t) (enum 30))) #f)