[racket-users] Re: graphql library?

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

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

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 pret

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

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 st

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

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 th

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

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 a

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

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

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

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 st

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

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

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

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 to

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

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, whic

[racket-users] opengl

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