4 ms·
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). First
by sklogic 11y ago
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 constant type
A4=Vx
A3=Vplus
A3=fun(integer, fun(integer, integer)) // from environment lookup
A3=fun(V1, A2) // application rule
A2=fun(V2, A1) // application rule
Then this long Prolog query (all equations are comma separated) is executed and you'll get all An type values to attach to your AST, as well as variable x type.
> Prolog could handle dependent types
It's Turing-complete. You can encode anything you want in it.
- nickpsecurity 11y ago"Then your typing pass walking over this segment of AST would generate the following (mostly trivial) equations" Thanks for the example. That does seem straight-forward. "It's Turing-complete. You can encode anything you want in it." The reason I mention it is that many people doing proofs and such specifically avoid first-order logic in favor of HOL or Coq. They sometimes mention FOL is too limited or you have to go out of your way for what they're doing. Not specialist enough to have figured out what they're talking about. There appears, though, to be some cutoff point where one is better off using HOL-style tools for analysis, proof, synthesis, whatever. Wish I had references on-hand if it's not clear already what I'm talking about.
- jnbiche 11y agoYou'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?
- xixixao 11y agoI think they meant you'll get the type for A1, A2 etc.
- sklogic 11y agoSorry 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.
- jnbiche 11y agoAh perfect, thanks. This whole thread has been a huge boon to me, very glad for all the input.