Zulip Chat Archive

Stream: lean4

Topic: Showing functions in an unsafe way


Trebor Huang (Dec 02 2022 at 08:47):

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 (Dec 02 2022 at 08:49):

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

Mario Carneiro (Dec 02 2022 at 09:10):

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 (Dec 02 2022 at 09:11):

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

Trebor Huang (Dec 02 2022 at 09:11):

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

Mario Carneiro (Dec 02 2022 at 09:12):

yes? this is meta stuff after all

Sebastian Ullrich (Dec 02 2022 at 09:12):

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 (Dec 02 2022 at 09:18):

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 (Dec 02 2022 at 09:19):

I can break that python code with so many functions

Mario Carneiro (Dec 02 2022 at 09:19):

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

Trebor Huang (Dec 02 2022 at 09:20):

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

Sebastian Ullrich (Dec 02 2022 at 09:21):

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

Mario Carneiro (Dec 02 2022 at 09:21):

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 (Dec 02 2022 at 09:22):

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 (Dec 02 2022 at 09:24):

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

Sebastian Ullrich (Dec 02 2022 at 09:26):

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

Mario Carneiro (Dec 02 2022 at 09:38):

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 (Dec 02 2022 at 09:40):

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 (Dec 02 2022 at 09:41):

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 (Dec 02 2022 at 09:42):

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

Trebor Huang (Dec 02 2022 at 10:23):

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 (Dec 02 2022 at 10:25):

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 (Dec 02 2022 at 10:26):

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

Mario Carneiro (Dec 02 2022 at 10:26):

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 (Dec 02 2022 at 10:27):

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

Mario Carneiro (Dec 02 2022 at 10:28):

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


Last updated: Dec 20 2023 at 11:08 UTC