Next | Types Are Theorems; Programs Are Proofs | 27 |
((a ∨ (a → b)) → b) → b
1 | Assume (a ∨ (a → b)) → b) | Assume we have f :: (Either a (a -> b)) -> b | |||
2 | Assume a | Assume we have x :: a | |||
3 | From (2), conclude a ∨ (a → b) | (∨I)
| Left x | :: Either a (a -> b) | |
4 | From (3) and (1), conclude b | (→E)
| f (Left x) | :: b | |
5 | From (2) and (4), conclude a → b | (→I) | (disch. 2) | \x -> f (Left x) | :: a -> b |
6 | From (5) conclude a ∨ (a → b) | (∨I) | Right (\x -> f (Left x)) | :: Either a (a -> b) | |
7 | From (6) and (1), conclude b | (→E)
| f (Right (\x -> f (Left x))) | :: b | |
5 | From (1) and (7), conclude (a ∨ (a → b)) → b) → b | (→I) | (disch. 1)
| \f -> f (Right (\x -> f (Left x))) | :: ((Either a (a -> b)) -> b) -> b |
If nothing else this should convince you that Haskell types can be surprising
Next | Next |