Chapter 5: Types

The Idea of Order at Key West.

Here are some quotes about types from various external resources that I find interesting.

A type may be viewed as a set of clothes (or a suit of armor) that protects an underlying untyped representation from arbitrary or unintended use. It provides a protective covering that hides the underlying representation and constrains the way objects may interact with other objects.

—Luca Cardelli

The great idea of constructive type theory is that there is no distinction between programs and proofs. Theorems are types (specifications), and proofs are programs.

—Robert Harper

So the main idea behind modern verfication – be it with static analysis, model checkers or type systems – is reduction of the state space (and heuristic approaches – like SAT solvers – that allow us to tackle larger state spaces).

—Ron Pressler https://pron.github.io

Make illegal states unrepresentable!

—Yaron Minsky https://blog.janestreet.com/effective-ml-revisited/

5.1 Types

A deep understanding of types and how to read an interpret them is fundamental to reading and writing Haskell.

In this chapter, we’re going to take a deeper look at the type system and

  • learn more about querying and reading type signatures;

  • explore currying;

  • take a closer look at different kinds of polymorphism;

  • look at type inference and how to declare types for our functions.

5.2 What are types for?

“Type systems in logic and mathematics have been designed to impose constraints that enforce correctness.”

“For our purposes, we can say that well-designed type systems help eliminate some classes or errors as well as concerns such as what the effect of a conditional over a non-Boolean value might be.”

These two sentences from the book seemed a bit out of place. Turns out they’re paraphrased from an awesome paper. Here is some more of it, to elaborate on the idea.

So types let us think at a higher level of abstraction, and prevent execution errors.

Execution errors include things such as, unintended memory access, or operations that don’t make semantic sense, like adding numbers to strings.

In Haskell, type-checking occurs at compile time.

No type system can eliminate all possibility for error, so runtime errors and exceptions still exist, and testing of program is necessary.

Some possible errors that well-typed programs can exhibit are listed here.

Good type systems can also enable compiler optimizations because the compiler can know and predict certain things about the execution of a program based on the types.

Furthermore, types can serve as documentation of your program.

Working with a good type system can eliminate those tests that only check that you’re passing the right sort of data around.

5.3 How to read type signatures

The compiler doesn’t know which specific numeric types a value is until the type is either declared or the compiler is forced to infer a specific type based on the function.

Instead, it gives the numeric literal type type with the broadest applicability (most polymorphic) and says it’s a constrained polymorphic :: Num a => a value.

5.3.1 Understanding the function type

The arrow, (->), is the type constructor for functions in Haskell.

The (->) type constructor takes two arguments and has no data constructors.

The arrow in an infix operator that has two parameters and associated to the right.

·∾ :info (->)
data (->) (a :: TYPE q) (b :: TYPE r)      -- Defined in ‘GHC.Prim’
infixr -1 ->

instance  Applicative ((->) a)              -- Defined in ‘GHC.Base’
instance  Functor ((->) r)                  -- Defined in ‘GHC.Base’
instance  Monad ((->) r)                    -- Defined in ‘GHC.Base’
instance  Monoid b => Monoid (a -> b)       -- Defined in ‘GHC.Base’
instance  Semigroup b => Semigroup (a -> b) -- Defined in ‘GHC.Base’

The parameterization suggests that we will apply the function so some argument that will be bound to the first parameter, with the second parameter representing the return or result type.

In the expression fst :: (a, b) -> a we can know for certain that the result a is the same a in (a, b).

How do we know it’s the same a? We can see that the type variable have the same type, and that nothing happens in between the input and output to transform the parameters value.

5.3.2 Type class constrained type variables

Num a => a -> a reads “for the polymorphic type a which has an instance of the Num type class, a returning a” or more simply “Num constrained a to a”. This is known as a type class constraint, or constraint.

In this signature, a is still polymorphic, but constrained to types the implement the type class Num.

Type classes offer a standard set of functions that can be used across several concrete types.

A type signature might have multiple type class constraints on one or more of the variables.

Here’s and example of what constrained type signatures can look like:

-- multiple expressions can be annotated with a type at the same time
(+), (-) :: Num a => a -> a -> a

-- a and b have are constrained to types that implement Num
:: (Num a, Num b) => a -> b -> b

-- a is constrained to types that implement both Num and Ord
:: (Ord a, Num a) => a -> a -> Ordering

-- ...another way to write it...
:: Ord a => Num a => a -> a -> Ordering

The syntax used to denote multiple required type classes that resembles a tuple in the type class constraint (everything between the :: and =>) does not show up on the term level. It does, however show up in the kind signature. For example :kind Eq will return Eq :: * -> Constraint.

5.3.3 Exercises: Type Matching

Page 125.

First, here is a terminal recording where I answer all the questions.

1, 2. Match the functions to their type signatures:

  1. not –> c. _ :: Bool -> Bool:

    ·∾  :type not
not :: Bool -> Bool

  2. length –> d. _ :: [a] -> Int:

    ·∾  :type length
length :: Foldable t => t a -> Int

  3. concat –> b. _ :: [[a]] -> [a]:

    ·∾  concat [[1..10],[11..20]]
[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]

·∾  :type concat
concat :: Foldable t => t [a] -> [a]

  4. head –> a. _ :: [a] -> a:

    ·∾ :type head
head :: [a] -> a

  5. (<) –> e. _ :: Ord a => a -> a -> Bool:

    ·∾ :type (<)
(<) :: Ord a => a -> a -> Bool

5.4 Currying

First off, here’s a video.

All functions in Haskell take one argument, and return one result. Currying refers to the nesting of multiple functions, each accepting one argument and returning one result, to allow the illusion of multiple parameter functions.

Each arrow in a type signature represents one argument and one result, with the final type being the final result.

5.4.1 Partial application

The ability to apply only some of a functions arguments is called partial application.

5.4.2 Manual currying and uncurrying

  • Uncurried functions: One function, many arguments.

  • Curried functions: Many functions, one argument apiece.

You can convert the two with the curry and uncurry functions, or by using pattern matching, or breaking out parameters into multiple nested lambdas.

·∾ f x y = x+y
·∾ g (x,y) = x+y

·∾ :type uncurry f
uncurry f :: Num c => (c, c) -> c
·∾ :type g
g :: Num a => (a, a) -> a

·∾ :type curry g
curry g :: Num t => t -> t -> t
·∾ :type f
f :: Num a => a -> a -> a

·∾ g (1,2) == f 1 2
True

5.4.3 Sectioning

The term sectioning specifically refers to partial application of infix operators. It looks something like this:

·∾  twoSupN = (2^)
·∾  twoSupN 5
32

·∾  nSupTwo = (^2)
·∾  nSupTwo 5
25

5.4.5 Exercises: Type Arguments

First, the terminal recording. I don’t recommend you watch this one, it needs editing. I only leave it here as proof of work.

Given a function and its type, tell us what type results from applying some or all of the arguments.

  1. If the type of f is a -> a -> a -> a, and the type of x is Char then the type of f x is

    1. Char -> Char -> Char:

      ·∾ f :: a -> a -> a -> a; f = undefined
·∾ x :: Char; x = undefined

·∾ -- f x should have type Char -> Char -> Char, I think.
·∾ -- Char specializes the a's. x consumes one argument,
·∾ -- reducing the number of type variables by one.

·∾ :type f x
f x :: Char -> Char -> Char

    2. x -> x -> x -> x

    3. a -> a -> a

    4. a -> a -> a -> Char

  2. If the type of g is a -> b -> c -> b, then the type of g 0 'c' "woot" is

    1. String

    2. Char -> String

    3. Int

    4. Char:

      ·∾ g :: a -> b -> c -> b; g = undefined

·∾ -- g 0 'c' "woot"
·∾ -- a:: Num a => a , b :: Char; c :: String
·∾ -- ... since it returns b the type should be Char.

·∾ :type g 0 'c' "woot"
g 0 'c' "woot" :: Char

  3. If the type of h is (Num a, Num b) => a -> b -> b, then the type of h 1.0 2 is:

    1. Double

    2. Integer

    3. Integral b => b

    4. Num b => b:

      ·∾ h :: (Num a, Num b) => a -> b -> b; h = undefined

·∾ -- h 1.0 2
·∾ -- a :: Num a => a; b :: Num b => b
·∾ -- ... should be Num

·∾ :type h 1.0 2
h 1.0 2 :: Num b => b

  4. If the type of h is (Num a, Num b) => a -> b -> b, then the type of h 1 (5.5 :: Double) is

    1. Integer

    2. Fractional b => b

    3. Double:

      ·∾ h :: (Num a, Num b) => a -> b -> b; h = undefined

·∾ -- h 1 (5.5 :: Double)
·∾ -- a :: Num a => a; b :: Double
·∾ -- ... since it returns b, it should be Double

·∾ :type h 1 (5.5 :: Double)
h 1 (5.5 :: Double) :: Double

    4. Num b => b``

  5. If the type of jackal is (Ord a, Eq b) => a -> b -> a, then the type of jackal "keyboard" "has the word jackal in it"

    1. [Char]:

      ·∾ jackal :: (Ord a, Eq b) => a -> b -> a; jackal = undefined

·∾ -- jackal "keyboard" "has the word jackal in it"
·∾ -- a :: String; b :: String
·∾ -- ... should be String

·∾ :type jackal "keyboard" "has the word jackal in it"
jackal "keyboard" "has the word jackal in it" :: [Char]

·∾ -- String is an alias for [Char], so this makes sense.

    2. Eq b => b

    3. b -> [Char]

    4. b

    5. Eq b => b -> [Char]

  6. If the type of jackal is (Ord a, Eq b) => a -> b -> a, then the type of jackal "keyboard"

    1. b

    2. Eq b => b

    3. [Char]

    4. b -> [Char]:

      ·∾ jackal :: (Ord a, Eq b) => a -> b -> a; jackal = undefined

·∾ -- jackal "keyboard"
·∾ -- a :: String; b
·∾ -- ... since a is returned, it should be String
·∾ -- ... or jackal :: b -> String , rather

·∾ :type jackal "keyboard"
jackal "keyboard" :: Eq b => b -> [Char]

·∾ -- Right, I forgot about the Eq constraint.

    5. Eq b => b -> [Char]

  7. If the type of kessel is (Ord a, Num b) => a -> b -> a, then the type of kessel 1 2 is

    1. Integer

    2. Int

    3. a

    4. (Num a, Ord a) => a:

      ·∾ kessel :: (Ord a, Num b) => a -> b -> a; kessel = undefined
·∾ -- kessel 1 (2 :: Integer)
·∾ -- a :: Ord a => a ; b :: Integer
·∾ -- ... should be Ord a => a

·∾ :type kessel 1 (2 :: Integer)
kessel 1 (2 :: Integer) :: (Ord a, Num a) => a

·∾ -- Right, of course, since we pass a numeric
·∾ -- literal it adds the Num constraint.

    5. Ord a => a

    6. Num a => a

  8. If the type of kessel is (Ord a, Num b) => a -> b -> a, then the type of kessel 1 (2 :: Integer) is

    1. (Num a, Ord a) => a

    2. Int

    3. a

    4. Num a => a

    5. Ord a => a

    6. Integer:

      ·∾ kessel :: (Ord a, Num b) => a -> b -> a; kessel = undefined

·∾ -- kessel (1 :: Integer) 2
·∾ -- a :: Integer; b :: Num b => b
·∾ -- The return type should be Integer.

·∾ :type kessel (1 :: Integer) 2
kessel (1 :: Integer) 2 :: Integer

  9. If the type of kessel is (Ord a, Num b) => a -> b -> a, then the type of kessel (1 :: Integer) 2 is

    1. Num a => a

    2. Ord a => a

    3. Integer:

      ·∾ kessel :: (Ord a, Num b) => a -> b -> a; kessel = undefined

·∾ -- kessel (1 :: Integer) 2
·∾ -- a :: Integer; b :: Num b => b
·∾ -- ... should be Integer

·∾ :type kessel (1 :: Integer) 2
kessel (1 :: Integer) 2 :: Integer

    4. (Num a, Ord a) => a

    5. a

5.5 Polymorphism

Polymorphic

poly- “many”, morph “form”, -ic “made of”

“made of many forms”

Monomorphic

mono- “one”, morph “form”, -ic “made of”

“made of one form”

In Haskell, polymorphism divides into two categories: parametric polymorphism and constrained polymorphism.

Ad-hoc, or constrained, polymorphism in Haskell is implemented with type classes.

Parametric polymorphism refers to type variables, or parameters, that are fully polymorphic. When unconstrained by a type class, their final, concrete type could be anything.

Recall that when you see a lowercase name in a type signature, like a, it is a polymorphic type variable.

If a variable represents a set of possible values, then a type variable represents a set of possible types.

Parametricity means that the behavior of a function with respect to the types of its (parametrically polymorphic) arguments is uniform.

5.5.1 Exercises: Parametricity

  1. Given :: a -> a, attempt to make a function that does something other than return the same value. It also has to terminate. This is impossible, but try:

    ·∾ f :: a -> a; f = undefined

·∾ f x = 'c'
·∾ :type f
f :: p -> Char

·∾ f x = f x
·∾ :type f
f :: t1 -> t2
·∾ -- hey, that almost works, but doesn't terminate

  2. Write both possible implementations of a function with the type signature of a -> a -> a.:

    Prelude> :type \x -> \y -> y
\x -> \y -> y :: t1 -> t -> t

Prelude> :type \x -> \y -> x
\x -> \y -> x :: t1 -> t -> t1

  3. Implement a -> b -> b:

    Prelude> :type \a -> \b -> b
\a -> \b -> b :: t1 -> t -> t

5.5.2 Polymorphic constants

Numeric literals like (-10) and 6.3 are polymorphic and stay so until given a more specific type.

5.5.3 Working around constraints

fromIntegral takes an integral value and forces it to implement the Num type class, rendering it polymorphic.

This can be useful when working with functions that return a type which is too concrete for further use

·∾ 6 / length [1,2,3]

<interactive>:8:1: error:
    • No instance for (Fractional Int) arising from a use of ‘/’
    • In the expression: 6 / length [1, 2, 3]
      In an equation for ‘it’: it = 6 / length [1, 2, 3]

·∾ :type (/)
(/) :: Fractional a => a -> a -> a

·∾ :type length
length :: Foldable t => t a -> Int

·∾ -- length returns an Int, which is too concrete.

·∾ :type fromIntegral
fromIntegral :: (Integral a, Num b) => a -> b

·∾ 6 / fromIntegral (length [1,2,3])
2.0

5.6 Type inference

Type inference is a compiler feature that allows it to infer types without requiring the programmer to write them explicitly every time.

Haskells type inference is built on an extended version of the Damas-Hindly-Milner type system.

This particular system enables global type inference – where no type annotations are required at all.

In other languages, inference may be local to function bodies (local type inference, such as in Rust), or even only inferred when you explicitly request it with a keyword, like auto in C++ (weird, right?).

Haskell will infer the most generally applicable (polymorphic) type that is still correct.

Well, most of the time. The monomorphism restriction is a counter-intuitive rule in Haskells type inference implementation - If you forget to provide a type signature, sometimes this rule will fill the free type variables with specific types using “type defaulting” rules.

Thankfully, this is turned off by default since GHC 7.8.1. If not, you can use :set -XNoMonomorphismRestriction.

More on the Haskell Wiki, and in the Haskell 2010 Language Report.

Also, here is a wonderful video on type inference.

5.6.1 Exercises: Apply Yourself

Figure out how the type would change and why, make a note of what you think the new inferred type would be and then check your work in GHCi.

First, a terminal recording.

  1. -- Type signature of general function
(++) :: [a] -> [a] -> [a]

-- How might that change when we apply
-- it to the following value?
myConcat x = x ++ " yo"

    myConcat :: String -> String is my guess:

    ·∾ :type myConcat
myConcat :: [Char] -> [Char]

  2.   -- General function
  (*) :: Num a => a -> a -> a

  -- Applied to a value
  myMult x = (x / 3) * 5

My guess is ``myMult :: (Fractional a) => a -> a``.
Let's see::

  ·∾ :type myMult
  myMult :: Fractional a => a -> a

  3. take :: Int -> [a] -> [a]
myTake x = take x "hey you"

    Should be myTake :: Int -> String, probably:

    ·∾ :type myTake
myTake :: Int -> [Char]

  4. (>) :: Ord a => a -> a -> Bool
myCom x = x > (length [1..10])

    This must be Int -> Bool, since length returns an Int. Let’s see:

    ·∾ :type myCom
myCom :: Int -> Bool

  5. (<) :: Ord a => a -> a -> Bool
myAlph x = x < 'z'

    This one is straight-forward. Must be Char -> Bool:

    ·∾ :type myAlph
myAlph :: Char -> Bool

5.7 Asserting types for declarations

Adding type signatures to top level declarations in your code can provide guidance about a functions purpose. It’s generally a good idea to write them.

It’s been mentioned that the types can express intent by giving them more meaningful names. This is a good intuition, but some ways of naming types, such as type aliases (defined with the type keyword) and wrapper types (defined with newtype), can lead to issues with tooling.

One of these is that searching API documentation by type signature with Hoogle becomes a lot harder. Generally the tooling isn’t smart enough to resolve type aliases to their underlying types for searches, linting in editors, and other static analysis. This means you have to know the name of the type aliases by memory to search for them – you can’t just search for :: String -> String even though it’s semantically just an alias for :: Name -> EmailAddr.

So, just use your best judgement.

Lest you begin to think that type signatures are somehow exclusive to top-level bindings, here’s an example of assigning a type to a function within a where clause:

triple x = tripleItYo x
  where tripleItYo :: Integer -> Integer
        tripleItYo y = y * 3

5.8 Chapter Exercises

5.8.1 Multiple choice

  1. A value of type [a] is

    1. a list of alphabetic characters

    2. a list of lists

    3. a list whose elements are all of some type a

    4. a list whose elements are all of different types

  2. A function of type [[a]] -> [a] could

    1. take a list of strings as an argument

    2. transform a character into a string

    3. transform a string into a list of strings

    4. take two arguments

  3. A function of type [a] -> Int -> a

    1. takes one argument

    2. returns one element of type a from a list

    3. must return an Int value

    4. is completely fictional

  4. A function of type (a, b) -> a

    1. takes a list argument and returns a Char value

    2. has zero arguments

    3. takes a tuple argument and returns the first value

    4. requires that a and b be of different types

5.8.2 Determine the type

First, a terminal recording.

  1. All function applications return a value. Determine the value returned by these function applications and the type of that value.

    1. (* 9) 6

      ·∾ -- This should have type Num a => a, I think, since (*) comes from Num.
·∾ :type (*)
(*) :: Num a => a -> a -> a

    2. head [(0,"doge"),(1,"kitteh")]

      ·∾ -- Im guessing :: Num a => (a, String)
·∾ :type head [(0,"doge"),(1,"kitteh")]
head [(0,"doge"),(1,"kitteh")] :: Num a => (a, [Char])

    3. head [(0 :: Integer ,"doge"),(1,"kitteh")]

      ·∾ -- :: (Integer,String), I think.
·∾ :type head [(0 :: Integer,"doge"),(1,"kitteh")]
head [(0 :: Integer,"doge"),(1,"kitteh")] :: (Integer, [Char])

    4. if False then True else False

      ·∾ -- this is a Bool
·∾ :type if False then True else False
if False then True else False :: Bool

    5. length [1, 2, 3, 4, 5]

      ·∾ -- length returns Int, so this will be :: Int
·∾ :type length [1,2,3,4,5]
length [1,2,3,4,5] :: Int

    6. (length [1, 2, 3, 4]) > (length "TACOCAT")

      ·∾ -- length returns Int, (>) returns Bool
·∾ -- ... so I'm guessing :: Bool
·∾ :type length [1,2,3,4] > length "TACOCAT"
length [1,2,3,4] > length "TACOCAT" :: Bool

  2. Given:

    x = 5
y = x + 5
w = y * 10

    What is the type of w?

    ·∾ -- Since w will reduce to a value, and all functions (*) (+) come from Num
·∾ -- I'm guessing w :: Num a => a
·∾ :type w
w :: Num a => a

  3. Given:

    x = 5
y = x + 5
z y = y * 10

    What is the type of z?

    ·∾ -- So, z needs one argument, so there will be two type variables
·∾ -- ...both with a constraint of Num
·∾ -- z :: Num a => a -> a is my guess
·∾ :type z
z :: Num a => a -> a

  4. Given:

    x = 5
y = x + 5
f = 4 / y

    What is the type of f?

    ·∾ – Hmm… ·∾ :type (/) (/) :: Fractional a => a -> a -> a ·∾ – f will fully reduce ·∾ – I’m guessing f :: Fractional a => a ·∾ :type f f :: Fractional a => a

  5. Given:

    x = "Julie"
y = " <3"
z = "Haskell"
f = x ++ y ++ z

    What is the type of f?

    ·∾ -- So, f will fully reduce
·∾ :type (++)
(++) :: [a] -> [a] -> [a]
·∾ -- (++) takes lists, but since they're strings, it will specialize to String
·∾ -- my guess is that f :: String
·∾ :type  f
f :: [Char]

5.8.3 Does it compile?

For each set of expressions, figure out which expression, if any, causes the compiler to squawk at you and why. Fix it if you can.

  1. bigNum = (^) 5 $ 10
wahoo = bigNum $ 10

    Ok, this will fail becuase bigNum doesn’t take any arguments. Also, the use of $ here is weird and unescessary.

    Here’s the error:

    Prelude> wahoo = bigNum $ 10
<interactive>:3:1: error:
    • Non type-variable argument in the constraint: Num (t -> t1)
      (Use FlexibleContexts to permit this)
    • When checking the inferred type
        wahoo :: forall t t1. (Num (t -> t1), Num t) => t1

  2. x = print
y = print "woohoo!"
z = x "hello world"

    This is fine, right?

    Prelude> :info print
print :: Show a => a -> IO ()   -- Defined in ‘System.IO’
Prelude> x = print
Prelude> y = print "woohoo!"
Prelude> z = x "hello world"
Prelude> z
"hello world"

    Right!?

  3. a = (+)
b = 5
c = b 10
d = c 200

    Well, c and d won’t work.:

    Prelude> a = (+)
Prelude> b = 5
Prelude> c = b 10
<interactive>:41:1: error:
    • Non type-variable argument in the constraint: Num (t -> t1)
      (Use FlexibleContexts to permit this)
    • When checking the inferred type
        c :: forall t t1. (Num (t -> t1), Num t) => t1
Prelude> d = c 200
<interactive>:42:5: error: Variable not in scope: c :: Integer -> t

  4. a = 12 + b
b = 10000 * c

    There is no c here… so yeah:

    Prelude> a = 12 + b; b = 10000 * c
<interactive>:32:25: error: Variable not in scope: c
Prelude>

5.8.4 Type variable or specific type constructor?

  1. You will be shown a type declaration, and you should categorize each type. The choices are a fully polymorphic type variable, constrained polymorphic type variable, or concrete type constructor.:

    f :: Num a => a -> b -> Int -> Int
--           [0]  [1]   [2]    [3]

    Here, the answer would be: constrained polymorphic (Num) ([0]), fully polymorphic ([1]), and concrete ([2] and [3]).

  2. Categorize each component of the type signature as described in the previous example, f :: zed -> Zed -> Blah.

    • Polymorphic, concrete, concrete.

  3. Categorize each component of the type signature f :: Enum b => a -> b -> C.

    • Polymorphic, constrained, concrete.

  4. Categorize each component of the type signature f :: f -> g -> C.

    • Polymorphic, polymorphic, concrete.

5.8.5 Write a type signature

For the following expressions, please add a type signature. You might not have precisely the same answer as GHCi gives (due to polymorphism, etc).

  1. functionH:

    functionH :: [a] -> a
functionH (x:_) = x

    proof that it works:

    ·∾ functionH (x:_) = x
·∾ :type functionH
functionH :: [a] -> a

  2. functionC:

    functionC :: Ord a => a -> a -> Bool
functionC x y =
  if (x > y) then True else False

    Checking my answer, here:

    ·∾ functionC x y = if x > y then True else False
·∾ :type functionC
functionC :: Ord a => a -> a -> Bool

  3. functionS:

    functionS :: (a, b) -> b
functionS (x, y) = y

    Does it blend?:

    ·∾ functionS (x,y) = y
·∾ :type functionS
functionS :: (a, b) -> b

5.8.6 Given a type, write the function

  1. There is only one function definition that typechecks and doesn’t go into an infinite loop when you run it.

    Type signature:

    i :: a -> a

    Function:

    i a = a

    Proof:

    ·∾ :{
 ⋮ i :: a -> a
 ⋮ i a = a
 ⋮ :}
·∾ :type i
i :: a -> a
·∾ i True
True

  2. There is only one version that works.

    Type signature:

    c :: a -> b -> a

    Function:

    c a b = a

    Proof:

    ·∾ :{
 ⋮ c :: a -> b -> a
 ⋮ c a b = a
 ⋮ :}
·∾ :type c
c :: a -> b -> a
·∾ c 1 2
1

  3. Given alpha equivalence are c’’ and c (see above) the same thing?

    Yes, it’s the same function as c.

    Type signature:

    c'' :: b -> a -> b

    Function:

    c'' b a = b

    Proof:

    ·∾ :{
 ⋮ c'' :: b -> a -> b
 ⋮ c'' b a = b
 ⋮ :}
·∾ :type c''
c'' :: b -> a -> b
·∾ c'' 1 2
1
·∾ c 1 2
1
·∾ -- c and c'' are the same function, with
·∾ -- different names and differently named type variables

  4. Only one version that works.

    Type signature:

    c' :: a -> b -> b

    Function:

    c a b = b

    Proof:

    ·∾ :{
 ⋮ c' :: a -> b -> b
 ⋮ c' a b = b
 ⋮ :}
·∾ :type c'
c' :: a -> b -> b
·∾ c' 1 2
2

  5. There are multiple possibilities, at least two of which you’ve seen in previous chapters.

    Type signature:

    r :: [a] -> [a]

    Function:

    r a = a

    Proof:

    ·∾ :{
 ⋮ r :: [a] -> [a]
 ⋮ r a = a
 ⋮ :}
·∾ :type r
r :: [a] -> [a]
·∾ r [1..8]
[1,2,3,4,5,6,7,8]

  6. Only one version that will typecheck.

    Type signature:

    co :: (b -> c) -> (a -> b) -> a -> c

    Function:

    co g f a = g (f a)

    Proof:

    ·∾ :{
 ⋮ co :: (b -> c) -> (a -> b) -> a -> c
 ⋮ -- (a -> b) === f
 ⋮ -- (b -> c) === g
 ⋮ co g f a = g (f a)
 ⋮ :}
·∾ :type co
co :: (b -> c) -> (a -> b) -> a -> c

  7. One version will typecheck.

    Type signature:

    a :: (a -> c) -> a -> a

    Function:

    a f a = a

    Proof:

    ·∾ :{
 ⋮ a :: (a -> c) -> a -> a
 ⋮ a f a = a
 ⋮ :}
·∾ :type a
a :: (a -> c) -> a -> a
·∾ a id 3
3

  8. One version will typecheck.

    Type signature:

    a' :: (a -> b) -> a -> b

    Function:

    a' f b = b

    Proof:

    ·∾ :{
 ⋮ a' :: (a -> b) -> b -> b
 ⋮ -- (a -> b) === f
 ⋮ -- ...but it doesn't take any a's
 ⋮ a' f b = b
 ⋮ :}
·∾ :type a'
a' :: (a -> b) -> b -> b
·∾ a' succ 8
8

5.8.7 Fix it

Won’t someone take pity on this poor broken code and fix it up? Be sure to check carefully for things like capitalization, parentheses, and indentation.

  1. 
fstString :: String -> String
fstString x = x ++ " in the rain"

sndString :: String -> String
sndString x = x ++ " over the rainbow"

sing = if x > y then fstString x else sndString y
  where x = "Singin"
        y = "Somewhere"

  2. 
sing' = if x > y then sndString y else fstString x
  where x = "Singin"
        y = "Somewhere"

  3. module Arith3Broken where

main :: IO ()
main = do
  print (1 + 2)
  print 10
  print (negate (-1))
  print ((+) 0 blah)
  where blah = negate 1

5.8.8 Type-Kwon-Do

The focus here is on manipulating terms in order to get the types to fit. Your goal is to make the ???’d declaration pass the typechecker by modifying it alone. Not all terms will always be used in the intended solution for a problem.

  1. h = ??? becomes h x = g (f x)

    module One where

f :: Int -> String
f = undefined

g :: String -> Char
g = undefined

h :: Int -> Char
h x = g (f x)

  2. e = ??? becomes e x = w (q x)

    module Two where

data A
data B
data C

q :: A -> B
q = undefined

w :: B -> C
w = undefined

e :: A -> C
e x = w (q x)

  3. xform = ??? becomes xform (x, y) = (xz x, yz y)

    module Three where

data X
data Y
data Z

xz :: X -> Z
xz = undefined

yz :: Y -> Z
yz = undefined

xform :: (X, Y) -> (Z, Z)
xform (x, y) = (xz x, yz y)

  4. munge = ??? becomes munge xToY yToWz = fst (yToWz (xToY x))

    module Four where

munge :: (x -> y) -> (y -> (w, z)) -> x -> w
munge xToY yToWz x = fst (yToWz (xToY x))

5.10 Follow-up resources

  1. Luis Damas; Robin Milner. Principle type-schemes for functional programs (pdf)

  2. Christopher Strachey. Fundamental Concepts in Programming Languages (pdf)

    (Popular origin of the parametric/ad-hoc polymorphism distinction.)

Additionally, here are some things not from the book that I found relevant and interesting.

  1. A video by Chris Allen on how to query and interact with the type system. He discusses some techniques for using existing type signatures as guidance for implementing “stubbed-out” functions at the term level.

  2. Luca Cardelli. Type Systems. (pdf)

    This paper discusses what a type system is, some of the notation for describing them formally, and has a few examples of how to determine whether something is well-typed or not (using type judgements in the sequent calculus).

  3. Luca Cardelli. On Understanding Types, Data Abstration, and Polymorphism (pdf)

    This is really a paper on understanding subtyping in object-oriented languages formally, but the first few sections have a very readable exposition of how type systems arise from untyped “universes”. I quoted heavily from it already, but I think the entire first sections are worth a read.

  4. A short video on currying and partial application.

  5. A surprisingly detailed video (maybe brutally so) on how type inference works in Haskell. It goes over the algorithm for type inference detailed in the Haskell language report.