Learning meta - Lambda expression to SKI combinators

Stream: general

[Tomas Skrivan]

I'm trying to learn how to reflect on expression. So I thought, I will try to implement conversion from lambda expressions to SKI basis. I have managed to convert expr representing a lambda expression to a expr that uses only SKI combinators and does not contain any lambdas. (This assumes that dependent types are not used)

Thus I have function meta def to_SKI_basis : expr → expr. However, I would like to have a function meta def to_SKI_basis' {X : Type} (x : X) [reflected x] : X which actually takes an expression of type X and produces another expression of type X that does not contain any lambdas or fail when dependent types are used.

How do I achieve this? I should probably somehow use tactic.infer_type, but I'm unable to figure out how. I don't even understand what tactic expr really is. What is interaction_monad and tactic_state? Is there a tutorial how all this meta stuff works?

Here is my current progress:

open expr

def I {X : Type} (x : X) : X := x
def K {X Y : Type} (x : X) (y : Y) : X := x
def S {A X Y: Type} (f : A→X→Y) (x : A→X) (a : A) : Y := (f a) (x a)

meta def II {elab : bool} := (@expr.const elab (mk_simple_name "I") list.nil)
meta def KK {elab : bool} := (@expr.const elab (mk_simple_name "K") list.nil)
meta def SS {elab : bool} := (@expr.const elab (mk_simple_name "S") list.nil)

meta def to_SKI_basis : expr → expr
| (app f x) := (app (to_SKI_basis f) (to_SKI_basis x))
| (lam var_name bi var_type body) :=
  if ¬(body.has_var_idx 0) then
     (app KK (to_SKI_basis body))
  else
    match body with
      | (var _) := II
      | (app f x) := (app (app SS (to_SKI_basis (lam var_name bi var_type f))) (to_SKI_basis (lam var_name bi var_type x)))
      | (lam var_name' bi' var_type' body') := to_SKI_basis (lam var_name bi var_type ((to_SKI_basis (lam var_name' bi' var_type' body')).lower_vars 0 1))
      | e' := e'
    end
| e := e

--- Test
constants {X Y : Type}
#eval (to_SKI_basis `(λ (x : X) (y : X→Y), y x)).to_string
| "S (K (S I)) (S (K K) I)"

meta def to_SKI_basis' {X : Type} (x : X) [reflected x] : X := sorry

[Mario Carneiro]

It's not possible to make a function with that type meta def to_SKI_basis' {X : Type} (x : X) [reflected x] : X (unless you do the silly thing and return x). What you really want is a program that produces an expression that when handed to lean would typecheck at type X

[Mario Carneiro]

And this is what by does

[Mario Carneiro]

by is how you "escape" the tactic mode: if tac : tactic unit then by tac : X, where tac is responsible for producing an expr that would typecheck as an X

[Mario Carneiro]

Here's how you could make and use a simple tactic wrapper around your function:

meta def to_SKI_basis' (e : expr) : tactic unit := tactic.exact (to_SKI_basis e)

example : X → (X → Y) → Y := by to_SKI_basis' `(λ (x : X) (y : X→Y), y x)

[Mario Carneiro]

It doesn't work though, because you have some bugs in the implementation

[Tomas Skrivan]

Thanks a lot! It makes sense that it is not possible to write the function as I have originally thought.
Now, I should be able to fix to_SKI_basis so it works as intended when using by.

[Mario Carneiro]

Note that since now everything is in a tactic, you can consider putting the whole code inside the tactic monad. This has the advantage that you can use functions like tactic.infer_type to infer the types of subterms, or tactic.mk_app for e.g. applying S to two arguments and automatically figuring out the substitutions for A X Y

[Tomas Skrivan]

And the best place to learn the basics of tactic monad is the tutorial on tactic writing? Currently I don't really understand what you are suggesting.

[Mario Carneiro]

Here's your function converted into monadic style:

meta def to_SKI_basis : expr → tactic expr
| (app f x) := do
  f' ← to_SKI_basis f,
  x' ← to_SKI_basis x,
  pure (app f' x')
| (lam var_name bi var_type body) :=
  if ¬(body.has_var_idx 0) then do
    body' ← to_SKI_basis body,
    pure (app KK body')
  else
    match body with
      | (var _) := pure II
      | (app f x) := do
        f' ← to_SKI_basis (lam var_name bi var_type f),
        x' ← to_SKI_basis (lam var_name bi var_type x),
        pure (app (app SS f') x')
      | (lam var_name' bi' var_type' body') := do
        a ← to_SKI_basis (lam var_name' bi' var_type' body'),
        to_SKI_basis (lam var_name bi var_type (a.lower_vars 0 1))
      | e' := pure e'
    end
| e := pure e

meta def to_SKI_basis' (e : expr) : tactic unit := do
  e' ← to_SKI_basis e,
  tactic.exact e'

Because tactic computations are stateful, you have to use bind or do notation here to call them in a well defined order, so you can't use pure function composition anymore. Other than that it is a mere syntactic transformation that doesn't change the behavior of the code at all.

But now you can insert a call to tactic.mk_app in one of those sequences of instructions to create expressions using information from the typing context, query the types of terms and so on.