Understanding P. Ragde's Proust

[Adrian Manea]

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 "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!

[Matt Jadud]

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

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

[Adrian Manea]

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

To unsubscribe from this group and stop receiving emails from it, send an email to racket...@googlegroups.com.

[Sorawee Porncharoenwase]

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))]

To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/1cde88c7-0eb8-4cf6-9a80-3708b7e35a6b%40googlegroups.com.

[Adrian Manea]

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))]

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/1cde88c7-0eb8-4cf6-9a80-3708b7e35a6b%40googlegroups.com.

[Matt Jadud]

Hi Adrian,

I commented on the gist with a "new" version.

As far as I can tell, the type-check function only handles one structural case: Lam. As a result, if you try and run a lone TA structure through it, the code will fail. (See my comments in the code.)

The type-infer function handles more structural cases (e.g. Lam, TA, App). Again, not having read the article, I don't know if it makes sense for this tooling to be able to parse and do anything with a lone annotation. 

In short, given the code as-is, this works:

(check-proof
 `((lambda x => x) : (A -> A)))

this does not:

(check-proof `((x : A) : A))

Hope that helps,

Matt

To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/1cde88c7-0eb8-4cf6-9a80-3708b7e35a6b%40googlegroups.com.

[Adrian Manea]

Hi Matt,

Thank you very much for the help! I think I understand now. At this stage, the code is meant especially for lambdas (in fact, the only example in the article so far is for a lambda term). In what follows, the author details more about the other cases. So I'll assume that our intuition is correct, i.e. that it should only work for lambdas so far and I'll continue to work on the rest of the article and the code and come back later if things don't work out further.

Adrian

On Sunday, March 15, 2020 at 3:14:03 PM UTC, Matt Jadud wrote:

Hi Adrian,

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/1cde88c7-0eb8-4cf6-9a80-3708b7e35a6b%40googlegroups.com.

[Prabhakar Ragde]

On Sunday, March 15, 2020 at 10:00:59 AM UTC-4, Adrian Manea wrote:

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 "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.

Hi! Sorry, I only get this list as a digest, so I didn't see your message until this morning. The code in the paper is not complete, and the paper isn't written so that a beginner in Racket could easily extract a working program from it. When I teach students this material, I give them a working starter file, and I will send that to you by private email, where we can also continue to discuss as needed.

I am at this moment working on converting my course materials on this topic into a free online resource similar to the one I did for functional data structures. But this is not ready yet. I hope to finish it in the next few months and I will post here when it is ready. --PR

[Adrian Manea]

Dear Prof. Ragde,

Thank you very much for the reply! I watched your talk at the Racket con more carefully today and noticed you specifically point out that you don't give your students the whole code and that the entire project is presented as a "proof of concept" and used especially for didactic purposes.

I totally appreciate this approach and I have to say I don't feel quite prepared to fill in the details myself. So I'm doing my best to learn some preliminaries and general Racket first!

Thank you,

Adrian

[Prabhakar Ragde]

The "free online resource" I alluded to earlier is up on my Web page now.

https://cs.uwaterloo.ca/~plragde/flaneries/LACI/

I call it a "flânerie", but it's a mini-textbook on logic and proof assistants, using Racket to first construct a small proof assistant (Proust), expanding it to handle propositional and predicate logic, and then moving into discussion of the much larger Agda and Coq systems. --PR

[Adrian Manea]

Thank you very much for coming back and posting this resource! I will be reading it carefully and I'm already sure there is a lot of useful content! Much appreciated.