[HN Gopher] The Lisp in the Cellar: Dependent types that live up...
___________________________________________________________________
The Lisp in the Cellar: Dependent types that live upstairs [pdf]
Downloadable: https://zenodo.org/records/15424968/files/deputy-
els.pdf
Author : todsacerdoti
Score : 78 points
Date : 2025-05-20 13:38 UTC (9 hours ago)
(HTM) web link (zenodo.org)
(TXT) w3m dump (zenodo.org)
| droideqa wrote:
| Sadly "deputy clojure" on Google brings no results...
|
| The only hint is this repo[0] referenced in the paper.
|
| [0]: https://gitlab.com/fredokun/deputy
| agumonkey wrote:
| Pretty readable code
| reuben364 wrote:
| Thinking out aloud here.
|
| One pattern that I have frequently used in EMACS elisp is that
| redefining a top-level value overwrites that value rather than
| shadowing it. Basically hot reloading. This doesn't work in a
| dependently typed context as the type of subsequent definitions
| can depend on values of earlier definitions.
| def t := string def x: t := "asdf" redef t := int
|
| redefining t here would cause x to fail to type check. So the
| only options are to either shadow the variable t, or have
| redefinitions type-check all terms whose types depend on the
| value being redefined.
|
| Excluding the type-level debugging they mention, I think a lean
| style language-server is a better approach. Otherwise you are
| basically using an append-only ed to edit your environment rather
| than a vi.
| extrabajs wrote:
| I don't see the connection to dependent types. But anyway, is
| 'redef' part of your language? What type would you give it?
| reuben364 wrote:
| I just wrote redef to emphasize that I'm not shadowing the
| original definition. def a := 1 def
| f x := a * x -- at this point f 1 evaluates to 1
| redef a := 2 -- at this point f 1 evaluates to 2
|
| But with dependent types, types can depend on prior values
| (in the previous example the type of x depends on the value t
| in the most direct way possible, as the type of x is t). If
| you redefine values, the subsequent definitions may not type-
| check anymore.
| resize2996 wrote:
| > EMACS elisp
|
| I used this to write the front end for an ATM machine.
| wk_end wrote:
| I've fantasized about some kind of a dependently-typed
| Smalltalk-like thing before, and in those fantasies the
| solution would be that changes would be submitted in the form
| of transactions - they wouldn't be live until you bundled them
| all together into one big change that would be fully type-
| checked, as you describe.
| dang wrote:
| Any URL for this that we can open in a browser (as opposed to the
| dreaded "Content-Disposition: attachment")?
| Jtsummers wrote:
| https://zenodo.org/records/15424968 - This at least takes you
| to a webpage where you can view the paper. If you select to
| download it, it still downloads of course instead of just
| opening in the browser.
| dang wrote:
| Thanks! I've switched to that above, and put the downloadable
| link in the top text.
| reikonomusha wrote:
| Related context: The 2025 European Lisp Symposium [1] was just
| wrapped a few hours ago in Zurich. There was content on:
|
| - Static typing a la Haskell with Coalton in Common Lisp
|
| - Dependent typing with Deputy in Clojure (this post)
|
| - The Common Lisp compiler SBCL ported to the Nintendo Switch
|
| - Common Lisp and AI/deep learning
|
| - A special retrospective on Modula and Oberon
|
| - Many lightning talks.
|
| [1] https://european-lisp-symposium.org/2025/index.html
| no_wizard wrote:
| I feel like Lisp would be an ideal language for AI development.
| Its exceedingly good for DSL development and pattern matching.
| Its already structurally like math notation as well, which I
| would think would lend itself to thinking how models would
| consume information and learn
| rscho wrote:
| Well... believe it or not, some have thought of using lisp
| for AI for quite some time. ;-)
| froh wrote:
| indeed.
|
| Peter Norvig, 1992
|
| Paradigms of AI Programming: Case Studies in Common Lisp
|
| https://g.co/kgs/hck8wsE
|
| https://en.m.wikipedia.org/wiki/Peter_Norvig
|
| it's no coincidence Google is actively maintaining sbcl,
| either.
| Zambyte wrote:
| Why not go all the way to the source? John McCarthy coined
| the term "artificial intelligence", and then invented /
| discovered LISP in pursuit of it in the 1950s :D
| ayrtondesozzla wrote:
| https://quantumzeitgeist.com/lisp-and-the-dawn-of-
| artificial...
|
| Lisp was the de facto language of artificial intelligence in
| the U.S. for many years. Apparently Prolog was popular in
| Europe (according to Norvig's PAIP)
| fithisux wrote:
| Impressive.
___________________________________________________________________
(page generated 2025-05-20 23:01 UTC)