Thank you very much! This solves the problem with the lambda expressions. However, I can't seem to work out other examples, so I'm guessing the type-infer function still has some problems or I'm still missing something. I've added some more test cases in the Gist.
On Sunday, March 15, 2020 at 2:32:42 PM UTC, Sorawee Porncharoenwase wrote: > > 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] > <javascript:>> 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] <javascript:>. >> 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/d883c74b-a43b-438d-97ee-e57464646a79%40googlegroups.com.
