tag:blogger.com,1999:blog-8068466035875589791.post1696606496486600848..comments2024-03-26T00:37:39.585-07:00Comments on Semantic Domain: Abstract Binding TreesNeel Krishnaswamihttp://www.blogger.com/profile/06853898957395028131noreply@blogger.comBlogger9125tag:blogger.com,1999:blog-8068466035875589791.post-55994106740391076322019-09-06T22:37:08.980-07:002019-09-06T22:37:08.980-07:00This post has been very helpful and illuminating f...This post has been very helpful and illuminating for me as well! <br /><br />I have been slightly hung up on the implementation of substitution, however. It is either due to a mistake I have made elsewhere in porting the implementation, or to a small omission in the code presented here.<br /><br />The rule for substitution on abstractions is given as<br /><br />```<br /> let rec subst t x body = <br /> (* ... *)<br /> | Abs(x, e) -><br /> let x' = fresh (V.union (freevars t) (freevars body)) x in<br /> let e' = subst t x (rename x x' e) in <br /> abs(x', e')<br />```<br /><br />iiuc, this needs some sort of guard to protect against the case when the "subject" of the substitution in the `subst` function head is equal to the `x`in `Abs(x,e)`. I.e., something like `| Abs (z, e) when Var.equal x z -> abs z e`. Otherwise it seems like we can end up substituting a variable that should be bound in the abstraction. (It was looking at Paul Chiusano's Haskell version that clued me in to this.)<br /><br />Additionally, iiuc, the `x` in the pattern match on the `Abs (x, e)` shadows the `x` in the `subst` function head. As a result, it seems like we end up substituting for the wrong variable when we recurse into the abstraction body at `let e' = subst t x (rename x x' e) in `. Renaming the variables in the `Abs` rule to `z` and `z'` prevents this.<br /><br />If these observations are correct, I hope my remark might save future seekers some time. If not, I would be grateful if someone else would correct my misunderstanding! Regardless, thanks for the knowledge and the surrounding discussion.Shon Federhttps://www.blogger.com/profile/13356575990639223654noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-5549471361129404522017-02-06T02:58:55.059-08:002017-02-06T02:58:55.059-08:00Hi Evan, the ABT functor takes a "signature&q...Hi Evan, the ABT functor takes a "signature" as an argument. A signature is basically a datatype containing of all the term formers in the language -- eg, for lambda calculus with booleans, it would be lambdas, applications, boolean constants, and conditionals. The ABT module then gives you a recursive type with those term formers, plus variable references and variable abstractions. We have to write Tm because of the way ML datatypes work -- ideally we'd like to say that Tm has all the constructors of the signature plus variables and abstractions, but that can't be expressed in plain ML. So we wrap all of F.t's constructors in a Tm, which is okay.Neel Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-42339946149233235032017-01-30T20:14:32.024-08:002017-01-30T20:14:32.024-08:00I must be out of my mind. What is the Tm construct...I must be out of my mind. What is the Tm constructor in the ABT module supposed to be? I don't see this in Harper's book. Where did it come from? What is it abbreviating? Does this have to do with "symbols" which are introduced near the end of section 1.2?Evan Rineharthttps://www.blogger.com/profile/18247994138100958669noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-6163644164212578082015-08-10T10:57:07.226-07:002015-08-10T10:57:07.226-07:00Given the lack of answers, here's my 2 cents: ...Given the lack of answers, here's my 2 cents: you should be able to reuse encodings of letrec for HOAS. Googling `letrec hoas` shows that solutions exist, but I can't survey them yet — https://gist.github.com/t0yv0/834748 is not obviously elegant.<br /><br />Meanwhile, I'm porting your post to Scala (https://github.com/Blaisorblade/abt); I'm seeing what I can improve using extractors, and I'd like to wrap other implementation techniques behind the ABT interface (or is that stupid?). Let's see where I get.Anonymoushttps://www.blogger.com/profile/04485097839438234853noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-20514732618383365772015-04-16T18:01:03.361-07:002015-04-16T18:01:03.361-07:00Neel, could you show how you'd do let rec with...Neel, could you show how you'd do let rec with this scheme? I can't quite see how it would work, since each binding in the let rec needs to be able to refer to all other bindings in the block.<br /><br />By the way, thanks very much for these posts, they have been super helpful to me!Paul Chiusanohttps://www.blogger.com/profile/04844651950877109501noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-34425339170859281922015-03-26T04:59:54.238-07:002015-03-26T04:59:54.238-07:00Dear Paolo, there is a close connection between HO...Dear Paolo, there is a close connection between HOAS and ABTs, but they aren't quite the same. <br /><br />With higher-order abstract syntax, we use meta-level lambda-abstraction to represent binding. So we work modulo the alpha-beta-eta theory of the lambda calculus. With ABTs, we work modulo *only* the alpha-equivalence induced by the binding structure. <br /><br />Because the typed lambda calculus is strongly normalizing, we can prove that an ABT representation of a calculus with binding is isomorphic to the the beta-normal, eta-long forms of a HOAS representation. Another way of putting it is that ABTs is HOAS minus the ability to do partial application or lambda-abstraction, so the only equational theory we need to consider for them is alpha-equivalence.<br /><br />Neel Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-69686609403992892102015-03-24T09:30:31.560-07:002015-03-24T09:30:31.560-07:00Thanks for the post. But Harper's chapter note...Thanks for the post. But Harper's chapter notes don’t cite Nuprl, but AUTOMATH and LF, so I always guessed that ABTs are HOAS done on paper (and without reusing binding from the metalanguage, which in fairness is the distinguishing feature of HOAS—but not the only one).<br /><br />The difference is that HOAS uses the metalanguage instead of making you write the ABT module, but you should get similar guarantees anyway. I imagine the relation is somewhere in the proof of adequacy of HOAS, and it should boil down to “you can reuse binding from the metalanguage, because the metalanguage is a lambda calculus so it uses the same definitions”.<br /><br />Two critical properties are shared among your code and HOAS (I quote you):<br />- "Binding trees have only one binding form, and we never introduce any others."<br />- "Abstractions are purely binders, with no reduction rules associated with them, and abstract binding trees are simply equated up to alpha-equivalence."Anonymoushttps://www.blogger.com/profile/04485097839438234853noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-71729876676194866942015-03-19T13:07:22.201-07:002015-03-19T13:07:22.201-07:00Fyi, I ported your post to Haskell.Fyi, I <a href="https://gist.github.com/pchiusano/e51c4aec00ceb9e83393" rel="nofollow">ported your post to Haskell</a>.Paul Chiusanohttps://www.blogger.com/profile/04844651950877109501noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-80670540398831441752015-03-17T11:54:37.616-07:002015-03-17T11:54:37.616-07:00Thanks for putting this post together. Since posti...Thanks for putting this post together. Since posting my question I did read up on ABTs. <br /><br />> That said, the problem which motivates types-for-binding is a real one: how can we make substitution safe, once and for all?<br /><br />Well, it's more than that. Using types for binding ensures that *every* operation that manipulates terms is well-formed with respect to variable binding, and the typechecker ensures this. With ABTs, we get no such guarantees - you could easily implement subst incorrectly in a way that still typechecks! What ABTs buy you is the ability to define (some of) these operations once and for all, for any collection of operators. There may be operations that aren't ABT-generic but must be implemented specific to the functor chosen (again without much help from the typechecker), whereas with using types-for-binding a la bound, you have much fewer opportunities to screw up implementations (possibly at a cost of having to 'prove' more things to the compiler). It seems like it will depend on what you are doing. <br /><br />You might be interested in this discussion [1] and these examples [2].<br /><br />> In fact, I tend to view term representations with highly-structured syntax as strong evidence for layering violations: the parser shouldn't know too much about the binding or type structure of a program, because conceptually binding structure is determined after we produce the syntax tree.<br /><br />I see what you are saying. However this (desirable) separation of layers can be handled quite nicely with the types-for-binders approach. The way this is handled is by having the parser produce terms whose free variables are of type string (essentially unresolved references). A separate phase 'resolves' these variables to produce a closed expression. That is, the term is of type `Term a`, where `a` is the type of free variables in the expression, and the parser produces a `Term String`, and we have a function like `resolve :: Term String -> Maybe (Term a)`, which converts to the resolved expression. Functions like `resolve` have a very nice signature, and again, they are very difficult to screw up due to the types. Check out the parser for the Ermine compiler [3] for an example of this.<br /><br />[1]: http://pchiusano.github.io/2015-02-25/dumb-data.html#comment-1876005495<br />[2]: https://gist.github.com/pchiusano/687abb31875e058bfff5<br />[3]: https://github.com/ermine-language/ermine/blob/master/src/Ermine/Parser/Term.hs#L55Paul Chiusanohttps://www.blogger.com/profile/04844651950877109501noreply@blogger.com