I'm trying to fully understand all of Haskell's concepts.
In what ways are algebraic data types similar to generic types, e.g., in C# and Java? And how are they different? What's so algebraic about them anyway?
I'm familiar with universal algebra and its rings and fields, but I only have a vague idea of how Haskell's types work.
This is a type where we specify the shape of each of the elements. Wikipedia has a thorough discussion. "Algebraic" refers to the property that an Algebraic Data Type is created by "algebraic" operations. The "algebra" here is "sums" and "products": "sum" is alternation ( A | B , meaning A or B but not both)
In programming languages, it carries a similar meaning. An algebraic data type is a composite containing variables. a composite can further contain other types as variables as well. A recursive type can contain another instance of itself as a variable.
Rust's enums are most similar to algebraic data types in functional languages, such as F#, OCaml, and Haskell.
Haskell has three basic ways to declare a new type: The data declaration, which defines new data types. The type declaration for type synonyms, that is, alternative names for existing types. The newtype declaration, which defines new data types equivalent to existing ones.
Haskell's algebraic data types are named such since they correspond to an initial algebra in category theory, giving us some laws, some operations and some symbols to manipulate. We may even use algebraic notation for describing regular data structures, where:
+
represents sum types (disjoint unions, e.g. Either
).•
represents product types (e.g. structs or tuples)X
for the singleton type (e.g. data X a = X a
)1
for the unit type ()
μ
for the least fixed point (e.g. recursive types), usually implicit.with some additional notation:
X²
for X•X
In fact, you might say (following Brent Yorgey) that a Haskell data type is regular if it can be expressed in terms of 1
, X
, +
, •
, and a least fixed point.
With this notation, we can concisely describe many regular data structures:
Units: data () = ()
1
Options: data Maybe a = Nothing | Just a
1 + X
Lists: data [a] = [] | a : [a]
L = 1+X•L
Binary trees: data BTree a = Empty | Node a (BTree a) (BTree a)
B = 1 + X•B²
Other operations hold (taken from Brent Yorgey's paper, listed in the references):
Expansion: unfolding the fix point can be helpful for thinking about lists. L = 1 + X + X² + X³ + ...
(that is, lists are either empty, or they have one element, or two elements, or three, or ...)
Composition, ◦
, given types F
and G
, the composition F ◦ G
is a type which builds “F-structures made out of G-structures” (e.g. R = X • (L ◦ R)
,where L
is lists, is a rose tree.
Differentiation, the derivative of a data type D (given as D') is the type of D-structures with a single “hole”, that is, a distinguished location not containing any data. That amazingly satisfy the same rules as for differentiation in calculus:
1′ = 0
X′ = 1
(F + G)′ = F' + G′
(F • G)′ = F • G′ + F′ • G
(F ◦ G)′ = (F′ ◦ G) • G′
References:
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With