I can encode booleans in pure lambda calculus like this:
type Bool = forall t. t -> t -> t true : Bool = \x y -> x false : Bool = \x y -> y
Is there a procedure to optimize the following "dumb" function
dumb = \(b : Bool) -> b false false
dumb = \(b : Bool) -> false
I can imagine this is quite easy in Haskell with an ADT for example.
One way I can think of is counting the inhabitants of the type Bool (2) and then applying the function to both the inhabitants, discovering that the function will have the same result for any argument. This seems quite difficult to do in general though.