| Next | Types Are Theorems; Programs Are Proofs | 4 |
// These three are all the same
\x -> (\y -> x) :: a -> (b -> a)
\x -> \y -> x :: a -> (b -> a)
\x -> \y -> x :: a -> b -> a
A more interesting example:
\x -> \f -> f x :: a -> (a -> t) -> t
| Next | Next |