Skip to content

Instantly share code, notes, and snippets.

@adimanea adimanea/proust.rkt
Last active Mar 15, 2020

Embed
What would you like to do?
P. Ragde's Proust
;; 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))))
@jadudm

This comment has been minimized.

Copy link

jadudm commented Mar 15, 2020

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)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.