Next Types Are Theorems; Programs Are Proofs 6

a → (b → b) is inhabited

We know that b→b is inhabited (id for example)

So

        \a -> id        :: a -> (b -> b)
       
        \a -> (\b -> b) :: a -> (b -> b)

Next Next