2
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Are you familiar with Parametricity/Free theorems? I'm 99% sure the free theorem for forall t . t -> t -> t would let you conclude that its only inhabitants are equivalent to true and false 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$ May 10, 2019 at 18:16
  • 1
    $\begingroup$ Yes that is what I meant with the last paragraph. I was wondering if there maybe was another way to optimize this case, that's why I asked the question. $\endgroup$
    – Labbekak
    May 10, 2019 at 18:22
  • $\begingroup$ Not an expert, but my impression is that if you care about optimizations then you shouldn't be using Church encodings. Maybe Mendler encodings would have something more useful? But I'm not sure. Without the type discipline, you definitely can't make that optimization, since there are non-boolean functions that could be passed in. $\endgroup$ May 10, 2019 at 18:25
  • $\begingroup$ Thanks for the link, that's very interesting! Yeah good point about types. $\endgroup$
    – Labbekak
    May 10, 2019 at 18:29

1 Answer 1

4
$\begingroup$

Without further assumptions you cannot perform the optimization because it is unsound in general. For example, we could interpret System F in a model that has fixed point operators, in which case there will be elements of Bool that are different from false and true (namely "undefined" ). In such a model, dumb will not be equal to \ b . false because dumb ⊥ = ⊥ but (\b . false) ⊥ = false.

In your question you assumed that we know what it means to "optimize" a function. If we leave aside questions about efficiency, we still have to answer the question what it means for two closed terms in System F to be equal. There are several possibilities:

  • closed terms $M$ and $N$ are equal if they reduce to the same normal form,
  • closed terms $M$ and $N$ are equal if they are equal in some preferred model,
  • closed terms $M$ and $N$ are equal if they are observationally equivalent,
  • closed terms $M$ and $N$ are equal if they are extensionally equivalent (they give extensionally equivalent results when applied to extensionally equivalent arguments).

Parametricity, which was mentioned in the comments, may be helpful with some of the above. But it's difficult to discuss "optimization" until we know what counts as "equal", or else we cannot tell which optimizations are valid.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.