20
$\begingroup$

Inspired from the roundtable discussion held by Richard Eisenburg in WITS, I'm wondering if implicit arguments are really necessary for proof assistants?

Right now, they generate a lot of problems. For example, inserting implicit lambda bindings and potential implicit arguments at the end of an application is very difficult. Also, the algorithm for solving meta variables is complex.

What it we remove this feature completely? Is there any other (hopefully simpler) ways to omit certain information in a proof assistant?

$\endgroup$
1
  • 2
    $\begingroup$ This seems highly unlikely for a dependently typed proof assistant $\endgroup$
    – Couchy
    Feb 8 at 18:25

3 Answers 3

14
$\begingroup$

I would argue no, they are only necessary for reducing the suffering caused by other issues. In particular, one of the largest reasons we need implicits are various issues caused by bundling problems.

To see what I mean by this, let's consider an example. We might define a monoid like so:

record Monoid : Set where
  field
    Carrier : Set
    unit    : Carrier -> Carrier -> Carrier
    mul     : Carrier
    ...

However, we will run into trouble if we try to use only this definition. Namely, we don't have a way of talking about a monoid on a specific carrier set! To do this, we need to introduce yet another definition:

record MonoidOn (Carrier : Set) : Set where
  field
    unit    : Carrier -> Carrier -> Carrier
    mul     : Carrier
    ...

Now, once we start working with these, we need to start using implicits, lest we drown in a pile of arguments that are totally redundant. However, if we had some way of definitionally constraining the Carrier field from our original Monoid definition, then we wouldn't be in a position where we even needed implicits!

Another thing that makes use reach for implicits are families of types. As an example, consider the definition of a category:

record Category : Set where
  field
    Obj : Set
    Hom : Obj -> Obj -> Set
    id  : (X : Obj) -> Hom X X
    seq : (X Y Z : Obj) -> Hom X Y -> Hom Y Z -> Hom X Y
    ...

Here we run into similar issues: if we don't have implicits, then the laws are going to be brutal to state. Associativity will require 4 (!!!) redundant arguments, which is a show-stopper. However, if we look closely, we can see that this too is a bundling issue. If we work with the total space of Hom, and had our imaginary way of constraining things definitionally, then we wouldn't have our parameter explosion, and thus would not need implicits. With these ingredients, we might write Category like so:

record Category where
  field
    Obj : Set
    Hom : (s : Obj) -> (t : Obj) -> Set
    id : (x : Obj) -> Hom [ s = x, t = x ]
    seq : (f : Hom) -> (g : Hom [ s = f.t ]) -> Hom [ s = f.s, t = g.t ]
    assoc (f : Hom) -> (g : Hom [ s = f.t ]) (h : Hom [ s = g.t ]) ->
      Id (Hom [ s = f.s, t = h.t]) (seq (seq f g) h) (seq f (seq g h))
    ...

Luckily, our magic imaginary way of constraining things does exist under the guise of singleton types, or, more generally, extension types. Currently, cooltt supports all of these tricks, and allows us to write things concisely without using any implicits at all. This is also very easy to implement: we already had extension types, and the elaborator tricks required slide in at under 100 lines.

To summarize, implicits let us hide the fact that some parameter explosion occurred because we unbundled a bunch of stuff. Instead, let's try to prevent the explosion from happening in the first place by bundling as often as we can.

$\endgroup$
7
  • $\begingroup$ How does this help with associativity of some binary operation? Usually, you can make all of its arguments implicit, but I don't see how this problem can be solved by bundling. Also, polymorphic functions (like {A : Set} -> List A -> List A -> List A) seem to be a problem. $\endgroup$ Feb 8 at 22:50
  • $\begingroup$ I've updated my answer to clarify somewhat! For polymorphic functions, this is the same situation as Hom: we implicitly convert the family List : Set -> Set to it's total space Σ (A : Set) (List A), and then use the same singleton/extension type machinery as before to get (x : List) -> List [ A = x.A ] -> List [ A = x.A ] $\endgroup$ Feb 8 at 23:01
  • 3
    $\begingroup$ Maybe I'll feel differently if I ever undertake a substantial formalization effort in a proof assistant like this, but looking in from the outside I feel like this is a trick that works in some cases to make things manageable without implicits, but you have to be clever about how you design things in order to make it work -- kind of like a glorified version of how bidirectional typechecking allows omitting certain type annotations. Whereas implicit arguments are a general feature that even a total newcomer to formalization can understand and use: "Computer, guess this for me." $\endgroup$ Feb 10 at 5:31
  • 5
    $\begingroup$ @MikeShulman While I am skeptical that what Reed describes is a general solution, I'm also unhappy about how implicit arguments are handled in systems like Agda and Coq. The interaction between unification and reduction is very subtle, and does change from point release to point release. Gonthier's proof of the four colour theorem works in Coq 7.3, and not in 7.2 or 7.4! $\endgroup$ Feb 10 at 9:27
  • 5
    $\begingroup$ This is an unsatisfying state of affairs, and I think it's worth exploring sacrificing some inference in order to specify a predictable envelope of what can and can't be inferred. $\endgroup$ Feb 10 at 9:33
10
$\begingroup$

The only proof assistant I know of that doesn't have the usual notion of implicit arguments is Cedille. However:

  • It is a CC without a universe hierarchy and has syntactic stratification between terms, types, and kinds;
  • It does in fact have "spine-local type inference" that lets you omit type applications (but not term applications);
  • It is a Curry-style (unannotated, theoretically) type system so you're naturally supposed to write a lot more types; and
  • Whether it counts as a useable and ergonomic proof assistant is up to taste. See this library file, for instance, for a sense of how verbose a file might look like (although the lack of syntax highlighting certainly doesn't help!).

I think whether a proof assistant can do without implicit arguments depends on the type theory it's based on. I get the sense that it's the syntactic stratification and erased terms (confusingly also called "implicits", even though it's a completely different thing) of Cedille make it easier to write proofs even without implicit arguments.

$\endgroup$
4
  • 1
    $\begingroup$ Thank you! I didn't expect cedille to have such a design. I think cooltt also have something that deals with implicits $\endgroup$
    – ice1000
    Feb 8 at 21:55
  • $\begingroup$ That is definitely not the only one. $\endgroup$ Feb 8 at 22:25
  • $\begingroup$ What's a CC? .. $\endgroup$
    – mudri
    Feb 10 at 11:24
  • $\begingroup$ Calculus of Constructions, specifically with an impredicative kind (Prop or ⋆) and its sort (Type or □) that you can't quantify over (e.g. (λX: Type. e) is ill-formed) $\endgroup$
    – ionchy
    Feb 10 at 21:20
5
$\begingroup$

This question presumes that proof assistants necessarily support dependent type theories. There is no use for implicit arguments in proof assistants based on simple type theory, such as Isabelle or any member of the HOL family.

There are implicit coercions (type casts), e.g. from integers to reals. They are not essential and can be switched off.

$\endgroup$
1
  • 1
    $\begingroup$ My understanding is that Isabelle has ML-style inference, which implicitly instantiates type quantifiers as needed. Maybe you can do without that, but I can't! More generally, any proof assistant (dependently-typed or not) which lets you work with ML-style programs as a subsystem is going to want decent type inference. $\endgroup$ Feb 10 at 13:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.