Menu
id is the only function of type a -> a, and
fst the only function of type (a,b) -> a. In these simple cases, this is fairly straightforward to see. But in general, how would you go about proving this? What if there are multiple possible functions of the same type?
Alternatively, given a function's type, how do you derive the unique (if this is true) function of that type?
Edit: I'm particularly interested in what happens when we start adding constraints into the types.
209
Proving uniqueness The most common technique to prove the unique existence of a certain object is to first prove the existence of the entity with the desired condition, and then to prove that any two such entities (say, and ) must be equal to each other (i.e. ).
For example, the operation a∗b defined by normal multiplication ab on R is considered uniquely defined—the operation takes any ordered pair in R and produces one, and only one value in R. As Pinter describes uniquely defined: In other words, the value of a∗b must be given unambiguously.
The limit of a function is unique if it exists. f(x) = L2 where L1,L2 ∈ R. For every ϵ > 0 there exist δ1,δ2 > 0 such that 0 < |x − c| < δ1 and x ∈ A implies that |f(x) − L1| < ϵ/2, 0 < |x − c| < δ2 and x ∈ A implies that |f(x) − L2| < ϵ/2.
To prove a function, f : A → B is surjective, or onto, we must show f(A) = B. In other words, we must show the two sets, f(A) and B, are equal. We already know that f(A) ⊆ B if f is a well-defined function.
The result you are looking for derives from Reynolds' parametricity, and was most famously shown by Wadler in theorems for free.
The most elegant way of proving basic parametricity results I have seen use the notion of a "Singleton Type". Essentially, given any ADT
data Nat = Zero | Succ Nat
there exists an indexed family (also known as a GADT)
data SNat n where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
and we can give a semantics to our language by "erasing" all the types to an untyped language such that Nat and SNat erase to the same thing. Then, by the typing rules of the language
id (x :: SNat n) :: SNat n
SNat n has only one inhabitant (its singleton), since the semantics is given by erasure, functions can not use the type of their arguments, so the only value returnable from id on any Nat is the number you gave it. This basic argument can be extended to prove most of the parametricity results and was used by Karl Crary in A Simple Proof Technique for Parametricity Results although the presentation I have here is inspired by Stone and Harper
190
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
