Types
Originally posted on dev.to/gillchristian.
There are many ways of trying to understand programs. People often rely too much on one way, which is called “debugging” and consists of running a partly-understood program to see if it does what you expected. Another way, which ML advocates, is to install some means of understanding in the very programs themselves.
Robin Milner
I've interrupted the 100DaysOfFP far too long already, partly because I was busy and partly because I was lazy. I'll try to be more constant from now on.
This week on the Delft Haskell Study Group we went over the 4th and 5th chapter of Haskell Programming from First Principles, "Basic datatypes" and "Types", respectively.
As the last one, this is just my notes and some quotes from the book as a recap of the chapter.
Basic datatypes
Haskell has a robust and expressive type system. Types play an important role in the readability, safety, and maintainability of Haskell code as they allow us to classify and delimit data, thus restricting the forms of data our programs can process. Types, also called datatypes, provide the means to build programs more quickly and also allow for greater ease of maintenance.
Sum (or union) types (disjunction):
data Bool = False | True
Product types (conjunction):
data (,) a b = (,) a b
data (,,) a b c = (,) a b c
-- ...
Lists:
data [] a = [] | a : [a]
Numeric types:
IntIntegerFloatDoubleRationalScientific
λ> :i Num
class Num a where
(+) :: a -> a -> a
(-) :: a -> a -> a
(*) :: a -> a -> a
negate :: a -> a
abs :: a -> a
signum :: a -> a
fromInteger :: Integer -> a
λ> :i Fractional
class Num a => Fractional a where
(/) :: a -> a -> a
recip :: a -> a
fromRational :: Rational -> a
Data constructors in Haskell provide a means of creating values that inhabit a given type. Data constructors in Haskell have a type and can either be constant values (nullary) or take one or more arguments, like functions.
Type constructors in Haskell are not values and can only be used in type signatures. Just as data declarations generate data constructors to create values that inhabit that type, data declarations generate type constructors which can be used to denote that type.
Types
Haskell is based on System F and Hindley-Milner type systems, with some improvements on top.
What are types for?
Type systems in logic and mathematics have been designed to impose constraints that enforce correctness.
A type system defines the associations between different parts of a program and checks that all the parts fit together in a logically consistent, provably correct way.
Type signatures
'f' :: Char
"foo" :: String -- or [Char]
True :: Bool
not :: Bool -> Bool -- function from Bool to Bool
fst :: (a, b) -> a -- get a tuple's first value
(+) :: Num a => a -> a -> a -- type class constraint
The arrow (->) is the type constructor.
λ> :i (->)
data (->) (a :: TYPE q) (b :: TYPE r) -- Defined in ‘GHC.Prim’
infixr 0 ->
Associates to the right (thus infixr).
f :: a -> a -> a
-- is the same as
f :: a -> (a -> a)
-- and
map :: (a -> b) -> [a] -> [b]
-- is the same as
map :: (a -> b) -> ([a] -> [b])
The function constructor simplified could be data (->) a b.
One thing to noticed from that is, functions take only one argument and return one result. Enter currying.
Currying refers to the nesting of multiple functions, each accepting one argument and returning one result, to allow the illusion of multiple-parameter functions.
The benefit of currying is partial application.
λ> add a b = a + b
λ> addOne = add 1
λ> add 1 2
3
λ> addOne 2
3
λ> 1 + 2
3
λ> add = (+)
λ> add 1 2
3
λ> (+1) 2
3
λ> addOne = (+1)
λ> addOne 2
3
Polymorphism
To me the way Haskell implements polymorphism is one of its key features. I won't go into much detail, just add the book's definitions, since it could be very long otherwise.
Polymorph, invented in the early 19th century from the Greek words poly for “many” and morph for “form”. The -ic suffix in polymorphic means “made of.”
In Haskell, polymorphism divides into two categories: parametric polymorphism and constrained polymorphism.
Parametricity is the property that holds in the presence of parametric polymorphism. Parametricity states that the behavior of a function will be uniform across all concrete applications of the function. Parametricity 4 tells us that the function:
id :: a -> a
Can be understood to have the same exact behavior for every type in Haskell without us needing to see how it was written. It is the same property that tells us:
const :: a -> b -> a
const must return the first value — parametricity and the definition of the type requires it!
f :: a -> a -> a
Here, f can only return the first or second value, nothing else, and it will always return one or the other consistently without changing. If the function f made use of (+) or (*), its type would necessarily be constrained by the type class Num and thus be an example of ad-hoc, rather than parametric, polymorphism.
Ad-hoc polymorphism (sometimes called “constrained polymorphism”) is polymorphism that applies one or more type class constraints to what would’ve otherwise been a parametrically uniformity of behavior across all concrete applications, the purpose of ad-hoc polymorphism is to allow the functions to have different behavior for each instance. This ad-hoc-ness is constrained by the types in the type class that defines the methods and Haskell’s requirement that type class instances be unique for a given type. For any given combination of type class and a type, such as Ord and Bool, there must only exist one unique instance in scope. This makes it considerably easier to reason about type classes.
-- ad-hoc polymorphism via the Num type class
(+) :: Num a => a -> a -> a
-- parametric polymorphism a
c :: a -> a -> a
This is when the book starts to get interesting. But that's it for now 😄
Disclaimer, most of the content of this blogpost is quoted from Haskell Programming from First Principles. I don't meant to plagiarize the book, these are only notes as a recap of chapters 4 and 5.