frontpage.
newsnewestaskshowjobs

Made with ♥ by @iamnishanth

Open Source @Github

Open in hackernews

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

https://zenodo.org/records/15424968
65•todsacerdoti•5h ago
Downloadable: https://zenodo.org/records/15424968/files/deputy-els.pdf

Comments

droideqa•4h 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•2h ago
Pretty readable code
reuben364•3h 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•12m ago
I don’t see the connection to dependent types. But anyway, is ‘redef’ part of your language? What type would you give it?
dang•3h ago
Any URL for this that we can open in a browser (as opposed to the dreaded "Content-Disposition: attachment")?
Jtsummers•3h 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•3h ago
Thanks! I've switched to that above, and put the downloadable link in the top text.
reikonomusha•3h 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•56m 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•12m ago
Well... believe it or not, some have thought of using lisp for AI for quite some time. ;-)
froh•11m 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.

fithisux•2h ago
Impressive.

FDA to limit access to Covid-19 shots

https://arstechnica.com/health/2025/05/under-anti-vaccine-advocate-rfk-jr-fda-to-limit-access-to-covid-19-shots/
1•AdmiralAsshat•24s ago•0 comments

Super Creepy Laptop Ad

https://jetgirl.art/super-creepy-laptop-ad/
1•nivethan•1m ago•0 comments

Samsung Back to Working on Upstreaming Tesla FSD SoC Support in the Linux Kernel

https://www.phoronix.com/news/Samsung-Tesla-FSD-PCIe-SoC-2025
1•Bender•1m ago•0 comments

Together Code Sandbox

https://www.together.ai/blog/code-sandbox
1•handfuloflight•1m ago•0 comments

The Lost Decade of Small Data? (Article on DuckDB)

https://duckdb.org/2025/05/19/the-lost-decade-of-small-data.html
2•oli200110•2m ago•0 comments

What If Every Picture You've Ever Seen Exists?

2•cin4ed•2m ago•0 comments

The Tech Industry Is Huge–and Europe's Share of It Is Small

https://www.wsj.com/tech/europe-big-tech-ai-1f3f862c
1•danielcampos93•3m ago•0 comments

Is "Specification Repair" the AI Endgame?

https://aboard.com/is-specification-repair-the-ai-endgame/
1•gbseventeen3331•4m ago•0 comments

Alone and Adrift in the Pacific

https://www.theatlantic.com/magazine/archive/2025/06/commercial-fisherman-shipwreck/682580/
1•anarbadalov•5m ago•0 comments

The Evolution of the Alpha Male Aesthetic

https://www.bloomberg.com/features/2025-maga-man-style-history/
1•mooreds•6m ago•1 comments

Behind Netflix's UK launch: Why now, why no DVDs, and what's next? (2012)

https://www.wired.com/story/netflix-reed-hastings-feature/
1•microsoftedging•7m ago•1 comments

Show HN: AI Agent for Documentation and other apps

https://sitegui.com/agent/platform_assistant
1•ciaovietnam•8m ago•0 comments

Nonprofit news media leaders are struggling to stop leaning on foundations

https://theconversation.com/nonprofit-news-media-leaders-are-struggling-to-stop-leaning-on-the-foundations-that-say-they-should-branch-out-more-255821
2•rntn•10m ago•0 comments

Why figuring out what's behind a big gender paradox won't be easy (2018)

https://arstechnica.com/science/2018/10/gender-differences-in-personality-are-bigger-in-egalitarian-countries/
1•Tomte•10m ago•0 comments

Why does Taylor Swift write so many one-note melodies? (2017)

https://www.bbc.com/news/entertainment-arts-41886475
1•Tomte•10m ago•0 comments

Why Windows 11’s most important new feature is post-quantum cryptography

https://arstechnica.com/security/2025/05/heres-how-windows-11-aims-to-make-the-world-safe-in-the-post-quantum-era/
1•Ivan92•11m ago•0 comments

Show HN: Bricks – One Click Dashboards from Your Data Using AI

https://app.thebricks.com/sign-up
1•manpreetsgarha•11m ago•0 comments

Financial Datasets: Connect your LLM to the stock market

https://www.financialdatasets.ai/
1•handfuloflight•13m ago•0 comments

Enter the maze of Hong Kong's tech wonderland

https://restofworld.org/2022/tech-markets-hong-kong/
1•outrunner•13m ago•0 comments

Show HN: A Social Media Feed for Busy B2B SaaS Founders

https://getmentio.com/
3•Mredfox•15m ago•1 comments

Starfish Space announces plans for first commercial satellite docking

https://www.nasaspaceflight.com/2025/05/starfish-plans-first-commercial-satellite-docking/
1•LorenDB•16m ago•0 comments

Computational Public Space [video]

https://www.youtube.com/watch?v=PixPSNRDNMU
1•coloneltcb•17m ago•0 comments

Optional Rust-in-FreeBSD Support May 2025 Status Report

https://hardenedbsd.org/article/shawn-webb/2025-05-20/optional-rust-freebsd-support-may-2025-status-report
2•todsacerdoti•17m ago•0 comments

Show HN: I made a SaaS to generate viral scripts for faceless Shorts

https://zeroface.ai/
1•maximedupre•19m ago•0 comments

Hosting SQLite databases on GitHub Pages – (or IPFS or any static file hoster) (2021)

https://phiresky.github.io/blog/2021/hosting-sqlite-databases-on-github-pages/
2•thunderbong•19m ago•0 comments

Do electric cars need a gearbox?

https://www.youtube.com/watch?v=YAryICHkKjA
2•janosch_123•20m ago•1 comments

Agentic AI Systems – Tools, System Design, and Resources for AI Agents

https://github.com/alirezadir/Agentic-AI-Systems
2•alirezadeer•20m ago•0 comments

Pushing a whole stack of branches with a single Git command

https://andrewlock.net/pushing-a-whole-stack-of-branches-with-a-single-git-command/
1•bpugh•22m ago•0 comments

Docker Launches Hardened Images, Intensifying Secure Container Market

https://thenewstack.io/docker-launches-hardened-images-intensifying-secure-container-market/
1•CrankyBear•22m ago•0 comments

Can You Fool the Audience?

https://www.honest-broker.com/p/can-you-fool-the-audience
1•paulpauper•26m ago•0 comments