Are these really algebraic data types?

[JeffreyBenjaminBrown]

Coconut's documentation for the data keyword states that it lets you create immutable ADTs. I see a nice concise language for creating immutable product types, but for it to truly offer an algebra, I believe[1] it would have to offer sum types.

The data keyword lets us multiply two types. For instance, we can multiply the int type with the string type by making a type T that has two fields, one of them an int and the other a string. In every instance of T both fields are mandatory.

If we could add the types int and string, it would mean we could create a new type T for which every instance could include either a string or an int, without including the other. That is, the type T would offer multiple constructors, which when called create instances of T with different fields.

Right?

---

[1] My understanding* of the term "algebra" is that it implies both addition and multiplication, and that for types, "multiplication" is the conjunction (and) operator, while "addition" is the disjunction (or) operator.

That interpretation seemed very weird to me until I noticed its implications for the size of the sets in question: If type A has 5 members and type B has 6, then their sum has 11 members, while their product has 30.

Sorry if I'm stating things you already know; I'm trying to keep a wide potential readership.

[evhub]

@JeffreyBenjaminBrown I think this needs to be documented better, because my thinking on how best to do this in Coconut has evolved a lot since I wrote most of the documentation, but I'll show you my current thinking as to how to translate sums and products into Coconut. Consider the Haskell data type

data Something = SomeInt Integer | SomeFloatPair Double Double | Nothing

then, I would translate that into

class Something
data SomeInt(x: int) from Something
data SomeFloatPair(x: float, y: float) from Something
data Nothing() from Something

which basically does the exact same thing. There are a couple of remaining things with that implementation that I am unsatisfied with, however. First, I think the idiomatic syntax here is pretty good but it needs to be documented so people know that this is the idiomatic way to do it. Second, if you want the equivalent of adding deriving (Eq, Ord) to the Haskell code, you have to write something like this derivingEqOrd function (which you can see used here), which is rather messy. At some point, I would like to go through the documentation and clean up all my uses of algebraic data type so that they all actually make sense.

[3noch]

This is still an open sum type, rather than a closed one, correct? I don't think subclassing even allows for closed sum types. Without closed sum types you cannot [easily] check totality.

[evhub]

@3noch Yeah, you're totally right on that one. I'm not sure what the use case would be for totality checking, though--what sort of situation are you thinking about where you would want to be able to do that? You could check for pattern-matching totality, but Coconut's pattern-matching, by design, doesn't do that, and I'm not sure where else you would want to. Thoughts?

[JeffreyBenjaminBrown]

I like totality checking because it lets me know if I've covered all cases when defining a function. Without it, effectively, the compiler lets you call functions that don't exist.

Apparently totality checking enables some kinds of optimizations that would not be possible otherwise. I don't really understand the arguments.

[3noch]

In a dynamic language this is mostly moot because you're essentially choosing to have all your errors at runtime anyway. The only thing you could is try to throw exceptions sooner rather than later, but always during runtime. The best that could be done here would be some sort of MyPy integration I think. I'm not sure if MyPy supports totality checking of sums.

[eindiran]

You can get something like closed sum types using tagged unions: Union[int, float, None]

[3noch]

@eindiran Is that Coconut syntax? I didn't realize you could define anonymous sum types that way. If so, how do you pattern match/check which of the slots is occupied? Closed sum type and tagged union are synonyms.

[evhub]

@3noch The Union[int, float, None] syntax @eindiran is referring to is standard Python typing syntax which can be checked by e.g. mypy.

[3noch]

Cool! I was never able to dive into Python 3 types when I used Python actively. Neat to see it supports that kind of flexibility.

[JavaScriptDude]

ADTs and pattern matching are what attracted me to investigate Coconut but the docs are definitely wanting for a n00b like me.

When you update the docs, can you please illustrate various usecases for ADTs and go into ways of using them in pattern matching. Maybe follow docs like Elm or Reasonml for examples of well laid out samples.

[eindiran]

@JavaScriptDude Is this the Elm documentation on pattern matching that you are talking about? https://guide.elm-lang.org/types/pattern_matching.html Similarly, are these the ReasonML docs? https://reasonml.github.io/docs/en/pattern-matching

[JavaScriptDude]

Yes, those are the docs. Even their docs could be expanded a bit.

It would be good to illustrate how one would match against ADT types. From my research, type validation is done with the expression "where type() is ". I could not find any coconut specific shorthand for type checking in match statements.

[evhub]

@JavaScriptDude Type checking in match statements (as documented here) is just data_type(arguments). For example:

class Tree
data Empty() from Tree
data Leaf(n) from Tree
data Node(l, r) from Tree

match Tree() in Empty():
    print("match!")
match Empty() in Empty():
    print("match!")
match Tree() in Leaf(1):
    print("no match")
match Tree(n) in Leaf(1):
    print("match %s!" % n)
match Leaf(n) in Leaf(1):
    print("match %s!" % n)