← Feed

Posts

• Post #4299219

  I’ve seen a number of people speak about a representation of datatypes in ML where a datatype is given by a module with an abstract type and its constructors. Obviously, this is missing some additional information to define pattern matching, e.g. a recursor. Has anyone actually worked out all of the details?

• Post #4299218

• Post #4299217

  The latest Lean soundness hole (https://github.com/leanprover/lean4/issues/14576), which also affects alternative implementations of the kernel, is proof that God only ever intended for us to use W-types, and certainly not nested inductives.

• Post #4299216

  we need to consider deceleration

• Post #3721908

  @joe@f.duriansoftware.com @slava@mathstodon.xyz I know we talked about this as part of a shitpost thread, but can either of you think of a good way to combine traits (i.e. type classes) and bytewise equality / hashing while still preserving as much parametricity as possible? The natural thing is to have some marker trait with C++ style specialization, but that destroys a lot of the properties that you would want. @joe@f.duriansoftware.com mentioned (jokingly but maybe not) to just make it requi...

• Post #3613086

  @dotstdy@mastodon.social @ianh@mastodon.social Has any recent language adopted uncurried single arg style where product types are used for multiple args rather than implicit currying? I know that Swift originally started in this direction, but I forget the actual reason why they backed away from this. Can you refresh my memory, @joe@f.duriansoftware.com ?

• Post #3028188

  @joe@f.duriansoftware.com Why did Swift never get block expressions? Was nice trailing lambda syntax worth more?

• Post #2742134

  I'm always curious about peoples' pure C compiler codebases, so I took a look at Vercel's new Zero language (https://zerolang.ai). You can tell that someone is just fed up with the bullshit of using unions in C when you see this: struct Expr { ExprKind kind; char *text; char *resolved_type; bool moves_ownership; bool mutable_borrow; bool bool_value; bool array_repeat; Expr *left; Expr *right; ExprVec args; TypeArgVec type_args; TypeArgVec checked_type_args;...

• Post #2578883

  A conversation with @jiribenes about parsers in Effekt (https://effekt-lang.org) made me realize this interesting question: can determinization of non-deterministic LL(1) parsers a specific of a general program transformation for programs with a nondeterminism effect?

• Post #2578882

  I treat garbage collected languages like Undertale and always go for a pacifist run.

• Post #2578881

  @joe It occurred to me while walking today that if all of the arguments for stackless coroutines are valid, then Rust should actually switch to CPS for compiling all (non-recursive?) functions.

• Post #2236928

  C++ is the final stage of programming languages, a pure Simulacrum with no relationship to reality whatsoever.

• Post #2101897

  @jonmsterling Do you think it is possible to make an ML/prover combo in the LCF style so that the metalanguage’s module/locale/… system can adequately model mathematical hierarchies, or is the pure LCF architecture relegated to history?

• Post #1889578

  @joe@f.duriansoftware.com What do you think is the maximal subset of effect handlers that can be supported well in a C-like language (with a C-like compilation model)?

• Post #1870929

  GitHub is the only web app that got less reliable after it stopped being (as much of) a Rails monolith.

• Post #1870928

  For a long time I believed that one of the advantages of dependent type theory for applications to SW/HW verification was that it naturally incorporates proof by reflection (since the kernel type checker can do nontrivial computations). In particular, this comes in handy when dealing with decision procedures. Even when they can produce a proof (e.g. SAT solvers producing resolution proofs), the proof term is usually too large for this approach to scale to real problems. And there are many cases...

• Post #1643525

  LLVM is so afraid of optimizing around atomics that it is more pessimistic about an inlined atomic than an extern function: https://discourse.llvm.org/t/missed-store-forwarding-in-the-presence-of-atomic-operations/90653

• Post #1629772

  Rust's lack of relative enum constructor names makes me dread having two enums with the same name.

• Post #1629771

  The province of Saskatchewan (except for the Alberta border city of Lloydminster) has never followed daylight savings time, opting for permanent Central Standard Time. Alberta is now adopting permanent Mountain Daylight Time, which is synchronized with Saskatchewan. This is a great real-world example of the difference between intensional and extensional equality.

• Post #1629770

  Despite Rust deliberately making your life miserable if you dare attempt to use unstable features that have existed for years, I caved and used the `gen_blocks` feature (https://github.com/rust-lang/rfcs/pull/3513) to reimplement a complicated iterator whose logic I had initially written by hand. They should really finish sanding the edges and stabilize this feature so that nobody needs to write iterators as explicit state machines ever again.

• Post #1556656

  You either die a hero or live long enough to break subject reduction.

• Post #1490236

  One of the most pressing naming discussions of our time: when you have a sum type `Token`, `Expr`, etc. and then a wrapper containing it + some common info (like trivia for `Token`, a source span for other nodes) what do you call the two? I used to always default to `Expr` and `ExprData`, but rustc generally defaults to `ExprKind` and `Expr`, despite `ExprKind` containing lots of data beyond just the plain `enum` that it represents: https://doc.rust-lang.org/beta/nightly-rustc/rustc_ast/ast/enum...

• Post #1490235

  I just saw an ad that began with “inflight Wi-Fi has come a long way since I was a kid”. I am officially unc, also chopped.

• Post #1111453

  combined Davos/POPL keynote ideas "You'll own nothing and you'll be happy: a garbage collection rejoinder" "The great shift/reset: a continuation or delimiter of progress?" "Late-staged programming: are the economics of macros sustainable?"

• Post #998432

  Can someone please tell Leo that these obviously LLM-generated blog posts are cringe? https://leodemoura.github.io/blog/2026-4-2-why-lean/

• Post #921274

  Sci-fi novel idea: you're a human who wakes up with amnesia every day and reads your AGENTS.md file.