You need to add a case in parse-expr to deal with annotations, which is in the form (<expr> : <type>).
E.g., [`(,e : ,t) (TA (parse-expr e) (parse-type t))] On Sun, Mar 15, 2020 at 7:21 AM Adrian Manea <[email protected]> wrote: > 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]> >> 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]. >>> 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 > <https://groups.google.com/d/msgid/racket-users/1cde88c7-0eb8-4cf6-9a80-3708b7e35a6b%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/CADcuegu87gdH%2BLcoPv_FZawaEH_rX95Xv3hLRUU1nQDGJrEqEg%40mail.gmail.com.
