Hi Matt, Thank you very much for the details! What you're saying makes sense and is in accordance with my intuition. But the code doesn't work as it is.
I created a Gist for it here: https://gist.github.com/adimanea/7aa7921c913e70fb9a8b1524b5bd2d3c Everything is from the article, except for the (struct TA (type var)) which I created instead of the Ann ("type annotation") and the examples I used for tests. Regards, Adrian On Sunday, March 15, 2020 at 2:10:55 PM UTC, Matt Jadud wrote: > > Hi Adrian, > > The article seems to be missing a type definition for Ann. > > Perhaps some of this you already know... > > (match expr ...) > > is a pattern matcher, working to find a pattern that 'expr' fits. > > [(Lam _ _) ...] > > is attempting to match a pattern where a 'expr' is a struct called Lam, > and that structure has two fields. In this case, the value of those fields > is ignored, so the variable '_' is used to (by convention, not by syntax) > tell the programmer that these values do not matter. (At least, I'm > reasonably confident this is by convention and not by syntax.) > > The form > > [(Ann e t) ...] is matching the structure 'Ann', and binding the value in > the first field to the identifier 'e', and the second value to 't'. Then, > the expression following is executed (assuming the pattern matched). > > In the article, there is no struct definition for 'Ann'. I suspect it is a > typo/oversight. This would work: > > (struct Ann (e t)) > > would be a reasonable definition. It says "Ann" is a data structure with > two fields, called "e" and "t". > > I haven't read the article, so "better" names for those fields is not > something I am going to come up with right now. The name in the definition > matters (to you, the programmer), but the identifier used to bind in the > pattern is not critical. (Or, it is again something that should be > important to you, but it does not need to match the names of the fields in > the struct definition.) > > Hopefully that helps, and helps you move forward a bit. Ask more questions > if that didn't help. And, perhaps putting your code as-is in a Github Gist > or similar, so that others can look at exactly what you're working with > would be useful. > > (I have no idea how complete or incomplete the code in the article is, > which is why I suggest you put it in a pastebin/gist to share... there > might be other things that were glossed in the article? I don't know.) > > Cheers, > Matt > > > On Sun, Mar 15, 2020 at 10:01 AM Adrian Manea <[email protected] > <javascript:>> wrote: > >> 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] <javascript:>. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/racket-users/6bdfed6a-13c7-4e86-8dcf-5d61b18e15d7%40googlegroups.com >> >> <https://groups.google.com/d/msgid/racket-users/6bdfed6a-13c7-4e86-8dcf-5d61b18e15d7%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/1cde88c7-0eb8-4cf6-9a80-3708b7e35a6b%40googlegroups.com.
