If e :: ∀a,b. a → b → a, then for all types A,B: for all x::A, y::B : x = e x y
Meaning: e must be const.
If e :: ∀a,b. (a → b) → a → b, then for all types A,B: for all f :: A → B, x :: A : f x = e f x
Meaning: e must be function application.
If e :: ∀a,b. (a → a → b) → a → b, then for all types A,B: for all op :: A → A → B, x :: A : op z z = e op z
Reminder: We assume that all values and functions are total (i.e., they terminate).
If e :: ∀a. a, then for all type A: for all x::A : x =
eA
Further deduce that e should not exist. (Hint: Here is one way: Deduce
both eBool = False and eBool = True.)
If e :: ∀a,b. a → b, then for all types A,B: for all x::A, y::B : y =
e x
Furthe deduce that e should not exist.
If e :: ∀a. (Integer → a) → a, then for all type A, f :: Integer → A: f (e id) = e f
Meaning: e must hide a secret constant and apply f to it; the secret can be discovered by e id.
Idea: ⟨(a,b)⟩ relates two tuples componentwise.
Rigorously: (xl,yl) ⟨(a,b)⟩ (xr,yr) iff xl⟨a⟩xr and yl⟨b⟩yr.
Pragmatically: If ⟨a⟩ is a function f and ⟨b⟩ is a function g, then
⟨(a,b)⟩ simplifies to: pmap f g, defined by:
pmap f g (x,y) = (f x, g y)
If e1 :: ∀a,b. (a,b) → a, then for all types A,B: for all x::A, y::B : e1 (x,y) = x
If e2 :: ∀a,b. (a,b) → b, then for all types A,B: for all x::A, y::B : e2 (x,y) = y
Meaning: We can define “fst (x,y) = x”, and fst will have the same type as e1. What you are proving is that e1 must also be equivalent to fst. Similarly for e2.
Idea: xm ⟨Maybe a⟩ ym iff both are Nothing, or, both are Just and the pair of elements are related by ⟨a⟩.
Rigorously: ⟨Maybe a⟩ is the smallest relation such that:
Pragmatically: If ⟨a⟩ is a function h, then ⟨Maybe a⟩ simplfies to:
mmap h, defined by:
mmap h Nothing = Nothing
mmap h (Just x) = Just (h x)
(Idea: mmap is like list’s map but for Maybe.)
If e :: ∀a. (Integer → a) → Maybe a, then for all type A: for all f :: A → Integer : mmap f (e id) = e f
Meaning: e must hide a fixed secret Maybe Integer and apply f to the element (if any); the secret can be discovered by e id.
If e :: ∀a. Maybe a, then for all type A: for all x::A : mmap (const
x) e() = eA
Further deduce that e should never be Just something, not even for just
one particular type A. (This is similar to the (∀a. a) exercise.)
If e :: ∀a,b. a → Maybe b, then for all types A,B: for all x::A, y::B
: mmap (const y) (e ()) = e x
Further deduce that e x should never be Just something. (Similar to the
previous one.)
If u :: ∀a. a → Maybe a, then for all types A,B: for all h :: A → B, x :: A : mmap h (u x) = u (h x)
Meaning: See the next one.
If f :: ∀a. Maybe a → Maybe a, then for all types A,B: for all h :: A → B, xm :: Maybe A : mmap h (f xm) = f (mmap h xm)
Meaning: To appreciate the meaning of the above two, you should write all possibilities (2 for u, 2 for f). You will notice that in all cases, if the output is a Just with an element, it must come straight from the input, so applying h to the element (if any) before or after doesn’t matter.
(Advanced students go on to recognize: In category theory, f is a natural transformation from Maybe to Maybe, and u is a natural transformation from identity to Maybe.)
You can furthermore deduce that u and f have only the possibilities you wrote. (Hint: u () has only 2 possibilities, and plugging each into the proved equation gives the general case. Likewise for f with f Nothing and f (Just ()).)
In addition, we can prove that a polymorphic inverse of u—a generic way to “extract a from Maybe a”—should be impossible:
If e :: ∀a. Maybe a → a, then for all types A,B: for all h :: A → B,
xm :: Maybe A : h (e xm) = e (mmap h xm)
Further deduce that e should not exist. (Hint: Apply to e()
Nothing, then it is similar to ∀a. a.)
Idea: xe ⟨Either a b⟩ ye iff: both are Left or both are Right, and the pair of elements are related by ⟨a⟩ or by ⟨b⟩ as appropriate.
Rigorously: ⟨Either a b⟩ is the smallest relation such that:
Pragmatically: If ⟨a⟩ is a function f and ⟨b⟩ is a function g, then
⟨Either a b⟩ simplifies to: emap f g, defined by:
emap f g (Left x) = Left (f x)
emap f g (Right u) = Right (g u)
If e :: ∀a. a → Either a a, then for all type A: for all x :: A : emap (const x) (const x) (e ()) = e x
Meaning: If e () = Left (), then e = Left generally. If e () = Right (), then e = Right generally. So e is always Left or always Right.
If e :: ∀a,b. a → b → Either a b, then for all types A,B: for all x::A, y::B : emap (const x) (const y) (e () ()) = e x y
Meaning: Similar to the previous one.
Idea: xs ⟨[a]⟩ ys iff both lists have the same length and every pair of elements is related by ⟨a⟩.
Rigorously (assuming finite lists): ⟨[a]⟩ is the smallest relation such that:
Pragmatically: If ⟨a⟩ is a function h, then ⟨[a]⟩ simplifies to: map h.
If e :: ∀a. (Integer → a) → [a], then for all type A: for all f :: Integer → A : map f (e id) = e f
Meaning: e must hide a fixed secret [Integer] and apply f to each element; the secret can be discovered by e id.
If e :: ∀a. [a], then for all type A: for all x::A : map (const x)
e() = eA
Further deduce that e should never be a non-empty list, not even for
just one particular type A. (Similar to the (∀a. a) exercise.)
If e :: ∀a,b. a → [b], then for all types A,B: for all x::A, y::B :
map (const y) (e ()) = e x
Further deduce that e x should never be a non-empty list. (Similar to
the previous one.)
If e :: ∀a. [a] → [a], then for all types A,B: for all h :: A → B, xs :: [A] : map h (e xs) = e (map h xs)
Meaning: To appreciate the meaning, you should first gain some experience from creatively making a lot of different functions of that type. (Some examples: reverse, take 4, drop 3.) You will notice that you only have freedom to: restructure the list (e.g., change order, change length), drop elements, duplicate elements; but any element you put in the output list must come straight from the input list. Therefore, applying f to the elements before or after doesn’t matter.
In category theory, one may say “e is a natural transformation from List to List”.
There are also “from List to Maybe”, “from Maybe to List”, and further combinations!
If e :: ∀a. a → [a], then for all types A,B: for all h :: A → B, x :: A : map h (e x) = e (h x)
If e :: ∀a. [a] → a, then for all types A,B: for all h :: A → B, xs
:: [A] : h (e xs) = e (map h xs)
Further deduce that e should not exist. (Similar to ∀a. Maybe a → a.)
Fortunately, the following exists:
If e :: ∀a. [a] → Maybe a, then for all types A,B: for all h :: A →
B, xs :: [A] : mmap h (e xs) = e (map h xs)
Further deduce e [] = Nothing.
If e :: ∀a. Maybe a → [a], then for all types A,B: for all h :: A → B, xm :: Maybe A : map h (e xm) = e (mmap h xm)
If e :: ∀a. [a] → [a] → [a], then for all types A,B: for all h :: A → B, xs1, xs2 :: [A] : map h (e xs1 xs2) = e (map h xs1) (map h xs2)
If e :: ∀a. [[a]] → [a], then for all types A,B : for all h :: A → B, xss :: [[A]] : map h (e xss) = e (map (map h) xss)
If e :: ∀a. [Maybe a] → [a], then for all types A,B: for all h :: A → B, xms :: [Maybe A] : map h (e xms) = e (map (mmap h) xms)
If e :: ∀a,c. [Either a c] → [a], then for all types A,B,C,C’: for all h :: A → B, k :: C → C’, xes :: [Either A C] : map h (e xes) = e (map (emap h k) xes)
If e :: ∀a,c. [Either c a] → [a], then for all types A,B,C,C’: for all h :: A → B, k :: C → C’, xes :: [Either C A] : map h (e xes) = e (map (emap k h) xes)
To appreciate what the cryptic title means, go through the exercises in this section and try to spot a pattern of how an algebraic data type can be represented by a polymorphic type. :)
If e :: ∀a. a → a → a, then for all type A: for all f,t :: A : (if e False True then t else f) = e f t
Meaning: e can have only two possibilities (determined by and discoverable from e False True): Always output the 1st argument, or always output the 2nd argument.
If e :: ∀a. a → a, then for all type A: for all x :: A : x = e x
Meaning: e has only one possibility (the polymorphic identity function), so it is like ().
We will need the following helpers:
If e :: ∀a. (Integer → String → a) → a, then for all type A: for all f :: Integer → String → A : foldTuple f (e mkTuple) = e f
Meaning: e can only apply f to a fixed secret pair of integer and string; the pair is discoverable by e fst and e snd.
We will need the following helper, like list’s foldr but for Either:
If e :: ∀a. (Integer → a) → (String → a) → a, then for all type A: for all f :: Integer → a, g :: String → a : foldEither f g (e Left Right) = e f g
Meaning: e can only hide a fixed secret integer or string, and apply f to the integer or g to the string accordingly; e Left Right discovers the secret.
We will need the following fold function for natural numbers:
foldNat z s 0 = z
foldNat z s (n+1) = s (foldNat z s n)
(Idea: apply s to z for n times; also analogous to list’s foldr.)
If e :: ∀a. a→(a→a)→a, then for all type A: for all z :: A, s :: A →
A : foldNat z s (e 0 succ) = e z s
(where succ = λn. n+1)
Meaning: e can only apply s to z for a fixed secret natural number of times; the secret number can be discovered by e 0 succ. Possibilities of e correspond exactly to possibilities of natural numbers.
We will need this helper, like list’s foldr but for Maybe:
If e :: ∀a. a → (Integer → a) → a, then for all type A: for all z :: A, f :: Integer → a : foldMaybe z f (e Nothing Just) = e z f
Meaning: e can only hide a fixed secret Nothing or Just integer, and output z or apply f to the integer accordingly; the secret can be discovered by e Nothing Just.
If e :: ∀a. (Integer → a → a) → a → a, then for all type A: for all op :: Integer → A → A, z :: A : foldr op z (e (:) []) = e op z
Meaning: e can only perform foldr on a fixed secret list of integers; the secret list can be discovered by e (:) [].
We will need the following binary tree type (with integer elements) and a fold function analogous to list’s foldr:
data BTZ = Nil | Bin BTZ Integer BTZ
foldBTZ :: (a → Integer → a → a) → a → BTZ → a
foldBTZ op z Nil = z
foldBTZ op z (Bin lt x rt) = op (foldBTZ op z lt) x (foldBTZ op z rt)If e :: ∀a. (a → Integer → a → a) → a → a, then for all type A: for all op :: A → Integer → A → A, z :: A : foldBTZ op z (e Bin Nil) = e op z
Meaning: e can only perform foldBTZ on a fixed secret tree; the secret tree can be discovered by e Bin Nil.