Feature request: Command (or Auto parameter) for searching unique type inhabitant

[UlfNorell]

From carlos.c...@gmail.com on November 07, 2013 19:43:27

Introduce a new command (say "AutoU") that fills a hole only if a unique type inhabitant is found.

Alternatively (but I prefer a new command), introduce a new parameter (say, "-u") to command Auto: when -u is inserted, the search should find a unique type inhabitant, instead of a first one, to fill a hole.

The fact that the search space is generally too large is not a problem: this is dealt with well by the timeout mechanism.

• Carlos

Original issue: http://code.google.com/p/agda/issues/detail?id=945

[UlfNorell]

From guillaum...@gmail.com on November 07, 2013 11:16:32

The fact that the search space is generally too large is not a problem: this is dealt with well by the timeout mechanism.

What do you mean by that? If you want to guarantee that you have a unique solution, then you will have to go through the whole search space, you cannot limit it by a timeout mechanism.

[UlfNorell]

From andreas....@gmail.com on November 07, 2013 12:26:43

One could use the instance search for that feature. Instance search search for unique inhabitants, but it is very incomplete...

Status: InfoNeeded
Labels: Type-Enhancement Auto

[UlfNorell]

From ulf.nor...@gmail.com on November 07, 2013 23:42:00

@guillaume: I assume the command would fail if you hit the timeout, regardless of how many solutions were found.

As Wolfram noted on the mailing list, you can get this behaviour already by using -l to first list all solutions and if exactly one is found without hitting the timeout you run auto again without -l. I have my doubts as to how useful this is going to be in practice, but if you find yourself using this trick all the time it's probably worth it adding a -u flag.

Also, I'm not sure I understand your use case. Auto is limited in what it can do: it only uses locally bound variables, constructors and explicitly specified defined functions, and it doesn't do pattern matching unless you use -c. This means that it's not really clear what it actually means that auto has found a unique solution--there might still be other solutions that's outside of what auto can do.

Do you have any examples where you care about the solution being unique, and in what sense should it be unique?

[UlfNorell]

From carlos.c...@gmail.com on November 08, 2013 04:38:50

Yes. (Just like Auto works.)

I think it's worth it (otherwise I wouldn't have written the request). In fact I'd prefer another command (AutoU or Auto1) instead of a parameter, as it's written in the request.

The request was created by a suggestion of Nils Danielsson, in a Agda mailing list thread (Agda bug, Nov. 6). Please have a look at the example in this thread.

[UlfNorell]

From nils.anders.danielsson on November 08, 2013 06:10:13

This means that it's not really clear what it actually means that auto has found a unique solution--there might still be other solutions that's outside of what auto can do.

The property "Agsy can't find any other solution" doesn't seem useful to me. It might be interesting to know if the solution is unique up to definitional or propositional equality. For instance, if we had internal parametricity, then there would be a unique solution for the type (A : Set) → A → A.

For unique solutions up to propositional equality the following trick can be used:

witness : ∀ {a} {A : Set a} → (∃ λ (x : A) → ∀ y → x ≡ y) → A witness = proj₁

foo : … foo = witness ?

However, Agsy doesn't even manage to find a solution when … is the unit type, so I doubt this is going to be very useful (with the current implementation of Agsy).

[UlfNorell]

From ulf.nor...@gmail.com on November 08, 2013 21:58:56

Yes. (Just like Auto works.)

Well, Auto only hits the timeout if it finds no solution. AutoU would timeout if it's found no more than one.

Please have a look at the example in this thread.

As far as I can see there's no example where AutoU would be useful in that thread. In the first example where Auto inserts nothing AutoU would fail with a timeout. In the second example where you got the out of scope variable there are multiple solutions so AutoU would again fail.

Two examples where the command fails do not make a compelling case for why it's needed. There needs to be examples where (a) it works, and (b) you care about uniqueness (whatever that means in this case).

[UlfNorell]

From carlos.c...@gmail.com on November 09, 2013 05:54:45

"Just like" was meant to say (not that their behaviour is exactly the same but just) that the timeout mechanism is used in both cases for avoiding searching too long.

"nothing" is not correct in this case, because if mgu2 (Var v) (Con c) gives "just something", then mgu2 (Con c) (Var v) should also give "just something' " (the order of arguments to mgu2 is irrelevant). The fact that the search mechanism cannot deduce it doesn't imply that nothing can be correct. So not giving an answer would be better in this case. (I don't know why you are sure that a timeout would be hit in this case.)

[UlfNorell]

From ulf.nor...@gmail.com on November 09, 2013 06:16:51

I'm sure that the timeout would be hit because I tried it. As has been said before AutoU can be simulated by using the -l flag to Auto and counting the number of solutions. It doesn't tell you when it hits the timeout in this case but you can be pretty sure that it did if it takes longer than a second.

Why do you say that the order of arguments to mgu2 is irrelevant? I can implement a function mgu2 of the type you gave where the order of the arguments matter.

[UlfNorell]

From carlos.c...@gmail.com on November 09, 2013 10:05:29

Ok. I understand now. Thanks.

Ok, I agree (for the order of arguments of mgu2 to be irrelevant the type would have to include a proof of why the types do not unify).

But I still would have preferred to use AutoU, instead of Auto with parameter "-l" first to see if there is only one solution, and then Auto without "-l" to see that solution.

I used parameter -l (for the first time); it gives: Listing solution(s) 0-0 0 nothing Sorry, again, I don't understand 0-0 (I don't understand how 0-0 means that there is more than one solution).

[UlfNorell]

From ulf.nor...@gmail.com on November 09, 2013 22:01:49

It doesn't. Auto just found the one solution, but if you pay attention to how long it takes you can figure out that it hit the timeout. You can see for sure that it does by giving the flag -s 1 (skip the first solution), in which case it prints "Only 1 solution(s) found at time out (5s)".

[UlfNorell]

From carlos.c...@gmail.com on November 10, 2013 13:39:05

The road: "Auto inside { -l }, if there is one solution then pay attention to how long it takes (perhaps by doing it again) to conclude if it hit the timeout or not" is enough to motivate AutoU.

Carlos

[UlfNorell]

From ulf.nor...@gmail.com on November 10, 2013 21:15:25

Or use -s 1. But, no, it's not enough, because we still don't have a single example where AutoU would actually be useful.

[UlfNorell]

From carlos.c...@gmail.com on November 11, 2013 04:58:44

In my view this is an example. But (I agree) it's not a big issue, just a matter of (a better) user interface, so we should spend our time on other things. I mean I'd always use AutoU first, and then maybe Auto, if there is no unique solution; in this case I think it is better to receive no answer from AutoU than to receive Listing solution(s) 0-0 0 nothing as an answer, become surprised if not paying attention to the fact that -5s have indeed passed because of the timeout, and then do some further analysis to conclude that this is not really the only solution.

[UlfNorell]

From ulf.nor...@gmail.com on November 11, 2013 06:13:48

What I think isn't clear to me is what it is you actually care about. These two cases are to me indistinguishable:

• AutoU finds a single solution but times out searching for more [FAIL]
• AutoU finds a single solution exhausting its search space [SUCCESS]

In both cases there may or may not be other solutions. In the first case AutoU might not have looked hard enough and in the second case there may be solutions outside the set of programs that AutoU searches. Why is it important for you to fail in the first case, while not caring that the second case succeeds?

[UlfNorell]

From carlos.c...@gmail.com on November 11, 2013 07:20:09

In the second case the single solution found may not be the one the user is looking for (in the example given, for me, it was not). The situation has improved by including the sentence "The type inhabitant found is not necessarily unique." in the wiki, but the fact that the answer received gives a single type inhabitant and does not explicitly say that, because a timeout has occurred, other solutions may exist overweighs the importance of not overlooking the incuded message's content. Even if AutoU is not supported, Auto's answer should be modified to include that other type inhabitants may exist, when a timeout occurs. Even then, I think firstly using AutoU would be even better, because it would eliminate the possibility of a surprise.

[UlfNorell]

From guillaum...@gmail.com on November 11, 2013 07:39:53

The point is that even if the timeout is not hit and that Auto finds exactly one solution, other inhabitants may still exist. In other words, it may be the case that the term you are looking for cannot possibly be found by Auto, even if there was an infinite timeout (or if you had an infinitely powerful computer). And the set of terms that will be considered by Auto is not specified, so the property of uniqueness you are suggesting is basically meaningless.

[UlfNorell]

From carlos.c...@gmail.com on November 11, 2013 08:28:18

That is irrelevant (ortogonal). The irrelevance holds even though I don't knew that there are examples in which Auto does not find a type inhabitant that exists, and I now don't know how to construct such an example, even after you said that it exists.

I am saying that if a timeout exists then report that it has occurred together with the solution found, do not just silently present the solution found.

I did not suggest any property. I suggested that if a timeout occurs then (report that it has occurred and) do not just simply present a single solution, because it could help users not to think it is a single one.

[UlfNorell]

From guillaum...@gmail.com on November 11, 2013 08:56:15

Here is an example (I didn’t try it with the latest darcs version, but hopefully it still works):

module Test where

data + (A B : Set) : Set where inl : A → A + B inr : B → A + B

record Unit : Set where constructor unit

postulate A : Set a : A

c : Unit + A c = ?

In this example, Auto only find the solution inl unit and not inr a which would also be correct. So Auto does not hit the timeout (it takes far less than 5 seconds) and a unique solution is found, but this is maybe not the solution the user was looking for.

Now what should AutoU do? You’re proposing:

Introduce a new command (say "AutoU") that fills a hole only if a unique type inhabitant is found

So AutoU should fill the hole with inl unit given that a unique type inhabitant was found. The problem is that this inl unit is only unique with respect to a somewhat arbitrary search space: apparently postulates are not being considered by Auto. If you replace the postulates by arguments, then inr a will also be found by Auto.

Auto is just an heuristic, there is no guarantee that even something obvious will be found, so asking for uniqueness doesn’t make sense.

[UlfNorell]

From ulf.nor...@gmail.com on November 11, 2013 08:56:26

So has this turned into a request that Auto reports whether or not it hit the timeout when using -l? I could get behind that.

[UlfNorell]

From carlos.c...@gmail.com on November 11, 2013 09:47:05

You’re proposing:

There's no place for AutoU given that such an example exists.

If the search space continues to be "somewhat arbitrary" (and that "there is no guarantee that even something obvious will be found"), then: i) the feature request should be modified, to ask that "Auto reports whether or not it hit the timeout when using -l"; ii) this should be documented in the wiki right at the 1st paragraph.

[UlfNorell]

From ulf.nor...@gmail.com on November 11, 2013 12:04:45

Fixed. Auto -l now prints "after timeout (Ns)" when it times out.

Status: Fixed