Code generation for what is essentially a no-op function

Stream: new members

[Iurii Zamiatin]

Hi! I am Iurii, new to this Zulip instance. I have a question about runtime representation of Lean types.

As a beginner, I thought a good learning project would be to formalize simple programming language based on untyped lambda calculus. You can see my attempt at https://gist.github.com/RiscInside/6da4a485b83e6e7e55e7398b62005dce.

I use Expr n as an type for lambda-calculus with de-brujin indices where n is the highest index of the free variable (Expr 0 represents expression with no free terms). I have a function called Expr.leftExtend which translates Expr n to Expr (n + 1). This function does not actually do anything with the term - it simply propogates information down the tree.

-- Left-extend `Expr n` to `Expr (n + 1)`
def Expr.leftExtend (e : Expr n) : Expr (n + 1) :=
  match e with
  | evar m m_lt_n   => evar m (Nat.lt_trans m_lt_n (Nat.lt_succ_self n))
  | emku _          => emku (n + 1)
  | euop u e        => euop u (e.leftExtend)
  | ebop b e₁ e₂    => ebop b (e₁.leftExtend) (e₂.leftExtend)
  | eabs e          => eabs (e.leftExtend)
  | elet e₁ e₂      => elet (e₁.leftExtend) (e₂.leftExtend)
  | ecas e e₁ e₂    => ecas (e.leftExtend) (e₁.leftExtend) (e₂.leftExtend)
  | efix e          => efix (e.leftExtend)

As I do quite a few left extensions during substitution, I hoped that lean compiler would be able to pick up on the fact that this function is, in fact, a no-op. To check that, I transpiled this lean file to C with lean -c tiny.c Tiny.lean. It turns out, however, that lean does indeed generate code for this function and it is very much not a no-op

LEAN_EXPORT lean_object* l_Expr_leftExtend(lean_object* x_1, lean_object* x_2) {
_start:
{
switch (lean_obj_tag(x_2)) {
case 0:
{
uint8_t x_3;
x_3 = !lean_is_exclusive(x_2);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_2, 0);
lean_dec(x_4);
x_5 = lean_unsigned_to_nat(1u);
// ...

Is there a way to tell lean compiler this function actually does nothing?

[Mario Carneiro]

Automatic detection of identity functions like this is on the roadmap but it will probably be a while. To take the code generation into your own hands you can use unsafeCast and implemented_by

[Iurii Zamiatin]

Thanks. WIll I lose the ability to reason about this function?

[Mario Carneiro]

unsafe def Expr.leftExtendImpl (e : Expr n) : Expr (n + 1) := unsafeCast e

-- Left-extend `Expr n` to `Expr (n + 1)`
@[implemented_by Expr.leftExtendImpl]
def Expr.leftExtend (e : Expr n) : Expr (n + 1) :=
  match e with
  ...

[Mario Carneiro]

nope

[Mario Carneiro]

for reasoning purposes is it not different at all

[Mario Carneiro]

however it is now up to you to ensure that the unsafe implementation in fact matches the model

[Iurii Zamiatin]

Thanks a lot. Is there a GitHub issue tracking implementation of this functionality?

[Mario Carneiro]

I don't think there is, but it would be reasonable to open one

[Iurii Zamiatin]

I have opened the issue at https://github.com/leanprover/lean4/issues/1972. I believe this thread can now be closed (although I am not sure how to do it :smile:)