Algebraic Data Types (ADT) are a powerful way of defining new types in Haskell by combining existing types through sum and product constructions. These allow for highly expressive data representations, which are essential for modeling various kinds of structures in programming.
In Haskell, you can define ADTs using the data
keyword. ADTs are typically inductive types, meaning that they can be constructed from smaller instances or components.
Sum Types:
A sum type allows us to define a type that can be one of several possible types (like an OR
in logic).
In Haskell, sum types are defined by having multiple constructors, each representing a possible type.
Example:
data Bool = False | True
Here, the Bool
type is a sum type, and the constructors False
and True
are the two values it can take.
Product Types:
A product type combines multiple types together (like an AND
in logic), typically corresponding to tuples in Haskell.
Example:
data Point = MakePoint Float Float
The Point
type is a product type because it combines two Float
values into one Point
.
These types can be combined to define more complex types. For example, the Maybe
type is a sum type because it can be either Nothing
(no value) or Just a
(a value of type a
).
To define an ADT, Haskell uses the data
keyword:
data TypeName = Constructor1 Type1 | Constructor2 Type2 | ... | ConstructorN TypeN
TypeName
: The name of the new type.
Constructor1, Constructor2, ..., ConstructorN
: The constructors that create new values for this type.
Type1, Type2, ..., TypeN
: The types associated with each constructor.
Example of a Sum Type:
data Bool = False | True
The Bool
type is a sum type with two constructors: False
and True
.
Example of a Product Type:
data Point = MakePoint Float Float
Point
is a product type, as it combines two Float
values into one Point
value. This is structurally similar to a tuple (Float, Float)
.
Pattern matching is a key feature in Haskell when working with ADTs. It allows you to extract and work with the components of a value by matching it against different constructors.
For example, let's define the Bool
type:
data Bool = False | True
You can pattern-match on Bool
values:
isTrue :: Bool -> Bool
isTrue True = True
isTrue False = False
In this example:
The function isTrue
matches against the True
and False
constructors.
The value passed to isTrue
is checked to see if it matches True
or False
, and the corresponding result is returned.
One of the most powerful aspects of ADTs is their ability to define recursive types. This is when a type is defined in terms of itself.
Example: List Type
data List a = Empty | Cons a (List a)
Here:
The List
type is recursive because it refers to itself in the second constructor Cons a (List a)
.
Empty
represents the empty list.
Cons
represents a non-empty list, where the first element is of type a
and the rest of the list is of type List a
.
With recursion, we can define operations on lists, like finding the length or checking if an element exists:
length :: List a -> Int
length Empty = 0
length (Cons _ xs) = 1 + length xs
member :: Eq a => a -> List a -> Bool
member _ Empty = False
member x (Cons y ys) = x == y || member x ys
ADTs are often called inductive types because the type can be defined in terms of itself in a way that allows us to perform recursive computations. The recursion typically starts with a base case (like Empty
for a list), and other cases are built from smaller instances.
For example:
data List a = Empty | Cons a (List a)
This type can be thought of as an inductive definition:
Base case: The empty list Empty
has no elements.
Inductive case: A list of elements is constructed by the Cons
constructor, which adds a new element to an existing list.
Maybe
TypeA classic example of a sum type in Haskell is the Maybe
type. It’s used to represent a value that might be absent.
data Maybe a = Nothing | Just a
Nothing
represents the absence of a value.
Just a
represents a value of type a
.
You can use pattern matching to handle these cases:
safeDivide :: Int -> Int -> Maybe Int
safeDivide _ 0 = Nothing
safeDivide x y = Just (x `div` y)
Here, safeDivide
returns Nothing
when dividing by zero and Just result
otherwise.
When programming in Haskell, ADTs help you model complex data structures in a clean and expressive way. ADTs provide a way to ensure that all possible cases are covered by the use of constructors, and they allow you to leverage recursion effectively.
Example: Binary Tree
data Tree a = EmptyTree | Node a (Tree a) (Tree a)
The Tree
type is defined recursively.
EmptyTree
represents an empty tree.
Node
represents a node with a value of type a
and two subtrees (left and right).
You can define recursive functions over trees, such as calculating the size of a tree or finding a value:
size :: Tree a -> Int
size EmptyTree = 0
size (Node _ left right) = 1 + size left + size right
search :: Eq a => a -> Tree a -> Bool
search _ EmptyTree = False
search x (Node y left right)
| x == y = True
| otherwise = search x left || search x right
Haskell’s strong, static type system makes it possible to catch many errors at compile time. By using ADTs, you can ensure that the data you're working with fits a certain structure, and you can use pattern matching to guarantee all possible cases are handled.
In Haskell, the type system can help ensure that your data is well-formed and your functions operate on valid inputs. For example, if you attempt to pass a non-list value to a function that expects a list, Haskell will give a compile-time error.
Expressiveness: ADTs allow you to define complex data structures and operations on them with high-level abstractions.
Type Safety: Using ADTs ensures that only valid data structures are used, reducing errors.
Pattern Matching: ADTs integrate well with pattern matching, enabling clean and readable code.
Definition of Sum and Product Types: Know the difference between sum types (multiple options) and product types (combinations of values).
Recursive Data Types: Understand how recursive data types like lists and trees work.
Pattern Matching: Be comfortable writing functions using pattern matching on ADTs.
Inductive Types and Proof by Induction: ADTs are inductive types, so knowing how to prove properties using induction will be useful.
Common Examples of ADTs: Maybe
, Either
, List
, and Tree
are frequently tested in exercises.
Function Definitions on ADTs: Practice writing functions that work with ADTs, including handling all constructors in pattern matching.
Definition:
Enumeration Types (or Enum Types) are algebraic data types that define a finite set of distinct values. These values are typically represented by constructors that don’t take any arguments.
They are a subset of algebraic data types, where the type is defined by a collection of possible values.
Syntax (Haskell):
data TypeName = Constructor1 | Constructor2 | ... | ConstructorN
In this case, TypeName
is the name of the new type, and Constructor1
, Constructor2
, ..., ConstructorN
are the possible values or cases that this type can take.
Example: Bool
type
The Boolean type is an example of an enumeration type that has two possible values: True
and False
.
import Prelude hiding (Bool, False, True)
data Bool = False | True deriving (Show)
implies :: Bool -> Bool -> Bool
True implies False = False
_ implies _ = True
Explanation:
The type Bool
is defined with two constructors False
and True
. These constructors do not take any arguments.
The implies
function is a Boolean operator defined using pattern matching, where:
If the first argument is True
and the second is False
, the result is False
.
For any other combination of arguments, the result is True
.
Example: WeekDay
type
Let’s define an enumeration for the days of the week:
data WeekDay = Sunday | Monday | Tuesday | Wednesday | Thursday | Friday | Saturday deriving (Show)
meaning :: WeekDay -> String
meaning Sunday = "sun's day"
meaning Monday = "moon's day"
meaning Tuesday = "Tiw's day"
meaning Wednesday = "Woden's day"
meaning Thursday = "Thor's day"
meaning Friday = "Frige's day"
meaning Saturday = "Saturn's day"
Explanation:
WeekDay
is an enumeration type with constructors for each day of the week.
The function meaning
takes a WeekDay
and returns a string representing the historical meaning of the day (e.g., "sun's day" for Sunday).
Conceptual Questions on Enumeration Types:
What kind of algebraic type is the following?
data Date = Year Integer | Month Integer | Day Integer deriving (Show)
Answer:
This is a Sum Type, not an Enumeration type.
An Enumeration type has constructors that take no arguments, but in the Date
type, each constructor (Year
, Month
, Day
) takes an Integer
as an argument. Therefore, this is a Sum Type, which means it can take values of one of several forms, each with different data.
Definition:
Recursive Types are algebraic data types in which the type definition refers to itself. These types allow for the construction of complex data structures by nesting smaller instances of the same type.
Examples of Recursive Types:
Natural Numbers (Nat)
data Nat = Zero | Suc Nat deriving (Show)
Nat
is a recursive type representing natural numbers. The two constructors are:
Zero
: represents the number 0.
Suc Nat
: represents the successor of a natural number, i.e., Suc Zero
is 1, Suc (Suc Zero)
is 2, and so on.
Important property of recursive types: The set of values in a recursive type is countably infinite. This means that we can list all possible values (0, 1, 2, 3, …), but the list will never end.
Lists of Integers
data ListInteger = Nil | Cons Integer ListInteger deriving (Show)
ListInteger
is a recursive type for lists of integers.
The two constructors are:
Nil
: represents an empty list.
Cons Integer ListInteger
: represents a list where an integer is added to the front of an existing list.
Binary Tree (BinTree)
data BinTreeFloat = Leaf Float | Branch BinTreeFloat Float BinTreeFloat deriving (Show)
BinTreeFloat
is a recursive type representing binary trees with float values stored at the nodes.
The two constructors are:
Leaf Float
: represents a leaf node with a float value.
Branch BinTreeFloat Float BinTreeFloat
: represents a branch node with a left and right subtree and a float value.
Important Questions on Recursive Types:
The set of values in a recursive type is:
Answer: B. Sometimes finite and sometimes infinite.
Recursive types can represent both finite and infinite sets. For example, a recursive type like Nat
represents an infinite set (natural numbers), while a finite recursive type like a tree with a limited depth can represent a finite set of values.
To understand how recursive types work, let’s define functions that operate on these types using pattern matching.
Example: Nat
functions (Addition and Multiplication)
natPlus :: Nat -> Nat -> Nat
natPlus Zero y = y
natPlus (Suc x) y = Suc (natPlus x y)
natTimes :: Nat -> Nat -> Nat
natTimes Zero y = Zero
natTimes (Suc x) y = natPlus y (natTimes x y)
natPlus
: Adds two natural numbers.
If the first number is Zero
, return the second number.
If the first number is Suc x
, recursively add x
and y
, and then apply Suc
to the result.
natTimes
: Multiplies two natural numbers.
If the first number is Zero
, return Zero
(because anything times 0 is 0).
If the first number is Suc x
, recursively multiply x
and y
, then add y
to the result.
Example: Fibonacci Numbers
To calculate Fibonacci numbers, we need to define a recursive function:
natFib :: Nat -> Nat
natFib Zero = Zero
natFib (Suc Zero) = Suc Zero
natFib (Suc (Suc x)) = natFib x `natPlus` natFib (Suc x)
Explanation:
The base cases are:
natFib Zero = Zero
(the Fibonacci of 0 is 0).
natFib (Suc Zero) = Suc Zero
(the Fibonacci of 1 is 1).
The recursive case computes Fibonacci for all other numbers by summing the previous two Fibonacci numbers.
Definition:
Structural Induction is a proof technique used to prove properties of recursive data types. For the type Nat
, the principle of induction is:
Base case: Prove the property holds for the simplest value (Zero
).
Inductive step: Assume the property holds for an arbitrary value, and prove it holds for the successor of that value (Suc x
).
Example: Proving 0 + x = x
for all natural numbers x
.
Base case: Prove P 0: 0 + 0 = 0
holds (which it does by the definition of addition).
Inductive step: Assume P x
holds (i.e., 0 + x = x
), and prove P (Suc x)
holds (i.e., 0 + Suc x = Suc x
).
Algebraic Data Types (ADT) are used to define complex types in programming, especially in functional programming languages like Haskell.
They are composed of a set of constructors that can create values of the type. These constructors can be parametrized and recursive.
Product Types (e.g., Tuples)
A product type combines multiple values into one. A tuple is a classic example.
Example: A 2-tuple in Haskell could be written as:
data Pair a b = Pair a b
Sum Types (e.g., Disjoint Unions)
A sum type allows a value to be one of several different types. It is like having multiple alternatives.
In Haskell, sum types are typically defined with the |
(OR) symbol.
Example: A basic List type:
data List a = Nil | Cons a (List a)
These allow types to be defined with parameters, making them more flexible and reusable. A parameterized ADT can define a family of types rather than just one specific type.
Example: List of Any Type (a
is a parameter)
data List a = Nil | Cons a (List a)
List Type:
List a
can hold any type a
. The constructors for this list are:
Nil
(the empty list)
Cons a (List a)
(a value a
and a recursively defined List a
).
Pattern Matching for List:
head2 :: List a -> Maybe a
head2 Nil = Nothing
head2 (Cons x y) = Just x
The Maybe
type is used here to represent the possibility that a list might be empty (i.e., no head).
Maybe Type:
The Maybe
type represents an optional value. It can either be Just a
(a valid value) or Nothing
(no value).
It is typically used to handle errors or partial functions (where a result might not exist).
data Maybe a = Just a | Nothing
BinTree Type (Binary Tree):
A Binary Tree is a recursive structure with two possible forms:
Leaf a
(a leaf node with a value of type a
)
Branch (BinTree a) a (BinTree a)
(a branch node with a left and right subtree, and a value of type a
).
Examples:
data BinTree a = Leaf a | Branch (BinTree a) a (BinTree a)
Recursive data types are types that are defined in terms of themselves. A List is a classic example of recursion in Haskell.
Function to compute the number of nodes in a binary tree:
binTreeNodes :: BinTree a -> Integer
binTreeNodes (Leaf _) = 1
binTreeNodes (Branch s _ t) = (binTreeNodes s) + 1 + (binTreeNodes t)
This function recursively counts nodes by adding the left and right subtree nodes and the current node.
Function to compute the sum of values in a binary tree:
binTreeSum :: Num a => BinTree a -> a
binTreeSum (Leaf x) = x
binTreeSum (Branch s x t) = (binTreeSum s) + x + (binTreeSum t)
The function recursively adds values from the left subtree, current node, and right subtree.
Problem: Compute the height of a binary tree.
binTreeHeight :: BinTree a -> Integer
binTreeHeight (Leaf _) = A
binTreeHeight (Branch s _ t) = B + C (binTreeHeight s) (binTreeHeight t)
Options for A, B, and C:
A is the height of a leaf node, which is usually 1
(since it can be considered a height of 1 from the root).
B is typically 2
, which accounts for the current branch.
C is max
, since we need the maximum of the two heights between the left and right subtrees to find the total height.
Correct Answer: D - 1, 2, max. This gives the correct height of a binary tree by considering the root node plus the maximum of the left and right subtrees.
When you define an ADT, you're defining a language of expressions.
Expressions of the language are created using the constructors of the ADT.
Recursive types lead to infinite languages (infinite sets of possible values) because you can keep applying constructors recursively.
newtype
is used to define a new type that wraps an existing type. It's used for type safety or domain-specific purposes, such as distinguishing between types that would otherwise be the same.
Syntax:
newtype NewType = Constructor OldType
Key Characteristics:
Compile-Time Distinction: newtype
is treated as a distinct type during type-checking (compile-time).
Runtime Efficiency: Once the program is compiled, the newtype
is treated as the original type, which ensures no runtime overhead.
Examples:
Natural Numbers:
newtype Natural = Natural Integer
This ensures that you treat the type as a natural number, excluding negative numbers during type-checking.
Vector3:
newtype Vector3 a = MakeVector3 (a, a, a)
Here, Vector3 a
is a 3-dimensional vector, and it ensures the structure of the vector is validated at compile time.
Function Types:
newtype Function a b = Function (a -> b)
Algebraic Data Types (ADT) allow for concise and expressive definitions of complex data structures.
Parameterized Types make ADTs general and reusable for different types.
Recursive Types allow for the creation of infinite data structures.
Pattern Matching is a powerful tool for defining and manipulating data types.
newtype
provides a way to create distinct types from existing ones, adding clarity and type safety without affecting runtime performance.