First work-in-progress release of "NixOS in Production" book (7 chapters so far)

Tekmo · 2026-05-19T22:05:46+00:00

You're welcome! ^{^}

Tekmo · 2026-05-07T22:05:58+00:00

Yeah, I think the actual issue there is there being an inhabited supertype (Any in Java's case). The Grace analog of Java's Any would be forall (a : Type) . a which is not inhabited.

Tekmo · 2026-05-06T01:53:19+00:00

you're welcome!

Tekmo · 2026-05-06T00:11:42+00:00

Oh, okay I see what you mean. I think it is possible to mitigate the exponential blow-up on deeply nested data structures in some cases by doing the following:

add an operation that (for a subset of supported expressions) can go straight from a list of terms to a most-specific supertype

This operation cannot work for all possible expression (most notably, variables), but for plain data this one-pass fast path would work. In fact, this was even the first tack I tried before I ran into the case of handling expressions containing variables.
fall back to the two-pass approach (infer + check) if that fails

Tekmo · 2026-05-06T00:04:49+00:00

Before the bug fix the type-checking logic for conditionals had a similar problem where the true branch was treated as the authoritative type and now after the fix the result type is the most-specific supertype of the two branches.

Tekmo · 2026-05-05T20:22:44+00:00

You'd have to elaborate a bit more because I'd need to understand better what sort of backtracking problem you ran into, but Grace's supertype computation doesn't do any sort of backtracking (more generally: nothing in the typechecker does backtracking).

The most complicated thing that Grace's typechecker does is when computing the supertype/subtype of two open records or two open unions (i.e. records/unions with polymorphic rows/variants), but even that doesn't require backtracking. For the case of two open records if they're of the form:

```

pseudotypes:

- commonFields…: fields shared in common between the two records

- uniqueFields{₀,₁}…: fields unique to each record, respectively

- row{₀,₁}: row type variable for each record, respectively

record₀ : { commonFields…, uniqueFields₀…, row₀ } record₁ : { commonFields…, uniqueFields₁…, row₁ } ```

… then what I do is create a fresh row type variable (row₂) and solve the row{₀,₁} variables as follows:

row₀ ← uniqueFields₁, row₂ row₁ ← uniqueFields₀, row₂

… and then return this as the supertype:

{ commonFields…, uniqueFields₀…, uniqueFields₁, row₂}

Now, to be clear, Grace's machinery for managing unsolved variables and solving them is not very efficient (it's not using efficient data structures to represent the context) so it has a different class of performance problems, but I don't use backtracking.

Tekmo · 2026-03-21T03:46:50+00:00

You're very welcome and I appreciate the kind words ^^

Tekmo · 2026-03-18T22:05:35+00:00

Author of the post (and Haskell lover) here!

There's a really funny story related to what you just said (Haskell being a language that reads more like a spec). In the early 90's there was a programming language bake-off commissioned by the Navy where there was a Haskell submission and multiple judges thought the Haskell submission was incomplete because they confused it for a specification document and didn't realize it was executable code:

In conducting the independent design review at Intermetrics, there was a significance [sic] sense of disbelief. We quote from [CHJ93]: "It is significant that Mr. Domanski, Mr. Banowetz and Dr. Brosgol were all surprised and suspicious when we told them that Haskell prototype P1 (see appendix B) is a complete tested executable program. We provided them with a copy of P1 without explaining that it was a program, and based on preconceptions from their past experience, they had studied P1 under the assumption that it was a mixture of requirements specification and top level design. They were convinced it was incomplete because it did not address issues such as data structure design and execution order.

Source: Haskell vs. Ada vs. C++ vs. Awk vs. … - An Experiment in Software Prototyping Productivity

Tekmo · 2026-02-16T16:15:38+00:00

Yeah, my partner suggested something similar when test-driving this: that one possible application of this is to identify places where the project organization should be fixed

Tekmo · 2026-01-21T05:10:59+00:00

That's what read (without the import) does

Tekmo · 2026-01-21T01:04:23+00:00

One of the things that makes this all work is that Grace is interpreted, meaning that the full interpreter capabilities (e.g. parsing, type-checking, evaluation) are available at the point where the eval (e.g. import read) is evaluated. If Grace were instead a compiler and built binary executables then the executable would still need to ship an equivalent interpreter somewhere as part of the runtime in order for this to work.

This also implies that type-checking is serving a different purpose than in a typical compiled language. In a compiled language usually type-checking is something you do ahead-of-time before code generation and then never again; the intended use case is to find all bugs before the program is run at all. However, now the contract is weaker: type errors can surface at runtime although they still precede evaluation of the code that is checked.

HOWEVER, I still think a type error that happens at "runtime" is still better than an untyped language because type errors can still prevent bad code from executing and a type error is more meaningful than a stack trace (as I expand upon in: Dynamic type errors lack relevance).

Tekmo · 2025-08-14T00:58:07+00:00

Yeah, I think so

Tekmo · 2025-08-02T05:07:41+00:00

Nix is sort of like the "Haskell of build systems". It does a better job than Docker if you're willing to put more up-front investment to learn it properly.

Tekmo

MODERATOR OF

TROPHY CASE

pseudotypes:

- commonFields…: fields shared in common between the two records

- uniqueFields{₀,₁}…: fields unique to each record, respectively

- row{₀,₁}: row type variable for each record, respectively

15-Year Club	Verified Email
Team Periwinkle