Showing functions in an unsafe way

Stream: lean4

[Trebor Huang]

I wonder if there is a way to hack lean to convert functions into strings.
In duck type systems this can be done fairly easily, e.g. Python

def fresh():
    i = 0
    while True:
        yield "x" + str(i)
        i += 1
fresh = fresh()

class LC:
    var: str
    body: "LC"
    fun: "LC"
    arg: "LC"
    def __init__(self, node):
        """Internal use."""
        self.node = node

    def __rrshift__(self, var:str):
        assert isinstance(var, str)
        tm = LC("Lam")
        tm.var = var
        tm.body = self
        return tm

    def __call__(self, arg:"LC"):
        tm = LC("App")
        tm.fun = self
        tm.arg = untangle(arg)
        return tm

    @staticmethod
    def v(name):
        tm = LC("Var")
        tm.var = name
        return tm

    def __repr__(self):
        match self.node:
            case "Var":
                return self.var
            case "Lam":
                return f"\\{self.var}. {self.body}"
            case "App":
                return f"({self.fun}) {self.arg}"
            case _:
                assert False

def untangle(term):
    if isinstance(term, LC):
        return term
    var = next(fresh)
    return var >> untangle(term(LC.v(var)))

term = lambda x: lambda y: y(x)
print(untangle(term))

Of course one cannot distinguish judgementally equal terms without meta stuff, but restricting to simply-typed normal forms, can we do that?

[Trebor Huang]

I'm trying to hack into Haskell using stuff like unsafeCoerce

[Mario Carneiro]

It's not really even hacking, the APIs are designed to support this already and you don't need unsafe code

import Lean

def foo (x : Nat) : Nat := x + x

open Lean Meta
elab "decl_to_string" decl:ident : term => do
  let val := ((← getEnv).find? decl.getId).get!.value!
  return mkStrLit (toString (← ppExpr val))

def bar := decl_to_string foo

#print bar
-- def bar : String :=
-- "fun x => x + x"

[Mario Carneiro]

@Sebastian Ullrich is there a shortcut for the format/paren/delab combo here? I was surprised not to find it

[Trebor Huang]

Well yes but shouldn't that count as "meta stuff"?

[Mario Carneiro]

yes? this is meta stuff after all

[Sebastian Ullrich]

Mario Carneiro said:

Sebastian Ullrich is there a shortcut for the format/paren/delab combo here? I was surprised not to find it

It's ppExpr

[Trebor Huang]

For instance, the Python code can correctly run even if given a statically unknown function. If I understood correctly then the Lean version can't right?

[Mario Carneiro]

I can break that python code with so many functions

[Mario Carneiro]

if you are restricting the inputs why not just pass an inductive and pattern match on it?

[Trebor Huang]

For mental exercise? And to figure out exactly what is allowing Python to do that, is it because of duck typing?

[Sebastian Ullrich]

Nothing to do with typing, everything to do with the mode of runtime execution

[Mario Carneiro]

You can do the equivalent of the python program in lean but it won't act on all types, only a very specific class of types

[Sebastian Ullrich]

I guess the hacky Lean equivalent would be to check if a function pointer points to an interpreter landing pad, in which case the environment and decl name can be derived and passed to meta code like above

[Sebastian Ullrich]

If you have only native code and no environment at all, you are certainly out of luck

[Sebastian Ullrich]

Oh, I guess I was thinking in a bit of a different direction than the Python code

[Mario Carneiro]

Here's the equivalent of the python code:

inductive LC
  | var : Nat → LC
  | fn : Nat → LC → LC
  | app : LC → LC → LC
  deriving Repr

instance : CoeFun LC fun _ => LC → LC where
  coe := .app

class Untangle (α : Sort _) where
  untangle : α → StateM Nat LC
open Untangle

instance [Untangle β] : Untangle (LC → β) where
  untangle f := do
    let n ← modifyGet fun n => (n, n+1)
    return .fn n (← untangle (f (.var n)))

def Untangle.run [Untangle α] (a : α) : LC := (untangle a).run' 0

instance : Untangle LC where
  untangle := pure

#eval run fun x y : LC => y x
-- LC.fn 0 (LC.fn 1 (LC.app (LC.var 1) (LC.var 0)))

[Mario Carneiro]

the only unfortunate part is that we have to use LC explicitly in the type of the input function, but this is necessary for the term to typecheck in the first place since otherwise you can't apply y to x

[Mario Carneiro]

in particular, the python trick does not work if you passed it a typed function like fun {α β} (x : α) (y : α → β) => y x, because then you can't pass an LC in for y because it's not a function type

[Mario Carneiro]

that's what I mean by saying this only works on a specific class of types

[Trebor Huang]

I think the thing is python allows this unconditional and dynamic overloading of function application. So this inverts a little bit of the control flow..

[Mario Carneiro]

If the issue is to find some types that act like the python type, then sure, we can make a PythonVal type and do all the same stuff. But if you want it to work on arbitrary lean types then you have to face the fact that lean is a strongly typed language and some types just aren't LC or convertible to/from it

[Trebor Huang]

So it is also doable in untyped languages with Call/cc

[Mario Carneiro]

if I have a function that adds two UInt8s, there is just no way you can safely call that function with LC arguments

[Mario Carneiro]

so if the scheme involves literally executing the function then you are out of luck

[Mario Carneiro]

the point is that python is a uni-typed language, there is one big sum-type over all the stuff you want to store and so you can pattern match on that using instanceof. From the lean perspective, that's a narrow view of types and there are lots of other types that aren't that