Hacker News new | ask | show | jobs
by dddbbb 2097 days ago
Haskell's Either is a 'true' sum type, it corresponds exactly to the way sums have been defined in the literature for decades, and also is the Curry-Howard representation of logical or. It necessarily must be inside a Either-like wrapper in order to be type safe, String and Int are ultimately different and so at some point we must discriminate between them. foo could call further functions with its argument inside itself accepting Either String Int, but eventually a destructor will be hit somewhere in the call stack.

If String and Int do implement the same behaviour under some circumstance, then a typeclass should be used to define that behaviour. Then foo can have type (Bar baz) => baz -> Int, where String and Int have Bar instances.

2 comments

Right, so I must have used the wrong words “sum type” when I should have said “union type”, but I thought the intended meaning was clear.

It doesn’t necessarily need to be inside an Either wrapper, that is an implementation detail, neither does there need to be a typeclass specifically defined for it. For example the new Dotty dialect of Scala has support for union types as I described them [1]. This is nice because it makes union of types an actual union operator, satisfying actual commutativity (A | B) = (B | A) and idempotence (A | A) = A, which Either does not without some extra explicit isomorphisms.

[1]: https://dotty.epfl.ch/docs/reference/new-types/union-types.h...

I’m curious, is the ‘true’ sum types, I mean where true is in quotes, based on the premise that lazy language can not have logically true sum types? Or is it in the quotes for some other reason?
I was just responding to the parent comment's claim that Haskell's sum types are not true sum types.