dvanhorn

#lang typed/racket
(define-type Term (U VAR LAM APP))
(struct: VAR ([x : String]) #:transparent)
(struct: LAM ([x : String] [m0 : Term]) #:transparent)
(struct: APP ([m1 : Term] [m2 : Term]) #:transparent)

(define-type Sem (U Ind Fun))

(define-type Env (U R1 R2))
(struct: R1 ())

dvanhorn

#lang typed/racket
(define-type Term (U VAR LAM APP))
(struct: VAR ([x : String]) #:transparent)
(struct: LAM ([x : String] [m0 : Term]) #:transparent)
(struct: APP ([m1 : Term] [m2 : Term]) #:transparent)

(define-type Sem (U TM FUN))
(struct: TM ([l : (Integer -> Term)]))
(struct: FUN ([f : ((-> Sem) -> Sem)]))

dvanhorn

#lang racket

;; Mogensen-Scott encoding
(define-syntax encode
  (syntax-rules (λ)
    [(encode (λ (x) e))
     (λ (VAR) (λ (APP) (λ (LAM) (LAM (λ (x) (encode e))))))]
    [(encode (e0 e1))
     (λ (VAR) (λ (APP) (λ (LAM) ((APP (encode e0)) (encode e1)))))]
    [(encode x)