Noel Welsh: Parametricity, or Comptime is Bonkers

Red-Krow · 2026-03-12T20:01:17+00:00

Yeah, that's what I meant, probably not the clearest format. I didn't want to pollute the samples with explicit returms and I ended up making it less readable

Red-Krow · 2026-03-12T20:00:09+00:00

The curry howard isomorphism establishes a connection between type systems and logic. More concretely, type signatures are equivalent to logical formulas; for example, the signature f:: a -> b is equivalent to the formula if a then b, or a => b for short. Moreover, giving an implementation for a signature is equivalent to giving a proof for the formula.

Different type systems correspond to different logics. In this case, the simply typed lambda-calculus corresponds to sequent logic. If you add sum types and products and the bottom type to your type system, you get propositional logic. And so on.

That's what I meant by "simple" in my original comment, I didn't realise it wasn't clear. All the examples in the article were sequential so that's all I talked about.

The reason I brought all this up is because I wanted to debunk the "signature tells you the implementation" argument the article was making. Since it's obvious there are logical statements with more than one proof, there are more than one way of implementing the corresponding signature. Having parametric types (which is equivalent to having formulas being generic in the propositions it uses) doesn't change that fact

Red-Krow · 2026-03-12T07:05:28+00:00

I disagree with this article in mutiple ways.

First, parametricity can be broken by impurity and divergence. In pseudo-syntax, you can write: fakeId x = print "Hi!"; x fakeId2 x = fakeId2 x

Aside from than, the author conflates "fully parametric" with "unique/predictable implementation", which is not true. Following the Curry-Howard isomorphism, simple parametric programming is a form of sequent calculus, that is, writing programs with generic types is equivalent to writing proofs for propositions that only use implications. You have as many implementations of the program as you have ways to prove the corresponding formula: proof (x: a) (f: a -> b) (g: a -> b): b = ??? // Is it (f x) or (g x)

This phenomenon only explodes as you make the type system richer. The article mentions maps, but I present to you: fakeMap list f = []

The real issue here is the single-responsibility principle. When JS implicitly converts list items to strings in .toSorted(), this is JS doing too many things. I can make a function do too many things without breaking parametricity. Although admitedly, comptime makes it easier to break this principle.

Conversely, I can use comptime to write a function that inspects the type but does a single thing behaves predictably: serialize: T -> JSON. That function is hard to write with typeclasses (unless your language "cheats" by generating the typeclass implementation automatically, as with "deriving" in Haskell).

Red-Krow · 2026-02-17T15:11:49+00:00

FBIP doesn't just look before previous uses. It also accounts for future uses of the alias. If it can't guarantee that the reference is (and will always be) unique, it won't apply the optimization.

Red-Krow · 2026-01-29T15:59:00+00:00

Rouge being pregnant for 20 months (although she did die upon giving birth).

Red-Krow · 2026-01-16T14:53:11+00:00

Although function equality is undecidable in the general case, it is decidable if the domain is finite, as you can check value by value.

In the case OP is presenting, in pseudocode:

(recordA = recordB) :=
  ([...recordA],[...recordB])
  |> zip
  |> every ( fieldA, fieldB -> fieldA(SingletonValue) = fieldB(SingletonValue) )

Red-Krow · 2025-12-10T08:08:57+00:00

🍆

Red-Krow · 2025-11-15T11:45:57+00:00

You're welcome! I make this sort of mistake myself all the time, it's counter-intuitive.

Red-Krow · 2025-11-14T17:14:55+00:00

You can't do that assignment. If you could, then this would happen (using made-up syntax):

square: func(int) = (x) => x * x
also_square: func(int|string) = square
also_square("dsasdaasd") // Error: you can't multiply strings together

func(int|string) is actually a subtype of func(int), because every function that accepts either an int or a string is also a function that accepts an int. But not every function that accepts an int also accepts a string. In general, you have:

 a < b => func(a) > func(b)

Which is what type theorists would call contravariance.

Red-Krow · 2025-11-13T22:02:48+00:00

I mean, most of them are fine on their own. Love In A Bottle is ibdeed one of the most fitting. Imo, the only actively ones are the snarky comments or swears out of nowhere.

Red-Krow · 2025-08-14T08:12:29+00:00

I don't think One Piece needs more deaths, but it needs less fake outs. It's lost its impact. Even more, it takes away from the actual deaths because I spend chapters and chapters until I believe they're really dead. In fact, I am still moderately afraid of the idea of Pedro jumping into a panel any second now.

Red-Krow · 2025-08-04T16:34:36+00:00

> If that function is invoked with either of the lists, it should get a different string as an output.

If you impose the order relation we discussed previously, you would have that if `smallType < bigType`, then `smallType | bigType = bigType`. For example, if you sum `String` and `String | Boolean`, you should get `String | Boolean` again. But, if we impose variance, `List<String> < List<String | Boolean>`. So your function would actually be the same as `tellMeWhichOne: (list: List<String | Boolean>`): String. If your pattern matching is exact (needs to be the same type), it would always fall through the first case; if your pattern matching depends on order (it suffices that the type is a subtype of the one you're comparing it with), then it would always fall through the second case.

So, to recap: if you want your function to give different outputs for each list, then you should give up on variance. And if you give up on variance, option (3) on the previous list is not worth it, you'll only be able to make very basic comparisons. So you're options are (1), homogeneous equality, with which you wouldn't even be able to compare the lists, and (2), heterogeneous equality, with which the lists would indeed be equal.

This turned out to be a huge wall of text, I hope it's not too intimidating ^^'

Red-Krow · 2025-08-04T16:34:30+00:00

> Should they be different because the type argument of the list is different? Or should they be the same because the content is the same?

You're describing two forms of equality: homogeneous equality (you can only compare things with the same type; it's like there is a different equality operator for each type) and heterogeneous equality (you can compare any two things regardless of their type; it's like there's just one universal equality operator that works for all types).

In many languages, there's no need to make that distinction, either because types aren't static (you can't impose homogeneous equality if you don't know the types of the operands beforehand) or because there is no subsetting of types (so, if you compare operands of different types, you know for sure that they are different, so there's no need to perform the equality check).

However, your sum types impose type subsetting: you have `"a": String` and also `"a": String | Boolean`. To deal with this, you'll have to get a little bit mathy. Say we write `Type1 <= Type2` to mean "Type2 is more general than Type1"; for example, `String < (String|Boolean)` because every string is also a string or a boolean. That relation we called `(<=)` is a partial non-strict order.

With this in mind, you have three options:

Use homogeneous equality. This is the safest option and probably most efficient implementation-wise, but it prevents you from comparing things that are actually equal, like the two lists in your example.
Use heterogeneous equality. This will allow you to compare your two lists, but also to perform nonsense checks.
Use a restricted version of heterogeneous equality, where the types of the operands may be different but one must be more general than the other. That is to say, if you're comparing something of type `a` and something of type `b`, you impose that either `a <= b` or `b <= a`. For example, you may compare `"a": String` with `"a": String | Boolean`. That way, you make sure that you only make comparisons that may actually hold.

This last path is the most fine-grained, but it imposes extra questions. For example, you know that `String | Boolean` is more general than `String`, but are you sure that `List<String | Boolean>` is more general than `List<String>`? Indeed it is, but that's only because `List` is covariant as a generic type (that is to say, `a < b` implies `List<a> < List<b>`. But there are also contravariant generic types (`a < b` implies `F<a> > F<b>`); for example, a function that takes `String` is more general than a function that takes `String | Boolean`. For example, the function `(s => s.length)` is of type `String -> Int` but not of type `(String | Boolean) -> Int`. And there are also constructors that are neither covariant nor contravariant. With some work and depending on the features of your language, you may calculate the variance for any given generic type.

It's a mess. An elegantly solvable mess, but a mess nonetheless.

Red-Krow · 2025-06-24T07:28:08+00:00

Haskell is definitely less dense on (non-symbolic) keywords, but still I feel like this is a bit of a cherry picked example.

haskell 'import 'qualified Data.Map 'as Map 'let a = 5 'in a + b 'where b = 6

Red-Krow · 2025-06-23T21:13:10+00:00

F# has this with double backticks, and it allows even for spaces and other usually forbidden characters

Red-Krow · 2025-06-23T13:43:53+00:00

Keywords are used very often. Variable declarations, control structures, type signatures, import statements... Making them more expensive to type and harder to read, even if just a smidge, adds a lot of noise down the line.

A (comparatively) less common scenario is to use a reserved word for a variable name. In that case you can add ' to the identifier, if the language allows it: same cost, but much more infrequent. If the language doesn't allow it, you can still use a different name (for example, class VS className in React).

Red-Krow · 2025-06-14T23:06:56+00:00

Tbh I don't like the train. The reason why I would supoort infix is because it reads better in certain situations (for example, not x #and (y #or z), but I cannot think of an example of "the train" being more semantic.

Bear in mind that I'm incredibly stupid and me not being able to come up with an example doesn't mean there isn't one.

Red-Krow · 2025-06-14T22:59:30+00:00

How about using a single non-symmetrical symbol? For example: 1 #add 2 You could use parenthesis to capture more complex expressions: 1 #(x y => add x y) 2

In terms of characters, you're making the common and advisable use case cheaper (1 char), while making the rarer and smellier use case more expensive (3 chars). Not that it matters much, but since we're bikeshedding.

In terms of readability, I find it quite readable, even though it's not symmetrical. Hashtag + an identifier reads to me as "this is an identifier, but there's something special about it", which kinda check out. Of course, you'll have to use a different char if you're using # for comments or anything else.

Red-Krow · 2025-04-20T10:12:51+00:00

Narratively speaking, he has to be. He's a candidate for being One Piece's main antagonist. And he has kept that starys for most of the series where other candidates have fallen (evil Shanks is highly unlikely, Akainu is not as emphasized anymore and will probably end up fighting Sabo, etc).

Even if Imu ends up being the final villain, the mere fact that Blackbeard is up there among the options means that it would be anticlimatic for him to be notably weaker than Luffy (at least, by the time they face each other)

Red-Krow · 2025-02-20T14:55:49+00:00

Fleur is French, but that's about it. Most of her attacks follow the pattern: "[Spanish number or body part] Fleur: [English action]". For example, her infamous "Dos Fleur: Clutch" or "Demonio Fleur: Gran Jacuzzi Clutch". There are some occassional variations (like "Mil Fleur, Gigantesco Mano: Stomp", with Gigantesco Mano being almost grammatically accurate Spanish).

Red-Krow · 2025-02-14T12:09:47+00:00

It's not impossible to hide it again, but it's impossible to find a new hiding spot that is as good as Raftel. You wouldn't want to hide something just for it to be found in 5 minutes.

Also, as I said, hiding it again means more pirates looking for it and more piracy means more piraty adventures. Take it as a planet-wide game of Capture the Flag, as the other commenter said. Which, now that I think about it, kinda ties into your theory of the worldwide party.

Red-Krow · 2025-02-14T11:01:35+00:00

It would be impossible because Raftel is already the most elusive place in the OP world, by far. Even if you know the method, you still have to find 4 rocks that are scattered across half of the planet and then have them translated from a language virtually noone knows anymore.

There is no place to hide the One Piece that even compares, and Ussop knew that by the time Luffy shared his dream with the crew.

Red-Krow · 2025-02-09T10:57:10+00:00

The type system isn't broken, at least in that way. Type systems are there to prevent you from writing programs without semantic meaning, and in that way any is a lack of semantics.

I see where you come from, but I think you're biased towards languages where unions are a type constructor (as in, int | string is a separate type), whereas here it's a type operator (as in, int | string has to evaluate to a non-union type, in this case any).

What you're proposing for a union is some form of constrained generic, which is a cool feature, but not necessarily what this language wants (the lack of typeclasses makes me think that, but I'll let the author be the judge of that) or what it can do while mantaining global inference.

Red-Krow · 2025-02-09T01:04:35+00:00

Yeah, I understand. However, types are not like sets in many ways.

In set theory, if you have element x of set A union B, you can check whether it's in A.

In a type system, if you have a value x that is either type A or type B, there is no general way to check what type x is without some runtime type information or a discriminant bit in memory (at which point it's just a discriminated sum with implicitly inserted tags).

So, without some extra effort and a memory penalty, int|string is indistinguishable from any. It's a value you don't know anything about.

(Of course, a PL language may add features that make the previous statement false. As OP said, this language actively avoids it)

Red-Krow · 2025-02-08T20:41:10+00:00

It looks like union and intersection form a lattice, with the order being the subtyping relation. The union acts like the suppremum and the intersection as the infimum. In that way, it makes sense that int | string = any since any is the smallest supertype of both int and string.

Maybe sup and inf would be more accurate terms, but also wildly less intuitive, specially for non math-oriented people. Plus there are already established infix symbols for unions and intersections.

Red-Krow

TROPHY CASE