#lang 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 equiv?) ;; proust-pred-forall-db: for-all, with deBruijn indices ;; Prabhakar Ragde (September 2021) ;; 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 ;; Structures for Expr (abstract syntax tree representing terms). (struct Lam (namehint body) #:transparent) (struct App (rator rand) #:transparent) (struct Var (index) #:transparent) (struct Def (name) #:transparent) (struct Ann (expr type) #:transparent) (struct Arrow (namehint domain range) #:transparent) (struct Type () #:transparent) ;; A Context is a (Listof (List Symbol Expr)) ;; Association list mapping variables (represented by positions in a list) to expressions ;; The symbol is for printing. ;; Global variables (define defs empty) (define deftypes empty) ;; Parsing ;; parse-expr : sexp -> Expr (define (parse-expr s) (parse-expr-nlst s empty)) ;; parse-expr-nlst : sexp (Listof Symbol) -> Expr ;; helper that keeps a list of binder names in nlst (most recent first) (define (parse-expr-nlst s nlst) (match s [`(λ ,(? symbol? x) => ,e) (Lam x (parse-expr-nlst e (cons x nlst)))] [`(∀ (,(? symbol? x) : ,t) -> ,e) (Arrow x (parse-expr-nlst t nlst) (parse-expr-nlst e (cons x nlst)))] [`(∀ (,(? symbol? x) : ,t) ,(? list? a) ... -> ,e) (Arrow x (parse-expr-nlst t nlst) (parse-expr-nlst `(∀ ,@a -> ,e) (cons x nlst)))] [`(,t1 -> ,t2) (Arrow '_ (parse-expr-nlst t1 nlst) (parse-expr-nlst t2 (cons #f nlst)))] [`(,t1 -> ,t2 -> ,r ...) (Arrow '_ (parse-expr-nlst t1 nlst) (parse-expr-nlst `(,t2 -> ,@r) (cons #f nlst)))] [`(,e : ,t) (Ann (parse-expr-nlst e nlst) (parse-expr-nlst t nlst))] ['Type (Type)] [`(,e1 ,e2) (App (parse-expr-nlst e1 nlst) (parse-expr-nlst e2 nlst))] [`(,e1 ,e2 ,e3 ,r ...) (parse-expr-nlst `((,e1 ,e2) ,e3 ,@r) nlst)] ['_ (error 'parse "cannot use underscore\n")] [(? symbol? x) (cond [(list-index x nlst) => Var] [(assoc x defs) (Def x)] [else (error 'parse "unbound variable: ~a\n" x)])] [else (error 'parse "bad syntax: ~a\n" s)])) (define (list-index x lst) (list-index-helper x lst 0)) (define (list-index-helper x lst n) (cond [(empty? lst) #f] [(equal? x (first lst)) n] [else (list-index-helper x (rest lst) (add1 n))])) ;; Unparsing, that is, pretty-printing. ;; pretty-print-expr : Context Expr -> String (define (pretty-print-expr ctx e) (match e [(Lam x b) (define name (freshen x ctx)) (format "(λ ~a => ~a)" name (pretty-print-expr (cons (list name #f) ctx) b))] [(App e1 e2) (format "(~a ~a)" (pretty-print-expr ctx e1) (pretty-print-expr ctx e2))] [(Var n) (symbol->string (first (list-ref ctx n)))] [(Def x) (symbol->string x)] [(Ann e t) (format "(~a : ~a)" (pretty-print-expr ctx e) (pretty-print-expr ctx t))] [(Arrow '_ t1 t2) (format "(~a -> ~a)" (pretty-print-expr ctx t1) (pretty-print-expr (cons (list #f #f) ctx) t2))] [(Arrow x t1 t2) (define name (freshen x ctx)) (format "(∀ (~a : ~a) -> ~a)" name (pretty-print-expr ctx t1) (pretty-print-expr (cons (list name #f) ctx) t2))] [(Type) "Type"])) (define (freshen x ctx) (if (assoc x ctx) (freshen (string->symbol (string-append (symbol->string x) "_")) ctx) x)) ;; pretty-print-context : Context -> String (define (pretty-print-context ctx) (first (pretty-print-context-helper ctx))) ;; pretty-print-context-helper : Context -> (list String Context) (define (pretty-print-context-helper ctx) (cond [(empty? ctx) (list "" empty)] [else (match-define (list rst fctx) (pretty-print-context-helper (rest ctx))) (define firstname (freshen (first (first ctx)) fctx)) (define firsttype (pretty-print-expr fctx (second (first ctx)))) (list (string-append (format "\n~a : ~a" firstname firsttype) rst) (cons (list firstname firsttype) fctx))])) ;; substitution ;; based on PLFA (Wadler/Kokke) from an idea by McBride ;; A Var is a natural number (starting at 0) ;; ext : (Var -> Var) -> (Var -> Var) ;; Given vvmap which maps variables in context Γ to variables in context Δ, ;; produces the resulting map from variables in context Γ,B to variables in context Δ,B (define (ext vvmap) (lambda (v) (if (zero? v) 0 (add1 (vvmap (sub1 v)))))) ;; rename : (Var -> Var) Expr -> Expr ;; Given vvmap which maps variables in context Γ to variables in context Δ, ;; and expr in context Γ, produces the resulting expression in context Δ ;; (contexts are implicit, they're not needed in the computation) (define (rename vvmap expr) (match expr [(Lam x b) (Lam x (rename (ext vvmap) b))] [(App e1 e2) (App (rename vvmap e1) (rename vvmap e2))] [(Var n) (Var (vvmap n))] [(Def _) expr] [(Ann e t) (Ann (rename vvmap e) (rename vvmap t))] [(Arrow x t1 t2) (Arrow x (rename vvmap t1) (rename (ext vvmap) t2))] [(Type) expr])) ;; exts : (Var -> Expr) -> (Var -> Expr) ;; Given a map from variables to expressions in context Γ, ;; produces the resulting map from variables to expressions in context Γ,B (define (exts vtmap) (lambda (v) (if (zero? v) (Var 0) (rename add1 (vtmap (sub1 v)))))) ;; psubst: (Var -> Expr) Expr -> Expr ;; Given vtmap which maps variables to expressions in context Γ, ;; and expr in context Γ, produces the resulting expression (parallel substitution) (define (psubst vtmap expr) (match expr [(Lam x b) (Lam x (psubst (exts vtmap) b))] [(App e1 e2) (App (psubst vtmap e1) (psubst vtmap e2))] [(Var n) (vtmap n)] [(Def _) expr] [(Ann e t) (Ann (psubst vtmap e) (psubst vtmap t))] [(Arrow x t1 t2) (Arrow x (psubst vtmap t1) (psubst (exts vtmap) t2))] [(Type) expr])) ;; substitution for (Var 0) and shifting down of all other variables, ;; which is what's needed for beta-reduction (define (subst repl expr) (psubst (lambda (var) (if (zero? var) repl (Var (sub1 var)))) expr)) #| ;; McBride's original version with single traversal function (struct Kit (vr tm wk) #:transparent) (define (trav k tau expr) (match expr [(Lam x b) (Lam x (trav k (lift k tau) b))] [(App e1 e2) (App (trav k tau e1) (trav k tau e2))] [(Var n) ((Kit-tm k) (tau n))] [(Def _) expr] [(Ann e t) (Ann (trav k tau e) (trav k tau t))] [(Arrow x t1 t2) (Arrow x (trav k tau t1) (trav k (lift k tau) t2))] [(Type) expr])) (define (lift k tau) (lambda (var) (if (zero? var) ((Kit-vr k) var) ((Kit-wk k) (tau (sub1 var)))))) (define (rename rho) (lambda (expr) (trav (Kit identity Var add1) rho expr))) (define (psubst sigma expr) (trav (Kit Var identity (rename add1)) sigma expr)) (define (subst repl expr) (psubst (lift (Kit (lambda _ repl) Var Var) identity) expr)) ;; Version using arithmetic instead of add1/sub1 ;; Based on TaPL chapter 7 and the associated OCaml implementation (define (tmap vtf c expr) (define (walk k t) (match t [(Lam x b) (Lam x (walk (add1 k) b))] [(App e1 e2) (App (walk k e1) (walk k e2))] [(Var n) (vtf k n)] [(Def _) t] [(Ann e t) (Ann (walk k e) (walk k t))] [(Arrow x t1 t2) (Arrow x (walk k t1) (walk (add1 k) t2))] [(Type) t])) (walk c expr)) (define (tshift-above d c expr) (tmap (lambda (k x) (if (>= x k) (Var (+ x d)) (Var x))) c expr)) (define (tshift d expr) (tshift-above d 0 expr)) (define (tsubst j s t) (tmap (lambda (k x) (if (equal? x (+ j k)) (tshift k s) (Var x))) 0 t)) (define (subst s t) (tshift -1 (tsubst 0 (tshift 1 s) t))) |# ;; Erasing hints (because they interfere with equivalence) ;; Alternative: use advanced features of Racket's structs to ignore certain fields (define (erasehints expr) (match expr [(Lam _ b) (Lam #f (erasehints b))] [(App e1 e2) (App (erasehints e1) (erasehints e2))] [(Var n) (Var n)] [(Def _) expr] [(Ann e t) (Ann (erasehints e) (erasehints t))] [(Arrow _ t1 t2) (Arrow #f (erasehints t1) (erasehints t2))] [(Type) expr])) ;; Alpha equivalence (produces #t/#f) (define (alpha-equiv? e1 e2) (equal? (erasehints e1) (erasehints e2))) ;; Reducing a term ;; reduce : Expr -> Expr ;; Reduces recursively everywhere, especially in bodies of for-alls and lambdas (define (reduce expr) (match expr [(Var _) expr] [(Def x) (reduce (second (assoc x defs)))] [(Arrow x a b) (Arrow x (reduce a) (reduce b))] [(Lam x b) (Lam x (reduce b))] [(App f a) (define fr (reduce f)) (define fa (reduce a)) (match fr [(Lam _ b) (reduce (subst fa b))] [else (App fr fa)])] [(Ann e t) (reduce e)] [(Type) (Type)])) ;; Definitional equality (define (equiv? e1 e2) (alpha-equiv? (reduce e1) (reduce e2))) ;; Context lookup is more complicated because a type is an expression ;; whose indices are relative to the context it was defined in, ;; but the context grew when it was added and maybe subsequently. ;; So the type has to be renamed on the way back from the recursion. (define (lookup ctx n) (cond [(empty? ctx) (error 'lookup "empty context, index ~a\n" n)] ; shouldn't happen [(zero? n) (rename add1 (second (first ctx)))] [else (rename add1 (lookup (rest ctx) (sub1 n)))])) ;; 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 -> true/error ;; Produces true if expr has type type in context ctx (or error if not). (define (type-check ctx expr type) (match expr [(Lam x b) (type-check ctx type (Type)) (match (reduce type) [(Arrow _ tt tw) (type-check (cons (list x tt) ctx) b tw)] [else (cannot-check ctx expr type)])] [else (if (equiv? (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 e t) (error 'type-check "cannot typecheck ~a as ~a in context:\n~a" (pretty-print-expr ctx e) (pretty-print-expr ctx 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 expr) (match expr [(Var n) (lookup ctx n)] [(Def x) (cond [(assoc x deftypes) => second] [else (cannot-synth ctx expr)])] [(Lam x b) (cannot-synth ctx expr)] [(App f a) (match (reduce (type-synth ctx f)) [(Arrow _ tt tw) #:when (type-check ctx a tt) (subst a tw)] [else (cannot-synth ctx expr)])] [(Ann e t) (type-check ctx t (Type)) (type-check ctx e t) t] [(Arrow x tt tw) (type-check ctx tt (Type)) (type-check (cons (list x tt) ctx) tw (Type)) (Type)] [(Type) (Type)])) ;; 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 expr) (error 'type-synth "cannot infer type of ~a in context:\n~a" (pretty-print-expr ctx expr) (pretty-print-context ctx))) ;; Definitions ;; def : symbol Expr -> void ;; Side effect is to mutate global defs, deftypes to include new def if it checks out (define (def name expr) (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) (printf "~a\n" (pretty-print-expr empty (type-synth empty (parse-expr expr))))) (define (reduce-one expr) (printf "~a\n" (pretty-print-expr empty (reduce (parse-expr expr)))))