5 ms·

> What I want more than anything is a guide written on the same level on how to build a toy statically-typed language, with algebraic data types. The answers h

by sklogic 11y ago

> What I want more than anything is a guide written on the same level on how to build a toy statically-typed language, with algebraic data types. The answers here might be useful: http://stackoverflow.com/questions/12532552/what-part-of-milner-hindley-do-you-not-understand http://stackoverflow.com/questions/12532552/what-part-of-mil... > Is there no very simple introduction on writing a simple ML, with type checking? Any recommended resources? I'd recommend reading A. Field, P. Harrison, "Functional Programming". Despite the title, the book is about implementation techniques. P.S. I keep suggesting to everyone interested in implementing type systems to use a very simple technique: 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.

nickpsecurity 11y ago
"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 the inference engine runs through it to dump out true or false for various predicates and rules? Am I understanding it right? Also, didn't realize Prolog could handle dependent types and such. That's neat to know.
- 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 ago
    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?
    - xixixao 11y ago
      I think they meant you'll get the type for A1, A2 etc.
    - sklogic 11y ago
      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.
      - jnbiche 11y ago
        Ah perfect, thanks. This whole thread has been a huge boon to me, very glad for all the input.

by sklogic 11y ago

nickpsecurity 11y ago

"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 the inference engine runs through it to dump out true or false for various predicates and rules? Am I understanding it right? Also, didn't realize Prolog could handle dependent types and such. That's neat to know.

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 ago
  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?
  - xixixao 11y ago
    I think they meant you'll get the type for A1, A2 etc.
  - sklogic 11y ago
    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.
    - jnbiche 11y ago
      Ah perfect, thanks. This whole thread has been a huge boon to me, very glad for all the input.