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