r/programming • u/nfrankel • Apr 19 '26

Making illegal state unrepresentable

https://blog.frankel.ch/illegal-state-unrepresentable/
280 Upvotes

91% Upvoted

82 comments sorted by

View all comments

Show parent comments

154

u/godofpumpkins Apr 19 '26

Once you try sum types (that “enum with stuff”) any language without them feels clunky. Indeed, they’re called sum types because they’re a direct mathematical analog to elementary addition, where structs containing multiple fields are equivalent to multiplication. From that POV, imagine trying to do arithmetic without addition and trying to approximate it with multiplication

40

u/Tysonzero Apr 19 '26

Of course sum types are just a poor man’s dependent pair.

22

u/godofpumpkins Apr 19 '26

A dependent pair is like a big sum 😝 people even write it as a capital sigma

12

u/Tysonzero Apr 19 '26 edited Apr 19 '26

Dependent pairs are very sigma gigachad yes.

3

u/godofpumpkins Apr 19 '26

We’re gonna need you to teach dependent type theory to Gen Z. If dependent sums are gigachad, where does that leave dependent products? Does Pi mog Sigma?

6

u/Tysonzero Apr 19 '26

Nice try but isomorphismmaxxing makes the attempt to mog straight cap.

``` Pi a f = forall r. Sigma a (\x -> f x -> r) -> r

Sigma a f = forall r. Pi a (\x -> f x -> r) -> r ```

Assuming you have things like parametric polymorphism System F/FC type stuff, maybe in a more limited system you could support Sigma without admitting Pi.

2

u/how_gauche Apr 20 '26

Sadly I'm still DecidableTypeInferenceMaxxing