Beautiful Racket

Post by jnbiche » Sat, Mar 05, 2016, 10:42 PM UTC

sklogic wrote: post #48

nickpsecurity wrote: post #47

Earlier quoted context omitted.

"find an embeddable Prolog compiler for your language of choice (e.g., MiniKanren for Racket), and then simply emit a flat list of Prolog equations out of your source language AST (do the lexical scoping pass first). Easy. And easily extendable to dependent typing and all that fancy stuff." So, you represent the AST associations and type-checks as Prolog logic rules that operate on predicates describing the AST? And…

For example, you have an AST node for 'x + 2', encoded as 'apply(apply(var("+"), var("x")), const("2"))' (we're talking about ML, so it is curried here). Firstly, all the expression nodes must be annotated with type tags: 'A1:apply(A2:apply(A3:var("plus"),A4:var("x")), A5:const("2"))'. Then your typing pass walking over this segment of AST would generate the following (mostly trivial) equations A5=integer // from con…

Post by xixixao » Sun, Mar 06, 2016, 9:14 AM UTC

jnbiche wrote: post #51

sklogic wrote: post #48

Earlier quoted context omitted.

For example, you have an AST node for 'x + 2', encoded as 'apply(apply(var("+"), var("x")), const("2"))' (we're talking about ML, so it is curried here). Firstly, all the expression nodes must be annotated with type tags: 'A1:apply(A2:apply(A3:var("plus"),A4:var("x")), A5:const("2"))'. Then your typing pass walking over this segment of AST would generate the following (mostly trivial) equations A5=integer // from con…

You've sent me way down the rabbit hole here. I'm going back and reviewing Prolog for the first time in years (at least the syntax isn't strange since I've been using Erlang recently). I don't quite understand this phrase "you'll get all An type values to attach to your AST". Do you just mean "all type values" or is "An type" a technical term?

Post by jnbiche » Sun, Mar 06, 2016, 10:26 AM UTC

sklogic wrote: post #54

jnbiche wrote: post #51

Earlier quoted context omitted.

You've sent me way down the rabbit hole here. I'm going back and reviewing Prolog for the first time in years (at least the syntax isn't strange since I've been using Erlang recently). I don't quite understand this phrase "you'll get all An type values to attach to your AST". Do you just mean "all type values" or is "An type" a technical term?

Sorry for a confusing wording. I was referring to the newly generated tag variables A1, A2, ..., An. The next typing pass after solving the equations is to substitute those tags with the type values found by Prolog.