Inheriting defaults from parent structures

Stream: lean4

[Thomas Murrills]

I'm wondering what the best way to inherit defaults from a parent structure to a child structure is. For example

structure SharedFoo where
  a : Bool

structure Bar extends SharedFoo where
  a := true
  b : Nat := 0

structure Foo extends SharedFoo where
  a := true -- intended to be a "global" setting for `a`
  bar : Bar := { a } -- we want that by default, this instance of Bar uses the parent `a` for the value of `a`

The "problem" with this is that when specifying a Foo, setting bar's other fields (b) will cause the default value of the field a to be decoupled from the a used in Foo. For example, in def x : Foo := { a := false, bar := { b := 2 } }, we find that x.bar.a is true—the default from Bar, when we'd like it to inherit the "global" value false as its default, from the surrounding instance for Foo.

Long message incoming: tl;dr it's useful for complicated config structures, and you can do it with a parameter to the structure which sets the defaults, or maybe by changing the underlying elaborator. And the question: is there support for making it more convenient than it currently is, one way another? If so, how?

Motivation

You might say that every Bar instance should get the same defaults wherever it's created (whether inside Foo or otherwise), but the situation is a bit different when Bar's only purpose in life, so to speak, is to be the type of a field of Foo.

Consider the following (real) situation as a motivating example: you're writing a config structure for a complicated thing, and you want lots of knobs to control all the different components. Many of the components involve running the same type of process, in part, but you'd like to provide the ability to modulate each one of the components' instances of these processes separately if need be. That means you at least want structures like

structure SharedProcessConfig where
  a : Bool := true

structure Comp1Config extends SharedProcessConfig -- plus other fields
structure Comp2Config extends SharedProcessConfig -- plus other fields

structure WholeThingConfig where
  c1 : Comp1Config
  c2 : Comp2Config

However, you'd like the ability to control a in all components at once as a convenient "global" setting in WholeThingConfig, but in a manner which could be overridden by one or two components manually.

Some approaches

One way to get around this is to give each Comp*Config a parameter which sets the defaults. For example

structure SharedProcessConfig where a : Bool

structure Comp1Config (defaults : SharedProcessConfig) extends SharedProcessConfig where
  a := defaults.a
  -- plus other fields

-- likewise for Comp2Config

structure WholeThingConfig extends SharedProcessConfig where
  a := true
  c1 : Comp1Config { a } := {}
  c2 : Comp2Config { a } := {}

The thing is that this does get a bit tedious after doing a bit of it. (defaults : SharedProcessConfig) extends SharedProcessConfig where a := defaults.a, but for all fields, and for each subconfig you write, is quite cluttered; and one even needs to define structure SharedProcessConfigWithDefaults (defaults : SharedProcessConfig) in some cases for the type of the field that eventually actually controls the shared process.

We could maybe automate this via an inheriting or inheriting_as_default elaborator, so that one could write something roughly like

...
structure Comp1Config extends SharedProcessConfig -- plus other fields
structure Comp2Config extends SharedProcessConfig -- plus other fields

structure WholeThingConfig extends SharedProcessConfig where
  -- creates Comp(1/2)ConfigInheritingFromWholeThingConfig (a) behind the scenes with appropriate defaults
  -- we can also maybe create coercions to/from the "base" structures for convenience
  c1 : Comp1Config inheriting a := {}
  c2 : Comp2Config inheriting a := {}

but this is a fair bit of trickery, and I'm a little wary of trying to make types like this invisible.

A totally different approach would be to modify elaborator for structures and structure instances in a way which, say, stores extra information in the structure info, then, during instance elaboration, checks some hint stored in the infotree to see if it needs to consult a parent structure's info and instance syntax for its defaults. But I haven't really worked this out yet, and an addition to core would be a bigger undertaking; I'm thinking of this as probably a potential addition to std4 or mathlib4 (if anything), but thought I'd post here since it technically only concerns lean4.

Is there support for figuring out how to make inheriting defaults more convenient, one way or another? Is there another way to do this currently which I'm totally missing, or even just a better way to approach the problem of complicated configs? Or is the whole feature just too niche? :)

[Kyle Miller]

I would avoid using default initializers and instead do the following:

structure SharedFoo where
  a : Bool

structure Bar extends SharedFoo where
  b : Nat

structure Foo extends SharedFoo where
  bar : Bar

def SharedFoo.default : SharedFoo := { a := true }

def Bar.default (d : SharedFoo := SharedFoo.default) : Bar :=
  { toSharedFoo := d, b := 0 }

def Foo.default (d : SharedFoo := SharedFoo.default) : Foo :=
  { toSharedFoo := d, bar := .default d }

def myCfg : Foo := .default { SharedFoo.default with a := false }

#eval myCfg.a
-- false
#eval myCfg.bar.a
-- false

[Kyle Miller]

The pattern is that you make default constructors that take the shared configuration and thread it to each of the default constructors for each field, and then when you construct a configuration later you make use of the default constructors along with { ... with ...} notation to override values.

[Kyle Miller]

The structure Comp1Config (defaults : SharedProcessConfig) pattern doesn't seem like a good idea because then every value for defaults yields a completely different type -- that's likely not what you want.

[Thomas Murrills]

Hmm, I am specifically looking for “natural” structure instance input syntax, though, so that you can actually just write { a := false, bar := { b := 2 } }. I’d worry that this makes that a bit clunky when we have nested config structures. It also means that I need to “teach” the user of a potentially already-complicated config about the default constructors, and shifts the responsibility onto them for remembering it at every level, instead of saying “inner values of a are taken to be the nearest outer value of a by default” and having it “just work”.

[Thomas Murrills]

Though, does having each value of defaults yield a different type cause an issue somehow?

[Thomas Murrills]

Also, hmmm…upon looking closer, I’m not sure .default constructors actually address the issue. How do we set b := 2 in Foo.bar in the example given? If we use Foo.default, we only get to set a; if we use Bar.default and modify b with with, then we don’t know about the parent a unless we explicitly write it in, and that’s what we want to avoid doing.

[Kyle Miller]

def myCfg : Foo :=
  { Foo.default { SharedFoo.default with a := false } with bar.b := 3 }

(One variation would be to let SharedFoo have default initializers, to cut down on the syntax a little and only need to write {a := false} in there.)

[Thomas Murrills]

That does work, but that means that you have to set each field of bar in a “flat” way, instead of in a packaged way, which I don’t think would be very readable when bar is the name of a subconfig and has several fields (and also there are other subconfigs, each which may also be provided)

[Kyle Miller]

This all seems to be very, and I'm not sure there's any avoiding needing to teach users of this configuration how it works no matter what design you use.

Are you sure you're solving a well-motivated problem right now? Do actually have configurations that you expect to need reconfiguration that need such nested structure and which need rules for which defaults override which?

[Kyle Miller]

Could you instead make a single configuration object that flattens everything for your particular application? If it makes things simpler to work with, I think it's perfectly ok if each individual sub-command doesn't make use of all the configuration fields in this flattened configuration object.

[Kyle Miller]

(My particular suggestion is one way to keep having nested configuration objects while also trying to avoid relying on any sort of magic :magic: -- anyone can follow the definitions of the default functions to see what will happen.)

[Kyle Miller]

I'm asking this because I feel like you're veering into enterprise-grade configuration patterns, and it's not clear that there are enterprise-grade applications for it, and life is better when we can keep things simple when we can.

This is for fail_if_no_progress right? In principle it's nice that you're making it be so configurable, but in practice, do you have concrete applications in mind where all these configurations will be exercised? Or are there a few basic configurations that anybody will use? Do we need different equality relations and transparencies for types, values, local declarations types and values, and metavariable contexts, all independently?

[Thomas Murrills]

So, this is for the full bells-and-whistles version of fail_if_no_progress, where the objective is to compare goal lists and have as many knobs as possible present in the background in case anyone wants them. As it happens, I did already implement the default initializer version I put forward in the time between my last message and your first message :sweat_smile: The configs are each for different components of the goals. I’d rather not flatten them all into one config, in part because I like the pattern of being able to control whether e.g. local contexts are compared by having something like Option (LocalContextComparisonConfig defaults) [name pending] rather than a separate boolean toggle—but maybe this is not a shared view. In that case, I could flatten them, but would need much longer field names to distinguish everything—and at that point may as well be using with bar.b := …

[Thomas Murrills]

Yes! Sorry, was in the middle of typing. :)

[Thomas Murrills]

So, that’s true, there’s an argument for more or less saying “why would you do that? don’t do that!” about comparing different Expr’s in different places in different ways; it’s not motivated yet. I can, though, at least imagine wanting to check some Expr’s with beq and some with isDefEq, or the hypotheses at instances transparency to see through instances but the goal at reducible transparency, but if people don’t think there will ever be a use for it, I can simplify things and avoid all of this. :)

I do think the notion of having a “global setting” and a “local setting” in configs is pretty useful in general, though, and I do think it ought to be easier than setting up default constructors. I can appreciate that they’re less magical, but personally I’d worry they’re sufficiently more wordy and time-consuming to infer the meaning of that they wind up being much more complex for the person writing the structure instance. To me, being able to write (the analogue of) { a := false, bar := { b := 2 } } is just cleaner and simpler.

At least one redeeming (magic-reducing) quality of having the defaults in the type explicitly (and not doing something like inheriting) is that you at least can’t extricate the Bar _ instance from its context: def bar’ := { b := 2 } doesn’t have enough info to typecheck. On the other hand, that makes it annoying to use the standalone comparison functions which take in Bar’s. You can probably imagine a way around that—have BarWithDefaults (defaults) and BarWithDefaults.toBar which simply forgets the type info—but it is another step.

[Thomas Murrills]

Hmm, one thing I haven’t added to the configs yet but can see a real use case for is functions which override the standard comparisons in a certain way. Ultimately there’s too much complexity out there for one config to cover it all. And I can see people wanting these functions to be defined differently at different spots, and for outer functions to propagate inwards by default…so I suppose that would be the closest to a reasonable motivating hypothetical.

[Kyle Miller]

Often the best configuration system is to give a good API to let people write the exact tactic that they want. At some point a configuration system permits so much that it becomes a programming language on its own, so one may as well just program a new tactic :wink:

[Kyle Miller]

Stepping back, what is fail_if_no_progress itself solving? Do you have other applications than simp? (And I hope simp will eventually at least have its own configuration option to have it detect it's made no progress.)

I would go through this effort to design such a featureful configuration system for only two reasons: (1) if there are multiple concrete situations I want to support right now, not just the tempting "I could imagine this being useful" that afflicts us all, or (2) if this is a personal exercise to see what's possible, but I wouldn't contribute it because I wouldn't want to make other people support it in the future (it's not a waste though: you'll be ready when a time comes that it's necessary)

[Kyle Miller]

(If you're not familiar with it, there's "worse is better". I remember the 1989 paper it comes from being an interesting read.)

[Thomas Murrills]

That’s insightful; thanks! :) I’ll think about it from this perspective further after I sleep, and try to keep things simple and maintainable while still featureful. I’m not familiar, so I look forward to reading it! :)