4 ms·

> 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 givin

> 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.

wiseowise 1y ago
> 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.
- gf000 1y ago
  You mistyped "backwards compatible change" going back to close to 3 decades.
- ackfoobar 1y ago
  > 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 1y ago
    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 1y ago
      > I have no idea I can tell. Thankfully the OCaml textbook has this explicitly called out. https://dev.realworldocaml.org/variants.html#combining-records-and-variants 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 1y ago
        That's for embedded records. You can have the same thing as Kotlin but with better syntax.
        ackfoobar 1y ago
        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-names https://dev.realworldocaml.org/records.html#reusing-field-na...
nukifw 1y ago
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 1y ago
  Unless you reach an unsound part of the type system I don't see how. Could you provide an example?
  - nukifw 1y ago
    - You can use GADTs (https://ocaml.org/manual/5.2/gadts-tutorial.html 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 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 1y ago
      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.
sunnydiskincali 1y ago
> 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 1y ago
  > 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?
voidhorse 1y ago
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 1y ago
  > 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 1y ago

> 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.

gf000 1y ago
You mistyped "backwards compatible change" going back to close to 3 decades.
ackfoobar 1y ago
> 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 1y ago
  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 1y ago
    > I have no idea I can tell. Thankfully the OCaml textbook has this explicitly called out. https://dev.realworldocaml.org/variants.html#combining-records-and-variants 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 1y ago
      That's for embedded records. You can have the same thing as Kotlin but with better syntax.
      - ackfoobar 1y ago
        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-names https://dev.realworldocaml.org/records.html#reusing-field-na...

nukifw 1y ago

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 1y ago
Unless you reach an unsound part of the type system I don't see how. Could you provide an example?
- nukifw 1y ago
  - You can use GADTs (https://ocaml.org/manual/5.2/gadts-tutorial.html 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 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 1y ago
    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.

sunnydiskincali 1y ago

> 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 1y ago
> 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?

voidhorse 1y ago

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 1y ago
> 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.