As somebody who first learned Python, and then Haskell, and then left both, this review reminds me of many of my own experiences.
I was reading through some of Hillel Wayne’s blog posts, and one of them discussed the Curry-Howard correspondence, which somehow proves a 1:1 association between aspects of a mathematical proof and aspects of a type system. You can convert a proof into a type, if your type system supports it. I think Haskell’s type system respects this. I don’t think Python’s type system does.
Yes, but undefined happens to be a value of every type, in Haskell; this corresponds to being able to prove any statement, including the false ones. So while it is indeed possible to turn proofs into programs, it’s not possible to turn Python or Haskell programs into useful valid proofs.
(Somebody may pedantically note that every Python or Haskell program gives a proof, just not of the fact that we might hope that they prove; they usually have Python-shaped or Haskell-shaped holes in them.)
I don’t think you can do anything like [fmap] with Python or any other practitioner’s language that I’m familiar with.
I think that this is part of the roots of the Haskeller memetic complex. Because Haskell has the lightweight syntax of an ML, and its prelude is rich in algebraic tools, suddenly there is a blindness as to the fact that the tools have been there all along. For example, in Python 3:
>>> plusOne = lambda x: x + 1
>>> lmap = lambda f: lambda xs: [f(x) for x in xs]
>>> nada = object()
>>> mmap = lambda f: lambda x: nada if x is nada else f(x)
>>> dot = lambda f: lambda g: lambda x: f(g(x))
>>> zf = dot(lmap)(mmap)(plusOne)
>>> zf([1, 2, 3])
[2, 3, 4]
>>> zf([1, nada, 3])
[2, <object object at 0x7ff65c5db0d0>, 4]
Even the base error type, bottom or |, is defined as an evaluation that never completes successfully, either because a computation failed, or because there’s an infinite loop. … I don’t think Python’s BaseException has a built-in notion of infinite loops evaluating to an error condition. This appears super powerful to me, because the big error type introduced by going over network connections are network timeouts, which appear to most programs as infinitely long computations.
There are many opinions on this, but I am of the opinion that the sort of incompleteness generated by an unresponsive network peer, known as FLP impossibility or perhaps FLP “incompleteness” of network requests, is not the same as the incompleteness that Turing, Gödel, Tarski, Lawvere, and others showed via diagonalization. They are connected, in that the FLP result implies that a Turing machine which simulates many computers on a network may encounter a Turing-complete subproblem which prevents the simulated network peers from responding.
In Alice-and-Bob framing, suppose Alice is waiting for Bob to reply over the network. The FLP impossibility of Alice having to wait forever for Bob’s reply is connected to the Turing undecidability of whether a simulation of Alice and Bob will hang forever while simulating Bob’s preparation of their reply.
Haskell has Test.QuickCheck, a property-based testing framework that generates values to check a declared property. Python has hypothesis, but having used it a tiny bit for an open-source contribution, I don’t think it’s the same without the Haskell type system.
I think that this is another memetic root; specifically, the root is type-driven dispatch. To compare apples to apples, a better analogue of QuickCheck in Python might be PayCheck, while Hedgehog is closer to Hypothesis in Haskell. As soon as the one-dimensional comparison becomes two-dimensional, the flexibility of Hypothesis, and crucially the ability to select arbitrary strategies for generating test cases, far outweighs the convenience of simple type-checking. This makes sense, in a certain way; if Haskell’s type system were sound in the first place, then QuickCheck would be little more than a totality checker. Hypothesis’ own author recommends Hedgehog over QuickCheck, and in my language, Monte, I implemented both a classic unit-test runner and also a Hypothesis-style property test runner.
Ultimately, I don’t think [indentation] is a big issue. Haskell has code auto-formatters like haskell-formatter, much like Python’s black. Use it and move on. Bikeshed about something else, you know?
Since you didn’t mention it, and none of your code samples seem to use it, and to give an example of something to bikeshed over, it’s worth pointing out that Haskell supports curly-brace-oriented syntax as well as indentation. This is a recurring topic in programming language design: We want code to be readable, and that leads to caring about whitespace.
This makes sense, in a certain way; if Haskell’s type system were sound in the first place, then QuickCheck would be little more than a totality checker.
I don’t think that follows unless you’re using incredibly specific types. There are many total functions of type Ord a => [a] -> [a], but not all of them would pass the tests of a sorting function.
This is a fair observation. QuickCheck test selection indeed is driven not just by types, but by typeclasses and associated behaviors, and I was remiss to dismiss it so glibly.
The main desire is that one might express algebraic laws, and ultimately all of these testing tools are only approximations to actual equational reasoning. That doesn’t preclude a type system from giving useful annotations.
Wow, amazing comment! I understand about half of this. I wish I had more than one upvote to give you.
I am really curious as to whether Python’s NoneType would map to Haskell’s bottom in that regards. Would that be the Python-shaped hole you’re talking about?
I did see a tutorial by David Beazley on implementing a lambda calculus in Python. I didn’t think it was all that practical tbh, and I think he said the same in the video: https://www.youtube.com/watch?v=pkCLMl0e_0k
Could you give a brief summary of how FLP impossibility and Turing incompleteness are different? I know of “Turing completeness” and that it’s a thing, but my knowledge ends there. I haven’t heard of FLP impossibliity before. Bookmarked that website.
Huh, the author of hypothesis says QuickCheck doesn’t have integrated shrinking. From his statement on generators rather than type classes, I understand your point on how Hedgehog and Hypothesis are more similar.
(I do care about whitespace and clean code; I read through “Clean Code” my second year out of college, but in my experience as a practitioner so far I’d rather use a tool and automated process to have a consistent way of doing things with multiple people, in order to spend political capital elsewhere.)
(Phew this got long, time to turn it into a blog post ;) )
I am really curious as to whether Python’s NoneType would map to Haskell’s bottom in that regards.
It’s important to distinguish between the empty type and the unit type. In (type) theory there are no values of the empty type, and there is one value of the unit type. In a language without _|_, like Agda, we might define them something like this:
data Empty : Type
data Unit : Type where
unit : Unit
This says that Empty is a Type, that Unit is a Type, that unit is a Unit. Since we’ve given no contructors (or “introduction forms”) for Empty, there’s no way to make one. Likewise we can write function types like Int -> Empty which have no values (since there’s no way for any function to return a value of type Empty), we can write tuple types like Pair Int Empty that have no values, etc. We can also write function types like Empty -> Int which do have values (e.g. const 42), but which can never be called (since there are no Empty values to give as an argument). Incidentally, the fact that we can have types with no values is one of the reasons we can’t have a value with type forall a. a (in Haskell) or (a : Type) -> a (in Agda): they claim to return a value of any type, but we might ask for an Empty.
The unit type is trivial, literally. Since there’s only one value of this type (unit), whenever we know that a value will have type Unit we can infer that the value must be unit, and hence (a) if it’s a return value, we can always optimise the function to simply unit and (b) if it’s an argument, it has no effect on the return value (there’s nothing to branch on). In this sense, the unit type contains 0 bits of information (compared to Bool which contains 1 bit).
As an aside, Either is called a “sum type” because it contains all the values from its first argument plus those of its second: Either Unit Unit is equivalent to Bool (with values Left unit and Right unit). Pairs are called “product types” since they contain every combination of their first argument and second arguments, which is the number of values in each multiplied together. In this sense Empty acts like zero: the type Either Zero a doesn’t contain any Left values, so it’s equivalent to a, just like 0 + a = a for numbers. Likewise Pair Empty a contains no values, since there’s nothing to put in the first position, just like 0 * a = 0 for numbers. Either Unit a acts like 1 + a, since we have all of the values of a (wrapped in Right) plus the extra value Left unit; note that this is also the same as Maybe a, where Right acts like Just and Left unit acts like Nothing. Pair Unit a is the same as a since each a value can only be paired with one thing, and we know that thing is always unit; this is just like 1 * a = a with numbers.
Back to your question: things get confusing when we try to apply this to “real” languages, especially since a lot of the terminology is overloaded. In Haskell the type Unit is written () and the value unit is also written ().
In Haskell the type Empty is called Void, but that is not the same as void in languages like Java! In particular, remember that we cannot have a function which returns Empty, so void being Empty would mean we could not implement methods like public static void putStrLn(String s). Such methods certainly do exist, since they’re all over the place in Java, but what happens if we call them? They will run, and return a value back to us (hence it can’t be Empty). What is the value we get back? We know, without even running the method, that we’ll get back null. That’s just like the Unit type (where we know the value will be unit without having to run the code). Hence Java’s void acts like Unit, and null acts like unit.
If we follow a similar line of reasoning in Python, we find that None acts like unit (or Java’s null) and hence NoneType is like Unit (or Java’s void). AFAIK Python doesn’t have anything which acts like Empty (Haskell’s Void) since, lacking any values, Empty is only useful for type-level calculations (of the sort which get erased during compilation), which Python doesn’t tend to do.
That just leaves “bottom”. There are a couple of ways to think about it: we can be “fast and loose” where we ignore bottom as a nuisance, which mostly works since bottom isn’t a “proper” value: in particular, we can’t branch on it; hence any time we do a calculation involving bottoms which results in a “proper” value, we know that the bottoms were irrelevant to the result, and hence can be ignored. Any time a bottom is relevant, we have to abandon our nice, logical purity in any case, since catching them requires IO, so why bother complicating our pure logic by trying to include them?
Alternatively we can treat bottom as an extra value of every type, in a similar way to null inhabiting every type in Java. From this perspective Haskell’s Void type does contain a value (bottom), and the () type contains two values (() and bottom). In this sense we might think of Java’s void corresponding to Haskell’s Void, but I find this line of thinking difficult to justify. In particular, we can branch on null in Java (in fact we should be doing such “null checks” all the time!), whereas (pure) Haskell doesn’t even let us tell whether we have () or bottom.
As a final thought, whenever comparing dynamic and static languages, it’s important to not conflate different concepts which just-so-happen to have similar names. In particular I find it useful to think of dynamically typed languages as being “uni-typed”: that is, every value has the same type, which we might write in Haskell as a sum like data DynamicValue = S String | I Int | L List | O Object | E Exception | .... Python is actually even simpler than this, since “everything is an object” (not quite as much as in Smalltalk, but certainly more than e.g. Java), so Python values are more like a pair of a class (which itself is a Python value) and a collection of instance properties.
This is important because “dynamic types”, like in Python, aren’t directly comparable to “static types” like those of Haskell; they’re more comparable to “tags” (e.g. constructors). In particular, think about a Python function branching based on its argument’s “dynamic type”; this is the same as a Haskell function branching on its argument’s constructor. What does this tell us about “bottom” in Python? From this perspective, there isn’t one (at least not reified; an infinite loop might be comparable, but it’s not something we can e.g. assign to a variable). Python’s None is just a normal value like any other, in the same way that Haskell’s Nothing is a normal value (we might sometimes use it to stand for an error, but that’s not inherent to the system); likewise Python’s exceptions are also normal values (we can assign them to variables, return them from functions, etc.); the idea of “throwing and catching” (or raise/except for Python) is actually a perfectly normal method of control flow (it’s actually a limited form of delimited continuation), and this is orthogonal to error representation and handling.
This makes raising an exception in Python very different to triggering a bottom in Haskell, since Haskell provides no way to branch on a bottom (or whether we even have one). In Python we can raise a value (with the exception “tag”) as an alternative to using return, and we can catch those values, inspect their tag and value, etc. to determine what our overall return value will be, with none of this being visible by the caller. To do anything like that in Haskell we need some “proper” data to inspect and branch on, hence why I say None, exceptions, etc. are just normal values (even though they’re used to represent errors, and we treat them specially because of that; but the same could be said about Either String values in Haskell, for example). Consider that in Haskell the only way to even check if a bottom exists is to use IO, but the idea behind IO is that it’s like State RealWorld, i.e. every IO a value is a pair of (RealWorld, a), so conceptually we never “actually” see a bottom; it’s more like triggering a bottom changes the RealWorld, and we’re branching on that.
Thank you for the clarification on None vs bottom! I think it definitely helps me understand how much more different Python is from Haskell.
I like the idea of saying data DynamicValue = S String | I Int | L List | O Object | E Exception for dynamic languages, and I think from a type theory perspective I finally understand what people say when they say “In {Ruby, Python}, everything is an object”.
I hate try/catch logic in Python. It works, but I much rather prefer the functorial structure espoused by Haskell.
I agree on the description on IO! The book does mention IO is technically without effects, since it is merely a description of what IO actions should be taking place instead of imperatively executing IO.
I like the idea of saying data DynamicValue = S String | I Int | L List | O Object | E Exception for dynamic languages
That’s a good intuitive starting point, but it’s not the whole story. The “unitype framework” is a way of understanding dynamic types from a static typing perspective, but we can also start from a “dynamic typing perspective” and see where it gets us. A dynamically-typed language is one where you can manipulate type definitions at runtime, and test for type membership at runtime. So saying DynamicValue = S String | I Int ... will always be incomplete, because we might not know something’s type even after creating it!
An intuition I like here is that dynamic types are boolean predicates: x is of type T iff T(x). This means we can define the type of, say, all functions with format as an optional keyword, or the type of all iterables that aren’t strings, or the type of all types that appear as return values in functions.
(The downside of this is it gets hellishly confusing very quickly, and allows for a lot of spooky action at a distance. Also, there’s no guarantee that checking type membership is total. That’s one reason even highly dynamic languages shy away from going deep in dynamic types.)
I think from a type theory perspective I finally understand what people say when they say “In {Ruby, Python}, everything is an object”.
Everything can also be an object in a static system, too. My rule of thumb for what “everything is an object” means: are object methods also objects? Is the call stack an object? If you are using message passing, are the messages objects? Can you send messages to other messages?
RE: “Everything is an object”, I usually put it in quotes since the meaning is usually context-dependent. A colleague once said that to me regarding Java, and I replied that Java classes aren’t objects yet Python classes are; and Python’s if branches aren’t objects yet Smalltalk’s are (at least, the closures are); and so on.
RE: Unitypes, etc. yes the static/dynamic distinction can be built up from the dynamic side too (I tend not to think that way since fixed points and things trip me up). The important thing is that people aren’t talking past each other, e.g. it’s fine to argue about whether “foo can/can’t do bar”, but not so useful when each person is using “foo” and “bar” to mean different things ;)
The overloaded word “void” across languages is confusing. In Rust and Typescript (and others?) they called it “never”, which I think makes it really clear: values of this type never actually exist. And “this function returns never” is like a pun: “this function never returns” and “this function’s return type is ‘never’”.
I’m pleased to say that I made it to the end of this 1,857 page (by the e-reader PDF version) montrosity(sic).
Congratulations. It’s a long road but IMHO very worthwhile. Well done.
Does newtype exist as part of native top-level APIs for Haskel(sic) libraries? How much churn do production Haskell type signatures suffer from? This is an unknown quantity to me.
I have never worried about this in my few years of writing Haskell. Often people export the newtype but not its constructor, so you as a client of a library cannot know nor care what the representation is behind the newtype.
The Semigroup/Monoid and Applicative/Monad upgrade paths are both examples of probably the hardest change to make in a Haskell environment - introducing a new superclass. These are managed carefully, over the course of several GHC releases, and often include transitional packages that make it easier to write code for both the old and new versions (e.g., the fail package that assists with the MonadFail migration completed by GHC 8.8). I hope we get a better solution one day, but for now I believe two things are true:
These changes only happen when the power:weight ratio makes them well worthwhile.
The GHC team as done a good job of managing these changes across multiple GHC version.
Haskell has no null definition of type Char
I don’t understand this. The “not-a-”-ness that would be expressed by a “null Char” is encapsulated by the Nothing constructor of the Maybe data type.
Haskell can raise errors partway through evaluating an error message. This (feature?) seems alien to me:
I assume you mean “evaluating an expression”. This is a consequence of being a non-strict language. You can’t stream results and guarantee the absence of errors across a structure at the same time if you allow undefined or error into your language. Note that this works:
Thank you! I saw the spelling mistake I made; I updated the copy and credited you :)
It’s great to hear support for the upgrade paths for Semigroup/Monoid and Applicative/Monad. Both of them, after reading the error messages, were rather trivial to solve, so I wouldn’t say they should be a blocker for everybody, especially those of us who are already practitioners. The broken links issue is also along the same vein; even though it was a bit irritating, it’s not like the pages didn’t exist anymore, I found where I needed to go using one query in DuckDuckGo.
As for the “not-a-“ness, I think another user here or on Hacker News pointed out that in many languages, Char maps to Int (like an ASCII table), and it’s not really possible to have a null Int because anywhere on the number line would be a valid Int. So it wouldn’t make sense in that case to have an association to an invalid / null Char. I thought it was important to point out because the book had mentioned certain instances where program correctness and typecheck guarantees diverged. In practice, totally agree that lifting into Maybe or Either is the proper way to handle “ValueError”.
I understand the point about error handling; it just seems like there could be an under-the-hood optimization that would print out only the exception instead of eagerly logging everything. How would you tie this kind of stdout to an automated logging / monitoring tool (like if you were using an ELK stack) if it had to parse through arbitrary partially applied stdout?
It just doesn’t make sense to have an empty character. A character is a character. A string is 0 or more characters. It’s like having an empty int. There’s zero, but that’s not ‘no integer’, it’s an integer. If you want a ‘null character’ you can use '\0' but it IS a character.
There are some accurate observations in this article, and it seems that the author has gained a real appreciation for strong, static type systems. That’s great!
There are also a number of inaccuracies and basic misunderstandings here. Most of the “small nits” section is… frustrating to read.
Haskell has no null definition of type Char
I don’t understand what the author wants. A String is a sequence of Chars; that sequence can be empty. What would an empty Char even be? And why isn’t Maybe Char satisfactory for their use-case?
Int and Integer are two different types
Yes, they are. Integer is a dynamically-resized integer equivalent to Python’s integer type. Int is a fixed-size integer of at least the range [- 2^29, 2^29 - 1], similar to C’s long. If that range is exceeded, the behaviour is undefined.
ghci> maxBound :: Int
9223372036854775807
ghci> maxBound :: Integer
<interactive>:3:1: error:
• No instance for (Bounded Integer)
arising from a use of ‘maxBound’
Haskell can raise errors partway through evaluating an error message.
I’m not sure what they mean, but it seems the author is just discovering lazy evaluation. In Haskell, expressions are not evaluated until their results are needed. In map (+1) [2,3,undefined], the thing that “needs” the result is the print function which is implicitly called by every line.
print will print the first thing of the list, (+1) 2. This must be evaluated first, and then it’s printed. Then print waits for the next thing in the list, (+1) 3, which also needs to be evaluated before being printed. Finally print needs (+1) undefined to be evaluated, which causes the program to stop.
Haskell can raise errors partway through evaluating an error message.
I’m not sure what they mean, but it seems the author is just discovering lazy evaluation.
I have to admit, I hit this occasionally and I’ve been programming in Haskell for years. I don’t like unhelpful error messages, so if I find myself writing a partial function I’ll at least add an explicit branch for the unwanted case (rather than leaving it to a generic “unmatched pattern” error), and I’ll put in a call to error "..." with something useful and pertinent about what happened. Sometimes it might be useful to append (some representation/summary of) the inputs to the error message, to make it clear what went wrong (e.g. "foo/bar" isn't an absolute path). Sometimes those inputs can raise their own errors (e.g. if we branched on whether the first character is /, there would still be an error lurking in something like List.intercalate "/" ["foo", undefined]).
As a good rule of thumb: when writing error handling (even if it’s just reporting, rather than recovery), be extra cautious and don’t necessarily assume that your program’s invariants still hold (after all, something had to cause the error!).
It is always super weird to see someone quote me. Really cool! But also super weird. I’m not fully adjusted to that yet ;)
If you find Haskell’s type system interesting, I’d also recommend checking out an ML! The module system in ML is really cool, powerful, and unique. I’m shocked more languages haven’t adopted similar module systems.
Also, a couple of quick pedantic nitpicks:
I was reading through some of Hillel Wayne’s blog posts, and one of them discussed the Curry-Howard correspondence, which somehow proves a 1:1 association between aspects of a mathematical proof and aspects of a type system. You can convert a proof into a type, if your type system supports it. I think Haskell’s type system respects this. I don’t think Python’s type system does.
I don’t think I explained the CHC very well in that. All sound static type systems are “proofs”, where what you are proving is “this is well-typed”. This is true for both Haskell and Python (mypy). But different languages can encode different consequences of being well-typed, like if you can express the type of sorted lists, you can say “I’ve proven this is well-typed ⇒ this sort function correctly sorts the list.” Haskell’s type system is more powerful than most other commercial languages, but it’s not powerful enough to encode arbitrary theorems. For that you need dependent typing a la Idris or Coq.
Also proving type-safety for arbitrary theorems is really, really hard. Tradeoffs!
Python has hypothesis, but having used it a tiny bit for an open-source contribution, I don’t think it’s the same without the Haskell type system.
Gotta defend hypothesis a bit here! It sounds like you were using quickcheck in the context of learning from a book, while you were using hypothesis for a real-world project. In that context quickcheck is gonna seem more elegant. But Hypothesis is world-class and a lot of more modern PBT libraries follow its example. It’s a lot better at generating inputs like “two dictionaries where the values of the first dict are a superset of the keys in the second.”
OCaml seems really cool, and I’ve heard it used in industry; is it the most popular ML for practitioners? I also know of ReasonML used by Facebook to create Facebook Messenger. But I think there’s still so much to learn about Haskell, and between going broad and learning about type systems, I’d want to go deep into Haskell and become intermediate, or even advanced if I’m fortunate enough to have the time and resources to do so!
Hmm, I didn’t know that Idris or Coq would be powerful enough to encode arbitrary theorems. I think if I were to study more into type theory (an interesting subject), I’d try to learn those!
Yeah, I think Corbin mentioned that Hedgehog was closer to hypothesis than QuickCheck was; I think I was too quick in dismissing hypothesis. I do like the notion of using generators over types, and the integrated shrinking (when I wrote this I assumed that QuickCheck had integrated shrinking; I think that’s actually a Hedgehog or maybe hypothesis innovation). I definitely like your blog post point about creating integration tests from a combination of hypothesis and pycontracts, I’ll give that a shot for my next project :D
QuickCheck does shrinking. The Arbitrary typeclass has a shrink :: a -> [a] method which should return a list of smaller versions of its argument.
If you don’t want to create an instance of Arbitrary, you can use the function forAllShrink. It’s type is a more polymorphic version of (RandomSeed -> a) -> (a -> [a]) -> (a -> Bool) -> Bool: the first argument is a generating function, the second is a shrinking function and the third is the property to check.
I believe non-eager can mean either lazy or non-strict. At least according to the book, they’re two different things. Laziness is a stricter definition than non-lazy:
Haskell is not fully lazy; it is merely non-strict, so it is not required to remember the result of every function application for a given set of arguments, nor would it be desirable given memory constraints.
Complete laziness would imply complete memoization and no sharing of generated results, which would blow up memory.
As somebody who first learned Python, and then Haskell, and then left both, this review reminds me of many of my own experiences.
Yes, but
undefinedhappens to be a value of every type, in Haskell; this corresponds to being able to prove any statement, including the false ones. So while it is indeed possible to turn proofs into programs, it’s not possible to turn Python or Haskell programs into useful valid proofs.(Somebody may pedantically note that every Python or Haskell program gives a proof, just not of the fact that we might hope that they prove; they usually have Python-shaped or Haskell-shaped holes in them.)
I think that this is part of the roots of the Haskeller memetic complex. Because Haskell has the lightweight syntax of an ML, and its prelude is rich in algebraic tools, suddenly there is a blindness as to the fact that the tools have been there all along. For example, in Python 3:
There are many opinions on this, but I am of the opinion that the sort of incompleteness generated by an unresponsive network peer, known as FLP impossibility or perhaps FLP “incompleteness” of network requests, is not the same as the incompleteness that Turing, Gödel, Tarski, Lawvere, and others showed via diagonalization. They are connected, in that the FLP result implies that a Turing machine which simulates many computers on a network may encounter a Turing-complete subproblem which prevents the simulated network peers from responding.
In Alice-and-Bob framing, suppose Alice is waiting for Bob to reply over the network. The FLP impossibility of Alice having to wait forever for Bob’s reply is connected to the Turing undecidability of whether a simulation of Alice and Bob will hang forever while simulating Bob’s preparation of their reply.
I think that this is another memetic root; specifically, the root is type-driven dispatch. To compare apples to apples, a better analogue of QuickCheck in Python might be PayCheck, while Hedgehog is closer to Hypothesis in Haskell. As soon as the one-dimensional comparison becomes two-dimensional, the flexibility of Hypothesis, and crucially the ability to select arbitrary strategies for generating test cases, far outweighs the convenience of simple type-checking. This makes sense, in a certain way; if Haskell’s type system were sound in the first place, then QuickCheck would be little more than a totality checker. Hypothesis’ own author recommends Hedgehog over QuickCheck, and in my language, Monte, I implemented both a classic unit-test runner and also a Hypothesis-style property test runner.
Since you didn’t mention it, and none of your code samples seem to use it, and to give an example of something to bikeshed over, it’s worth pointing out that Haskell supports curly-brace-oriented syntax as well as indentation. This is a recurring topic in programming language design: We want code to be readable, and that leads to caring about whitespace.
I don’t think that follows unless you’re using incredibly specific types. There are many total functions of type
Ord a => [a] -> [a], but not all of them would pass the tests of a sorting function.This is a fair observation. QuickCheck test selection indeed is driven not just by types, but by typeclasses and associated behaviors, and I was remiss to dismiss it so glibly.
The main desire is that one might express algebraic laws, and ultimately all of these testing tools are only approximations to actual equational reasoning. That doesn’t preclude a type system from giving useful annotations.
Wow, amazing comment! I understand about half of this. I wish I had more than one upvote to give you.
I am really curious as to whether Python’s
NoneTypewould map to Haskell’sbottomin that regards. Would that be the Python-shaped hole you’re talking about?I did see a tutorial by David Beazley on implementing a lambda calculus in Python. I didn’t think it was all that practical tbh, and I think he said the same in the video: https://www.youtube.com/watch?v=pkCLMl0e_0k
Could you give a brief summary of how FLP impossibility and Turing incompleteness are different? I know of “Turing completeness” and that it’s a thing, but my knowledge ends there. I haven’t heard of FLP impossibliity before. Bookmarked that website.
Huh, the author of hypothesis says QuickCheck doesn’t have integrated shrinking. From his statement on generators rather than type classes, I understand your point on how Hedgehog and Hypothesis are more similar.
Hmm, there weren’t a whole lot of examples of curly-brace oriented syntax. Most examples used indentation. The Haskell wiki does mention it though: https://en.wikibooks.org/wiki/Haskell/Indentation#Explicit_characters_in_place_of_indentation
(I do care about whitespace and clean code; I read through “Clean Code” my second year out of college, but in my experience as a practitioner so far I’d rather use a tool and automated process to have a consistent way of doing things with multiple people, in order to spend political capital elsewhere.)
(Phew this got long, time to turn it into a blog post ;) )
It’s important to distinguish between the empty type and the unit type. In (type) theory there are no values of the empty type, and there is one value of the unit type. In a language without
_|_, like Agda, we might define them something like this:This says that
Emptyis aType, thatUnitis aType, thatunitis aUnit. Since we’ve given no contructors (or “introduction forms”) forEmpty, there’s no way to make one. Likewise we can write function types likeInt -> Emptywhich have no values (since there’s no way for any function to return a value of typeEmpty), we can write tuple types likePair Int Emptythat have no values, etc. We can also write function types likeEmpty -> Intwhich do have values (e.g.const 42), but which can never be called (since there are noEmptyvalues to give as an argument). Incidentally, the fact that we can have types with no values is one of the reasons we can’t have a value with typeforall a. a(in Haskell) or(a : Type) -> a(in Agda): they claim to return a value of any type, but we might ask for anEmpty.The unit type is trivial, literally. Since there’s only one value of this type (
unit), whenever we know that a value will have typeUnitwe can infer that the value must beunit, and hence (a) if it’s a return value, we can always optimise the function to simplyunitand (b) if it’s an argument, it has no effect on the return value (there’s nothing to branch on). In this sense, the unit type contains 0 bits of information (compared toBoolwhich contains 1 bit).As an aside,
Eitheris called a “sum type” because it contains all the values from its first argument plus those of its second:Either Unit Unitis equivalent toBool(with valuesLeft unitandRight unit). Pairs are called “product types” since they contain every combination of their first argument and second arguments, which is the number of values in each multiplied together. In this senseEmptyacts like zero: the typeEither Zero adoesn’t contain anyLeftvalues, so it’s equivalent toa, just like0 + a = afor numbers. LikewisePair Empty acontains no values, since there’s nothing to put in the first position, just like0 * a = 0for numbers.Either Unit aacts like1 + a, since we have all of the values ofa(wrapped inRight) plus the extra valueLeft unit; note that this is also the same asMaybe a, whereRightacts likeJustandLeft unitacts likeNothing.Pair Unit ais the same asasince eachavalue can only be paired with one thing, and we know that thing is alwaysunit; this is just like1 * a = awith numbers.Back to your question: things get confusing when we try to apply this to “real” languages, especially since a lot of the terminology is overloaded. In Haskell the type
Unitis written()and the valueunitis also written().In Haskell the type
Emptyis calledVoid, but that is not the same asvoidin languages like Java! In particular, remember that we cannot have a function which returnsEmpty, sovoidbeingEmptywould mean we could not implement methods likepublic static void putStrLn(String s). Such methods certainly do exist, since they’re all over the place in Java, but what happens if we call them? They will run, and return a value back to us (hence it can’t beEmpty). What is the value we get back? We know, without even running the method, that we’ll get backnull. That’s just like theUnittype (where we know the value will beunitwithout having to run the code). Hence Java’svoidacts likeUnit, andnullacts likeunit.If we follow a similar line of reasoning in Python, we find that
Noneacts likeunit(or Java’snull) and henceNoneTypeis likeUnit(or Java’svoid). AFAIK Python doesn’t have anything which acts likeEmpty(Haskell’sVoid) since, lacking any values,Emptyis only useful for type-level calculations (of the sort which get erased during compilation), which Python doesn’t tend to do.That just leaves “bottom”. There are a couple of ways to think about it: we can be “fast and loose” where we ignore bottom as a nuisance, which mostly works since bottom isn’t a “proper” value: in particular, we can’t branch on it; hence any time we do a calculation involving bottoms which results in a “proper” value, we know that the bottoms were irrelevant to the result, and hence can be ignored. Any time a bottom is relevant, we have to abandon our nice, logical purity in any case, since catching them requires
IO, so why bother complicating our pure logic by trying to include them?Alternatively we can treat bottom as an extra value of every type, in a similar way to
nullinhabiting every type in Java. From this perspective Haskell’sVoidtype does contain a value (bottom), and the()type contains two values (()and bottom). In this sense we might think of Java’svoidcorresponding to Haskell’sVoid, but I find this line of thinking difficult to justify. In particular, we can branch onnullin Java (in fact we should be doing such “null checks” all the time!), whereas (pure) Haskell doesn’t even let us tell whether we have()or bottom.As a final thought, whenever comparing dynamic and static languages, it’s important to not conflate different concepts which just-so-happen to have similar names. In particular I find it useful to think of dynamically typed languages as being “uni-typed”: that is, every value has the same type, which we might write in Haskell as a sum like
data DynamicValue = S String | I Int | L List | O Object | E Exception | .... Python is actually even simpler than this, since “everything is an object” (not quite as much as in Smalltalk, but certainly more than e.g. Java), so Python values are more like a pair of a class (which itself is a Python value) and a collection of instance properties.This is important because “dynamic types”, like in Python, aren’t directly comparable to “static types” like those of Haskell; they’re more comparable to “tags” (e.g. constructors). In particular, think about a Python function branching based on its argument’s “dynamic type”; this is the same as a Haskell function branching on its argument’s constructor. What does this tell us about “bottom” in Python? From this perspective, there isn’t one (at least not reified; an infinite loop might be comparable, but it’s not something we can e.g. assign to a variable). Python’s
Noneis just a normal value like any other, in the same way that Haskell’sNothingis a normal value (we might sometimes use it to stand for an error, but that’s not inherent to the system); likewise Python’s exceptions are also normal values (we can assign them to variables, return them from functions, etc.); the idea of “throwing and catching” (orraise/exceptfor Python) is actually a perfectly normal method of control flow (it’s actually a limited form of delimited continuation), and this is orthogonal to error representation and handling.This makes raising an exception in Python very different to triggering a bottom in Haskell, since Haskell provides no way to branch on a bottom (or whether we even have one). In Python we can raise a value (with the exception “tag”) as an alternative to using
return, and we can catch those values, inspect their tag and value, etc. to determine what our overall return value will be, with none of this being visible by the caller. To do anything like that in Haskell we need some “proper” data to inspect and branch on, hence why I sayNone, exceptions, etc. are just normal values (even though they’re used to represent errors, and we treat them specially because of that; but the same could be said aboutEither Stringvalues in Haskell, for example). Consider that in Haskell the only way to even check if a bottom exists is to useIO, but the idea behindIOis that it’s likeState RealWorld, i.e. everyIO avalue is a pair of(RealWorld, a), so conceptually we never “actually” see a bottom; it’s more like triggering a bottom changes theRealWorld, and we’re branching on that.Thank you for the clarification on
Nonevsbottom! I think it definitely helps me understand how much more different Python is from Haskell.I like the idea of saying
data DynamicValue = S String | I Int | L List | O Object | E Exceptionfor dynamic languages, and I think from a type theory perspective I finally understand what people say when they say “In {Ruby, Python}, everything is an object”.I hate try/catch logic in Python. It works, but I much rather prefer the functorial structure espoused by Haskell.
I agree on the description on IO! The book does mention IO is technically without effects, since it is merely a description of what IO actions should be taking place instead of imperatively executing IO.
That’s a good intuitive starting point, but it’s not the whole story. The “unitype framework” is a way of understanding dynamic types from a static typing perspective, but we can also start from a “dynamic typing perspective” and see where it gets us. A dynamically-typed language is one where you can manipulate type definitions at runtime, and test for type membership at runtime. So saying
DynamicValue = S String | I Int ...will always be incomplete, because we might not know something’s type even after creating it!An intuition I like here is that dynamic types are boolean predicates:
xis of typeTiffT(x). This means we can define the type of, say, all functions withformatas an optional keyword, or the type of all iterables that aren’t strings, or the type of all types that appear as return values in functions.(The downside of this is it gets hellishly confusing very quickly, and allows for a lot of spooky action at a distance. Also, there’s no guarantee that checking type membership is total. That’s one reason even highly dynamic languages shy away from going deep in dynamic types.)
Everything can also be an object in a static system, too. My rule of thumb for what “everything is an object” means: are object methods also objects? Is the call stack an object? If you are using message passing, are the messages objects? Can you send messages to other messages?
RE: “Everything is an object”, I usually put it in quotes since the meaning is usually context-dependent. A colleague once said that to me regarding Java, and I replied that Java classes aren’t objects yet Python classes are; and Python’s
ifbranches aren’t objects yet Smalltalk’s are (at least, the closures are); and so on.RE: Unitypes, etc. yes the static/dynamic distinction can be built up from the dynamic side too (I tend not to think that way since fixed points and things trip me up). The important thing is that people aren’t talking past each other, e.g. it’s fine to argue about whether “foo can/can’t do bar”, but not so useful when each person is using “foo” and “bar” to mean different things ;)
The overloaded word “void” across languages is confusing. In Rust and Typescript (and others?) they called it “never”, which I think makes it really clear: values of this type never actually exist. And “this function returns never” is like a pun: “this function never returns” and “this function’s return type is ‘never’”.
This was wonderfully clear. Thank you.
Congratulations. It’s a long road but IMHO very worthwhile. Well done.
I have never worried about this in my few years of writing Haskell. Often people export the newtype but not its constructor, so you as a client of a library cannot know nor care what the representation is behind the newtype.
The
Semigroup/MonoidandApplicative/Monadupgrade paths are both examples of probably the hardest change to make in a Haskell environment - introducing a new superclass. These are managed carefully, over the course of several GHC releases, and often include transitional packages that make it easier to write code for both the old and new versions (e.g., thefailpackage that assists with theMonadFailmigration completed by GHC 8.8). I hope we get a better solution one day, but for now I believe two things are true:I don’t understand this. The “not-a-”-ness that would be expressed by a “null
Char” is encapsulated by theNothingconstructor of theMaybedata type.I assume you mean “evaluating an expression”. This is a consequence of being a non-strict language. You can’t stream results and guarantee the absence of errors across a structure at the same time if you allow
undefinedorerrorinto your language. Note that this works:Re: your broken links complaint. Here is my favourite page for GHC language extensions, and I should probably just make it my homepage: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html
Thank you! I saw the spelling mistake I made; I updated the copy and credited you :)
It’s great to hear support for the upgrade paths for
Semigroup/MonoidandApplicative/Monad. Both of them, after reading the error messages, were rather trivial to solve, so I wouldn’t say they should be a blocker for everybody, especially those of us who are already practitioners. The broken links issue is also along the same vein; even though it was a bit irritating, it’s not like the pages didn’t exist anymore, I found where I needed to go using one query in DuckDuckGo.As for the “not-a-“ness, I think another user here or on Hacker News pointed out that in many languages, Char maps to Int (like an ASCII table), and it’s not really possible to have a null Int because anywhere on the number line would be a valid Int. So it wouldn’t make sense in that case to have an association to an invalid / null Char. I thought it was important to point out because the book had mentioned certain instances where program correctness and typecheck guarantees diverged. In practice, totally agree that lifting into
MaybeorEitheris the proper way to handle “ValueError”.I understand the point about error handling; it just seems like there could be an under-the-hood optimization that would print out only the exception instead of eagerly logging everything. How would you tie this kind of stdout to an automated logging / monitoring tool (like if you were using an ELK stack) if it had to parse through arbitrary partially applied stdout?
It just doesn’t make sense to have an empty character. A character is a character. A string is 0 or more characters. It’s like having an empty int. There’s zero, but that’s not ‘no integer’, it’s an integer. If you want a ‘null character’ you can use
'\0'but it IS a character.There are some accurate observations in this article, and it seems that the author has gained a real appreciation for strong, static type systems. That’s great!
There are also a number of inaccuracies and basic misunderstandings here. Most of the “small nits” section is… frustrating to read.
I don’t understand what the author wants. A
Stringis a sequence ofChars; that sequence can be empty. What would an emptyChareven be? And why isn’tMaybe Charsatisfactory for their use-case?Yes, they are.
Integeris a dynamically-resized integer equivalent to Python’s integer type.Intis a fixed-size integer of at least the range [- 2^29, 2^29 - 1], similar to C’slong. If that range is exceeded, the behaviour is undefined.I’m not sure what they mean, but it seems the author is just discovering lazy evaluation. In Haskell, expressions are not evaluated until their results are needed. In
map (+1) [2,3,undefined], the thing that “needs” the result is theprintfunction which is implicitly called by every line.printwill print the first thing of the list,(+1) 2. This must be evaluated first, and then it’s printed. Thenprintwaits for the next thing in the list,(+1) 3, which also needs to be evaluated before being printed. Finallyprintneeds(+1) undefinedto be evaluated, which causes the program to stop.I have to admit, I hit this occasionally and I’ve been programming in Haskell for years. I don’t like unhelpful error messages, so if I find myself writing a partial function I’ll at least add an explicit branch for the unwanted case (rather than leaving it to a generic “unmatched pattern” error), and I’ll put in a call to
error "..."with something useful and pertinent about what happened. Sometimes it might be useful to append (some representation/summary of) the inputs to the error message, to make it clear what went wrong (e.g."foo/bar" isn't an absolute path). Sometimes those inputs can raise their own errors (e.g. if we branched on whether the first character is/, there would still be an error lurking in something likeList.intercalate "/" ["foo", undefined]).As a good rule of thumb: when writing error handling (even if it’s just reporting, rather than recovery), be extra cautious and don’t necessarily assume that your program’s invariants still hold (after all, something had to cause the error!).
It is always super weird to see someone quote me. Really cool! But also super weird. I’m not fully adjusted to that yet ;)
If you find Haskell’s type system interesting, I’d also recommend checking out an ML! The module system in ML is really cool, powerful, and unique. I’m shocked more languages haven’t adopted similar module systems.
Also, a couple of quick pedantic nitpicks:
I don’t think I explained the CHC very well in that. All sound static type systems are “proofs”, where what you are proving is “this is well-typed”. This is true for both Haskell and Python (mypy). But different languages can encode different consequences of being well-typed, like if you can express the type of sorted lists, you can say “I’ve proven this is well-typed ⇒ this sort function correctly sorts the list.” Haskell’s type system is more powerful than most other commercial languages, but it’s not powerful enough to encode arbitrary theorems. For that you need dependent typing a la Idris or Coq.
Also proving type-safety for arbitrary theorems is really, really hard. Tradeoffs!
Gotta defend hypothesis a bit here! It sounds like you were using quickcheck in the context of learning from a book, while you were using hypothesis for a real-world project. In that context quickcheck is gonna seem more elegant. But Hypothesis is world-class and a lot of more modern PBT libraries follow its example. It’s a lot better at generating inputs like “two dictionaries where the values of the first dict are a superset of the keys in the second.”
OCaml seems really cool, and I’ve heard it used in industry; is it the most popular ML for practitioners? I also know of ReasonML used by Facebook to create Facebook Messenger. But I think there’s still so much to learn about Haskell, and between going broad and learning about type systems, I’d want to go deep into Haskell and become intermediate, or even advanced if I’m fortunate enough to have the time and resources to do so!
Hmm, I didn’t know that Idris or Coq would be powerful enough to encode arbitrary theorems. I think if I were to study more into type theory (an interesting subject), I’d try to learn those!
Yeah, I think Corbin mentioned that Hedgehog was closer to hypothesis than QuickCheck was; I think I was too quick in dismissing hypothesis. I do like the notion of using generators over types, and the integrated shrinking (when I wrote this I assumed that QuickCheck had integrated shrinking; I think that’s actually a Hedgehog or maybe hypothesis innovation). I definitely like your blog post point about creating integration tests from a combination of hypothesis and pycontracts, I’ll give that a shot for my next project :D
QuickCheckdoes shrinking. TheArbitrarytypeclass has ashrink :: a -> [a]method which should return a list of smaller versions of its argument.If you don’t want to create an instance of
Arbitrary, you can use the functionforAllShrink. It’s type is a more polymorphic version of(RandomSeed -> a) -> (a -> [a]) -> (a -> Bool) -> Bool: the first argument is a generating function, the second is a shrinking function and the third is the property to check.I loved the term “Sisyphian bugs”
Great stuff. I have also enjoyed your https://bytes.yingw787.com/posts/2019/12/06/monads/ article.
By the way, we have a typed implementation of several monads in Python: https://github.com/dry-python/returns Check it out.
You mean non-eager, I think.
I believe non-eager can mean either lazy or non-strict. At least according to the book, they’re two different things. Laziness is a stricter definition than non-lazy:
Complete laziness would imply complete memoization and no sharing of generated results, which would blow up memory.
https://wiki.haskell.org/Lazy_vs._non-strict