Types as axioms, or: playing god with static types
lexi-lambda.github.io
lexi-lambda.github.io
Recently I wrote a simple tree walk interpreter and had to implement boolean unary negation:
(UnaryOp::Not, Value::Bool(r)) => Ok(Value::Bool(!r)),
Turns out, when you have proper enums, booleans aren't the best tool. Something like `isLoading` can now be `data LoadingState = Loading | Success`.
Why is that better? Well if you want to add a third or fourth state, it's trivial.
data LoadingState = Loading | Success | Failure
data LoadingState a err = Loading | Success a | Failure err
But then you end up with invalid boolean states! Like isLoading = true, isError = true. Huh? By making a multi-state type, you can restrict to only the possible states.
[^1]: Meh actually more like 5th but you get my point
I think there's another reason to make invalid states inexpressible in the type. When you need to change existing code (perhaps years after it was first written) in a way that breaks key assumptions, you find that the current types don't allow expressing that change. This is a good warning sign that other code will need to be updated to take the new states into account. Without the type enforcing that invariant, it might have been much harder to tell that this particular change (out of all the changes you make over the years) is the one that breaks a key assumption. (A key assumption that might have been forgotten by now!)
Types become a message to your future self.
The distinction of the two "views" does not make much sense to me. In Haskell when doing `data A = X | Y` also "restricts" `A` to X or Y.
However, as much as I like and appreciate Haskell's typesystem, I find union types very powerful. All the reasons for not have subtyping in Haskell always drill down to problems with type inference or other "practical" issues that seem to be fixable by a more advanced compiler or by accepting some inconvenience - but maybe someone can enlighten me?
Also, being able to do `type X = A | B; type Y = C | D; type Z = X | Y` is very powerful and helps a lot when using code to describe business requirements without having to use wrappers and dealing with the overhead that they bring. Even more so when a typesystem is so powerful that it can express a pattern match on some type `Z` and do: `if(NOT A) ... else if (A) ...` while checking exhaustiveness. I wish more languages would adapt this.
Yes, but this is an approach based on thinking not on which values we want to exclude, but rather how to structure our data such that those illegal values aren’t even constructible.
You must have forgotten that you read about this approach in the article.
If the Haskell method gave you iterability for free I could see the benefit, but it doesn’t.
data EvenList a = EvenNil | EvenCons a a (EvenList a)
deriving (Functor, Foldable, Traversable)
The example is not about exactly the way you choose to represent the property in question. The example is a demonstration that it’s possible to capture these properties using your type system even if it doesn’t have any first-class support for constraining list types this way. You can choose whichever representation you like the most/is most natural in your language of choice, of course, and you should! The blog post is just pointing out that you shouldn’t give up altogether on being able to capture these properties without changing the type system itself.
> type NonEmptyArray<T> = [T, ...T[]];
I'm not very familiar with Typescript, but isn't that also a "constructive" approach, rather than a "constraining" one? It reads to me like "NonEmptyArray is an array that has one element and then more elements that come from pulling elements from another array".
Typescript uses a language construct here for a special usecase, but the point still stands.
The (arbitrary, 'philosophical') difference between Haskell's `data A = X | Y` and TypeScript's `type A = "X" | "Y"` is that the TypeScript values "X" and "Y" already exist (they're strings). Functions which produce and consume these values already exist: there are certainly many functions which act on `string`, and perhaps there are silly examples which produce such strings too, e.g. a 2D geometry library which uses them to represent axes.
> without having to use wrappers and dealing with the overhead that they bring
I think part of the author's argument is that including such wrappers in our values can sometimes be useful, to convey more information about the domain. As an extreme example, we can represent pretty much everything in number theory using `int`; e.g. the fundamental theorem of arithmetic tells us that `int` is equivalent to `prime[]` (and of course Euclid proved that `prime` is equivalent to `int`), but it's probably more useful to use the second representation, even though it introduces wrappers and overhead.
As a more sensible example, I prefer Haskell's `Maybe` type compared to the "nullable types" offered by some languages, since the latter loses all structure: `Just Nothing` represents a different failure case to `Nothing` (and we can easily collapse them using `join`), whilst `null` doesn't provide that distinction.
Thank you, that makes sense. My impression was that typescript was chosen as an arbitrary language and that this limitation would be irrelevant for the example, but maybe it was chosen specifically.
I'm mainly a Scala developer, and in Scala 3 we can pretty much do:
case object A
case object B
type X = A | B
type X = "A" | "B"
There is still a difference to Haskell though, in that the "case object A" is its own type and a subtype of X.
And I think that is why the article, while in general touches a very interesting topic, leaves a bad aftertaste for me.
It makes it sound as if one method is better than the other - almost like "union types take away your power, better do it like this". However, both approaches have their place.
> As a more sensible example, I prefer Haskell's `Maybe` type compared to the "nullable types" offered by some languages, since the latter loses all structure
And you just gave a very good example. The two are not the same by any means and I am happy to be able to work in a language that has a Maybe type in the standard library. The classic example is having a map where querying by a key might or might not return a value of type A. Because A can also be null/none, without a Maybe type, this cannot be properly expressed without losing information.
However, and I really want to emphasize this: union types _can_ emulate sum types like Maybe. Simply be creating a wrapper and using it. I.e. creating two unrelated classes/structs Just and None and then defining
struct Just A = ...
struct None = ...
type Maybe A = Just A | None
The other way around is not possible though. Using Haskell#s capabilities, it is not possible to emulate Typescript's (or other language's) union types, which I find very sad. They are a useful thing to have. The only thing that might come close is Haskell Liquid and some fancy typelevel programming machinery to emulate union types.
For example, let's say I have a square root function that will happily handle real or even complex input, and I will want to pass it's output to another function that only accepts real input. Maybe I'm asking too much from life, but it seems to me that I need to tell the compiler that if I pass in a nonnegative real input, I'm getting a nonnegative real output. AND I need to be able to assure my compiler the number I'm passing in is a nonnegative real.
Suppose we take your argument to its logical conclusion—a type system ought to be able to statically detect any property we desire. In general, this would amount to predicting exactly which value each variable contains at each point during the program’s execution. This is obviously not tractable.
Statically tracking information has a cost. As the article describes, tracking certain properties can require changing the way information is represented and manipulated, sometimes in ways that are meaningfully less pleasant. Static tracking can provide a lot of benefits, so often the tradeoff is worth it, and we choose to play the typechecker’s game, but we are selective about which properties we track because it’s easier to not track something if we don’t need to.
One thing that the blog post doesn’t really call out explicitly enough is that the information you track in the type system ought to be driven by what your application actually needs. The goal is to eliminate the need to write things like
throw new Error("this should never happen")
Strengthening the types allows us to avoid these kinds of situations. For example, suppose we write a function that takes a list of source spans in a file and returns a single source span that covers all of them, and we realize “wait, what do I return if I’m given no source spans?” There’s no reasonable value to return. So you can strengthen the type to accept only non-empty lists, then follow the type errors up the call chain until you find a place where you can report a reasonable error to the user if no values are provided (or avoid the error from ever happening in the first place).
But it’s not helpful to strengthen the types to track properties we don’t actually care about. For example, in theory, we could give our “combine source spans” function a really precise type that guarantees that the resulting source span’s starting location is always equal to the starting location of the earliest source span in the input list. That property ought to always be true. But proving it to the type system would be more complicated, and it wouldn’t actually get us anything: we wouldn’t avoid any “this should never happen” cases by doing that work. (Of course, if that changed, and we would, then we might go back and figure out how to strengthen the types.)
Type systems can continue to grow more sophisticated, able to capture increasingly many properties with less effort from the programmer, and that’s great! But they won’t ever be able to magically detect everything automatically. And that’s really what this blog post is all about: in the situations where you find you’re writing a function that can’t handle a particular case, and the type system doesn’t have any native support for ruling it out, you might be able to rearrange your data representation so that the case can’t be represented and therefore doesn’t need to be handled.
Most applications don’t take a lot of square roots, so most applications aren’t negatively impacted by coarse-grained typing of the square root function. Some type systems make different choices—Typed Racket, for example, puts a lot of effort into fine-grained typing just like you describe[1]—but those choices can impact other parts of the type system, sometimes in negative ways. (Subtyping, for example, makes some other extensions to the type system much, much harder.) So static typing is fundamentally about tradeoffs, and sadly, there are no silver bullets. There won’t ever be one “best” type system (though I think we can still argue that some are better than others).
What you describe is commonly called a "(value) dependent type system". There are languages that support this, e.g. Idris which was specifically built for that: https://www.idris-lang.org/
Here is an example where the printf function is built purely in Idris: https://paulosuzart.github.io/blog/2017/06/18/dependent-type...
The compiler will parse the input string such as "some number %d and a string %s" at compile time (!) and assess whether the following arguments passed to printf satisfy the shape of the string.
-- Bad.
data Session = Session
{ authenticated :: Bool
, challenge :: Maybe Challenge
, userId :: Maybe UserId
}
-- Good.
data Session
= Unauthenticated
| Authenticating Challenge
| Authenticated UserId
The first type permits a value like `Session { authenticated = True, challenge = Challenge "<some challenge>", userId = UserId 1 }`. That's a nonsensical value which doesn't make sense in terms of the business logic.
Generally, when you have types which permit values like this:
- Someone (you or a coworker) will eventually write some code that constructs such nonsensical values.
- This means that you need a lot of tests to ensure that all code using this type works correctly when given such nonsensical values.
By using the second definition of `Session`, you don't have to worry about this at all. Nonsensical values can never exist so you will not accidentally construct them. Therefore you need less tests to ensure your code is correct.
- - -
For some reason, people are really keen to get into code like this when boolean flags are involved. Consider the following code (this time in Python):
from dataclasses import dataclass
@dataclass
class Options:
connect_tls: bool
verify_cert: bool
some_other_setting: int
(This generally happens when someone is tasked with implementing the `verify_cert` option. They see the existing options type, the existing flag for `connect_tls` and just add a second boolean.)
When I review code like this, I generally advocate for using Enums:
from dataclasses import dataclass
from enum import Enum, auto
class ConnectionOptions(Enum):
# Could also be: `PLAIN = 'plain'` or `PLAIN = 1`
PLAIN = auto()
TLS_UNVERIFIED = auto()
TLS = auto()
@dataclass
class Options:
connection_options: ConnectionOptions
some_other_setting: int
[1]: https://twitter.com/ProgrammerDude/status/124908893689234637...
https://www.typescriptlang.org/play?#code/C4TwDgpgBAogbhAdgG...
I am not a TS type expert by any means, but I don't believe it's possible to express an even list in TS's type system.
But with that said, I enjoyed the article and I agree with the points its making.
Indeed, this is the whole point of the second half of the blog post: you can enforce lots of invariants by modifying the way you represent your data, at the cost of having to write some additional code to work with your alternative representation. Reread the conclusion.
For example, we could reframe the author's point from the logic side, and complain that lots of mathematics suffers from defining things as sets-with-contraints, when it may be simpler to follow a more algebraic approach.