Algebraic Data Types
tech.esper.com
tech.esper.com
In general, there are a lot of algebraic structures whose essence is captured by some diagramatic property like these, such as tensor products or fiber products. They're called universal properties. Unfortunately the wikipedia page looks pretty poorly written, but you might find it interesting nonetheless.
The importance of effective ADT usage is generally under-emphasized when discussing the benefits of statically typed FP languages* like OCaml and Haskell — even though it is the way to maximize the utility of such languages, IMO.
With the right data representation, composability improves and algorithms fall into place naturally. This is further enhanced by a language like OCaml — since the compiler catches type errors and non-exhaustive matches on ADTs, any bugs are likely holes in your application model.
There are many benefits in using ADTs, modules and other type-system features to guide your program design. Others have described those benefits very well already — just read anything by Yaron Minsky or Jane Street.
* Data modeling is critical for any problem domain, and statically typed, non-FP languages (Java, C++, etc) certainly have facilities to encourage effective modelling, but languages in the vein of OCaml and Haskell really push to make the type system do as much work as possible.
Switch statements are ok but not typesafe since nothing prevents you from desynchronizing the tag and data
More concretely, even without pattern matching, so long as, for instance, these three functions are all defined
pair : a -> b -> Pair a b
pi1 : Pair a b -> a
pi2 : Pair a b -> b
in1 : a -> Sum a b
in2 : b -> Sum a b
sum : Sum a b -> (a -> c) -> (b -> c) -> c
The trick is that unless you have first-class functions you probably cannot reify such a destructor. It always just lives in your syntax.
On the flip side, that's really what it means for a language to, say, lack sum types. It's not that the language doesn't have the ability to have choice, it's that it lacks the ability to represent choice in data. In other words, you probably can eliminate choice using if/switch/case/what-have-you but you can't construct it.
A list is either null or else has a head (h) and a tail (t) which is a list.
Rod Burstall picked up on this in "Proving Properties of Progams by Structural Induction" (1968) in an extension to Landin's ISWIM that used pattern matching on these. If you look closely the pattern matching was present in his if-then-else syntax, but he changed it to the more convenient "case".
Swift has it, but it lets you easily subvert its meaning ('trust me, it's not null'), so I don't think it's as useful as it is in the usual functional languages.
Here is a malformed question that occurs to me just now:
In a language like python i can form instances of a product type using tuples, but making instances of a sum (variant) type ... ?
How is it that the duality is broken when I no longer have variable declarations? Or is every object instance already a variant (of every possible subclass) ?
As a starter guide, I highly recommend reading Lawvere's Conceptual Mathematics.
A more useful type system would have "union types". They differ from sum types in that you can construct a union type from existing types in an ad-hoc manner. For example, if you have a function that returns a string or nil you can construct a union type "Union of string or nil". To do this with a sum type you'd have to have a common super type of string and nil and no other types.
There are also intersection types, about which I know very little.
This is only if you reject the notion of a dynamic type (as most type theorists do, but programmers do not). Otherwise, Python has a rich type system that is checked at run-time. It lacks sum types, but we could easily imagine a dynamically checked realization.
Note that most sum-types are implemented by having a runtime tag on which you can discriminate.
If an "average programmer" here and a type theorist spent 1 minute at the beginning of the conversation normalizing terms then nobody would have any argument here. I don't think anyone tries to claim that "types" and "static types" (or, in the type theorist's parlance, "tags" and "types") are the same... they just try to argue whether or not it's "right" to call one or the other by the name "type".
In particular, many things I can state about static types do not carry over to dynamic types and visa versa.
I believe many conversations get derailed early because among static type researchers, static types are known merely as "types" and dynamic types as "tags" or "classes". There are meaningful ways to compare these two kinds of things but somehow or another they ought to have different words since confusing the concepts will inhibit understanding quite severely.
This seems wrong. You can make a new type that simply contains one of those, right?
In a sense that's what you're doing with a sum type in Haskell, though there you get to produce new types automatically from higher kinded types.
I'm not sure you understand sum types. Sum types subsume normal unions; sum types and unions are essentially the same thing and capturing this kind of return type in Haskell or ML is extremely easy. "Supertypes" are completely unrelated and subtyping is not actually needed in languages with sum types (for example Haskell has sum types but doesn't have any real form of subtyping).
For example in Haskell you'd use the `Maybe` type constructor. If your type returns a `Maybe String` that means it either returns a string or nothing.
public static void test(Foo f) {
if (f isinstanceof SubA) {
SubA a = (SubA)f;
/* ... */
} else if (f isinstanceof SubB) {
SubB b = (SubB)f;
}
}
Standard ML approaches subtyping in a very different way that renders this kind of approach impossible. It gives you less freedom in that it eliminates downcasting, but that ultimately results in a safer language. Of course Standard ML has proper sum types with all of their compile-time guarantees so there's little reason for it anyway.
public static void test(MaybeFoo mf) {
switch(mf.type) {
case MaybeFoo.NOTHING:
/* ... */
break;
case MaybeFoo.JUST:
Foo f = mf.getFoo();
/* ... */
break;
}
}
(I could totally be missing/misunderstanding something, though...)
So that's the blindness. The pre/post conditions around how mf.type relates to its surroundings cannot be expressed first-class in the code. You are required to do risky things like call potentially partial code.
(a -> r) -> r -> Maybe a -> r
So, I think "bare primitive types lack meaning" is basically correct given that you interpret "meaning" as "meaningful uses/actions".
I would note that when I'm dealing with tagged unions in C, as soon as the operation gets at all complicated (more than maybe 3 lines?) I try to pass it off to another function operating on the internal value which restores safety outside the boilerplate. I agree that support for a true tagged union is ideal, though. (Actually, this might make a good attribute in GCC...)
type AST = Expr of ...
| Stmt of ...
| Comment of ...
let rec evaluate e =
match e with
| Expr # evaluate the ... of an Expr
| Stmt # ditto
| Comment # ditto
class AST {
public:
virtual bool evaluate() = 0; // again, forgive the C++ syntax
};
class Expr: public AST {
public:
virtual bool evaluate()
{
// Expr specific evaluate code
}
};
class Stmt: public AST {
public:
virtual bool evaluate()
{
// Ditto
}
};
class Comment: public AST {
public:
virtual bool evaluate()
{
// Ditto
}
};
Doesn't the discrimination of which branch of a sum type your data represents generally happen at runtime?
What I was getting at is that when we use the algebraic version of AST, we know exhaustively what forms it can take. The definition tells us. In the OO version, this is note true. If we restrict our use to the polymorphic functions, then this is fine. But if we try to inspect the OO version of AST, ask its true type, and then act on it, then we may get into trouble.
In Type theory, the product is a product in the sense of category theory, which is a very abstract notion of product indeed. The idea is that given objects, here types, A and B; you can form their product, A * B and that is also a valid object in the category. The diagram then universally identifies the A * B element as the one where you can project out of it via the 1st and 2nd projection such the at given diagram commutes, etc. And it is important to stress there are many products for which this property hold.
(Edited a bit to appease the automatic formatter at HN)
For any category, the product A * B of two objects A, B (if it exists) is unique only up to isomorphism (this follows from the universal mapping property).
In general, products A * B and C * D need not be isomorphic (and seldomly are), and neither do products from different categories. Many of the commonly-used products actually arise from a product in a suitable category, the cartesian product, for example, is a product in the category of sets.