Typed Lisp, a Primer (2019)

#1

Post by jedimind » Sat, Jul 18, 2020, 3:19 AM UTC

Typed Lisp, a Primer (2019)
alhassy.github.io

Re: Typed Lisp, a Primer (2019)

#2

Post by vindarel » Sat, Jul 18, 2020, 7:24 PM UTC

It's a great article. Related, for Common Lisp: https://lispcookbook.github.io/cl-cookbook/type.html

and also:

- 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 - 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).

Re: Typed Lisp, a Primer (2019)

#3

Post by dustingetz » Sat, Jul 18, 2020, 8:45 PM UTC

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.

Re: Typed Lisp, a Primer (2019)

#4

Post by jedimind » Sat, Jul 18, 2020, 8:55 PM UTC

dustingetz wrote: post #3

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 informat…

> 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?

Re: Typed Lisp, a Primer (2019)

#5

Post by dependenttypes » Sat, Jul 18, 2020, 9:42 PM UTC

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

Re: Typed Lisp, a Primer (2019)

#6

Post by omginternets » Sat, Jul 18, 2020, 10:11 PM UTC

dustingetz wrote: post #3

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 informat…

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.

Re: Typed Lisp, a Primer (2019)

#7

Post by dustingetz » Sat, Jul 18, 2020, 10:21 PM UTC

omginternets wrote: post #6

dustingetz wrote: post #3

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 informat…

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.

http://www.dustingetz.com/:datomic-in-four-snippets/

Re: Typed Lisp, a Primer (2019)

#8

Post by omginternets » Sat, Jul 18, 2020, 10:32 PM UTC

dustingetz wrote: post #7

omginternets wrote: post #6

Earlier quoted context omitted.

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.

http://www.dustingetz.com/:datomic-in-four-snippets/

Brilliant, thanks.

Re: Typed Lisp, a Primer (2019)

#9

Post by spellcard199 » Sat, Jul 18, 2020, 10:38 PM UTC

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 [2] https://akrl.sdf.org/gccemacs.html

Edit: grammar.

Re: Typed Lisp, a Primer (2019)

#10

Post by smabie » Sat, Jul 18, 2020, 11:16 PM UTC

spellcard199 wrote: post #9

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 - ty…

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!