Understanding higher-order code (Haskell)
daniel.yokomizo.org
Understanding higher-order code (Haskell)
1–3 of 3 posts
Re: Understanding higher-order code (Haskell)
#2> Also it states that there exists a program, such that if you give it something that is a proof of a theorem it'll return something that is a proof of the same theorem, for all possible theorems imaginable. Let's that thought sink for a while: for all possible theorems imaginable.
> Ignoring ⊥, in all forms, we can see that there's only a proof that's isomorphic to any given proof, namely the same given proof. In other words, the only program implements a → a is the identity:
It doesn't necessarily follow that the program is the identity for all types: it could be the identity for all types but, say, Int, where instead it returns 5. In Haskell this is not possible without FlexibleInstances, but we haven't assumed that property of the types-as-theorems model. (To interpret things literally, if I imagine a computer where I type in a proof of something and it prints out a proof of the same thing, I don't intuitively expect that it can't introspect on what I typed in.)
Re: Understanding higher-order code (Haskell)
#3> Also it states that there exists a program, such that if you give it something that is a proof of a theorem it'll return something that is a proof of the same theorem, for all possible theorems imaginable. Let's that thought sink for a while: for all possible theorems imaginable. > Ignoring ⊥, in all forms, we can see that there's only a proof that's isomorphic to any given proof, namely the same given proof. In ot…
The type of id is universally quantified, that's why the free theorem holds. If it was id :: Typeable a => a -> a then it could inspect the type representation and do something different if it's an Int or whatever, but in this case the theorem is different from ∀a. a → a. The Wadler paper goes in greater length about why the universal quantification holds.
Also the computer can't, at runtime, introspect what you typed due to erasure (i.e. the types are erased at runtime) which is part of proper parametricity.