CODEWITHSUNDEEP
scalahaskellfunctional-programming
Mandroid
Mandroid

Reputation: 7494

What is algebraic about ADT in functional programming?

In a Scala book I read this:

For example, this code is an ADT:

sealed trait Bool 
case object True extends Bool 
case object False extends Bool

....and further it says:

The “algebra” in ADTs is described on the Haskell wiki like this:

“Algebraic” refers to the property that an Algebraic Data Type is created by “algebraic” operations. The “algebra” here is “sums” and “products” (of types).

But where are those 'algebraic' operations in code snippet above?

Upvotes: 3

Views: 266

Answers (3)

Mario Galic
Mario Galic

Reputation: 48420

But where are those 'algebraic' operations in code snippet above?

They are implicit in the syntax of the language. The conceptual operation of "addition"

A + B

can be encoded in Scala as

sealed trait T 
case object A extends T 
case object B extends T

whilst conceptual operation of multiplication

A x B

can be encoded in Scala as

case class T(a: A, b: B)

What is algebraic about ADT

The term "algebra" has roots in mathematical field called abstract algebra. It is an endeavour which looks into different objects and different operations on those objects and hopes to find common behaviours between them. Roughly it is the process of taking away things and seeing what remains. Like when you learn to count and do arithmetic with apples as a child. At some point you "take away" the apples, and what remains are "numbers" which behave the same way as apples. The advantage of that is that now the same rules and laws you learned with arithmetic of apples, generalise to arithmetic of oranges and beyond. But mathematicians go even further and ask crazy question like what happens if we take away even the numbers themselves? Another way of looking at it is you write down some equation like

a + b = b + a       (commutativity law)

where addition + is defined in some abstract sense, and now try to find any kind of object that satisfy it. For example, integers satisfy it, as well as real numbers, etc., but turns out also certain kind of data types like sum types fit into that equation. So then mathematicians declare all the classes of objects, collectively, which work with addition operation in some sense, such that the result of the operation is commutative, as an algebraic structure, and give it some grand name like Abelian group etc. This is roughly the etymology of "algebraic" in "algebraic data type".

Upvotes: 6

leftaroundabout
leftaroundabout

Reputation: 120711

In Haskell you can write an ADT also with the generalized ADT syntax:

{-# LANGUAGE GADTs #-}

data Bool where
  False :: Bool
  True :: Bool

...which looks more like the Scala version, than the equivalent standard-Haskell notation does:

data Bool = False | True

As for how this is algebraic: Bool is an example of a sum type. The most general one of these is

{-# LANGUAGE TypeOperators, GADTs #-}

data (+) a b where
  Left :: a -> (a+b)
  Right :: b -> (a+b)

the standard version of which is

data Either a b = Left a | Right b

The generic product type would be

data (*) a b where
  Both :: a -> b -> (a*b)

which is isomorphic to (a,b).

Now you could define some finite types:

data One = One
type Two = One + One
type Three = One + Two
type Four = Two * Two

etc. etc.. As an exercise, prove that each of these has exactly as many different legal values as the name suggests.

Upvotes: 2

chepner
chepner

Reputation: 531185

The boolean type can be views as the sum of the unit type and the unit type. Apologies for writing the following in Haskell rather than Scala:

type MyBool = Either () ()

Since () has only a single value, the type Either () () has only two values, based on whether we use Left or Right on () to construct a value.

The proof that Bool and Either () () are isomorphic follows:

We can define two functions for converting Bool to an Either () () or vice versa.

b2e :: Bool -> Either () ()
b2e True = Right ()
b2e False = Left ()

e2b :: Either () () -> Bool
e2b (Right ()) = True
e2b (Left ()) = False

And we can trivially show that b2e and e2b are isomorphisms.

e2b (b2e True) == e2b (Right ()) == True
e2b (b2e False) == e2b (Left ()) == False
b2e (e2b (Right ())) == b2e True == Right ()
b2e (e2b (Left ())) == b2e False == Left ()

Thus e2b . b2e == b2e . e2b == id.

Upvotes: 3

Related Questions