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) (cond [(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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/6bdfed6a-13c7-4e86-8dcf-5d61b18e15d7%40googlegroups.com.
