•Predicate Proust with Equality, Typed Racket
Predicate Proust with Equality, Typed Racket
8.14.900

Predicate Proust with Equality, Typed Racket🔗

Here’s an updated version of Predicate Proust with Equality; it’s written in Typed Racket, to help you understand it, it does a TINY additional amount of error checking in the parser by prohibiting the use of e.g. λ as a variable name, and it refactors ‘reduce‘ to accept a list of bound variable names rather than a context.

I also changed the ‘reduce‘ rule for unbound variables to signal an error; I’m not confident this is correct.

Here’s a download link for this code: ./proust-pred-eq.rkt

  #lang typed/racket
  ; file contains Unicode characters - download rather than cut/paste from browser
   
  (provide def check-one reduce-one clear-defs parse-expr reduce type-check type-synth)
   
  ;; proust-pred-eq: for-all, equality.
  ;; Prabhakar Ragde (September 2021)
  ;; with contributions from Astra Kolomatskaia
   
  ;; Grammar:
   
  ;; expr = (λ x => expr)             ; lambda abstraction
  ;;      | (expr expr)               ; function application
  ;;      | x                         ; variable
  ;;      | (expr : expr)             ; expression annotated with type
  ;;      | (∀ (x : expr) -> expr)    ; dependent function type
  ;;      | (expr -> expr)            ; special case equiv to (∀ (_ : expr) -> expr)
  ;;      | Type                      ; the type of types
  ;;      | (expr = expr)             ; equality types
  ;;      | (eq-refl x)               ; equality introduction
  ;;      | (eq-elim expr expr expr expr expr) ; equality elimination
   
   
  ;; Structures for Expr (abstract syntax tree representing terms).
   
  (define-type Term (U Symbol Lam App Ann Arrow Type Teq Eq-refl Eq-elim))
  (struct Lam ([var : Symbol] [body : Term]) #:transparent)
  (struct App ([rator : Term] [rand : Term]) #:transparent)
  (struct Ann ([expr : Term] [type : Term]) #:transparent)
  (struct Arrow ([var : Symbol] [domain : Term] [range : Term]) #:transparent)
  (struct Type () #:transparent)
  (struct Teq ([left : Term] [right : Term]) #:transparent)
  (struct Eq-refl ([val : Term]) #:transparent)
  (struct Eq-elim ([x : Term] [P : Term] [px : Term] [y : Term] [peq : Term]) #:transparent)
   
   
  ;; A Context is a (Listof (List Symbol Expr))
  ;; association list mapping variables to expressions.
  (define-type Context (Listof (List Symbol Term)))
  (define (ctx-bind-name [pr : (List Symbol Term)]) : Symbol (first pr))
   
  ;; Parsing
   
  ;; parse-expr : sexp -> Expr
   
  (define (parse-expr [s : Sexp]) : Term
    (match s
      [`(λ ,(? legal-id? x) => ,e) (Lam x (parse-expr e))]
      [`(λ ,(? legal-id? x) ,(? legal-id? xs) ... => ,e)
       ;; cast must succeed by nature of match:
       (Lam x (parse-expr `(λ ,@(cast xs (Listof Sexp)) => ,e)))]
      [`(∀ (,(? legal-id? x) : ,t) -> ,e) (Arrow x (parse-expr t) (parse-expr e))]
      [`(∀ (,(? legal-id? x) : ,t) ,(? list? a) ... -> ,e) (Arrow x (parse-expr t) (parse-expr `(∀ ,@(cast a (Listof Sexp)) -> ,e)))]
      [`(,t1 -> ,t2) (Arrow '_ (parse-expr t1) (parse-expr t2))]
      [`(,t1 -> ,t2 -> ,r ...) (Arrow '_ (parse-expr t1) (parse-expr `(,t2 -> ,@r)))]
      [`(,e : ,t) (Ann (parse-expr e) (parse-expr t))]
      ['Type (Type)]
      [`(eq-refl ,a) (Eq-refl (parse-expr a))]
      [`(eq-elim ,e1 ,e2 ,e3 ,e4 ,e5)
          (Eq-elim (parse-expr e1) (parse-expr e2)  (parse-expr e3)  (parse-expr e4)  (parse-expr e5))]
      [`(,e1 = ,e2) (Teq (parse-expr e1) (parse-expr e2))]
      [`(,e1 ,e2) (App (parse-expr e1) (parse-expr e2))]
      [`(,e1 ,e2 ,e3 ,r ...) (parse-expr `((,e1 ,e2) ,e3 ,@r))]
      ['_ (error 'parse "cannot use underscore\n")]
      [(? symbol? x)
       (cond [(member x keywords)
              (error 'parse-expr "expected legal identifier, got: ~e" x)]
             [else x])]
      [else (error 'parse "bad syntax: ~a\n" s)]))
   
  (: legal-id? (Any -> Boolean : #:+ Symbol))
  (define (legal-id? x)
    (and (symbol? x) (not (member x keywords))))
   
  (define keywords : (Listof Symbol) '(∀ λ -> : = Type))
   
  ;; Unparsing, that is, pretty-printing.
   
  ;; pretty-print-expr : Expr -> String
   
  (define (pretty-print-expr [e : Term]) : String
    (match e
      [(Lam x b) (format "(λ ~a => ~a)" x (pretty-print-expr b))]
      [(App e1 e2) (format "(~a ~a)" (pretty-print-expr e1) (pretty-print-expr e2))]
      [(? symbol? x) (symbol->string x)]
      [(Ann e t) (format "(~a : ~a)" (pretty-print-expr e) (pretty-print-expr t))]
      [(Arrow '_ t1 t2) (format "(~a -> ~a)" (pretty-print-expr t1) (pretty-print-expr t2))]
      [(Arrow x t1 t2) (format "(∀ (~a : ~a) -> ~a)" x (pretty-print-expr t1) (pretty-print-expr t2))]
      [(Type) "Type"]
      [(Eq-refl a) (format "(eq-refl ~a)" (pretty-print-expr a))]
      [(Eq-elim e1 e2 e3 e4 e5)
        (format "(eq-elim ~a ~a ~a ~a ~a)" (pretty-print-expr e1) (pretty-print-expr e2)
                (pretty-print-expr e3) (pretty-print-expr e4) (pretty-print-expr e5))]
      [(Teq e1 e2) (format "(~a = ~a)" (pretty-print-expr e1) (pretty-print-expr e2))]))
   
  ;; pretty-print-context : Context -> String
   
   
  (define (pretty-print-context [ctx : Context]) : String
    (cond
      [(empty? ctx) ""]
      [else (string-append (format "\n~a : ~a" (first (first ctx)) (pretty-print-expr (second (first ctx))))
                           (pretty-print-context (rest ctx)))]))
   
  ;; Substitution
  ;; subst : Var Expr Expr -> Expr
   
  (define (subst [oldx : Symbol] [newx : Term] [expr : Term]) : Term
    (match expr
      [(? symbol? x) (if (equal? x oldx) newx x)]
      [(Arrow '_ t w) (Arrow '_ (subst oldx newx t) (subst oldx newx w))]
      [(Arrow x t w)
         (cond
           [(equal? x oldx) expr]
           [(side-cond? x (list newx) false)
              (define repx (refresh x (list newx w)))
              (Arrow repx (subst oldx newx t) (subst oldx newx (subst x repx w)))]
           [else (Arrow x (subst oldx newx t) (subst oldx newx w))])]
      [(Lam '_ b) (Lam '_ (subst oldx newx b))]
      [(Lam x b)
         (cond
           [(equal? x oldx) expr]
           [(side-cond? x (list newx) false)
              (define repx (refresh x (list newx b)))
              (Lam repx (subst oldx newx (subst x repx b)))]
           [else (Lam x (subst oldx newx b))])]
      [(App f a) (App (subst oldx newx f) (subst oldx newx a))]
      [(Ann e t) (Ann (subst oldx newx e) (subst oldx newx t))]
      [(Type) (Type)]
      [(Eq-refl a) (Eq-refl (subst oldx newx a))]
      [(Eq-elim e1 e2 e3 e4 e5)
        (Eq-elim (subst oldx newx e1) (subst oldx newx e2) (subst oldx newx e3)
                 (subst oldx newx e4) (subst oldx newx e5))]
      [(Teq a b) (Teq (subst oldx newx a) (subst oldx newx b))]))
   
  ;; Helpers for substitution
   
  ;; refresh : Var (Listof Expr) -> Var
   
  (define (refresh [x : Symbol] [lst : (Listof Term)]) : Symbol
    (if (side-cond? x lst true) (refresh (freshen x) lst) x))
   
  (define (freshen [x : Symbol]) : Symbol
    (string->symbol (string-append (symbol->string x) "_")))
   
  ;; checks if variable x occurs free in lst (list of expressions)
  ;; and, when check-binders? is #t, if x has a binding occurrence in lst
   
  (define (side-cond? [x : Symbol] [lst : (Listof Term)] [check-binders? : Boolean]) : Boolean
    (ormap (lambda ([expr : Term]) (sc-helper x expr check-binders?)) lst))
   
  (define (sc-helper [x : Symbol] [expr : Term] [check-binders? : Boolean]) : Boolean
    (match expr
      [(? symbol? y) (equal? x y)]
      [(Arrow '_ tt tw) (side-cond? x (list tt tw) check-binders?)]
      [(Arrow y tt tw)
         (cond
           [check-binders? (or (equal? x y) (side-cond? x (list tt tw) check-binders?))]
           [else (if (equal? x y) false (side-cond? x (list tt tw) check-binders?))])]
      [(Lam '_ b) (sc-helper x b check-binders?)]
      [(Lam y b)
         (cond
           [check-binders? (or (equal? x y) (sc-helper x b check-binders?))]
           [else (if (equal? x y) false (sc-helper x b check-binders?))])]
      [(App f a) (side-cond? x (list f a) check-binders?)]
      [(Ann e t) (side-cond? x (list e t) check-binders?)]
      [(Type) false]
      [(Eq-refl a) (sc-helper x a check-binders?)]
      [(Eq-elim e1 e2 e3 e4 e5)
        (side-cond? x (list e1 e2 e3 e4 e5) check-binders?)]
      [(Teq a b) (side-cond? x (list a b) check-binders?)]))
   
  ;; Code for finding fresh variable name not already used in a context
  ;; (similar to refresh, above) to be used later in type checking/synthesis
   
  (define (used-in-ctx? [ctx : Context] [x : Symbol]) : Boolean
    (or (and (assoc x deftypes) #t) (ormap (λ ([p : (List Symbol Term)]) (side-cond? x (rest p) false)) ctx)))
   
  (define (refresh-with-ctx [ctx : Context] [x : Symbol] [lst : (Listof Term)]) : Symbol
    (if (or (side-cond? x lst true) (used-in-ctx? ctx x)) (refresh-with-ctx ctx (freshen x) lst) x))
   
  ;; Alpha equivalence (produces #t/#f)
   
  (define (alpha-equiv? [e1 : Term] [e2 : Term]) (ae-helper e1 e2 empty))
   
  ;; vmap is association list mapping variables in e1 to variables in e2
   
  (define (ae-helper [e1 : Term] [e2 : Term] [vmap : (Listof (List Symbol Symbol))]) : Boolean
    (match (list e1 e2)
      [(list (? symbol? x1) (? symbol? x2))
         (define xm1 (assoc x1 vmap))
         (equal? (if xm1 (second xm1) x1) x2)]
      [(list (Lam x1 b1) (Lam x2 b2)) (ae-helper b1 b2 (cons (list x1 x2) vmap))]
      [(list (App f1 a1) (App f2 a2)) (and (ae-helper f1 f2 vmap) (ae-helper a1 a2 vmap))]
      [(list (Ann e1 t1) (Ann e2 t2)) (and (ae-helper e1 e2 vmap) (ae-helper t1 t2 vmap))]
      [(list (Arrow x1 t1 w1) (Arrow x2 t2 w2))
         (and (ae-helper t1 t2 (cons (list x1 x2) vmap)) (ae-helper w1 w2 (cons (list x1 x2) vmap)))]
      [(list (Type) (Type)) true]
      [(list (Eq-refl x1) (Eq-refl x2)) (ae-helper x1 x2 vmap)]
      [(list (Eq-elim x1 P1 px1 y1 peq1) (Eq-elim x2 P2 px2 y2 peq2))
         (and (ae-helper x1 x2 vmap) (ae-helper P1 P2 vmap) (ae-helper px1 px2 vmap)
              (ae-helper y1 y2 vmap) (ae-helper peq1 peq2 vmap))]
      [(list (Teq a1 b1) (Teq a2 b2))
         (and (ae-helper a1 a2 vmap) (ae-helper b1 b2 vmap))]
      [else false]))
   
  ;; Reduction
   
  ;; reduce: bound-vars Expr -> Expr
  ;; Reduces an expression by recursively looking up definitions
  ;; and doing substitution for applications
   
  (define (reduce [ctx : (Listof Symbol)] [expr : Term]) : Term
    (match expr
      [(? symbol? x)
       (cond
         [(member x ctx) x]
         [(assoc x defs) => (lambda (p) (reduce ctx (second p)))]
         ;; this is an error, right?
         [else (error 'reduce "unbound variable: ~e" x)])]
      [(Arrow '_ a b)
       (Arrow '_ (reduce ctx a) (reduce ctx b))]
      [(Arrow x a b)
       (define ra (reduce ctx a))
       (define rb (reduce (cons x ctx) b))
       (Arrow x ra rb)]
      [(Lam '_ b) (Lam '_ (reduce ctx b))]
      [(Lam x b) (Lam x (reduce (cons x ctx) b))]
      [(App f a)
       (define fr (reduce ctx f))
       (define fa (reduce ctx a))
       (match fr
         [(Lam x b) (reduce ctx (subst x fa b))]
         [else (App fr fa)])]
      [(Ann e t) (reduce ctx e)]
      [(Type) (Type)]
      [(Eq-refl x) (Eq-refl (reduce ctx x))]
      [(Eq-elim x P px y peq)
       (define peqr (reduce ctx peq))
       (match peqr
         [(Eq-refl _) (reduce ctx px)]
         [else (Eq-elim (reduce ctx x) (reduce ctx P) (reduce ctx px) (reduce ctx y) peqr)])]
      [(Teq a b) (Teq (reduce ctx a) (reduce ctx b))]))
   
  ;; Definitional equality
  (define (equiv? [ctx : Context] [e1 : Term] [e2 : Term]) (alpha-equiv? (reduce (map ctx-bind-name ctx) e1) (reduce (map ctx-bind-name ctx) e2))) 
   
  ;; This is the heart of the verifier.
  ;; type-check and type-synth are mutually-recursive functions that
  ;;   check an expression has a type in a context, and
  ;;   synthesize the type of an expression in a context, respectively.
  ;; They implement bidirectional type checking.
   
  ;; type-check : Context Expr Expr -> boolean
  ;; Produces true if expr has type t in context ctx (or error if not).
   
  (define (type-check [ctx : Context] [expr : Term] [type : Term]) : True
    (match expr
      [(Lam x b)
         (type-check ctx type (Type))
         (define tyr (reduce (map ctx-bind-name ctx) type))
         (match tyr
           [(Arrow x1 tt tw)
              (match (list x x1)
                [(list '_ '_) (type-check ctx b tw)]
                [(list '_ x1)
                   (cond
                     [(nor (side-cond? x1 (list b) false) (used-in-ctx? ctx x1))
                        (type-check (cons (list x1 tt) ctx) b tw)]
                     [else
                        (define newx (refresh-with-ctx ctx x1 (list b tyr)))
                        (type-check (cons (list newx tt) ctx) b (subst x1 newx tw))])]
                [(list x '_)
                   (cond
                     [(nor (side-cond? x (list tyr) false) (used-in-ctx? ctx x))
                        (type-check (cons (list x tt) ctx) b tw)]
                     [else
                        (define newx (refresh-with-ctx ctx x (list b tyr)))
                        (type-check (cons (list newx tt) ctx) (subst x newx b) tw)])]
                [(list x x1)
                   (cond
                     [(and (equal? x x1) (not (used-in-ctx? ctx x1))) (type-check (cons (list x tt) ctx) b tw)]
                     [(nor (side-cond? x (list tyr) true) (used-in-ctx? ctx x))
                        (type-check (cons (list x tt) ctx) b (subst x1 x tw))]
                     [else
                        (define newx (refresh-with-ctx ctx x (list expr tyr)))
                        (type-check (cons (list newx tt) ctx) (subst x newx b) (subst x1 newx tw))])])]
           [else (cannot-check ctx expr type)])]
      [else (if (equiv? ctx (type-synth ctx expr) type) true (cannot-check ctx expr type))]))
   
  ;; cannot-check: Context Expr Type -> void
  ;; Prints generic error message for type-check
  ;; Error messages can be improved by replacing uses of this with something more specific
   
  (define (cannot-check [ctx : Context] [e : Term] [t : Term])
    (error 'type-check "cannot typecheck ~a as ~a in context:\n~a"
           (pretty-print-expr e) (pretty-print-expr t) (pretty-print-context ctx)))
   
  ;; type-synth : Context Expr -> Type
  ;; Produces type of expr in context ctx (or error if can't)
   
  (define (type-synth [ctx : Context] [expr : Term]) : Term
    (match expr
      [(? symbol? x)
         (cond
           [(assoc x ctx) => second]
           [(assoc x deftypes) => second]
           [else (cannot-synth ctx expr)])]
      [(Lam x b) (cannot-synth ctx expr)]
      [(App f a) 
         (define t1 (reduce (map ctx-bind-name ctx) (type-synth ctx f)))
         (match t1
           [(Arrow '_ tt tw) #:when (type-check ctx a tt) tw]
           [(Arrow x tt tw) #:when (type-check ctx a tt) (subst x a tw)]
           [else (cannot-synth ctx expr)])]
      [(Ann e t) (type-check ctx t (Type)) (type-check ctx e t) t]
      [(Arrow '_ tt tw)
         (type-check ctx tt (Type))
         (type-check ctx tw (Type))
         (Type)]
      [(Arrow x tt tw)
         (type-check ctx tt (Type))
         (type-check (cons `(,x ,tt) ctx) tw (Type))
         (Type)]
      [(Type) (Type)]
      [(Teq e1 e2)
         (define t1 (type-synth ctx e1))
         (type-check ctx e2 t1)
         (Type)]
      [(Eq-refl x) (type-synth ctx x) (Teq x x)]
      [(Eq-elim x P px y peq)
         (define A (type-synth ctx x))
         (type-check ctx P (Arrow '_ A (Type)))
         (define Pann (Ann P (Arrow '_ A (Type))))
         (type-check ctx px (App Pann x))
         (type-check ctx y A)
         (type-check ctx peq (Teq x y))
         (App Pann y)]
      [other
       (cannot-synth ctx expr)]))
   
  ;; cannot-synth: Context Expr -> void
  ;; Prints generic error message for type-synth
  ;; Again, can improve things by being more specific at use sites
   
  (define (cannot-synth [ctx : Context] [expr : Term]) : Nothing
    (error 'type-synth "cannot infer type of ~a in context:\n~a"
           (pretty-print-expr expr) (pretty-print-context ctx)))
   
  ;; Definitions
   
  ;; Global variables
   
  (define defs : Context empty)
  (define deftypes : Context empty)
   
  ;; def : symbol Expr -> void
  ;; Side effect is to mutate global defs, deftypes to include new def if it checks out
   
  (define (def [name : Symbol] [expr : Sexp])
    (when (assoc name defs) (error 'def "~a already defined" name))
    (define e (parse-expr expr))
    (define et (type-synth empty e))
    (match e
      [(Ann ex tp) (set! defs (cons (list name ex) defs))
                   (set! deftypes (cons (list name tp) deftypes))]
      [else (set! defs (cons (list name e) defs))
            (set! deftypes (cons (list name et) deftypes))]))
   
  (define (clear-defs) (set! defs empty) (set! deftypes empty))
   
  (define (check-one [expr : Sexp])
    (printf "~a\n" (pretty-print-expr (type-synth empty (parse-expr expr)))))
   
  (define (reduce-one [expr : Sexp])
     (printf "~a\n" (pretty-print-expr (reduce empty (parse-expr expr)))))
   
  (require typed/rackunit)
   
  (check-true (type-check `((A ,(Type))) 'A (Type)))
   
  (check-equal? (parse-expr '(∀ (A : Type) -> (A -> A)))
                (Arrow 'A (Type) (Arrow '_ 'A 'A)))
   
  (check-equal? (parse-expr '(λ a => a))
                (Lam 'a 'a))
   
  ;; should succeed:
   
  (check-one '((λ a => (λ b => b)) : (∀ (A : Type) -> (A -> A))))
  (check-one '((λ a b c a2b b2c a => (b2c (a2b a))) : (∀ (a : Type) -> (∀ (b : Type) -> (∀ (c : Type) -> ((a -> b) -> (b -> c) -> (a -> c)))))))