Help: Recursive Classes?

Stream: general

[Kai Jellinghaus]

I am working through the book, and just completed the chapter on classes. I wanted to try to make a simple calculator-style example.

I figured something like this would be natural:

class Exp (α : Type) (o : Nat) where
  reduce : α → Exp β (o - 1)

But I obviously can't declare β in the "Signature" (not sure what that is referred to in Lean) because then I'd have to also declare it in the "return type" of reduce.

Am I modelling this wrong? At first I tried having a separate β that has to be [Exp ... o - 1] but I ran into similar problems about recursing in classes.

[Kenny Lau]

can you state in maths what you're doing? i have no clue what you intend with your code

[Kai Jellinghaus]

I can't really, I don't really come from Maths but from Software :sweat_smile:

The idea is to take a typical calculator example like "2 * 5 + 1" and turn it into a tree of expressions, and then reduce this step-by-step, (2 * 5 + 1 -> 10 + 1 -> 11).

This might look something like this in pseudo-C#:

interface Exp { Exp Reduce() };

// Example expression implementation
class ExpAdd : Exp {
    Exp Left;
    Exp Right;

    Exp Reduce() {
        if (Left is ExpCons && Right is ExpCons) return Left.Value + Right.Value;
        return new ExpAdd(Left.Reduce(), Right.Reduce());
    }
}

Of course most languages can't really safely represent this (The above implementation doesn't guarantee reducing actually makes any progress, it doesn't even really guarantee that the function returns).
In Rust this could be extended with lifetimes to ensure no cyclic expressions, maybe with const generics it could track the "order" (what I tried with o : Nat here) so complete reduction can be guaranteed.

I would've guessed the "Lean way" would be a type class, but it seems like I can't make a type class reference itself?
I hope this clarifies what I'm trying to do?

[Henrik Böving]

You can make this sort of dynamic dispatch work if you really want to by building a dependent sum type but the usual approach to solve the expression problem in languages like Lean would be to use an inductive

[Kai Jellinghaus]

Yeah, I first tried with inductive but couldn't really see how I can make the "order" tracking work (so it's clear that reduce must always improve the situation).
In my mind it is also a little ugly, doesn't it? You'd have to have an increasingly larger match? Can make sense of course, just doesn't seem "right"?

[Aaron Liu]

In Lean you (provably) can't create cyclic expressions (with an inductive)

[Aaron Liu]

Kai Jellinghaus said:

Yeah, I first tried with inductive but couldn't really see how I can make the "order" tracking work (so it's clear that reduce must always improve the situation).

What do you mean "order"? What did you try?

[Henrik Böving]

Kai Jellinghaus said:

In my mind it is also a little ugly, doesn't it? You'd have to have an increasingly larger match? Can make sense of course, just doesn't seem "right"?

You're asking about the expression problem here, one approach is to have a large match, the other is to have more and more type class instances, both of these approaches have their own pros and cons

[Kai Jellinghaus]

In Lean you (provably) can't create cyclic expressions (with an inductive)

Right which is really nice, but reduce could still create more nodes, ie reduce on Cons could create an (Add (Cons x - 1) (Cons 1)), leading to repeatedly calling reduce going nowhere.

[Henrik Böving]

https://en.wikipedia.org/wiki/Expression_problem

[Kai Jellinghaus]

Looks like that's what I'm asking? Not sure, at a glance the wikipedia link mentions avoiding recompiling, which is not really what I try, but I guess I don't want to modify existing code. Right now I can't get the version with more type class instances to compile at all :sweat_smile:

[Kai Jellinghaus]

What do you mean "order"? What did you try?

My math knowledge is wonky, so "order" may not be the right term, sorry.
Basically Cons is 0 (no further children) Add (Cons .) (Cons .) is 1, (Add (Add (Cons .) (Cons.)) (Cons .) is 2, etc. if this number decreases after a reduction, it's clear progress towards termination has been made.

[Aaron Liu]

Kai Jellinghaus said:

In Lean you (provably) can't create cyclic expressions (with an inductive)

Right which is really nice, but reduce could still create more nodes, ie reduce on Cons could create an (Add (Cons x - 1) (Cons 1)), leading to repeatedly calling reduce going nowhere.

You don't seem to be repeatedly calling it at all?

[Aaron Liu]

Kai Jellinghaus said:

What do you mean "order"? What did you try?

My math knowledge is wonky, so "order" may not be the right term, sorry.
Basically Cons is 0 (no further children) Add (Cons .) (Cons .) is 1, (Add (Add (Cons .) (Cons.)) (Cons .) is 2, etc. if this number decreases after a reduction, it's clear progress towards termination has been made.

When you write an inductive type Lean automatically makes a sizeOf instance which is some rough approximation to how big it is

[Aaron Liu]

This would be a lot easier with a #mwe

[Kai Jellinghaus]

Right, main would look something like this (can't do this in Lean this quickly yet, but I think the example should demonstrate):

var input = readline();
var exp = parse(input);

while (exp.o > 0):
    exp = exp.reduce();
    print(exp);

Inputting "2 * 5 + 1" will then print
"10 + 1", "11"b

[Kai Jellinghaus]

I'd love to provide a better example in Lean, but I don't have the skill to go beyond the given broken type class definition - can't really make implementations or parsing or whatever without it.

[Aaron Liu]

oh so you want that repeatedly calling reduce will make the exp.o go to zero

[Aaron Liu]

Am I correct in understanding that exp.o is some sort of depth function?

[Kai Jellinghaus]

Yes? Basically, by "reducing" constant expressions like (Add (Cons 1) (Cons 2)) to (Cons 3)

[Kai Jellinghaus]

o (I suppose order is the wrong term) is the depth yes. Could be a function, field, whatever.

[Aaron Liu]

ok so are these "expressions" supposed to be extensible?

[Kai Jellinghaus]

Yes. As in new structures can be defined w/ instances of the type class

[Aaron Liu]

what do you mean exactly be "new structures"?

[Kai Jellinghaus]

Like

structure ExpSub (α : Type) (β : Type) where
  l : α
  r : β
deriving Repr

structure ExpNeg (α : Type) where
  e : α
deriving Repr

structure ExpCons where
  e : Nat
deriving Repr

where I can then introduce ExpMul etc.

(Class instances missing of course)

[Aaron Liu]

oh ok that makes sense

[Aaron Liu]

You will end up having a large type living in the next universe up because of size issues

[Kai Jellinghaus]

Okay, I'm guessing that is bad (will need to read the book further). So what is the way to represent this kind of thing then? Is inductive really the way even if I would plan on expanding this to a ton of expression types? (A thousand line match seems like bad practice)

[Aaron Liu]

I don't know what will be best for your use case

[Kai Jellinghaus]

I understand you to say a big type class like this is probably bad practice? What would be an alternative? Maybe I'm just not informed enough and jumped into this too early, but not really sure at this point what other option I can consider beyond inductive (which seems to me like it would be hard to maintain, so bad practice) and a big type class, which is also bad practice or just outright not possible?

[Aaron Liu]

You would have to bundle both the type and the typeclass instance into the data, which gets you into DTT hell very quickly

[Kyle Miller]

How many expression nodes do you envision having? Knowing more about the scope is a good analogue for "can you state in maths what you're doing" — "can you state the program design problem more concretely?" (Not just the abstract 'design patterns' problems.)

Btw, "classes" in Lean can be thought of as being more like interfaces. They're all resolved at compile time, so unless you have some flexible data type that covers what you want to do at runtime, a purely class-based approach might limit you to evaluating expressions that are more-or-less known at compile time.

[Kai Jellinghaus]

let's say a few hundred? Mostly just exploring with an example I know well (and, I think, lends itself well to exploring safety & tradeoffs in a language)
And yes, thanks for the explanation. This is a bit of an X Y problem, but that is because there is no "real" problem, just me trying to apply what I learned :)

That makes sense. Parsing into a hierarchy would probably be an issue then.

[Kyle Miller]

Can you be more concrete? What would the few hundred expression node types look like? Are the known at compile time? Should users of the library be able to extend the set of them? (I know there's no "real" problem, but it's easier to talk about it like there is one.)

[Kai Jellinghaus]

Sure, I'll try. Beyond the basics of add/sub/mul/div I can imagine extending with simple built-in functions like pow/sqrt/sin/cos/etc. Could also build load/store on top of this, etc. So a design that at least somewhat scales is the goal.
Ideally these can be loaded & reduced at runtime. I haven't looked into parsing and such at all yet, just interested to see where it leads. If having everything known at compile time is very different, that's fine in my mind.
I don't really care about extending with new types, especially not at runtime, it just seems like a normal thing to reach for when more then a few options exist, for the sake of maintainability on my side (reducing coupling and all that).
Does that make sense?

[Kyle Miller]

Must pow/sqrt/sin/cos be nodes, or would it make sense having unop/binop nodes and types for operators? That's usually how expression trees tend to be handled.

[Kyle Miller]

e.g.

inductive Expr (Const Op Binop : Type) where
  | const (c : Const)
  | unop (op : Op) (e : Expr Const Op Binop)
  | binop (op : Binop) (e e' : Expr Const Op Binop)

[Kyle Miller]

That's for a simply-typed language. Where classes could come in potentially is in giving interpretations to Const/Op/Binop terms for the evaluator.

[Kyle Miller]

Here's an easily arbitrarily extensible language:

inductive Expr (α : Type) where
  | const (c : α)
  | unop (op : α → α) (e : Expr α)
  | binop (op : α → α → α) (e e' : Expr α)

def Expr.eval {α : Type} : Expr α → α
  | .const c => c
  | .unop op x => op x.eval
  | .binop op x y => op x.eval y.eval

It embeds the operations right in the tree. The cost of doing this is that you can't match on operations, for example you can't print the expression trees when encoded this way.

[Kyle Miller]

I came across https://github.com/leanprover/lean4/blob/master/doc/examples/phoas.lean and was reminded of this thread. Parametric higher order abstract syntax (PHOAS) is a really cool technique for doing a functional programming version of the visitor pattern. You can also extend the type to some degree after the fact as well.

[Kai Jellinghaus]

Oh that is really cool. Will have to dig more into that.
I haven't gotten this far yet, but proving the constant folding is sound is really cool in my mind.
Thanks a lot for the input :thinking:

[Yan Yablonovskiy 🇺🇦]

Perhaps of some relevance:
https://lean-lang.org/doc/reference/latest///Type-Classes/Instance-Declarations/#recursive-instances

"The standard idiom to work around this limitation is to create a local instance in a recursively-defined function that includes a reference to the function being defined, taking advantage of the fact that instance synthesis may use every binding in the local context with the right type."