[racket-users] opengl

[Hendrik Boom]

On Sun, Mar 15, 2020 at 02:09:22PM -0400, Hendrik Boom wrote:
> On Sun, Mar 15, 2020 at 10:48:48AM -0700, Eric Griffis wrote:
> > On Sat, Mar 14, 2020 at 10:25 PM Hendrik Boom  
> > wrote:
> > 
> > > By the way, I'm working on updating the opengl package to the current
> > > OpenGL 4.6 spec.  Because a change of format in Khronos's
> > > specfiles, it appears to require a complete rewrite to its
> > > specification translator.
> > 
> > This is good news! Through March, I'll be announcing several graphics
> > packages that could benefit from this directly. Let's try to keep a
> > conversation going.
> 
> I'm the guy behind Rackettown, https://github.com/hendrikboom3/rackettown
> It's an experiment about attribute management in procedurally-generated 
> content, although it looks like a fairly simple building-drawing 
> program.
> 
> I wanted to move to doing it in 3D, and it too a little while to realise 
> I needed to use openGl directly, rather than something like Pict3D.
> 
> I had some difficulty figuring out the arious tutorials, so I went to 
> the current red book (covering opengl 4.6) and discovered that the baby 
> steps used functions that weren't in the Racket binding (though they are 
> present in the openGL on my Linux system.
> 
> So ... I'm redoing the binding, after a fruitless attempt tp find 
> up-to-date versions of the old specfiles.
> 
> I'm hoping to test the new interface generator by comparing its output 
> with the one in the present Racket package.  That will always be a bit 
> awkward, because all the definitions are now in a new order, so a simple 
> diff won't do.  Not to mention checking out the errors that Stephan 
> discovered in the old specfiles.

For the time being I'll be calling my version opengl46.  Because I'll be 
comparing output with the old opengl, I have to have both versions 
around for a while without getting mixed up.

There seems also to be a typed opengl module within pict3d.  It's not 
clear to me how that one is related to the untyped opengl.

-- hendrik

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/20200315214304.b6ceyysh255otpln%40topoi.pooq.com.

Re: [racket-users] Re: Code generation performance

[Hendrik Boom]

On Sun, Mar 15, 2020 at 10:48:48AM -0700, Eric Griffis wrote:
> On Sat, Mar 14, 2020 at 10:25 PM Hendrik Boom  wrote:
> >
> > There's a port of glm in the Racket package library.
> > Is that the same one?  If not, is it also that huge?
> 
> Same repository, different branch. The master branch, which is a
> couple months old now, implements the matrix and vector types on top
> of a single, list-based, length-agnostic structure type. It's a
> snapshot of the moment I realized the volume of code and run-time
> loops were becoming a problem.
> 
> The new code is in the dev branch. It implements just the vector types
> in a manner similar to generic interfaces while also exposing a
> progression of increasingly type-specific variants. This allows me to
> prototype with a generic API, then eliminate the overhead of dynamic
> dispatch later by switching to more type-specific operations. (If it's
> not obvious, I'm working toward a pluggable type system harness, so
> the compiler can specialize and prune automatically.)
> 
> > By the way, I'm working on updating the opengl package to the current
> > OpenGL 4.6 spec.  Because a change of format in Khronos's
> > specfiles, it appears to require a complete rewrite to its
> > specification translator.
> 
> This is good news! Through March, I'll be announcing several graphics
> packages that could benefit from this directly. Let's try to keep a
> conversation going.

I'm the guy behind Rackettown, https://github.com/hendrikboom3/rackettown
It's an experiment about attribute management in procedurally-generated 
content, although it looks like a fairly simple building-drawing 
program.

I wanted to move to doing it in 3D, and it too a little while to realise 
I needed to use openGl directly, rather than something like Pict3D.

I had some difficulty figuring out the arious tutorials, so I went to 
the current red book (covering opengl 4.6) and discovered that the baby 
steps used functions that weren't in the Racket binding (though they are 
present in the openGL on my Linux system.

So ... I'm redoing the binding, after a fruitless attempt tp find 
up-to-date versions of the old specfiles.

I'm hoping to test the new interface generator by comparing its output 
with the one in the present Racket package.  That will always be a bit 
awkward, because all the definitions are now in a new order, so a simple 
diff won't do.  Not to mention checking out the errors that Stephan 
discovered in the old specfiles.

-- hendrik

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/20200315180922.ejb3eu6bsclm4nbf%40topoi.pooq.com.

Re: [racket-users] Re: Code generation performance

[Eric Griffis]

On Sat, Mar 14, 2020 at 10:25 PM Hendrik Boom  wrote:
>
> There's a port of glm in the Racket package library.
> Is that the same one?  If not, is it also that huge?

Same repository, different branch. The master branch, which is a
couple months old now, implements the matrix and vector types on top
of a single, list-based, length-agnostic structure type. It's a
snapshot of the moment I realized the volume of code and run-time
loops were becoming a problem.

The new code is in the dev branch. It implements just the vector types
in a manner similar to generic interfaces while also exposing a
progression of increasingly type-specific variants. This allows me to
prototype with a generic API, then eliminate the overhead of dynamic
dispatch later by switching to more type-specific operations. (If it's
not obvious, I'm working toward a pluggable type system harness, so
the compiler can specialize and prune automatically.)

> By the way, I'm working on updating the opengl package to the current
> OpenGL 4.6 spec.  Because a change of format in Khronos's
> specfiles, it appears to require a complete rewrite to its
> specification translator.

This is good news! Through March, I'll be announcing several graphics
packages that could benefit from this directly. Let's try to keep a
conversation going.

Eric

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAORuSUzrPxHccXWCUJ9TFEoZPA9ORm%2BNuDBR5oMYOQ1NS1Kfqg%40mail.gmail.com.

Re: [racket-users] Understanding P. Ragde's Proust

[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,
>
> 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
>
>
>
> On Sun, Mar 15, 2020 at 10:21 AM Adrian Manea  > 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  
>>> 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 
  "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)

Re: [racket-users] Understanding P. Ragde's Proust

[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



On Sun, Mar 15, 2020 at 10:21 AM Adrian Manea 
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 
>> 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
>>>  "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?
>>

Re: [racket-users] Understanding P. Ragde's Proust

[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 ( : ).
>
> E.g.,
>
> [`(,e : ,t) (TA (parse-expr e) (parse-type t))]
>
>
> On Sun, Mar 15, 2020 at 7:21 AM Adrian Manea  > 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  
>>> 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 
  "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 
>>

Re: [racket-users] Understanding P. Ragde's Proust

[Sorawee Porncharoenwase]

You need to add a case in parse-expr to deal with annotations, which is in
the form ( : ).

E.g.,

[`(,e : ,t) (TA (parse-expr e) (parse-type t))]


On Sun, Mar 15, 2020 at 7:21 AM Adrian Manea 
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 
>> 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
>>>  "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 subsc

Re: [racket-users] Understanding P. Ragde's Proust

[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
>
>
> On Sun, Mar 15, 2020 at 10:01 AM Adrian Manea  > 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 
>>  "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 racket...@googlegroups.com .
>> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/racket-users/6bdfed6a-13c7-4e86-8dcf-5d61b18e15d

Re: [racket-users] Understanding P. Ragde's Proust

[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


On Sun, Mar 15, 2020 at 10:01 AM Adrian Manea 
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
>  "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 racket-users+unsubscr...@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
> 
> .
>

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAAGM456YQqawEbaytizkn5X6NzJirLq5oj2RDWS620BkKaZZGg%40mail.gmail.com.

[racket-users] 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!


-- 
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+unsubscr...@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.

[racket-users] Re: graphql library?

[Darren Newton]

Not yet but have thought about it. We use GraphQL pretty heavily at work 
now. gRPC / Protocol Buffers as well.

On Saturday, March 14, 2020 at 2:26:13 PM UTC-4, 'John Clements' via 
users-redirect wrote:
>
> Uh oh… another protocol! Has anyone done any work on a GraphQL client 
> library in Racket? 
>
> https://graphql.org/code/#graphql-clients 
>
> John 
>
>

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/da13b6ca-11ad-45e1-aa5e-5835aa166fd9%40googlegroups.com.