4 ms·

> What about Lisps then? That's what I'm using at the moment, but I'm really missing the strict typing. It's often hard to debug even the simple passes if they

by sklogic 11y ago

> What about Lisps then? That's what I'm using at the moment, but I'm really missing the strict typing. It's often hard to debug even the simple passes if they're constructing invalid trees. A type system would have picked it up easily. For this reason I'm working on a hybrid DSL which combines all the power of a Nanopass-like visitors language and a Hindley-Milner type inference with a little twist to overcome the expression problem. Plus all the bells and whistles like an enforced totality, combined with locally allowed imperative things (updating hash maps, accumulating data destructively in lists, etc.).

chubot 11y ago
Is the DSL embedded in a Lisp or is it an entirely new language? Isn't there a lot of existing work on type systems and ADTs in Lisps? e.g. http://docs.racket-lang.org/ts-guide/types.html#%28part._.Union_.Types%29 http://docs.racket-lang.org/ts-guide/types.html#%28part._.Un... https://www.reddit.com/r/lisp/comments/16vwib/which_lisps_feature_generalized_algebraic_data/ https://www.reddit.com/r/lisp/comments/16vwib/which_lisps_fe... I ask because I have run into the typing problem writing language tools in Python, and then I switched to OCaml. I am not that experienced with it, but I see the problem you're talking about. I'm wondering if I should go to a Lisp. Racket looks interesting and this seems like something the community cares about.
- sklogic 11y ago
  Yes, it is a eDSL on top of Lisp (but I also have a proper ML which runs on top of Lisp, so it does not matter much). The issue with the existing type systems is that they do not solve the expression problem, for this reason I had to build a new one from scratch. I'd suggest taking a look at Nanopass (there is a Racket port). I doubt it will play well with any external type systems, but at least some of the ideas in it are very valuable.
  - nickpsecurity 11y ago
    I proposed integrating FLINT ML compiler and VLISP in some form for heightened correctness argument, ML safety, and LISP power. Kind of several copies of the software that corresponded with the strengths of each catching various problems and assuring correctness of tool itself. Never occurred to me to embed ML in LISP. Looks so obvious in hindsight. You might be onto something there. Integrating yours with mine, if I get back to using those, might embed CakeML or Ocaml subset in VLISP with it emulated in Racket or CL knockoff of it for fast, day-to-day development. Btw, what's the expression problem? I've either forgotten or not got that deep into PL design yet.
    - sklogic 11y ago
      The term was coined by Philip Wadler: https://en.wikipedia.org/wiki/Expression_problem https://en.wikipedia.org/wiki/Expression_problem The older versions of Bigloo used to contain an ML compiler built on top of Scheme (they dropped it later for some reason), so the concept is not new.
      - nickpsecurity 11y ago
        Appreciate the reference. Will look into it in the future. The Wikipedia summary made sense but the recompile part doesnt bother me as much as others. My preferrence is to make compiles fast as possible with good incremental compilation and caching. Ive even pushed for trying to FPGA-accelerate compiler passes if possible.
        sklogic 11y ago
        My solution allows incremental compilation. It is just a type system hack, and it does not even involve backtracking (my second favourite compilation technique), just a two pass typing instead of a single pass. As for the compilation speed, the Nanpass-like approach is very parallelisable and there is a lot of space for nice optimisations (like pass fusion).
        nickpsecurity 11y ago
chadzawistowski 11y ago
This article covers setting up Common Lisp with GADTs and exhaustive pattern-matching checks. https://chriskohlhepp.wordpress.com/metacircular-adventures-in-functional-abstraction-challenging-clojure-in-common-lisp/ https://chriskohlhepp.wordpress.com/metacircular-adventures-... > We note that we get a non-exhaustive match warning at compile time, not run time. This is the behaviour we would expect for example from OCaml. Indeed, in our little game we might change the simple use of keyword symbols to algebraic data types and thus add compiler hosted verification of our pattern matches. To bring our exploration of the meta-circular abstraction to a full circle: Abstract data-types are an ideal medium in which to represent Abstract Syntax Trees or ASTs. Indeed the whole of Lisp syntax is itself fundamentally an Abstract Syntax Tree. So let’s see if we can represent trees using the cl-algebraic-datatype package. That would amount to an Abstract Syntax Tree represented inside an Abstract Syntax Tree. We will close with that that little teaser.

by sklogic 11y ago

chubot 11y ago

Is the DSL embedded in a Lisp or is it an entirely new language? Isn't there a lot of existing work on type systems and ADTs in Lisps? e.g. http://docs.racket-lang.org/ts-guide/types.html#%28part._.Union_.Types%29 http://docs.racket-lang.org/ts-guide/types.html#%28part._.Un... https://www.reddit.com/r/lisp/comments/16vwib/which_lisps_feature_generalized_algebraic_data/ https://www.reddit.com/r/lisp/comments/16vwib/which_lisps_fe... I ask because I have run into the typing problem writing language tools in Python, and then I switched to OCaml. I am not that experienced with it, but I see the problem you're talking about. I'm wondering if I should go to a Lisp. Racket looks interesting and this seems like something the community cares about.

sklogic 11y ago
Yes, it is a eDSL on top of Lisp (but I also have a proper ML which runs on top of Lisp, so it does not matter much). The issue with the existing type systems is that they do not solve the expression problem, for this reason I had to build a new one from scratch. I'd suggest taking a look at Nanopass (there is a Racket port). I doubt it will play well with any external type systems, but at least some of the ideas in it are very valuable.
- nickpsecurity 11y ago
  I proposed integrating FLINT ML compiler and VLISP in some form for heightened correctness argument, ML safety, and LISP power. Kind of several copies of the software that corresponded with the strengths of each catching various problems and assuring correctness of tool itself. Never occurred to me to embed ML in LISP. Looks so obvious in hindsight. You might be onto something there. Integrating yours with mine, if I get back to using those, might embed CakeML or Ocaml subset in VLISP with it emulated in Racket or CL knockoff of it for fast, day-to-day development. Btw, what's the expression problem? I've either forgotten or not got that deep into PL design yet.
  - sklogic 11y ago
    The term was coined by Philip Wadler: https://en.wikipedia.org/wiki/Expression_problem https://en.wikipedia.org/wiki/Expression_problem The older versions of Bigloo used to contain an ML compiler built on top of Scheme (they dropped it later for some reason), so the concept is not new.
    - nickpsecurity 11y ago
      Appreciate the reference. Will look into it in the future. The Wikipedia summary made sense but the recompile part doesnt bother me as much as others. My preferrence is to make compiles fast as possible with good incremental compilation and caching. Ive even pushed for trying to FPGA-accelerate compiler passes if possible.
      - sklogic 11y ago
        My solution allows incremental compilation. It is just a type system hack, and it does not even involve backtracking (my second favourite compilation technique), just a two pass typing instead of a single pass. As for the compilation speed, the Nanpass-like approach is very parallelisable and there is a lot of space for nice optimisations (like pass fusion).
        nickpsecurity 11y ago

chadzawistowski 11y ago

This article covers setting up Common Lisp with GADTs and exhaustive pattern-matching checks. https://chriskohlhepp.wordpress.com/metacircular-adventures-in-functional-abstraction-challenging-clojure-in-common-lisp/ https://chriskohlhepp.wordpress.com/metacircular-adventures-... > We note that we get a non-exhaustive match warning at compile time, not run time. This is the behaviour we would expect for example from OCaml. Indeed, in our little game we might change the simple use of keyword symbols to algebraic data types and thus add compiler hosted verification of our pattern matches. To bring our exploration of the meta-circular abstraction to a full circle: Abstract data-types are an ideal medium in which to represent Abstract Syntax Trees or ASTs. Indeed the whole of Lisp syntax is itself fundamentally an Abstract Syntax Tree. So let’s see if we can represent trees using the cl-algebraic-datatype package. That would amount to an Abstract Syntax Tree represented inside an Abstract Syntax Tree. We will close with that that little teaser.