If it did any of those things, its type would change. What the quote is saying is that, given that we know fst
is of type (a, b) -> a
, we can make those deductions about it. If it had a different type, we would not be able to do so.
For instance, see that
snd :: (a, b) -> a
snd (x, y) = y
does not type-check, and so we know a value of type (a, b) -> a
cannot behave like snd
.
Parametricity is basically the fact that a polymorphic function of a certain type must obey certain laws by construction — i.e., there is no well-typed expression of that type that does not obey them. So, for it to be possible to prove things about fst
with it, we must first know fst
's type.
Note especially the word polymorphism there: we can't do the same kind of deductions about non-polymorphic types. For instance,
myFst :: (Int, String) -> Int
myFst (a, b) = a
type-checks, but so does
myFst :: (Int, String) -> Int
myFst (a, b) = 42
and even
myFst :: (Int, String) -> Int
myFst (a, b) = length b
Parametricity relies crucially on the fact that a polymorphic function can't "look" at the types it is called with. So the only value of type a that fst
knows about is the one it's given: the first element of the tuple.
与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…