Sum Types Are Coming (2015)
chadaustin.me
chadaustin.me
http://joeyh.name/blog/entry/making_propellor_safer_with_GAD...
They add the ability for constructors to carry constraints, which aids expressivity in some cases.
But the majority of GADT uses purely add safety. Can use ordinary ADT without a type-variable that is correlated with the data constructor, and crash at runtime if the constructors don't match.
You answered yourself: If you cannot have these runtime type mismatches, you don't need to write the corresponding bookkeeping and checking code.
The real power of GADTs comes from the fact that you can use the type at compile time. This means that in OCaml I can do something like:
type 'a t =
| Int : int t
| Float : float t
let print : type a. a t -> (a -> string) =
function
| Int -> string_of_int
| Float -> string_of_float
Although this is a slightly contrived and useless example, there are scenarios where this can prove immensely useful that are not that far away and really aren't so useful when done with ADTs. Think serializing -- you would have to convert to the ADT first which isn't so useful. If you're interested in something useful, take a look at [0] (shameless plug), a very early alpha version of a similar idea allowing conversion from and to JSON.
EDIT: this is not inlined as I recall. False memory. The reason it isn't is probably because you can use existential types in which case the type would not be known at compile time.
https://drup.github.io/2016/08/02/difflists/
I also have some slides (more entertaining and probably better introduction) here:
This especially happens nicely when the syntax is built into the language in a succinct way as in F# / OCaml (possibly others as well!)
In other words: learn to mathematics.
That breaks the HN guidelines by crossing into incivility. You'd stopped doing that on HN, which is great, so please don't resume.
This comment would be better if it (a) dropped the rude bit and (b) made the distinction from disjoint unions more clearly.
Just in case it's not clear, the union of sets "merges" elements that are identical whereas in the (direct) sum each element gets tagged with where it comes from.
Formally, we have a set that indexes over the sets we want to sum and then we just Cartesian product each set with it's index before unioning. In abstract nonsense we usually write
A ⊕ B = (A × {0}) ∪ (B × {1})
where ⊕ is the direct sum operator. So there direct sum of a set with itself is quite different from a plain union. For more than two sets we just index over things in the obvious way and write
⨁ᵢ Aᵢ = ∪ᵢ (Aᵢ × {i})
What parent means by universal property is that any that collection of functions {fᵢ : Aᵢ → C} can be decomposed into functions {gᵢ : Aᵢ → ⨁ᵢ Aᵢ} and a single, uniquie g: ⨁ᵢ Aᵢ → C where fᵢ = g ∘ gᵢ.
With a little thought, the universal property above seems obvious, and with a little more work, you can see that it is actually equivalent to the definition of direct sum above.
Thus we can actually take this universal property as the definition of direct sum and derive the original. The cool thing is that the universal property doesn't refer to set-specific operations---just functions/maps---so we actually have a definition for the direct sum of things more general than sets. That is, we can form the direct sum of things like monoids, groups, certain classes of differential functions, etc.
I could go on, but this road leads to madness^W category theory.
That's just a union. The disjoint union (https://en.wikipedia.org/wiki/Disjoint_union) is what you're calling the direct sum. The direct sum (https://en.wikipedia.org/wiki/Direct_sum) is an operation on algebraic structures to create new algebraic structures (e.g., one can direct-sum two groups to get a new group, and similarly rings, vector spaces, etc.), not just sets.
In case it's not clear, I just specialize tensor sum to the category Set; that's all. At the end I do mention how the tensor sum applies on a wider class of objects. In fact, any Cartesian category has (finite) tensor products, even if the objects aren't traditionally thought of as "algebraic structures", e.g. certain classes of topological spaces, Frolicher manifolds, etc.
As if that weren't enough, any talk about universal properties is utterly pointless as soon as object identities matter everywhere.
> A ⊕ B = (A × {0}) ∪ (B × {1})
Hardly nonsense! This makes clear the connection to sets in a way that words weren't doing for me.
(The Flow use of the name doesn't seem to quite match the mathematical definition.)
In any case, Flow doesn't require that the sides of the | are different.
> These disjoint unions are made up of any number of object types which are each tagged by a single property.
It is clearly a disjoint union in the set-theoretical, not category-theoretical sense.
Let's see their own example:
// @flow
type Success = { success: true, value: boolean };
type Failed = { success: false, error: string };
type Response = Success | Failed;
function handleResponse(response: Response) {
if (response.success) {
var value: boolean = response.value; // Works!
} else {
var error: string = response.error; // Works!
}
}
type X = { foo: string }
type Y = { foo: string, bar: string }
type Foo = X | Y
The way you sum a type with itself in Haskell would be something like
data Response = Success { result :: String }
| Failure { reason :: String }
From my understanding of the Flow documentation, the equivalent would be
type Response = {| success: true, result: string |}
| {| failure: true, reason: string |};
So although sum types and disjoint unions are different concepts, they can easily be used to simulate each other.
(0) There is a single physical universe that contains all values.
(1) The role of types is to “carve out” fragments of this universe.
(2) Say you have two values `x` and `y` of types `A` and `B`. Because it is possible to form the union type `A | B`, to which both `x` and `y` belong, the only way to make sure `x` and `y` cannot be conflated with each other is to make them physically distinct elements of the universe.
On the other hand, abstract types make the following assumptions:
(0) Each type is a “world” of its own, defined in terms of its logical structure. The values of a type are a mere consequence of this logical structure. Hence, it doesn't make sense to try to “split” or “merge” types.
(1) It doesn't make sense to argue that an int is different from a string, because it's just as nonsensical as arguing that they are equal. What they are is incommensurable.
(2) Say you have type two different abstract types `A` and `B`. Because they could share an underlying representation type `T`, you cannot rely on values of different types having physically distinct representations.
---
Suppose we had a language with both union and abstract types. The contradictions between the assumptions behind union and abstract types would lead to hilarious consequences:
signature ERROR_CODE =
sig
type error_code
(* specification of operations on error codes *)
end
(* we use opaque ascription, so that the internal representation
* of error codes becomes inaccessible to external parties *)
structure ErrorCode :> ERROR_CODE =
struct
type error_code = int (* prosaic representation *)
(* implementation of operations on error codes *)
end
type union = error_code | int (* union *)
(* suppose we also have flow typing so that this example works *)
fun test (u : union) =
if u is error_code then
ErrorCode.printErrMsg u
else
printInt u
val _ = test 42
ERR_DOUGLAS_ADAMS : The answer to the Ultimate Question of Life,
the Universe and Everything is the number forty-two.
I agree that being able to change the internals of a module without breaking external code is a good thing, but unlike other security guarantees, abstract types can break merely by having a stronger type system which is able to prove strictly more things (such as whether two types are equal). That makes implementing completely leak-free abstractions quite difficult.
It can even be hard to tell which language feature exactly causes the leak. In your example, it is not just the existence of the union type that causes the problem, but the operation "is T", which you probably assume to be of type "forall a. (a | T) -> Bool" or something. Obviously, that operation is doing all the work of looking at the underlying implementation and leaking it.
While you couldn't meaningfully type such an operation without union types, having unions in your type system does not mean that such a function will be available. Although working with unions without being able to tell the types apart would be quite inconvenient, you could nonetheless remove that ability from the language, either completely (effectively requiring all unions to be disjoint) or by having special markers to enable or disable it (similar to Haskell's type class constraints).
Flow doesn't go to such great lengths because it is still built on JavaScript objects, which don't really have a concept of privacy. If there were private symbols (i.e. unique properties which can only be accessed by the module which defines them), you could trivially implement abstract types similar to Haskell's newtype wrapper as { [some private symbol]: implementation-type }. Until such a thing is added, you'll have to limit yourself to disjoint unions to avoid abstraction leaks.
Indeed, which is why I'm not such a huge fan of overly powerful type systems.
> That makes implementing completely leak-free abstractions quite difficult.
It means the type system has to have the right amount of expressive power. Too little, and separation of concerns becomes difficult. Too much, and separation of concerns becomes difficult too!
It also means that we can't rely on types to prove everything we would like to prove about programs. This seems intuitively right, because type systems are first and foremost meant to be mechanically checkable, not to be flexible enough to express every possible software requirement.
> In your example, it is not just the existence of the union type that causes the problem, but the operation "is T", which you probably assume to be of type "forall a. (a | T) -> Bool" or something.
This is correct. But removing this `is T` operation would greatly reduce the appeal of union types in practice.
> you could trivially implement abstract types similar to Haskell's newtype wrapper as { [some private symbol]: implementation-type }.
Both Haskell's `newtype` and your proposal are poor replacements for actual abstract types.
The union of two types contains all values that are in either component type. The sum of them contains all of the values of the first type, each one associated with a tag like “I came from the left side” plus all of the elements from the second type with a similar tag.
The Union of Bool and Bool has 2 values, the Sum has 4.
If we define Maybe[A] to be the process of unioning on “null” to the values of A then Maybe[Maybe[A]] = Maybe[A]. If it’s defined with a Sum then that equation doesn’t hold.
What ml style language has the closest thing approaching a lisp style repl?
If you are a SLIME fan, you might notice that some of the key bindings to interact with the toplevel (the OCaml word for "REPL") are identical in Tuareg.
That said, although this will sound tongue-in-cheek: Having used Isabelle and Coq with their interactive editors, I find their approach better than a REPL. In these systems, you execute code directly from your source file, as opposed to (conceptually) sending snippets of code to a REPL. There is no concept of code you have written in the source (or the REPL) which is not synced up with the state of the REPL (or the source code, respectively). I wish other languages had modes like this. There seems to be one for Prolog, but I've never used it and don't know how well it works in practice: https://www.metalevel.at/ediprolog/
State machines are a great thing, and modelling a state machine as a sum type is reasonably common (it's not the best modelling for all state machines, but it's very good for many).
There does seem to be recent trend of popular, highly visible languages that are adding the feature though. I think the biggest thing though is really that the pattern matching syntax that makes them so easy to use is becoming more common.
You can have Sum types without pattern matching, and vice versa, but it seems to be much more common now to expect any new language to include pattern matching.
I don't think that lambdas/closures have such a problem in most programming languages. It's still unclear how to handle function pointers for lambdas/closures, but it should be a lot easier to make a lambda into a real function than changing a datatype definition when it's already used across the codebase.
So, I think sum types are really another one of those ideas which may prevent some bugs sometimes, but in the end are not generally super useful, and are just a little too clever and end up causing a more work than they save. At least unless there's a well-defined representation from which we can extract the type information, in which case I'd probably be happy to use them.
Though I do wonder if reflection on type information (at runtime?) would be useful and easy for you if you find basic algebraic data types "a little too clever" and "causing more work than they save".
What I would do with it? Like the result of (x+y), or any type of data, I can use it for whatever I need. I might simply want to count the number of occurences of each "type". Often I'm simply not interested in the data besides the "type", and in these cases I find that case-matching is a lot of boilerplate. And it doesn't reify the "type" to authoritative runtime values. Which, as you say, might be done with reification support from the language, but I don't want to bother with that -- and it would not allow me to choose the possible values of the type field, which might be a requirement if the options are defined somewhere else.
OK. If I understand correctly, you want to use that field in other contexts than doing a switch on it, whereas in Haskell the usual way of consuming the type tag is to do such a switch, as in the article's example:
case event of
ClickEvent x y -> <do click stuff>
PaintEvent color -> <do paint stuff>
// there are no other possible cases, so no default case needed
Sure, but you can do that with a case expression as above. Here is a complete example:
data Event = ClickEvent Int Int | PaintEvent Int
-- separate a list of Events into two lists, the first holding the payloads
-- of the click events, the other the payloads of the paint events
separate :: [Event] -> ([(Int, Int)], [Int])
separate [] = ([], [])
separate (event : events) =
case event of
ClickEvent x y -> ((x, y) : clicks, colors)
PaintEvent color -> (clicks, color : colors)
where
(clicks, colors) = separate events
example = [ClickEvent 1 2, PaintEvent 42, ClickEvent 3 4, PaintEvent 23]
> separate example
([(1,2),(3,4)],[42,23])
(Depending on the exact specification and performance requirements, the code might be written a bit differently in the real world.)
EDIT: Ah, you edited your post while I was writing. Oh well. Regarding reifying constructors as integers or whatever, yes, you might have to write a two-line function to do that.
You can do it with reflection, which somewhat confusingly Haskell calls "generics": https://wiki.haskell.org/GHC.Generics It's very old terminology, you'll have to forgive them. If you carefully trace the etymology back to the 1990s-ish when Haskell established that term, and trace the academic ideas of "generics" back that far, you can actually find the similarities with the old academic ideas of generics and what we today call reflection, but nowadays they are so separated it's really just of historical interest.
That said, very little code uses it, because generally in Haskell whenever you would want to do "OK, look at the type of a thing, then decide what to do based on the type, then do the thing" that almost always can be collapsed down to "Pattern match on the thing, then do the thing you wanted to do". You write what it is you want to do based on types into the pattern matching itself, collapsing the middle step where you have an explicit value representing the type into implicit knowledge contained in the branch of the pattern match that occurs.
I do understand why you are thinking that way and am not trying to say it's a bad thing in general. While it's not the first thing I reach for in my Go code, I do have some very reflection-heavy Go code that works that way. But in Haskell, there's almost (but not quite) always a better solution for Haskell. If you could program the way you are discussing in Haskell, you'd find the type checker would be an even bigger jerk to you than it can be when you program the "right" way; I think you'd have a hard time making that code work with GADTs, and GADTs are very, very common in Haskell.
https://github.com/radix/sumtypes/
(Same year - 2015 - as the original post ;)
There isn’t a One True Approach; I do all my work in Common Lisp or C++ and although both are multi-paradigm languages they aren’t substitutable for each other.
Also I think the name 'sum type' is bad. Nothing gets added or summed up, just combined and selectively chosen. For this reason I find supercharging 'enum', like Swift does, a more logical solution.
Various languages use different keywords to access the same concept:
- Rust: 'enum'
- Swift: 'enum'
- Haskell: 'data'
- F#: 'type'
- Ocaml: 'type'
> Also I think the name 'sum type' is bad. Nothing gets added or summed up, just combined and selectively chosen. For this reason I find supercharging 'enum', like Swift does, a more logical solution.
They're the same solution...
In any case, the name sum comes from viewing types "algebraically" as the article discusses. Doing addition of types with a sum type has a lot of similar properties to doing addition of numbers, and similarly doing multiplication of types with a product type (tuple, struct or class, in Swift) has a lot of similar properties to doing multiplication of numbers.
Playing with that a little, if adding a property to an interface is a product, eg:
interface Foo {
foo: string;
bar: number;
}
type Diff<T extends string, U extends string> = ({ [P in T]: P } & { [P in U]: never } & { [x: string]: never })[T];
type Omit<T, K extends keyof T> = Pick<T, Diff<keyof T, K>>;
interface Foo {
foo: string;
bar: number;
}
interface Bar {
bar: number;
}
type Out = Omit<Foo, keyof Bar>;
interface Out {
foo: string;
}
Out = Foo / Bar = (string * number) / number = string
The closest thing to a division would be a quotient set ( https://en.wikipedia.org/wiki/Quotient_set ), but there you're dividing by an equivalence relation. It is however possible to define an equivalence that undoes set multiplication: (A × B)/~ ≅ A if (a₁, b₁) ~ (a₂, b₂) holds iff a₁ = a₂, ignoring the other component.
Nowadays I consider that a mistake, and all unions have a discriminator property, and there is no need for custom type guards (exceptions would be when writing .d.ts files for JS that uses them untagged, that sort of thing) since it makes the code much more explicit.
Conjunction and disjunction also have other properties, like idempotence: A /\ A = A, which by analogy would suggest that a tuple of two integers is the same as a single integer. Similarly, A \/ A = A, which is exactly the problem mentioned by the featured article that is the difference between union types and proper sum types (aka tagged union types).
So while sum and product may not be great analogies, conjunction and disjunction seem worse.
TLDR: If you interpret sum types as + and product types (tuples/structs/objects) as *, type definitions can be read as polynomials. Recursive type definitions, like for linked lists, can be read as recurrence equations. If you do some calculus over these things and compute the derivative of these type formulas, you get back something meaningful: The formula corresponding to the type's Zipper (https://en.wikipedia.org/wiki/Zipper_(data_structure)), a data structure for efficiently traversing and modifying functional data structures.
I like Chris Taylor's series of posts on this topic, as well as this shorter one: https://codewords.recurse.com/issues/three/algebra-and-calcu...
E.G "boolean" dates back to George Boole, The Mathematical Analysis of Logic (1847)
https://en.wikipedia.org/wiki/Boolean_algebra#History
and "lambda" to Alonzo Church in the 1930s
- C: 'union'
If you've ever dealt with an AST, a sum type is really a wonderful way to represent the nodes. In C you probably want some sort of 'tag' to indicate the actual type of the union. Other languages handle that bookeeping for you.
for java i'm tempted to say 'interface' but that doesn't quite have the flavor of what you're driving at. definitely in the same spirit though.
The intuition is that for each types A and B with number of elemnts |A| and |B| the sum type A+B has number of elements |A|+|B|.
There are much more confusing things in type theory, like the ambiguity that the word 'type' has (I still don't grok the terminology, to be honest).
If you view types as sets of values, then a sum type is the addition (union) of two sets, while a product type is the product (combination) of two sets.
> For this reason I find supercharging 'enum', like Swift does, a more logical solution.
Both are logical, they just come from different trains of thought.
Extending "enum" comes from "developers" viewing sum types as extensions of C-style enums, sum types comes from computer science and set theory.
Either<u8, bool>
Tuple<u8, bool>
Of course, this simple numerical interpretation breaks down as soon as you have something like a linked list which has infinite possible values, but even then, you can fuzz the rules a bit and get useful information out of the math. But that is the core intuition.
(which honors the convention of expressing a dual using "co-" and indeed co-product is the dual of product)
They're not coming, they've been and gone, probably a couple of times
Of course, both have been in boost for some time now. C++ so far has been doing this at the library level. But it remains to be seen if they will make their way into actual interfaces, for example in standard algorithms.
> The "expression problem" is a phrase used to describe a dual problem that neither ObjectOrientedProgramming nor FunctionalProgramming fully addresses.
"dual problem", meaning you choose ObjectOrientedProgramming or FunctionalProgramming, which neither fully address.
neither "side" is able to resolve the ExpressionProblem
That's a huge difference in terms of code architecture - it enables things like exhaustive pattern matching, and allows the programmer to enforce stronger invariants in the code.
This is simply a distinction between closed and open sum types.
[1] https://caml.inria.fr/pub/docs/manual-ocaml/extn.html#s%3Aex...
[2] http://caml.inria.fr/pub/docs/manual-ocaml-400/manual006.htm...
The term "union" as used in C is highly related but not quite the same. If you add a tag to the union (and so have a "tagged union", often represented in C as a struct with an enum and a union) then you are equivalent in an information sense (but the usage is still different, as a C union says something very specific about how memory is used).