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
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
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
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
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
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
6 matches
Mail list logo
