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
to
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.
forall t . t -> t -> t
would let you conclude that its only inhabitants are equivalent totrue
andfalse
church-encoded. So you could then do an optimization where you evaluate both possible values and check if the results are equal. But I doubt this would scale past booleans. Church encodings are not known for their efficiency. $\endgroup$