Hi all,

I'm a mathematician delving into type theory and proof assistants and with 
special interests in Racket.

I'm now trying to understand and implement P. Ragde's Proust 
<https://arxiv.org/abs/1611.09473> "nano proof assistant" and work through 
the examples in his article. However, I'm pretty much a beginner in Racket 
and I'm getting some errors. Particularly in the type-infer function, 
that's also used in the type-check function.

Here is the code in the article:

(define (type-check ctx expr type)
  (match expr
    [(Lam x t)                           ; lambda expression
        (match type
           [(Arrow tt tw) (type-check (cons `(,x ,tt) ctx) t tw)]     ; 
arrow type
           [else (cannot-check ctx expr type)])]
    [else (if (equal? (type-infer ctx expr) type) true (cannot-check ctx 
expr type))]))

(define (type-infer ctx expr)
  (match expr
    [(Lam _ _) (cannot-infer ctx expr)]
    [(Ann e t)  (type-check ctx e t) t]
    [(App f a)                            ; function application
      (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)
             [(assoc x ctx) => second]
             [else (cannot-infer ctx expr)])]))

The first question I have is: what's the (Ann e t) supposed to mean, 
because I'm getting a syntax error? Is it a type annotation? If so, 
shouldn't everything be inside the #lang typed/racket module and type 
annotations everywhere?

Secondly, the functions don't seem to work like this, as I'm getting failed 
matches for everything that's not a lambda expression. Can you please help 
me clarify the code there or maybe it's already available somewhere? 
Because just typing in the examples in the article simply doesn't work. I 
can understand what they are supposed to do, but I lack the skills to fix 
things myself.

Thank you!

You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 

Reply via email to