frontpage.
newsnewestaskshowjobs

Open Source @Github

fp.

Open in hackernews

The Lisp in the Cellar: Dependent types that live upstairs [pdf]

https://zenodo.org/records/15424968
88•todsacerdoti•1y ago
Downloadable: https://zenodo.org/records/15424968/files/deputy-els.pdf

Comments

droideqa•1y ago
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•1y ago
Pretty readable code
reuben364•1y ago
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•1y ago
I don’t see the connection to dependent types. But anyway, is ‘redef’ part of your language? What type would you give it?
reuben364•1y ago
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.
extrabajs•1y ago
I see what you mean. But would you not experience the same sort of issue simply from redefining types in the same way? It seems this kind of destructive operation (whether on types or terms) is the issue. As someone who's used to ML, it seems strange to allow this kind of thing (instead of simply shadowing), but maybe it's a Lisp thing?
resize2996•1y ago
> EMACS elisp

I used this to write the front end for an ATM machine.

wk_end•1y ago
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•1y ago
Any URL for this that we can open in a browser (as opposed to the dreaded "Content-Disposition: attachment")?
Jtsummers•1y ago
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•1y ago
Thanks! I've switched to that above, and put the downloadable link in the top text.
reikonomusha•1y ago
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•1y ago
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•1y ago
Well... believe it or not, some have thought of using lisp for AI for quite some time. ;-)
froh•1y ago
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
fithisux•1y ago
Impressive.
kscarlet•1y ago
The only option that you described is called "hyperstatic global environment".

And it is called that for a reason, it is not very dynamic :) and probably too static to the taste of many Lisp and all Smalltalk fans.

•
1y ago
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•1y ago
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)

How Bluesky draws its logo on screenshots

https://timmarinin.net/2026/bluesky-screenshots/
266•gavide•4h ago•193 comments

Quake Shareware, a CD-ROM just a little too full

https://fabiensanglard.net/quake_shareware_cd/index.html
176•shdon•4h ago•78 comments

GPT-5.6 Sol Pricing Cut by 50%

https://openrouter.ai/openai/gpt-5.6-sol
174•Topfi•5h ago•102 comments

A Preview of DuckDB v2.0

https://duckdb.org/2026/08/17/duckdb-20-highlights
560•ibotty•13h ago•99 comments

Fairphone 6 and PostmarketOS working main camera

https://catcrafts.net/posts/fairphone-6-postmarketos-working-main-camera
93•pizzaiolo•4h ago•24 comments

GPU Offload in Rust: Portable, Safe, and Fast

https://arxiv.org/abs/2608.13759
167•linggen•9h ago•36 comments

AI-Generated GitHub Copilot “Autofix” Allowed Compromise of Snowflake's Jira

https://www.wiz.io/blog/red-agent-snowflake-copilot-cicd-bug
322•galnagli•12h ago•126 comments

Olo (Color)

https://en.wikipedia.org/wiki/Olo_(color)
337•inigyou•5d ago•67 comments

AI;DR (AI; Didn't Read)

https://www.rickmanelius.com/p/aidr-ai-didnt-read
638•mooreds•7h ago•398 comments

Repair Cafe – Fix Your Broken Items

https://www.repaircafe.org/
29•rglover•3h ago•8 comments

The Road to MS-DOS 2.0

https://nemanjatrifunovic.substack.com/p/the-road-to-ms-dos-2
26•whobre•5d ago•6 comments

GPT 5.6 Sol is the best "vision" model OpenAI ever released

https://blog.roboflow.com/openai-gpt-5-6/
307•plurby•14h ago•154 comments

Judge sets framework for Nine PBS to retrieve archival data

https://current.org/2026/08/judge-sets-framework-for-nine-pbs-to-retrieve-archival-data/
142•qingcharles•10h ago•56 comments

An update on leaving Gmail for Fastmail

https://moddedbear.com/an-update-on-leaving-gmail-for-fastmail/
131•neogodless•9h ago•98 comments

India has paved the way for charging merchants a fee on UPI transactions

https://www.bbc.com/news/articles/c8xnwqe00v1o
100•monkey_monkey•7h ago•103 comments

Los Puesteros, solitary men who look after ranches and livestock in Patagonia

https://www.newyorker.com/culture/photo-booth/the-lonely-men-at-the-end-of-the-world
113•bookofjoe•8h ago•41 comments

Sun Clock

https://sunclock.net/
183•Gecko4072•10h ago•56 comments

How to disable or avoid intrusive AI

https://www.librarian.net/notoai/
262•ColinWright•12h ago•161 comments

Israel creates fake think tank in likely attempt to dupe AI chatbots

https://responsiblestatecraft.org/israel-influence-chatgpt/
138•DeepLogin•6h ago•49 comments

How do functions like alloca allocate memory from the stack?

https://devblogs.microsoft.com/oldnewthing/20260817-40/?p=112617
35•ingve•5h ago•12 comments

Shattered skeleton is first confirmed death from trebuchet

https://www.science.org/content/article/shattered-skeleton-scottish-castle-first-confirmed-death-...
8•hermitcrab•4d ago•4 comments

Launch HN: Speko (YC S26) – OpenRouter for Voice AI

https://speko.ai/
92•abdik•11h ago•53 comments

GitHub degradation affects Cursor Origin, its new Git platform

https://status.cursor.com/incidents/l9h9vrd726jv
40•KGC3D•6h ago•11 comments

scScript for Linux

https://scapplications.com/
19•OptionOfT•4h ago•7 comments

Ask HN: Alternatives to GitHub

506•dhruv3006•13h ago•327 comments

A particle made of force: physicists say they've found mysterious 'glueball'

https://www.nature.com/articles/d41586-026-02498-1
105•Brajeshwar•5d ago•20 comments

A simple fix for LLM tail latency

https://engineering.myhoai.com/posts/a-simple-fix-for-llm-tail-latency/
40•oskrim•3d ago•16 comments

Roboflow Playground: Try and Compare 30 Computer Vision Models

https://blog.roboflow.com/roboflow-playground/
44•Bluestein•8h ago•3 comments

Google wins bankruptcy auction for Spirit Airlines emails, chats, documents

https://www.axios.com/2026/08/17/google-spirit-airlines-bankruptcy
38•sgustard•2h ago•12 comments

How to put 170 atoms in an atom

https://signoregalilei.com/2026/08/02/how-to-put-170-atoms-in-an-atom/
105•surprisetalk•12h ago•25 comments