6 ms·

Types as axioms, or: playing god with static types

109 points by pcr910303 6y ago

layer8 6y ago
What the article describes is a simple consequence of the Curry-Howard equivalence, that function types correspond to logical implication, and constructors are just a special case of function types.
- Ar-Curunir 6y ago
  Yes, and the author knows that, but most programmers don’t. Hence, the article is valuable as introductory and educational material.
- chriswarbo 6y ago
  I wouldn't say it's a "simple consequence" or "just" this-or-that. Yes, Curry-Howard gives us a logical perspective on our code; but there are still better and worse ways to represent things from a logical perspective. 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.
  - layer8 6y ago
    Actually, my aim was to give a broader perspective and draw attention to the fact that the inference rules as presented in the article are not limited to constructors, but can apply to any function. Thinking in those terms, you want to give functions a return type that matches the guarantees you want the function to give the caller (and argument types that match the guarantees the caller should give to the function). Furthermore, it means that using types in terms of a deductive system is not restricted to languages with ML/Haskell-like data constructors, but generally useful in any statically-typed language that supports user-defined types.
piinbinary 6y ago
This reminds me a lot of Parse, don't Validate (by the same author, apparently): https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/ https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va... 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.
valenterry 6y ago
I find it a bit strange - the example of "a list with an even number of elements" can be modeled in typescript as well (simply using a list of tuples with two elements). 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.
- chrisoverzero 6y ago
  >[…] (simply using a list of tuples with two elements). 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.
  - jakear 6y ago
    So instead of having a .push method that takes a list of two arguments, I have a Cons2 constructor that takes two arguments... groundbreaking. If the Haskell method gave you iterability for free I could see the benefit, but it doesn’t.
    - lexi-lambda 6y ago
      It actually does, though I didn’t mention it in the blog post. Here’s how you write it: data EvenList a = EvenNil | EvenCons a a (EvenList a) deriving (Functor, Foldable, Traversable) But that isn’t really the point of the example. As the blog post itself points out, it’s likely more useful to use a list of pairs in most situations, and that choice would still be a constructive representation. 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.
duijf 6y ago
My favorite real world example of how you can use these techniques to reduce bugs: -- Bad. data Session = Session { authenticated :: Bool , challenge :: Maybe Challenge , userId :: Maybe UserId } -- Good. data Session = Unauthenticated | Authenticating Challenge | Authenticated UserId (Credits to my friend Arian for the example [1]) 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 It does not make sense to have `Options(connect_tls=False, verify_cert=True, ...)`. There is no certificate to validate when you connect without TLS. (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 It's almost the same safety level as in Haskell (although the Enum has a default serialization, which you need to think about e.g. when you store it in a database). [1]: https://twitter.com/ProgrammerDude/status/1249088936892346371 https://twitter.com/ProgrammerDude/status/124908893689234637...
city41 6y ago
The TypeScript EvenList<T> type at the end does not work as the author is implying. https://www.typescriptlang.org/play?#code/C4TwDgpgBAogbhAdgGQJYGdgB4AqA+KAXigG0BdKAH1JwBoo7YEUNt8yBuAKC4GMB7RJigAjAFxMkaTFkQBXALYiIAJwLESARloAmTn0HCAhhPhTWsxcrVFS2nbQDMtACz6gA 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.
- lexi-lambda 6y ago
  I (the author) did not imply that the definition of EvenList I gave would admit [1, 2, 3, 4]—it only admits [1, 2, [3, 4, []]]. 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.
  - city41 6y ago
    Yup, my bad. Thanks for poking me.
hardwaregeek 6y ago
One corollary about using positive space is that you realize we overuse booleans a lot. I routinely use a lot of boolean logic in my JavaScript and TypeScript code. I use it to decide when to display a component, when a component is being hovered, when it's odd, etc. Recently I wrote a simple tree walk interpreter and had to implement boolean unary negation: (UnaryOp::Not, Value::Bool(r)) => Ok(Value::Bool(!r)), Why is this line important? Well it's quite possibly the first[^1] time I have used the boolean negation (!) operation in Rust! 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 You can even give it data to pass along data LoadingState a err = Loading | Success a | Failure err Turns out you can have a lot more states than two. Often times in the equivalent boolean case you end up with a couple booleans: isLoading, isError, etc. 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
- bigyikes 6y ago
  Thanks for this! I'm going to refactor a PR I opened yesterday.
- nicoburns 6y ago
  I'm hoping that JavaScript adds rust-style enums at some point. Seems like it would be a perfect fit.
- valenterry 6y ago
  I fully agree. Not only is it easier to extend, it also makes reading the code so much easier and prevents mistakes, whereas for booleans you have to rely on variable names and hope to not pass them around wrongly.
- phibz 6y ago
  Algebraic types are great. They let you encode portions of your logic in to the type system in a way that is readable and understandable.
gweinberg 6y ago
This was interesting but it seems to me that if you really want your type system to let you do everything you might reasonably want to do but also to catch any errors you could reasonably expect it to, you not only need a concept of subtype, you need to be able to tell your compiler that a function that can handle mutilple types can return different types based on the type passed in. 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.
- lexi-lambda 6y ago
  What is “reasonable”? 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") as much as possible. Null pointer dereferences, divisions by zero, and attempts to add a number to a string are all examples of this kind of situation. Fundamentally, the program needs to produce a value to continue—the expression has to evaluate to something—but there isn’t any way to get any reasonable output from the given inputs. The only option is to crash. 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). [1]: https://www2.ccs.neu.edu/racket/pubs/padl12-stff.pdf https://www2.ccs.neu.edu/racket/pubs/padl12-stff.pdf

109 points by pcr910303 6y ago

What the article describes is a simple consequence of the Curry-Howard equivalence, that function types correspond to logical implication, and constructors are just a special case of function types.

Ar-Curunir 6y ago
Yes, and the author knows that, but most programmers don’t. Hence, the article is valuable as introductory and educational material.
chriswarbo 6y ago
I wouldn't say it's a "simple consequence" or "just" this-or-that. Yes, Curry-Howard gives us a logical perspective on our code; but there are still better and worse ways to represent things from a logical perspective. 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.
- layer8 6y ago
  Actually, my aim was to give a broader perspective and draw attention to the fact that the inference rules as presented in the article are not limited to constructors, but can apply to any function. Thinking in those terms, you want to give functions a return type that matches the guarantees you want the function to give the caller (and argument types that match the guarantees the caller should give to the function). Furthermore, it means that using types in terms of a deductive system is not restricted to languages with ML/Haskell-like data constructors, but generally useful in any statically-typed language that supports user-defined types.

piinbinary 6y ago

This reminds me a lot of Parse, don't Validate (by the same author, apparently): https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/ https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va... 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.

valenterry 6y ago

I find it a bit strange - the example of "a list with an even number of elements" can be modeled in typescript as well (simply using a list of tuples with two elements). 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.

chrisoverzero 6y ago
>[…] (simply using a list of tuples with two elements). 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.
- jakear 6y ago
  So instead of having a .push method that takes a list of two arguments, I have a Cons2 constructor that takes two arguments... groundbreaking. If the Haskell method gave you iterability for free I could see the benefit, but it doesn’t.
  - lexi-lambda 6y ago
    It actually does, though I didn’t mention it in the blog post. Here’s how you write it: data EvenList a = EvenNil | EvenCons a a (EvenList a) deriving (Functor, Foldable, Traversable) But that isn’t really the point of the example. As the blog post itself points out, it’s likely more useful to use a list of pairs in most situations, and that choice would still be a constructive representation. 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.

duijf 6y ago

My favorite real world example of how you can use these techniques to reduce bugs: -- Bad. data Session = Session { authenticated :: Bool , challenge :: Maybe Challenge , userId :: Maybe UserId } -- Good. data Session = Unauthenticated | Authenticating Challenge | Authenticated UserId (Credits to my friend Arian for the example [1]) 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 It does not make sense to have `Options(connect_tls=False, verify_cert=True, ...)`. There is no certificate to validate when you connect without TLS. (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 It's almost the same safety level as in Haskell (although the Enum has a default serialization, which you need to think about e.g. when you store it in a database). [1]: https://twitter.com/ProgrammerDude/status/1249088936892346371 https://twitter.com/ProgrammerDude/status/124908893689234637...

city41 6y ago

The TypeScript EvenList<T> type at the end does not work as the author is implying. https://www.typescriptlang.org/play?#code/C4TwDgpgBAogbhAdgGQJYGdgB4AqA+KAXigG0BdKAH1JwBoo7YEUNt8yBuAKC4GMB7RJigAjAFxMkaTFkQBXALYiIAJwLESARloAmTn0HCAhhPhTWsxcrVFS2nbQDMtACz6gA 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.

lexi-lambda 6y ago
I (the author) did not imply that the definition of EvenList I gave would admit [1, 2, 3, 4]—it only admits [1, 2, [3, 4, []]]. 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.
- city41 6y ago
  Yup, my bad. Thanks for poking me.

hardwaregeek 6y ago

One corollary about using positive space is that you realize we overuse booleans a lot. I routinely use a lot of boolean logic in my JavaScript and TypeScript code. I use it to decide when to display a component, when a component is being hovered, when it's odd, etc. Recently I wrote a simple tree walk interpreter and had to implement boolean unary negation: (UnaryOp::Not, Value::Bool(r)) => Ok(Value::Bool(!r)), Why is this line important? Well it's quite possibly the first[^1] time I have used the boolean negation (!) operation in Rust! 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 You can even give it data to pass along data LoadingState a err = Loading | Success a | Failure err Turns out you can have a lot more states than two. Often times in the equivalent boolean case you end up with a couple booleans: isLoading, isError, etc. 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

bigyikes 6y ago
Thanks for this! I'm going to refactor a PR I opened yesterday.
nicoburns 6y ago
I'm hoping that JavaScript adds rust-style enums at some point. Seems like it would be a perfect fit.
valenterry 6y ago
I fully agree. Not only is it easier to extend, it also makes reading the code so much easier and prevents mistakes, whereas for booleans you have to rely on variable names and hope to not pass them around wrongly.
phibz 6y ago
Algebraic types are great. They let you encode portions of your logic in to the type system in a way that is readable and understandable.

gweinberg 6y ago

This was interesting but it seems to me that if you really want your type system to let you do everything you might reasonably want to do but also to catch any errors you could reasonably expect it to, you not only need a concept of subtype, you need to be able to tell your compiler that a function that can handle mutilple types can return different types based on the type passed in. 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.

lexi-lambda 6y ago
What is “reasonable”? 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") as much as possible. Null pointer dereferences, divisions by zero, and attempts to add a number to a string are all examples of this kind of situation. Fundamentally, the program needs to produce a value to continue—the expression has to evaluate to something—but there isn’t any way to get any reasonable output from the given inputs. The only option is to crash. 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). [1]: https://www2.ccs.neu.edu/racket/pubs/padl12-stff.pdf https://www2.ccs.neu.edu/racket/pubs/padl12-stff.pdf