These sources are about how languages are designed and what their type systems can catch. This page lists 38 sources, oldest first where dated.
Fast Functional Lists, Hash-Lists, Deques and Variable Length Arrays
This record covers the abstract of a technical report held in a university repository. The abstract claims large space and speed gains over linked lists. It also mentions an interpreter and a benchmark against OCAML.
Ten Years of Purely Functional Data Structures
Chris Okasaki recalls how the 1998 book grew from doctoral work on lazy data structures. The post covers the book's origins, its reception, and common complaints. About 35 reader comments follow, from 2008 to 2023, with requests and error reports. The evidence is memoir.
The Error Model
Joe Duffy describes how the Midori team treated bugs and recoverable errors as separate problems. The post is a long design history with code samples and the rejected alternatives. Its evidence is the team's experience, a few reported ratios and one anecdote.
The Missing Manual for Signals: State Management for Python Developers
Tuan Anh Bui, who maintains the Python library reaktiv, explains signals using that library. The guide argues signals suit systems where changes cascade through derived values. It gives patterns, anti-patterns and three scenario sketches. The evidence is argument and illustrative code.
xvw.lol - Guarded methods in OCaml
The note defines guarded methods and builds them in OCaml with a short worked example. The evidence is runnable-looking code, assertions and one compile error. The author calls the encoding somewhat heavy. The author says it is probably not useful.
Flix – A powerful effect-oriented programming language
This thread of 341 points discusses the Flix home page. Many comments question the JVM base, effect systems and built-in Datalog. One of the Flix developers, jorkadeen, answers many of them.
Formatting code should be unnecessary
The thread discusses Max Leiter's post on Ada tools that stored code as trees. Commenters mostly argue over plain text storage, formatters and bikeshedding. It is a broad mix of opinions, anecdotes and tool suggestions.
Death to type classes
This is a comment thread on a niche Haskell post at jappie.me. Many replies ask whether the post suits readers outside Haskell. Others explain Backpack, ML modules and past Haskell effect libraries. The evidence is opinion and explanation from commenters.
Compiling with Continuations
This is a comment thread about a review of an old compiler book. Commenters argue over whether code for the book exists. They also argue over whether continuation passing style is used. Several share personal experience implementing it. The evidence is anecdote and technical opinion.
The Programming Languages Zoo
This is a comment thread, and most of it wanders from the linked site. It starts with a question about a language that has every feature. It then covers design tradeoffs and whether languages are math or interface. Another strand asks about languages for coding agents. The evidence is opinion and links.
Interactive λ-Reduction
This is a comment thread where the paper behind the site is questioned and defended. The paper author joins to explain the aim and the terms. Commenters with interaction net knowledge add context. The evidence is argument and explanation.
Value numbering
Max Bernstein explains value numbering as a way to reuse equal pure instructions. The post goes from one block to whole functions, with Java excerpts. It then covers impure instructions and points to other approaches. The ending holds unfinished notes.
Stateless Actors
Massicotte works through several cases where a Swift actor holds no mutable properties. The post weighs each with short code samples and stated trade-offs. The post is reasoned opinion with no measurements.
Thermite
The entry describes Thermite as a Rust-shaped language with mandatory contracts on every function. It explains an assurance ladder that records how each obligation was checked. It also lists limits that the entry itself admits. The evidence is the catalogue's own description, not an independent test.
Show HN: Pure Effect – Reproduce production bugs on your laptop without a DB
The thread opens with the maker's launch text for the library. The text claims testing without mocks and local replay of production bugs. Replies question the evidence, compare it with Effect-TS and describe limits of the pattern. The evidence is the maker's description and commenter opinion.
Record type inference for dummies
Gabriella Gonzalez teaches type inference for anonymous records to readers new to type theory. The post grows a tiny language step by step, with inference rules and runnable Haskell. It ends by contrasting subtyping with row polymorphism. The evidence is worked code and examples.
Haskell koan: Type-checked non-empty strings
Mike Ledger describes a technique used in production at Bellroy for a NonEmptyText type. It combines RequiredTypeArguments with an overlapping instance that raises a custom type error. The post reports one measured benefit and ends with a longer DynamoDB table-name example.
RRB-Trees: Efficient Immutable Vectors (2012) [pdf]
This is a small thread of implementer comments. Commenters name libraries that use RRB-trees. One reports switching to B-trees after hitting a depth problem. Another starts designing a hybrid. The evidence is personal experience and links.
Ante: A New Way to Blend Borrow Checking and Reference Counting
Ovadia explains a work-in-progress language design. The post uses short code examples and compiler error comments. The post says some parts are implemented and some are theoretical. It also lists open problems that Ante's creator has raised.
Actegories
Bartosz Milewski defines monoidal categories, then actegories, and writes each as a Haskell class. The post says actegories matter for optics but does not reach lenses itself. Evidence is definitions, code and a few instances. Much of the mathematical notation did not survive text extraction.
NoiseLang: Where N = 5 is a Dirac delta
The author presents a language for writing probability as math. The post covers the idea, the compiler design, timings and demos such as estimating pi. Evidence is the author's own benchmarks on one machine, plus reader corrections.
Show HN: Wyzer Programming Language
The thread opens with a short launch post. Most replies say the README does not show the language's main ideas. One researcher explains how choreographic programming prevents deadlocks. A long side dispute covers garbage collection speed.
A Design Space Exploration of Async/Await
Gavin Gray summarizes a paper comparing async/await in several languages. The post opens with a short program that prints different output in different runtimes. It then lists nine design dimensions and a formal model. The evidence is the runtime comparison and the paper, which this page does not cover.
core - Rust (Crate core)
This is the front page of the reference docs for the core crate. It explains what core is and which symbols it expects the platform to supply. The rest is an index of primitive types, modules, macros, keywords and attributes.
COMEFROM
The article defines COMEFROM and explains how it differs from goto. It traces the idea to a 1973 Datamation piece and lists implementations in several languages. Its support is citations and short code examples.
Alloy
Alloy is a small ORM written in the Temper language. A CI pipeline compiles it to six target languages and updates six demo todo apps. The README includes a long security section the project assessed itself.
A conceptual overview of the ideas and objects which power asyncio
The README is the motivation and table of contents for a five-part guide. The author says the official docs lack an overview of design and architecture. It poses three questions the guide aims to answer.
The C++ Iceberg
The page is a list of terse titles. It is very short and gives no explanations itself. The page says its entries are clickable links to fuller material.
The Granule Project: A Research Project Studying the Next Generation of Functional Programming Languages
The page states the project's aim and lists its languages, Granule and Gerty. Most of it is a dated news feed of papers, awards, grants and hires. It describes the work but does not explain the technical ideas in depth.
Multiplicities
This is the project's own tutorial page on multiplicities in Idris 2. It explains erasure, linear use and matching on types through short code examples. The evidence is worked examples with compiler messages, not experiments.
Type Driven Development with Idris: Updates Required
This page is a changelog for readers of Edwin Brady's Idris book. It goes chapter by chapter with the exact edits to each code file. It is a practical reference, with no argument beyond the edits themselves.
Control structures for programming languages: from goto to algebraic effects
This is a short landing page for a forthcoming book by Xavier Leroy. It gives an abstract, a table of contents, and links to code samples. The page itself holds no chapter text.
Error and exception handling
This recipe teaches the Common Lisp condition system through short REPL examples. It stresses that conditions are not only errors and that handlers can choose restarts. The evidence is worked code with printed output.
Learn Programming with OCaml
This is a short download page, not the book. It names the authors and translator, the funder and the license. It links a PDF, an EPUB and the code.
Thinking in an array language (ngn-k-tutorial, chapter 12)
The chapter starts with a loop-based translation of a textbook algorithm. It removes globals and loops one at a time, ending in a short tacit function. Its support is the worked sequence of code.
Introduction - The Rust Programming Language
This is the introduction to the Rust project's own introductory book. It is promotional in tone and sets out the audience, chapter plan and reading advice. It offers claims about Rust but no tests or data.
CS 6120: The Self-Guided Course
The page is a lesson-by-lesson reading and viewing list for Cornell's CS 6120. It names papers for many lessons and says which lessons have implementation tasks. It lists the curriculum only; the lesson content was not read.
The Unison language
This is a short promotional home page by the language's makers. It lists five headline features and three code samples. It makes claims without evidence beyond those samples.
Glossary
- Abandonment
- Midori's term for fail-fast, where a bug tears down the whole process.
- ABI
- The binary-level interface that compiled code relies on to work together.
- Abilities
- Unison's name for effects, which mark what a function may do, such as I/O.
- Actegory
- A category on which a monoidal category acts, like scaling its objects.
- Actor
- A Swift type that runs code one task at a time to protect data.
- Algebraic effect
- A way to declare effects in a program and give them meaning with handlers.
- AM and FM
- Two ways of encoding a message in a radio wave.
- Amortized analysis
- A way to bound the average cost of operations over a sequence.
- ANF
- A compiler form that names every intermediate result.
- Anonymous record
- A record whose shape is written inline, with no named datatype declaration.
- Assurance ladder
- A scale that rates how strong the evidence is for each checked claim.
- AST
- A tree that represents the structure of a program.
- Async/await
- Syntax that lets concurrent code read like straight-line code.
- Asyncio
- Python's standard library for running many tasks concurrently in one thread.
- Awaitable
- An object that a coroutine can wait on with await.
- B-tree
- A balanced tree whose nodes hold many entries.
- Backpack
- A Haskell extension that lets code depend on module signatures, as OCaml modules do.
- Beta reduction
- The basic step that applies a function to its argument.
- Bifunctor
- A type constructor with two parameters that can be mapped over in both.
- Bikeshedding
- Spending debate on a trivial choice because everyone can have an opinion.
- Borrow checking
- A compile-time check that references to data are used safely and do not outlive it.
- Breakpoint
- A marked line where a debugger pauses a program.
- Bril
- A small teaching language made for this class.
- Call/cc
- A Scheme operation that captures the current continuation.
- Cancellation
- Asking a running task to stop before it finishes.
- Cargo
- Rust's bundled package manager and build tool.
- CC BY SA 4.0
- A Creative Commons license that allows sharing and changes with credit and the same license.
- Checked exception
- An exception that the type system makes a function declare.
- Choreographic programming
- Writing one global program of message exchanges that compiles into code for each machine.
- Coeffect
- A description of what a program needs from its context.
- Computed
- A value derived from other signals that is cached and recomputed when needed.
- Concat
- Joining two sequences into one.
- Condition
- A Lisp object that describes something noteworthy that happened in a program.
- Content-addressed code
- Code identified by a hash of its content rather than by a name.
- Continuation
- A representation of what a program will do next, treated as a value.
- Contract
- A written promise about what a function needs and what it guarantees.
- Control structure
- A language feature that decides the order in which a program runs.
- Core
- The smallest layer of the Rust standard library, usable without an operating system.
- Coroutine
- A function that can pause and resume.
- Covering
- A function is covering when it handles every possible input.
- CPS
- Continuation passing style, where every function is given its next step as an argument.
- Custom executor
- A way to choose which queue or thread an actor runs on.
- CWE
- A numbered public list of common software weakness types.
- Data flow analysis
- A method of tracking how values move through a program.
- Datalog
- A logic language for queries over facts and rules.
- Debouncing
- Waiting for input to pause before acting on it.
- Delta-Nets
- The paper's graph-based system for optimal lambda reduction.
- Dependent Haskell
- A planned direction for Haskell where types can depend on values.
- Dependent type
- A type that can mention values, such as a vector with a length.
- Dependent types
- Types that can depend on values.
- Deque
- A queue that allows adding and removing at both ends.
- DIANA
- An intermediate form for Ada programs, described in the post as stored instead of text.
- Dirac delta
- A distribution with all its weight on one single value.
- Directed acyclic graph
- A set of nodes linked one way with no loops.
- Distributed deadlock
- A state where separate services wait on each other forever.
- Dominator
- A block that every path to another block must pass through first.
- Each-right and each-left
- Operators that pair one value with every item of another.
- Effect
- Code that runs when signals it reads change, to touch the outside world.
- Effect library
- A library that models side effects such as I/O as values.
- Effect system
- A type feature that tracks what side effects code may perform.
- Effect-TS
- A larger, full-featured TypeScript effect framework.
- EPUB
- A file format for e-books.
- Erasure
- Removing values at compile time so they do not exist when the program runs.
- Esoteric language
- A language made as a joke or experiment, not for practical use.
- Event loop
- The scheduler that decides which waiting task runs next.
- Extension method
- A method added to a class from outside its definition.
- Fold
- An operator that combines a list to one value, such as a sum.
- Formal semantics
- A precise mathematical account of what each program step does.
- Functor (ML)
- In OCaml, a module-level function that takes a module and returns a module.
- GADT
- A generalized algebraic data type, which lets constructors refine type information.
- Garbage collection
- Automatic reclaiming of memory that a program no longer uses.
- Garbage collector
- A runtime part that frees unused memory automatically.
- GCD
- Apple's older Grand Central Dispatch system for running work on queues.
- Global actor
- An actor whose isolation can be applied to code across a whole program.
- Goto
- A statement that jumps to a labelled place in a program.
- Graded types
- Types that carry extra information about how a value is used.
- Guarded method
- A method that can be called only when the receiver's type meets a stated condition.
- Hash-consing
- Reusing one stored copy of equal items, found by hashing.
- HCI
- Human-computer interaction, the study of how people use computers.
- Hole
- A placeholder in code that the compiler reports the expected type of.
- HVM
- A runtime for interaction nets, built by the Higher Order Company.
- Iceberg list
- A meme format that sorts topics by depth, from well known to obscure.
- Immutable vector
- A list-like collection that is never changed, only copied with edits.
- Implicit argument
- An argument the compiler fills in without being written at the call.
- Interaction net
- A graph rewriting system where only local changes happen.
- INTERCAL
- An esoteric language designed as a parody of programming languages.
- Intermediate representation
- A simplified program form that a compiler uses between source code and machine code.
- IR
- An intermediate representation used inside a compiler.
- JIT
- A compiler that turns code into machine code while the program runs.
- JVM
- The Java Virtual Machine, a runtime that many languages compile to.
- K
- A terse array programming language descended from APL.
- Keeper
- An object that recovers from an error on the spot, without unwinding.
- Label
- A name marking a spot in code that a jump can target.
- Lambda calculus
- A tiny model of computation built only from functions and function application.
- Lazy evaluation
- Delaying a computation until its result is actually needed.
- Lean
- A proof assistant, used here to re-check solver answers.
- Libc
- The standard C library that most operating systems provide.
- Linear type
- A type whose values must be used exactly once.
- Linear types
- Types that force a value to be used exactly once.
- Linked list
- A list where each item points to the next item.
- Linter
- A tool that checks code for style problems or likely mistakes.
- LLVM
- An open-source compiler toolkit used to build and optimize languages.
- Map-reduce
- A pattern that transforms many items and then combines the results.
- Mass assignment
- A flaw where users set fields they should not be able to set.
- Metaobject protocol
- A way to define a language by objects that describe how the language itself behaves.
- Midori
- An experimental operating system whose language and design the post describes.
- Mocking
- Replacing a real dependency with a stand-in during a test.
- Monoidal category
- A category with a way to combine two objects, plus a unit object.
- Monomorphization
- Making a separate compiled copy of generic code for each type.
- Monte Carlo
- Estimating an answer by running many random trials.
- Most vexing parse
- A C++ rule that reads some object declarations as function declarations.
- Mtl
- A long-used Haskell library for stacking effects such as state and errors.
- No_std
- An attribute that stops Rust linking the full standard library.
- Non-blocking socket
- A network connection that returns at once instead of waiting for data.
- Non-null type
- A type whose values can never be null.
- O(N)
- A cost that grows in step with the number of items.
- OCaml
- A functional programming language with a strong static type system.
- Optics
- Composable tools such as lenses for reading and updating parts of data.
- Optimal reduction
- Reducing lambda terms while sharing work so nothing is done twice.
- ORM
- Object-relational mapper, a library that builds database queries from code.
- Overlapping instance
- A typeclass instance that wins over a more general one for matching types.
- Ownership
- Rust's system of rules for managing memory without a garbage collector.
- Panic handler
- A function that runs when a Rust program hits an unrecoverable error.
- Parser generator
- A tool that builds a parser from a grammar description.
- Perceus
- A reference counting method that reuses memory in place when a value is not shared.
- Persistent
- A data structure that keeps its old versions when changed.
- Phi function
- An SSA operation that merges values arriving from different paths.
- PII
- Personally identifiable information.
- PL
- Short for programming languages, as a field of study.
- Precondition
- A condition a caller must meet before a method may run.
- Prelude
- The set of definitions a language imports by default.
- Projectional editing
- Editing a program's tree directly while the editor shows a chosen view.
- Pure function
- A function that gives the same output for the same input and changes nothing else.
- Purely functional data structure
- A structure that is never changed in place, so old versions stay valid.
- Quantitative Type Theory
- A type theory where each variable has a usage quantity checked by the compiler.
- Radix tree
- A tree that finds items by successive pieces of an index.
- Receiver
- The object that a method is called on.
- Red-black tree
- A balanced search tree that keeps operations fast by coloring nodes.
- RefCell
- A Rust type that checks borrowing rules at run time and can panic.
- Reference counting
- Memory management that counts users of data and frees it at zero.
- Rejection conditioning
- Keeping only random trials that match what was observed.
- REPL
- An interactive prompt where code is typed and run.
- RequiredTypeArguments
- A GHC feature for passing a type to a function like a value.
- Restart
- A named way to recover that code can offer when a condition occurs.
- Reverse post order
- A block ordering where predecessors come before successors.
- Row polymorphism
- A way to write types for records with some fields plus named extras.
- RRB-tree
- A tree structure that stores sequences and supports fast indexing, slicing and joining.
- Runtime
- The system that schedules and runs a program's tasks.
- Sealed interface
- A type that code outside its module cannot extend.
- Seccomp
- A Linux feature that limits which system calls a program may make.
- Segfault
- A crash caused by a program touching memory it should not.
- Sendable
- A Swift marker for types that are safe to share between concurrent tasks.
- Session types
- Types that describe the order of messages in a conversation between programs.
- Show HN
- A Hacker News label for posts that show off a project.
- Signal
- A container for a value that tells dependents when it changes.
- Slime
- An Emacs mode for working interactively with Common Lisp.
- Smudge and clean filters
- Git hooks that transform files when they are checked out or staged.
- Spaceship operator
- A C++ operator that compares two values in one step.
- SQL injection
- An attack that smuggles database commands into user input.
- SSA
- Static single assignment, a code form where each name is assigned exactly once.
- Standard ML
- A strict functional programming language with a module system.
- Subtyping
- A rule letting a larger record type stand in for a smaller one.
- Systems programming
- Writing low-level software such as operating systems and embedded code.
- Tacit function
- A function defined without naming its arguments.
- Tail call elimination
- Reusing a stack frame when a function's last act is a call.
- Task
- A unit of asynchronous work that the runtime schedules.
- Temper
- A language that compiles one source to several other languages.
- Template Haskell
- A Haskell feature that runs code at compile time to generate other code.
- Tensor product
- The operation that combines two objects in a monoidal category.
- Type class
- A Haskell feature that lets one function name work differently for different types.
- Type equality witness
- A value whose existence proves that two types are the same.
- Type family
- A function that computes types from types.
- Type inference
- Working out the types of expressions without the programmer writing them.
- Type-level programming
- Doing computation in the type checker instead of at runtime.
- Typed hole
- A placeholder in a program that the checker reports as still unfilled.
- Typing derivation
- A step by step proof, drawn as a tree, that an expression has a type.
- UCM
- The Unison Codebase Manager, a tool used while writing Unison code.
- Unbound implicit
- An argument a function takes without it being named in the type.
- Undefined behavior (UB)
- Code whose result the language does not define, so anything may happen.
- Unification
- The compiler's process of working out what types and values must be equal.
- Union
- A type whose value is exactly one of several named variants, stored inline.
- Unwinding the stack
- Discarding function calls to return to an outer handler.
- Value numbering
- Labeling instructions so those with equal results can share one computation.
- View
- A data type that lets a function match on a value in a new way.
- VList
- A list data structure that stores items in growing blocks instead of single links.
- Vtable
- A table of function pointers that picks which method runs.
- WGSL
- The shader language used by the WebGPU standard.
- Zero-cost abstractions
- Higher-level features that compile to code as fast as hand-written low-level code.