P. Ragde's Proust

proust.rkt

;; P. Ragde --  Proust, a Nano Proof Assistant (2016)

#lang racket

(struct Lam (var body))                 ; lambda expression
(struct App (func arg))                 ; application
(struct Arrow (domain codomain))        ; function
(struct TA (type var))                  ; type annotation

;; expr = (lambda x => expr)
;;      | (expr expr)
;;      | (expr : type)
;;      | x

;; parse-expr : sexp -> Expr
(define (parse-expr s)
  (match s
    [`(lambda ,(? symbol? x) => ,e)         ; is it a lambda-expression?
     (Lam x (parse-expr e))]                ; then make it Lam
    [`(,func ,arg)                          ; is it an application?
     (App (parse-expr func)                 ; then make it App
          (parse-expr arg))]
    [`(,e : ,t) (TA (parse-expr e) (parse-type t))]
    [(? symbol? x) x]))                     ; otherwise, it's a symbol => return it

;; my tests
(parse-expr '(lambda x => x))                           ; => #<Lam>  OK
(parse-expr '(lambda x => (lambda y => (x y))))         ; => #<Lam>  OK
(parse-expr '(+ x))                                     ; => #<App>  OK
(parse-expr 'x)                                         ; => 'X      OK

;; type = (type -> type) | X

;; ;; parse-type : sexp -> Type
(define (parse-type t)
  (match t
    [`(,t1 -> ,t2)
     (Arrow (parse-type t1)
            (parse-type t2))]
    [(? symbol? X) X]
    [else (error "unrecognized type")]))

;; my tests
(parse-type '(A -> B))                      ; => #<Arrow>  OK
(parse-type 'X)                             ; => 'X        OK

;; type-check : Context Expr Type -> boolean
;; produces #t if expr has type t in context ctx (else error)
(define (type-check ctx expr type)
  (match expr
    [(Lam x t)
     (match type
       [(Arrow tt tw) (type-check (cons `(,x ,tt) ctx) t tw)]
       [else (cannot-check ctx expr type)])]
    [else (if (equal? (type-infer ctx expr) type) true
              (cannot-check ctx expr type))]))

(define (cannot-check ctx expr type)
  (error "cannot check the type of the expression in the provided context"))

;; type-infer : Context Expr -> Type
;; produces type of expr in context ctx (error if it can't)
(define (type-infer ctx expr)
  (match expr
    [(Lam _ _) (cannot-infer ctx expr)]
    [(TA e t) (type-check ctx e t) t]
    [(App f a)
     (define tf (type-infer ctx f))
     (match tf
       [(Arrow tt tw) #:when (type-check ctx a tt) tw]
       [else (cannot-infer ctx expr)])]
    [(? symbol? x)
     (cond
       [(assoc x ctx) => second]
       [else (cannot-infer ctx expr)])]))
     
(define (cannot-infer ctx expr)
  (error "cannot infer the type of the expression in the provided context"))

;; my test
(type-check empty
            (parse-expr '(lambda x => x))
            (parse-type '(A -> A)))                 ; => #t  OK

;; ONLY WORKS FOR LAMBDAS

;; not working
(define (check-proof p)
  (type-infer empty (parse-expr p)) true)

;; test:
(check-proof
 `((lambda x => (lambda y => (y x))) : (A -> ((A -> B) -> B))))    ; => #t OK
 
 ;; not working
 (check-proof
   `(x : A))
 (check-proof
   `((+ x) : (A -> A))))

Adding a version with a few print statements, one more test, and a bunch of comments.

;; P. Ragde --  Proust, a Nano Proof Assistant (2016)

#lang racket

(struct Lam (var body) #:transparent)                 ; lambda expression
(struct App (func arg) #:transparent)                 ; application
(struct Arrow (domain codomain) #:transparent)        ; function
(struct TA (type var) #:transparent)                  ; type annotation

;; expr = (lambda x => expr)
;;      | (expr expr)
;;      | (expr : type)
;;      | x

;; parse-expr : sexp -> Expr
(define (parse-expr s)
  (match s
    [`(lambda ,(? symbol? x) => ,e)         ; is it a lambda-expression?
     (Lam x (parse-expr e))]                ; then make it Lam
    [`(,func ,arg)                          ; is it an application?
     (App (parse-expr func)                 ; then make it App
          (parse-expr arg))]
    [`(,e : ,t) (TA (parse-expr e) (parse-type t))]
    [(? symbol? x) x]))                     ; otherwise, it's a symbol => return it

;; my tests
(parse-expr '(lambda x => x))                           ; => #<Lam>  OK
(parse-expr '(lambda x => (lambda y => (x y))))         ; => #<Lam>  OK
(parse-expr '(+ x))                                     ; => #<App>  OK
(parse-expr 'x)                                         ; => 'X      OK

;; type = (type -> type) | X

;; ;; parse-type : sexp -> Type
(define (parse-type t)
  (match t
    [`(,t1 -> ,t2)
     (Arrow (parse-type t1)
            (parse-type t2))]
    [(? symbol? X) X]
    [else (error "unrecognized type")]))

;; my tests
(parse-type '(A -> B))                      ; => #<Arrow>  OK
(parse-type 'X)                             ; => 'X        OK

;; type-check : Context Expr Type -> boolean
;; produces #t if expr has type t in context ctx (else error)
(define (type-check ctx expr type)
  ;; Added a printf to see things...
  (printf "checking ctx: ~a expr: ~a type: ~a~n" ctx expr type)
  (match expr
    [(Lam x t)
     (match type
       [(Arrow tt tw) (type-check (cons `(,x ,tt) ctx) t tw)]
       [else (cannot-check ctx expr type)])]
    [else
     ;; Added a printf... probably could have used the
     ;; debugger instead... 
     (printf "ctx: ~a expr: ~a type: ~a~n" ctx expr type)
     (if (equal? (type-infer ctx expr) type) true
              (cannot-check ctx expr type))]))

(define (cannot-check ctx expr type)
  (error "cannot check the type of the expression in the provided context"))

;; type-infer : Context Expr -> Type
;; produces type of expr in context ctx (error if it can't)
(define (type-infer ctx expr)
  (match expr
    [(Lam _ _) (cannot-infer ctx expr)]
    [(TA e t) (type-check ctx e t) t]
    [(App f a)
     (define tf (type-infer ctx f))
     (match tf
       [(Arrow tt tw) #:when (type-check ctx a tt) tw]
       [else (cannot-infer ctx expr)])]
    [(? symbol? x)
     (cond
       [(assoc x ctx) => second]
       [else (cannot-infer ctx expr)])]))
     
(define (cannot-infer ctx expr)
  (error "cannot infer the type of the expression in the provided context"))

;; my test
(type-check empty
            (parse-expr '(lambda x => x))
            (parse-type '(A -> A)))                 ; => #t  OK

;; ONLY WORKS FOR LAMBDAS

;; not working
(define (check-proof p)
  (type-infer empty (parse-expr p)) true)

;; test:
(check-proof
 `((lambda x => (lambda y => (y x))) : (A -> ((A -> B) -> B))))    ; => #t OK

;; Added this proof to see what is going on. This works.
;; That is because it is a lambda, which the type check/infer
;; tooling knows how to handle.
(check-proof
 `((lambda x => x) : (A -> A)))

;; This fails, because the type checker has no idea
;; how to handle a single type annotation outside of the context
;; of a lambda. The type-inferencer has patterns for a TA, but
;; the checker does not. That this fails "makes sense" in the context
;; of the code in the article... whether or not that is what you want
;; to happen is another thing entirely...
(parse-expr '(x : A))
(check-proof `((x : A) : A))


;; not working
; (check-proof `(x : A))
; (check-proof `((+ x) : (A -> A)))