5 ms·

Typed Lisp, a Primer (2019)

107 points by jedimind 6y ago

vindarel 6y ago
It's a great article. Related, for Common Lisp: https://lispcookbook.github.io/cl-cookbook/type.html https://lispcookbook.github.io/cl-cookbook/type.html and also: - https://medium.com/@MartinCracauer/static-type-checking-in-the-programmable-programming-language-lisp-79bb79eb068a https://medium.com/@MartinCracauer/static-type-checking-in-t... (by an author of the CLASP implementation, C++ & LLVM for CL) - https://github.com/stylewarning/coalton https://github.com/stylewarning/coalton - a library (pre-alpha): adding Hindley-Milner type checking to Common Lisp which allows for gradual adoption, in the same way Typed Racket or Hack allows for. It is as an embedded DSL in Lisp that resembles Standard ML or OCaml, but lets you seamlessly interoperate with non-statically-typed Lisp code (and vice versa).
dustingetz 6y ago
Clojure's take on types is not so much that types are bad at micro scale, it's that focusing on proving referential transparency above all else leads to cultural problems at the macro scale. For example, the Datomic Peer API is the most elegant and ergonomic database API I've ever seen. Queries compose as functions under the illusion that the database is a local data structure and this results in a beautiful information model. But if you tried to put IO types on Datomic you find that it spews IO everywhere. And yet it works incredibly well with good enough performance for a wide band of applications! I think you don't find stuff like that in Pure FP ecosystems because those communities coordinate under principles of RT and algebra, and are thus unable to consider a solution space rooted in a different set of principles.
- jedimind 6y ago
  > focusing on proving referential transparency above all else leads to cultural problems at the macro scale Can you elaborate on what you mean by that?
- omginternets 6y ago
  Do you have examples to illustrate the Datomic Peer API ergonomics you described? This is really interesting to me, and I’m still struggling to grok it.
  - dustingetz 6y ago
    http://www.dustingetz.com/:datomic-in-four-snippets/ http://www.dustingetz.com/:datomic-in-four-snippets/
    - omginternets 6y ago
      Brilliant, thanks.
- smabie 6y ago
  I've personally never thought the cost of tracking mutation and IO in a type system is particularly worth the complexity and hassle. But for everything else, an advanced Hindley Milner derived type system is absolutely, 100% worth it. I do think there might be some middle ground where you can annotate non pure functions in order to help the compiler with aggressive optimization.
- lmm 6y ago
  > But if you tried to put IO types on Datomic you find that it spews IO everywhere. So you put it in a monad and get on with your life? It's like one or two extra characters on your operators just to mark out where you're doing effect composition, and the benefit is that you can immediately see where all the effects are happening. Code is read more than it's written, so it's a really good tradeoff. > And yet it works incredibly well with good enough performance for a wide band of applications! How big is it, and how many people work on it? IME not tracking effects works great as long as everyone working on the codebase can keep the whole thing in their head. But you hit a wall (for me it's about 20kloc - I'm sure smarter people can push it a bit further, but everyone will have a limit eventually) once you can no longer reason about how one part affects every other part, and at that point a little helping hand from the compiler helps a lot.
  - deleted 6y ago
    [deleted]
  - dustingetz 6y ago
    The closest thing I can think of from the pure FP community that makes queries compose in a monad is Scala Slick, which adds an extraordinary amount of complexity to compose queries in exactly the wrong way. The whole FP community's thesis seems to be "take adderall and follow the math" and that thesis leads to Slick, not Datomic. (Both are early 2010s era so i think this is a fair comparison)
    - lmm 6y ago
      Slick is for querying traditional SQL RDBMSes, so it has to deal with a massive impedance mismatch compared to a greenfield project. I'd look at something like Facebook's Haxl (for querying GraphQL) for a fairer comparison IMO.
dependenttypes 6y ago
That reminds me, PG wrote that "static typing seems to preclude true macros" in http://www.paulgraham.com/hundred.html http://www.paulgraham.com/hundred.html despite it being obviously incorrect.
spellcard199 6y ago
After trying Typed Clojure, liking it, but giving it up because of Clojure's GPL-incompatible license, I got interested in Kawa Scheme because it has some rudimentary form of type checking. For example, this produces warnings: (define (f1 x::String y::String) (x:concat y)) (define (f2) (f1 3 3)) ;; /dev/tty:3:19: warning - type integer is incompatible with required type java.lang.String ;; /dev/tty:3:21: warning - type integer is incompatible with required type java.lang.String ;; /dev/tty:3:15: warning - cannot convert literal (of type gnu.math.IntNum) to Type java.lang.String ;; /dev/tty:3:15: warning - cannot convert literal (of type gnu.math.IntNum) to Type java.lang.String Unfortunately it does not support fully static type checking nor generics, otherwise it would be my favorite scripting language hands down. As for type checking Elisp, Elsa[1] seems an interesting project and I hope it becomes a stable option. On the other hand I wonder if in future type checking could also come from gccemacs[2], since one of the "long-term improvements" may be "better compile time warning and errors relying on the propagation engine". [1] https://github.com/emacs-elsa/Elsa https://github.com/emacs-elsa/Elsa [2] https://akrl.sdf.org/gccemacs.html https://akrl.sdf.org/gccemacs.html Edit: grammar.
- smabie 6y ago
  Typed Racket tends to work pretty well, and you can gradually add types to dynamic code. Probably the most mature type system of any Lisp. And if you feel like types are too constraining for a part of your code, you can just leave them out. You get the best of both worlds!
  - spellcard199 6y ago
    If Racket had packages functionally equivalent to the ones on the JVM that I can't live without (Selenium, JGraphX, ...) I would start learning it right away. However sticking to the JVM and Kawa I get a vaguely similar typed/untyped experience except for the un-lispyness of Java. Usually when I write a script I make a new Java project that also pulls the dependencies and then embed Kawa (or jshell/ammonite jupyter server) for interactivity. Between the pom.xml and the code itself embedding Kawa (or jshell/ammonite) in a java program is like 10 lines at most.
swatson741 6y ago
This is a good article but, the author doesn't show the limitations of type systems. If our world is small enough types can be very useful. There are many situations where we want to work in a small world. >type's have always been there I've seen this argument before and, I disagree with this statement as presented. The implication is that there is a type system underlying a language's semantics. But, really that's not true. It's more correct to say that objects have always been there.
User23 6y ago
CMUCL, and I assume SBCL by extension, has a rich type inference system[1] that I wish were more widely known. [1] https://pmsf.eu/pub/cmucl/doc/cmu-user-old/compiler.html#toc125 https://pmsf.eu/pub/cmucl/doc/cmu-user-old/compiler.html#toc...

107 points by jedimind 6y ago

It's a great article. Related, for Common Lisp: https://lispcookbook.github.io/cl-cookbook/type.html https://lispcookbook.github.io/cl-cookbook/type.html and also: - https://medium.com/@MartinCracauer/static-type-checking-in-the-programmable-programming-language-lisp-79bb79eb068a https://medium.com/@MartinCracauer/static-type-checking-in-t... (by an author of the CLASP implementation, C++ & LLVM for CL) - https://github.com/stylewarning/coalton https://github.com/stylewarning/coalton - a library (pre-alpha): adding Hindley-Milner type checking to Common Lisp which allows for gradual adoption, in the same way Typed Racket or Hack allows for. It is as an embedded DSL in Lisp that resembles Standard ML or OCaml, but lets you seamlessly interoperate with non-statically-typed Lisp code (and vice versa).

dustingetz 6y ago

Clojure's take on types is not so much that types are bad at micro scale, it's that focusing on proving referential transparency above all else leads to cultural problems at the macro scale. For example, the Datomic Peer API is the most elegant and ergonomic database API I've ever seen. Queries compose as functions under the illusion that the database is a local data structure and this results in a beautiful information model. But if you tried to put IO types on Datomic you find that it spews IO everywhere. And yet it works incredibly well with good enough performance for a wide band of applications! I think you don't find stuff like that in Pure FP ecosystems because those communities coordinate under principles of RT and algebra, and are thus unable to consider a solution space rooted in a different set of principles.

jedimind 6y ago
> focusing on proving referential transparency above all else leads to cultural problems at the macro scale Can you elaborate on what you mean by that?
omginternets 6y ago
Do you have examples to illustrate the Datomic Peer API ergonomics you described? This is really interesting to me, and I’m still struggling to grok it.
- dustingetz 6y ago
  http://www.dustingetz.com/:datomic-in-four-snippets/ http://www.dustingetz.com/:datomic-in-four-snippets/
  - omginternets 6y ago
    Brilliant, thanks.
smabie 6y ago
I've personally never thought the cost of tracking mutation and IO in a type system is particularly worth the complexity and hassle. But for everything else, an advanced Hindley Milner derived type system is absolutely, 100% worth it. I do think there might be some middle ground where you can annotate non pure functions in order to help the compiler with aggressive optimization.
lmm 6y ago
> But if you tried to put IO types on Datomic you find that it spews IO everywhere. So you put it in a monad and get on with your life? It's like one or two extra characters on your operators just to mark out where you're doing effect composition, and the benefit is that you can immediately see where all the effects are happening. Code is read more than it's written, so it's a really good tradeoff. > And yet it works incredibly well with good enough performance for a wide band of applications! How big is it, and how many people work on it? IME not tracking effects works great as long as everyone working on the codebase can keep the whole thing in their head. But you hit a wall (for me it's about 20kloc - I'm sure smarter people can push it a bit further, but everyone will have a limit eventually) once you can no longer reason about how one part affects every other part, and at that point a little helping hand from the compiler helps a lot.
- deleted 6y ago
  [deleted]
- dustingetz 6y ago
  The closest thing I can think of from the pure FP community that makes queries compose in a monad is Scala Slick, which adds an extraordinary amount of complexity to compose queries in exactly the wrong way. The whole FP community's thesis seems to be "take adderall and follow the math" and that thesis leads to Slick, not Datomic. (Both are early 2010s era so i think this is a fair comparison)
  - lmm 6y ago
    Slick is for querying traditional SQL RDBMSes, so it has to deal with a massive impedance mismatch compared to a greenfield project. I'd look at something like Facebook's Haxl (for querying GraphQL) for a fairer comparison IMO.

dependenttypes 6y ago

That reminds me, PG wrote that "static typing seems to preclude true macros" in http://www.paulgraham.com/hundred.html http://www.paulgraham.com/hundred.html despite it being obviously incorrect.

spellcard199 6y ago

After trying Typed Clojure, liking it, but giving it up because of Clojure's GPL-incompatible license, I got interested in Kawa Scheme because it has some rudimentary form of type checking. For example, this produces warnings: (define (f1 x::String y::String) (x:concat y)) (define (f2) (f1 3 3)) ;; /dev/tty:3:19: warning - type integer is incompatible with required type java.lang.String ;; /dev/tty:3:21: warning - type integer is incompatible with required type java.lang.String ;; /dev/tty:3:15: warning - cannot convert literal (of type gnu.math.IntNum) to Type java.lang.String ;; /dev/tty:3:15: warning - cannot convert literal (of type gnu.math.IntNum) to Type java.lang.String Unfortunately it does not support fully static type checking nor generics, otherwise it would be my favorite scripting language hands down. As for type checking Elisp, Elsa[1] seems an interesting project and I hope it becomes a stable option. On the other hand I wonder if in future type checking could also come from gccemacs[2], since one of the "long-term improvements" may be "better compile time warning and errors relying on the propagation engine". [1] https://github.com/emacs-elsa/Elsa https://github.com/emacs-elsa/Elsa [2] https://akrl.sdf.org/gccemacs.html https://akrl.sdf.org/gccemacs.html Edit: grammar.

smabie 6y ago
Typed Racket tends to work pretty well, and you can gradually add types to dynamic code. Probably the most mature type system of any Lisp. And if you feel like types are too constraining for a part of your code, you can just leave them out. You get the best of both worlds!
- spellcard199 6y ago
  If Racket had packages functionally equivalent to the ones on the JVM that I can't live without (Selenium, JGraphX, ...) I would start learning it right away. However sticking to the JVM and Kawa I get a vaguely similar typed/untyped experience except for the un-lispyness of Java. Usually when I write a script I make a new Java project that also pulls the dependencies and then embed Kawa (or jshell/ammonite jupyter server) for interactivity. Between the pom.xml and the code itself embedding Kawa (or jshell/ammonite) in a java program is like 10 lines at most.

swatson741 6y ago

This is a good article but, the author doesn't show the limitations of type systems. If our world is small enough types can be very useful. There are many situations where we want to work in a small world. >type's have always been there I've seen this argument before and, I disagree with this statement as presented. The implication is that there is a type system underlying a language's semantics. But, really that's not true. It's more correct to say that objects have always been there.

User23 6y ago

CMUCL, and I assume SBCL by extension, has a rich type inference system[1] that I wish were more widely known. [1] https://pmsf.eu/pub/cmucl/doc/cmu-user-old/compiler.html#toc125 https://pmsf.eu/pub/cmucl/doc/cmu-user-old/compiler.html#toc...