Next Types Are Theorems; Programs Are Proofs 6

a → (bb) is inhabited

We know that bb is inhabited (id for example)

So

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

Next Next