The Next Great Functional Programming Language
summary
Argues for a concrete design: drop ad‑hoc features (GHC has ~70 extensions) and drop pattern matching and records and modules in favor of a small dependently typed, total core that uses Church encodings and lenses/prisms for data, with proof search and persistent proof databases to automate correctness. Notes Idris is a research testbed not production ready, cites Liquid Haskell and Unison as inspirations, reports having written "three million lines" of code that motivates a layered language with a dependently typed total core and a constrained I/O layer.
AI-written summary · about
chapters (9)
- 0:00Start
- 7:01Pattern Matching
- 8:26Records
- 9:40Modules
- 18:51Nominative Typing
- 26:04Data
- 40:09Recursion
- 47:36My Ideal FPL
- 57:06Inspirations
related talks
56mIdris: Programming with Dependent Types
01h 03mKeynote: Why Functional Programming Matters
44mSome History of Functional Programming Languages
26m(...) How to turn (Liquid) Haskell into a theorem prover
01h 07m50,000 Lines of LLM Haskell: What Broke, What Held, and Letting Go
49mErlang Rationale
35mProof Theory Impressionism: Blurring the Curry-Howard Line
04mLambda Days 2017