I haven't seen any of Rich's contributions to any major open source Haskell project. I can't really speak to his experiences with Haskell in proprietary code bases. Has he been a prolific Haskell contributor/hacker/user?
From his talk he hasn't convinced me that he understands Haskell's type system. Not only does he misunderstand the contract given by `Maybe a` but he conflates `Either a b` with logical disjunction which is definitely a false pretense. He builds the rest of his specious talk on these ideas and declares, "it [type theory] is wrong!"
He goes on to describe, in a haphazard and ignorant way, half of a type theory. As I understood it these additions to "spec" are basically a row-based polymorphic type system. Why does he refuse to acknowledge or leverage the decades of research on these type systems? Is he a language designer or a hack?
I can't even tell to be honest. He has some good ideas but I think this was one of his worst talks.
I think this comment is a bit too harsh, and I would rather we just discuss the points he makes, not his credibility. The man has decades of experience in software system development and architecture, and has built one of the most popular programming languages in the world, as well as Datomic. If that hasn't given him the right to give his opinion during the keynote of a conference for the language he built, then I don't know how much you want from him.
To apply your own standards, have you been a prolific Clojure contributor/hacker/user? Have you contributed to any major open source Clojure projects?
Can you actually say what about Maybe/Either he got wrong because it seems like he understands it perfectly well, speaking as a Scala developer.
> I think this comment is a bit too harsh, and I would rather we just discuss the points he makes, not his credibility.
I was trying to address the points he made but parent appealed to his authority which I haven't found convincing.
> To apply your own standards, have you been a prolific Clojure contributor/hacker/user? Have you contributed to any major open source Clojure projects?
I have been a user on a commercial project. It's a fine enough language. I wouldn't call myself an expert. And I haven't given a keynote address where I call out Clojure for getting things I don't understand completely wrong.
> Can you actually say what about Maybe/Either he got wrong because it seems like he understands it perfectly well, speaking as a Scala developer.
His point about Maybe was misguided at best. The function `a -> Maybe a` is a different function than `a -> a`. Despite his intuition that the latter provides a stronger guarantee and shouldn't break code, callers may be expecting the Functor instance that the `Maybe` provides and therefore is a breaking change.
His point about `Either a b` was perhaps further from the mark. It is not a data type that represent logical disjunction. That's what the logical connective, disjunction, is for. Haskell doesn't have union types to my knowledge. Either is not a connective. It's a BiFunctor. His point that it's not "associative" or "communtative" or what-have-you simply doesn't make sense. In fact he calls Either "malarky" or, charitably, a "misnomer."
To his credit he says he's not bashing on type systems, only Maybe and Either. But he later contradicts himself in his conclusions. He goes on about reverse and how "the categoric definition of that is almost information free." And then, "you almost always want your return types to be dependent on their argument..." So basically, dependent types? But again, "you wouldn't need some icky category language to talk about that."
So again, I think he has some surface knowledge of type systems but I don't think he understands type systems. I'm only a beginner at this stuff and his errors were difficult to digest. I think if he wanted to put down Maybe and Either he should've come with a loaded weapon.
He's had better talks to be sure! I just don't think this one was very good. And in my estimation was one of the poorer talks this year.
>His point about `Either a b` was perhaps further from the mark. It is not a data type that represent logical disjunction. That's what the logical connective, disjunction, is for. Haskell doesn't have union types to my knowledge. Either is not a connective. It's a BiFunctor. His point that it's not "associative" or "communtative" or what-have-you simply doesn't make sense. In fact he calls Either "malarky" or, charitably, a "misnomer."
I don't agree with Hickey, but isn't there a connection between Either as a basic sum type and logical disjunction via the curry-howard correspondence?
And wouldn't "forall a b. Either a b" be the bifunctor, since it has a product type/product category as it's domain, while the result "Either X Y" (where X and Y are concrete types, not type variables) has the semantics of logical disjunction ie. it represents a type that is of type X or type Y?
Yes, there is a connection. Which makes it all the more strange: Either does correspond as you say which means it has the same properties as the connective. In the correspondence the functor arrow is implication and a pair of functions ‘a -> b’ and ‘b -> a’ is logical equivalence. Using these we can trivially demonstrate the equivalence of Either to the associativity laws using an isomorphism.
That’s what makes his talk strange. He talks about types as sets and seems to expect Either to correspond to set union? If he understood type theory then he’d understand that we use isomorphism and not equality.
You can express type equality in set theory and that is useful and makes sense.
But it doesn’t make sense in his argument.
Malarky? Come on. Doesn’t have associativity? Weird.
> The function `a -> Maybe a` is a different function than `a -> a`. Despite his intuition that the latter provides a stronger guarantee and shouldn't break code, callers may be expecting the Functor instance that the `Maybe` provides and therefore is a breaking change.
I don't really follow that. How can it be a breaking change? Can you give an example?
Where your downstream parsers match on `Nothing` and assume the stream hasn't been consumed in order to try an alternative parser or provide a default.
If you change an equation to use `option` instead you have a completely different parser with different semantics.
I was thinking of a case where I use your function in a combinator that depends on the Functor and Monoid instances provided by the `Maybe` type. If you change your function to return only the `a` and it doesn't provide those instances then you've changed the contract and have broken my code. And I suspect it should be easy to prove the equations are not equivalent.
From his talk he hasn't convinced me that he understands Haskell's type system. Not only does he misunderstand the contract given by `Maybe a` but he conflates `Either a b` with logical disjunction which is definitely a false pretense. He builds the rest of his specious talk on these ideas and declares, "it [type theory] is wrong!"
He goes on to describe, in a haphazard and ignorant way, half of a type theory. As I understood it these additions to "spec" are basically a row-based polymorphic type system. Why does he refuse to acknowledge or leverage the decades of research on these type systems? Is he a language designer or a hack?
I can't even tell to be honest. He has some good ideas but I think this was one of his worst talks.