8 ms·

Algebraic Data Types

157 points by ALee 12y ago

austinz 12y ago
Enjoyed this article. Another good read on ADTs: http://tel.github.io/2014/07/23/types_of_data/ http://tel.github.io/2014/07/23/types_of_data/, and for a Swift-specific take: http://tel.github.io/2014/07/26/types_of_data_in_swift/ http://tel.github.io/2014/07/26/types_of_data_in_swift/
- devty 12y ago
  thank you for the link!
doctorKrieger 12y ago
so the monad tutorials stopped being cool?
rrradical 12y ago
I wrote recently about the option type specifically (called Maybe in Haskell): http://asivitz.com/posts/learn_to_love_maybe_kick_null http://asivitz.com/posts/learn_to_love_maybe_kick_null 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.
jallmann 12y ago
Nice article, I never considered the duality of product and sum types before. 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.
- eru 12y ago
  ADTs are a bit like garbage collection: they originated in functional languages, they provide huge productivity gains, and they are (in theory) very easy to prop onto any kind of language. You can imagine a variant of C that has ADTs---they'd just be called tagged unions.
  - nimish 12y ago
    ADTs and pattern matching go together. Having tagged unions is awful without a good way to discriminate upon them. Switch statements are ok but not typesafe since nothing prevents you from desynchronizing the tag and data
    - tel 12y ago
      If you think of ADT definitions as defining how you construct types then you get a natural method for destructing them or using them automatically. This could be pattern matching or it could be explicit functions 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 You'll be equivalently expressive.
      - taejo 12y ago
        C already has product types, so it's sums that are more interesting, and indeed the destructors for sums are harder in C. The constructors in1 : a -> Sum a b in2 : b -> Sum a b are no problem, but the destructor sum : Sum a b -> (a -> c) -> (b -> c) -> c needs first-class functions.
        deleted 12y ago
        [deleted]
        dllthomas 12y ago
        C already has sum types, just slightly sloppy ones (as unions aren't required to have a tag).
nice_uname_nerd 12y ago
If you haven't seen any category theory, you might be interested to know that the diagrams the author draws are valuable and important in modern pure math as well. Those last two diagrams totally capture the idea of what a product or variant (coproduct, in math terminology) is. 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. http://en.wikipedia.org/wiki/Universal_property http://en.wikipedia.org/wiki/Universal_property
_pmf_ 12y ago
If they say "cross product", don't they actually mean "cartesian product"?
- throwaway283719 12y ago
  To mathematicians, the two are kind of interchangeable. I suppose "cartesian product" is a bit more specific, as "cross product" is also used to mean the vector cross product, which is different.
- jlouis 12y ago
  Beware here! There are a couple of different products you can sensibly form on data. So you have to make it very explicit which you mean when you talk about them. You can't generally interchange them in all contexts, but in some contexts you definitely can. 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)
  - mmarx 12y ago
    Any two of those many products, however, are isomorphic, and hence, while still distinguishable, they are “essentially” the same.
    - tel 12y ago
      If I'm reading the op right, this is incorrect. Oftentimes "products" in various contexts are "categorical products cut down by some sensible quotienting". In any category the categorical product will always be the largest (this is essentially what its definition entails) and only by careful choice of category will that correspond to some of the less formal "products" available.
kawa 12y ago
BTW: Union types ("tagged unions") predate OOP by some years and thus were there long before OCaml or Haskell. Algol68 had them and also Pascal for example. The invention of ML was pattern matching on those data structures.
- viraptor 12y ago
  Pascal's "tagged unions" don't offer anything more than C's though. It's still unsafe and always requires as much memory as the combination of largest cases. OCaml / Haskell / others don't allow type changes at least. That would be useful even without the pattern matching.
- ericssmith 12y ago
  FWIW, Peter Landin sowed the seeds in "Mechanical Evaluation of Expressions" in 1964 in his description of recursive discriminated union for lists: 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".
mathgenius 12y ago
I can never get enough of the arrow theory. 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) ?
- tel 12y ago
  "Arrow theory" here is better known as Category Theory. I highly, highly recommend learning more about it if you're interested. I cannot understate its beauty. As a starter guide, I highly recommend reading Lawvere's Conceptual Mathematics.
- noelwelsh 12y ago
  In a language like Python you can consider there to be one type called, say, ThePythonType, or which all types are a variant. Then all objects have type ThePythonType. 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.
  - seanmcdirmid 12y ago
    > In a language like Python you can consider there to be one type called, say, ThePythonType, or which all types are a variant. Then all objects have type ThePythonType. 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.
    - jlouis 12y ago
      A good way of getting at this is to call things at runtime "classes" or "tags" to make it apparent that their discrimination happens at runtime, not compile-time. The problem is that if you call both things types, you quickly run into a situation where you are essentially talking about different concepts entirely. Note that most sum-types are implemented by having a runtime tag on which you can discriminate.
frou_dh 12y ago
Sum types with compiler-enforced exhaustive pattern matching feel like a massive win and are the main thing I'd love to import in to traditional procedural programming. Switch statements and their ad hoc nature pale in comparison.

157 points by ALee 12y ago

Enjoyed this article. Another good read on ADTs: http://tel.github.io/2014/07/23/types_of_data/ http://tel.github.io/2014/07/23/types_of_data/, and for a Swift-specific take: http://tel.github.io/2014/07/26/types_of_data_in_swift/ http://tel.github.io/2014/07/26/types_of_data_in_swift/

devty 12y ago
thank you for the link!

doctorKrieger 12y ago

so the monad tutorials stopped being cool?

rrradical 12y ago

I wrote recently about the option type specifically (called Maybe in Haskell): http://asivitz.com/posts/learn_to_love_maybe_kick_null http://asivitz.com/posts/learn_to_love_maybe_kick_null 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.

jallmann 12y ago

Nice article, I never considered the duality of product and sum types before. 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.

eru 12y ago
ADTs are a bit like garbage collection: they originated in functional languages, they provide huge productivity gains, and they are (in theory) very easy to prop onto any kind of language. You can imagine a variant of C that has ADTs---they'd just be called tagged unions.
- nimish 12y ago
  ADTs and pattern matching go together. Having tagged unions is awful without a good way to discriminate upon them. Switch statements are ok but not typesafe since nothing prevents you from desynchronizing the tag and data
  - tel 12y ago
    If you think of ADT definitions as defining how you construct types then you get a natural method for destructing them or using them automatically. This could be pattern matching or it could be explicit functions 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 You'll be equivalently expressive.
    - taejo 12y ago
      C already has product types, so it's sums that are more interesting, and indeed the destructors for sums are harder in C. The constructors in1 : a -> Sum a b in2 : b -> Sum a b are no problem, but the destructor sum : Sum a b -> (a -> c) -> (b -> c) -> c needs first-class functions.
      - deleted 12y ago
        [deleted]
      - dllthomas 12y ago
        C already has sum types, just slightly sloppy ones (as unions aren't required to have a tag).

nice_uname_nerd 12y ago

If you haven't seen any category theory, you might be interested to know that the diagrams the author draws are valuable and important in modern pure math as well. Those last two diagrams totally capture the idea of what a product or variant (coproduct, in math terminology) is. 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. http://en.wikipedia.org/wiki/Universal_property http://en.wikipedia.org/wiki/Universal_property

_pmf_ 12y ago

If they say "cross product", don't they actually mean "cartesian product"?

throwaway283719 12y ago
To mathematicians, the two are kind of interchangeable. I suppose "cartesian product" is a bit more specific, as "cross product" is also used to mean the vector cross product, which is different.
jlouis 12y ago
Beware here! There are a couple of different products you can sensibly form on data. So you have to make it very explicit which you mean when you talk about them. You can't generally interchange them in all contexts, but in some contexts you definitely can. 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)
- mmarx 12y ago
  Any two of those many products, however, are isomorphic, and hence, while still distinguishable, they are “essentially” the same.
  - tel 12y ago
    If I'm reading the op right, this is incorrect. Oftentimes "products" in various contexts are "categorical products cut down by some sensible quotienting". In any category the categorical product will always be the largest (this is essentially what its definition entails) and only by careful choice of category will that correspond to some of the less formal "products" available.

kawa 12y ago

BTW: Union types ("tagged unions") predate OOP by some years and thus were there long before OCaml or Haskell. Algol68 had them and also Pascal for example. The invention of ML was pattern matching on those data structures.

viraptor 12y ago
Pascal's "tagged unions" don't offer anything more than C's though. It's still unsafe and always requires as much memory as the combination of largest cases. OCaml / Haskell / others don't allow type changes at least. That would be useful even without the pattern matching.
ericssmith 12y ago
FWIW, Peter Landin sowed the seeds in "Mechanical Evaluation of Expressions" in 1964 in his description of recursive discriminated union for lists: 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".

mathgenius 12y ago

I can never get enough of the arrow theory. 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) ?

tel 12y ago
"Arrow theory" here is better known as Category Theory. I highly, highly recommend learning more about it if you're interested. I cannot understate its beauty. As a starter guide, I highly recommend reading Lawvere's Conceptual Mathematics.
noelwelsh 12y ago
In a language like Python you can consider there to be one type called, say, ThePythonType, or which all types are a variant. Then all objects have type ThePythonType. 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.
- seanmcdirmid 12y ago
  > In a language like Python you can consider there to be one type called, say, ThePythonType, or which all types are a variant. Then all objects have type ThePythonType. 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.
  - jlouis 12y ago
    A good way of getting at this is to call things at runtime "classes" or "tags" to make it apparent that their discrimination happens at runtime, not compile-time. The problem is that if you call both things types, you quickly run into a situation where you are essentially talking about different concepts entirely. Note that most sum-types are implemented by having a runtime tag on which you can discriminate.

frou_dh 12y ago

Sum types with compiler-enforced exhaustive pattern matching feel like a massive win and are the main thing I'd love to import in to traditional procedural programming. Switch statements and their ad hoc nature pale in comparison.