Philosophical question about [..]

Stream: new members

[Martin Dvořák]

I have a philosophical question regarding Lean. Do you consider [..] to be a syntax for dependency injection?

[Mario Carneiro]

what syntax are you talking about? [..] isn't an operator, are you talking about instance arguments?

[Martin Dvořák]

Yes, instance arguments; sorry for not making it clear.

[Martin Dvořák]

I forgot that [..] has more meanings in Lean.

[Mario Carneiro]

also dependency injection sounds like a vague buzzword and reading the article on it didn't help

[Mario Carneiro]

I'm sure there is a way to interpret the term to make the answer 'yes'

[Eric Wieser]

I'd argue [some_typeclass] is no more "dependency injection" than (h : some_typeclass) is

[Martin Dvořák]

It was meant as a philosophical question; the absence of clear definition of "dependency injection" is not a bug.

I was talking about stuff like this.

lemma foo {T : Type} [inhabited T] : <something>

Here, we just assume that we get a guarantee that T is inhabited; we get it from somewhere. And if there are more instances that match the pattern, it is not a problem. We don't care what term default T is. We only need to know that default T exists and that, if we call default T twice in our proof, the returned terms will be equal to each other.

[Mario Carneiro]

We may or may not care what default T is. For instance you can have another argument that bounds its value

[Mario Carneiro]

but like Eric said the situation is exactly the same for regular arguments to a function

[Martin Dvořák]

Eric Wieser said:

I'd argue [some_typeclass] is no more "dependency injection" than (h : some_typeclass) is

In the latter case, we have to say explicitly what instance of some_typeclass we are using, don't we?

[Mario Carneiro]

we say it either way, but one comes with some automation to fill the argument. You can use automation to fill a regular argument too, or conversely specify a typeclass argument; and you are still not absolved of the responsibility to care what argument was inferred in fact when you let the automation take over, because it can directly influence the result or the side goals

[Martin Dvořák]

Would you say that the automatic filling of {T : Type} has the same level of vagueness as the automatic filling of [inhabited T] per se? Do they both give you an urge to check "what the automation inferred here" if the call to foo ends up being in your production code?

[Mario Carneiro]

the automatic filling of {T} doesn't require cross checking, because I know that if it was able to fill the argument, then it put "what it had to" there, there is no possibility of me being able to put anything else and still get a type-correct term

[Mario Carneiro]

unless I care to put something else that is definitionally equal in that slot for some reason

[Martin Dvořák]

Thank you for your explanation!

[Mario Carneiro]

with instance arguments, the degree to which typeclass inference can get the "wrong" result compared to what the user was hoping for depends on the class (whether it is a Prop or subsingleton, and whether there are different kinds of instances that are meaningfully different in the system)

[Martin Dvořák]

And now, less philosophically, more practically...

On the left side of :, there is a distinction between {} vs [] but on the right side, it is always () isn't it?

[Mario Carneiro]

you can use any binder type using something like : \forall {T : Type}, ...

[Eric Rodriguez]

what is the point of instance binders after a ∀ if you need to exactI all the time? e.g.

example {α : Type*}: ∀ [fintype α], by exactI fintype.card α = (finset.univ : finset α).card :=
λ h, by exactI finset.card_univ

[Mario Carneiro]

instance binders have no effect inside a theorem, they only affect users of the theorem

[Martin Dvořák]

Mario Carneiro said:

you can use any binder type using something like : \forall {T : Type}, ...

Is there a chapter in TPIL or any other source about this?

[Mario Carneiro]

@Eric Rodriguez For the reason you mention, it is generally preferable to keep instance arguments left of the colon, but sometimes you don't have any choice, for instance if your statement has more quantifier complexity (e.g. \exists k, \forall f [Ck_map f k], ...

[Mario Carneiro]

@Martin Dvořák what more would you like to know? \forall takes a list of binders with just the same syntax as binders left of the colon

[Mario Carneiro]

I don't have any particular recommendations, assuming this isn't already covered in #tpil

[Kyle Miller]

@Martin Dvořák If you imagine that to evaluate a function, you have to instantiate a class and set all its arguments before calling a run() method, then you could think of Lean instance arguments as being @Inject-annotated setters/members. Lean's typeclass system, from this point of view, is injecting dependencies from its database of instances, with the added fun that almost all of it is polymorphic (akin to dependency injection in Java with generics).

A difference is that Lean's system is to provide standard implementations of things that we wouldn't want to explicitly name each time, but as I'd understood it, dependency injection is more for wiring together systems through configuration. No one will later reconfigure the "default T" instance for a given "T" in this second sense.

[Martin Dvořák]

Does Lean sometimes provide default T automatically even when T is a custom type?

[Scott Morrison]

No, the language itself knows nothing about inhabited. It's just a typeclass defined as we go along. Mathlib certainly provides many inhabited T instances for particular T. (But perhaps I'm misunderstanding your question.)

[Martin Dvořák]

Thank you. I just wanted to make sure that, if I declare my own type, it will never become inhabited on its own.

[Scott Morrison]

On the wishlist for a while has been a "derive handler" for inhabited, so that you could just write @[derive inhabited] before a definition and hope automation can take care of it.