| ▲ | ackfoobar 5 days ago |
| > Sum types: For example, Kotlin and Java (and de facto C#) use a construct associated with inheritance relations called sealing. This has the benefit of giving you the ability to refer to a case as its own type. > the expression of sums verbose and, in my view, harder to reason about. You declare the sum type once, and use it many times. Slightly more verbose sum type declaration is worth it when it makes using the cases cleaner. |
|
| ▲ | sunnydiskincali 5 days ago | parent | next [-] |
| > This has the benefit of giving you the ability to refer to a case as its own type. A case of a sum-type is an expression (of the variety so-called a type constructor), of course it has a type. datatype shape =
Circle of real
| Rectangle of real * real
| Point
Circle : real -> shape
Rectangle : real * real -> shape
Point : () -> shape
A case itself isn't a type, though it has a type. Thanks to pattern matching, you're already unwrapping the parameter to the type-constructor when handling the case of a sum-type. It's all about declaration locality. (real * real) doesn't depend on the existence of shape.The moment you start ripping cases as distinct types out of the sum-type, you create the ability to side-step exhaustiveness and sum-types become useless in making invalid program states unrepresentable. They're also no longer sum-types. If you have a sum-type of nominally distinct types, the sum-type is contingent on the existence of those types. In a class hierarchy, this relationship is bizarrely reversed and there are knock-on effects to that. > You declare the sum type once, and use it many times. And you typically write many sum-types. They're disposable. And more to the point, you also have to read the code you write. The cost of verbosity here is underestimated. > Slightly more verbose sum type declaration is worth it when it makes using the cases cleaner. C#/Java don't actually have sum-types. It's an incompatible formalism with their type systems. Anyways, let's look at these examples: C#: public abstract record Shape;
public sealed record Circle(double Radius) : Shape;
public sealed record Rectangle(double Width, double Height) : Shape;
public sealed record Point() : Shape;
double Area(Shape shape) => shape switch
{
Circle c => Math.PI * c.Radius * c.Radius,
Rectangle r => r.Width * r.Height,
Point => 0.0,
_ => throw new ArgumentException("Unknown shape", nameof(shape))
};
ML: datatype shape =
Circle of real
| Rectangle of real * real
| Point
val result =
case shape of
Circle r => Math.pi * r * r
| Rectangle (w, h) => w * h
| Point => 0.0
They're pretty much the same outside of C#'s OOP quirkiness getting in it's own way. |
| |
| ▲ | ackfoobar 5 days ago | parent [-] | | > The moment you start ripping cases as distinct types out of the sum-type, you create the ability to side-step exhaustiveness and sum-types become useless in making invalid program states unrepresentable. Quite the opposite, that gives me the ability to explicitly express what kinds of values I might return. With your shape example, you cannot express in the type system "this function won't return a point". But with sum type as sealed inheritance hierarchy I can. > C#/Java don't actually have sum-types. > They're pretty much the same Not sure about C#, but in Java if you write `sealed` correctly you won't need the catch-all throw. If they're not actual sum types but are pretty much the same, what good does the "actually" do? | | |
| ▲ | tomsmeding 4 days ago | parent | next [-] | | > Not sure about C#, but in Java if you write `sealed` correctly you won't need the catch-all throw. Will the compiler check that you have handled all the cases still? (Genuinely unsure — not a Java programmer) | | | |
| ▲ | sunnydiskincali 4 days ago | parent | prev [-] | | > With your shape example, you cannot express in the type system "this function won't return a point". Sure you can, that's just subtyping. If it returns a value that's not a point, the domain has changed from the shape type and you should probably indicate that. structure Shape = struct
datatype shape =
Circle of real
| Rectangle of real * real
| Point
end
structure Bound = struct
datatype shape =
Circle of real
| Rectangle of real * real
end
This is doing things quick and dirty. For this trivial example it's fine, and I think a good example of why making sum-types low friction is a good idea. It completely changes how you solve problems when they're fire and forget like this.That's not to say it's the only way to solve this problem, though. And for heavy-duty problems, you typically write something like this using higher-kinded polymorphism: signature SHAPE_TYPE = sig
datatype shape =
Circle of real
| Rectangle of real * real
| Point
val Circle : real -> shape
val Rectangle : real * real -> shape
val Point : shape
end
functor FullShape () : SHAPE_TYPE = struct
datatype shape =
Circle of real
| Rectangle of real * real
| Point
val Circle = Circle
val Rectangle = Rectangle
val Point = Point
end
functor RemovePoint (S : SHAPE_TYPE) :> sig
type shape
val Circle : real -> shape
val Rectangle : real * real -> shape
end = struct
type shape = S.shape
val Circle = S.Circle
val Rectangle = S.Rectangle
end
structure Shape = FullShape()
structure Bound = RemovePoint(Shape)
This is extremely overkill for the example, but it also demonstrates a power you're not getting out of C# or Java without usage of reflection. This is closer to the system of inheritance, but it's a bit better designed. The added benefit here over reflection is that the same principle of "invalid program states are unrepresentable" applies here as well, because it's the exact same system being used. You'll also note that even though it's a fair bit closer conceptually to classes, the sum-type is still distinct.Anyways, in both cases, this is now just: DoesNotReturnPoint : Shape.shape -> Bound.shape
Haskell has actual GADTs and proper higher kinded polymorphism, and a few other features where this all looks very different and much terser. Newer languages bake subtyping into the grammar.> If they're not actual sum types but are pretty much the same, what good does the "actually" do? Conflation of two different things here. The examples given are syntactically similar, and they're both treating the constituent part of the grammar as a tagged union. The case isn't any cleaner was the point. However in the broader comparison between class hierarchies and sum-types? They're not similar at all. Classes can do some of the things that sum-types can do, but they're fundamentally different and encourage a completely different approach to problem-solving, conceptualization and project structure... in all but the most rudimentary examples. As I said, my 2nd example here is far closer to a class-hierarchy system than sum-types, though it's still very different. And again, underlining that because of the properties of sum-types, thanks to their specific formalization, they're capable of things class hierarchies aren't. Namely, enforcing valid program-states at a type-level. Somebody more familiar with object-oriented formalizations may be a better person to ask than me on why that is the case. It's a pretty complicated space to talk about, because these type systems deviate on a very basic and fundamental level. Shit just doesn't translate well, and it's easy to find false friends. Like how the Japanese word for "name" sounds like the English word, despite not being a loan word. | | |
| ▲ | ackfoobar 4 days ago | parent [-] | | You wrote a lot of words to say very little. Anyway, to translate your example: sealed interface Shape permits Point, Bound {}
final class Point implements Shape {}
sealed interface Bound extends Shape permits Circle, Rectangle {}
record Circle(double radius) implements Bound {}
record Rectangle(double width, double height) implements Bound {}
A `Rectangle` is both a `Bound` (weird name choice but whatever), and a `Shape`. Thanks to subtyping, no contortion needed. No need to use 7 more lines to create a separate, unrelated type.> the Japanese word for "name" sounds like the English word, despite not being a loan word. Great analogy, except for the fact that someone from the Java team explicitly said they're drawing inspirations from ML. https://news.ycombinator.com/item?id=24203363 | | |
| ▲ | sunnydiskincali 4 days ago | parent [-] | | > You wrote a lot of words to say very little. Substantiate this. > weird name choice but whatever I don't think this kind of snarky potshot is in line with the commentary guidelines. Perhaps you could benefit from a refresher? https://news.ycombinator.com/newsguidelines.html#comments > Thanks to subtyping, no contortion needed I see the same degree of contortion, actually. Far more noisy, at that. > No need to use 7 more lines to create a separate, unrelated type. You're still creating a type, because you understand that a sum-type with a different set of cases is fundamentally a different type. Just like a class with a different set of inheritance is a different type. And while it's very cute to compress it all into a single line, it's really not compelling in the context of readability and "write once, use many". Which is the point you were making, although it was on an entirely different part of the grammar. > Great analogy, except for the fact that someone from the Java team explicitly said they're drawing inspirations from ML. ML didn't invent ADTs, and I think you know it's more than disingenuous to imply the quotation means that the type-system in Java which hasn't undergone any fundamental changes in the history of the language (nor could it without drastically changing the grammar of the language and breaking the close relationship to the JVM) was lifted from ML. | | |
| ▲ | ackfoobar 4 days ago | parent [-] | | > Substantiate this. You never gave an example how sum types in Java/Kotlin cannot do what "real" sum types can. >> weird name choice but whatever > snarky potshot Sorry that you read snark. What I meant was "I find naming this 'Bound' weird. But since I am translating your example, I'll reuse it". > You're still creating an unrelated type How can a type participating in the inheritance hierarchy be "unrelated"? > I see the same degree of contortion, actually. Far more noisy, at that. At this point I can only hope you're a Haskeller and do not represent an average OCaml programmer. | | |
| ▲ | ackfoobar 2 days ago | parent [-] | | PS rereading this I think "hope you're a Haskeller" might be read as an insult. That's not my intention, here's why I mention Haskell. 1. It's THE other language with a type system based on HM. 2. Variant constructors as functions. OCaml does not do that, Haskell does (slightly more elegant). This hints sunnydiskincali is more familiar with Haskell than OCaml. 3. I was confused by `type shape = S.shape`. How does `RemovePoint(Shape).shape` has the `Point` case removed then? I tried that on a REPL ^1 and it didn't even compile. Again, syntax errors hinting at Haskell experiences. Well now I've written so much I may as well do a point-by-point refutation: ^2 > you create the ability to side-step exhaustiveness Big claim, sounds scary to someone not familiar with sum types. But Java/Kotlin both enforce exhaustiveness. You could have provided an example in your second response, instead you dump a bunch of code that does not compile. > Sure you can, that's just subtyping. Then you followed up with an example that is not subtyping, but an unrelated type of a new set of new values. > This is doing things quick and dirty. For this trivial example it's fine This is not fine. I undersold the verbosity of your "quick and dirty" solution saying "7 lines". To actually work with those two types, the pair of conversion functions `Shape.shape -> Bound.shape option` and `Bound.shape -> Shape.shape` is needed. > They're not similar at all. ~100 words in the paragraph, gestures to formalization, yet never explained how sum types implemented as sealed inheritance cannot be "enforcing valid program-states at a type-level". Thus my comment "a lot of words to say very little". > You're still creating a type I see you removed "unrelated" in an edit. The statement is now accurate but pointless. Of course I need to create a type, how else can I use the type system to say "this function won't return a point"? > disingenuous to imply the quotation means that the type-system in Java ... was lifted from ML. It would be more than disingenuous, colossally stupid even, if I did imply that. The wrongness would be on the level of claiming "English and Japanese are in the same language family". Your cognate/false friend analogy is much smaller in scope, just like Java taking sum types (implementing them as sealed inheritance) from ML. 1: https://ocsigen.org/js_of_ocaml/toplevel/ 2: https://xkcd.com/386/ | | |
| ▲ | ackfoobar 2 days ago | parent [-] | | I'm very embarrassed to say this. Those code examples weren't non-compiling OCaml, but valid SML. Once I remembered the existence of the language (in my defence it was never mentioned in the thread), I managed to compile the code, and confirm my suspicion: `val point: Bound.shape = Shape.Point` type-checks, because `type shape = S.shape`. To drive the point home, so does val DoesNotReturnPoint : Shape.shape -> Bound.shape = fn x => x
So the module example does not show "this function won't return a point" as one would have hoped. |
|
|
|
|
|
|
|
|
| ▲ | nukifw 5 days ago | parent | prev | next [-] |
| In the specific case of OCaml, this is also possible using indexing and GADTs or polymorphic variants. But generally, referencing as its own type serves different purposes. From my point of view, distinguishing between sum branches often tends to result in code that is difficult to reason about and difficult to generalise due to concerns about variance and loss of type equality. |
| |
| ▲ | ackfoobar 5 days ago | parent [-] | | Unless you reach an unsound part of the type system I don't see how. Could you provide an example? | | |
| ▲ | nukifw 5 days ago | parent [-] | | - You can use GADTs (https://ocaml.org/manual/5.2/gadts-tutorial.html) and indexes to give a concrete type to every constructors: ```ocaml
type _ treated_as =
| Int : int -> int treated_as
| Float : float -> float treated_as
let f (Int x) = x + 1 (* val f : int treated_as -> int *)
```
- You can use the structurale nature of polymorphic variants (https://ocaml.org/manual/5.1/polyvariant.html) ```ocaml
let f = function
| `Foo x -> string_of_int (x + 1)
| `Bar x -> x ^ "Hello"
(* val f : [< `Foo of int | `Bar of string] -> string` *)
let g = function
| `Foo _ -> ()
| _ -> ()
(* val g : [> `Foo of 'a ] -> unit *)
```
(Notice the difference between `>` and `<` in the signature?)And since OCaml has also an object model, you can also encoding sum and sealing using modules (and private type abreviation). | | |
| ▲ | ackfoobar 5 days ago | parent [-] | | Oh if you use those features to express what "sum type as subtyping" can, it sure gets confusing. But it's not those things that I want to express that are hard to reason about, the confusing part is the additions to the HM type system. A meta point: it seems to me that a lot of commenters in my thread don't know that vanilla HM cannot express subtypes. This allows the type system to "run backwards" and you have full type inference without any type annotations. One can call it a good tradeoff but it IS a tradeoff. | | |
| ▲ | nukifw 4 days ago | parent [-] | | Yes and my point was, when you want what you present in the first comment, quoting my post, you have tools for that, available in OCaml. But there is cases, when you do not want to treat each branch of your constructors "as a type", when the encoding of visitors is just rough. This is why I think it is nice to have sum type, to complete product type. So i am not sure why we are arguing :) | | |
| ▲ | ackfoobar 4 days ago | parent [-] | | > So i am not sure why we are arguing :) I think we agree on a lot of points. The rest is mostly preferences. Some other comments in my thread though... | | |
|
|
|
|
|
|
| ▲ | voidhorse 4 days ago | parent | prev | next [-] |
| I'm not sure why people are debating the merits of sum types versus sealed types in response to this. I prefer functional languages myself, but you are entirely correct that sealed types can fully model sum types and that the type level discrimination you get for free via subtyping makes them slightly easier to define and work with than sum types reliant on polymorphism. Operationally these systems and philosophies are quite different, but mathematically we are all working in more work less an equivalent category and all the type system shenanigans you have in FP are possible in OOP modulo explicit limits placed on the language and vice versa. |
| |
| ▲ | ackfoobar 4 days ago | parent [-] | | > I'm not sure why Me neither. > you are entirely correct that sealed types can fully model sum types I want to be wrong, in that case I learn something new. |
|
|
| ▲ | wiseowise 5 days ago | parent | prev [-] |
| > Slightly more verbose sum type declaration is worth it *when it makes using the cases cleaner.* Correct. This is not the case when you talk about Java/Kotlin. Just ugliness and typical boilerplate heavy approach of JVM languages. |
| |
| ▲ | ackfoobar 5 days ago | parent | next [-] | | > Just ugliness and typical boilerplate heavy approach of JVM languages. I have provided a case how using inheritance to express sum types can help in the use site. You attacked without substantiating your claim. | | |
| ▲ | wiseowise 5 days ago | parent [-] | | Kotlin's/Java's implementation is just a poor man's implementation of very restricted set of real sum types. I have no idea what > This has the benefit of giving you the ability to refer to a case as its own type. means. | | |
| ▲ | ackfoobar 5 days ago | parent [-] | | > I have no idea I can tell. Thankfully the OCaml textbook has this explicitly called out. https://dev.realworldocaml.org/variants.html#combining-recor... > The main downside is the obvious one, which is that an inline record can’t be treated as its own free-standing object. And, as you can see below, OCaml will reject code that tries to do so. | | |
| ▲ | wiseowise 5 days ago | parent [-] | | That's for embedded records. You can have the same thing as Kotlin but with better syntax. | | |
| ▲ | ackfoobar 5 days ago | parent [-] | | If you don't do inline records you either - create a separate record type, which is no less verbose than Java's approach - use positional destructuring, which is bug prone for business logic. Also it's funny that you think OCaml records are "with better syntax". It's a weak part of the language creating ambiguity. People work around this qurik by wrapping every record type in its own module. https://dev.realworldocaml.org/records.html#reusing-field-na... |
|
|
|
| |
| ▲ | gf000 5 days ago | parent | prev [-] | | You mistyped "backwards compatible change" going back to close to 3 decades. |
|