--- Day changed Thu Feb 02 2017
SuprDewdis there a way to prevent an expression from reducing temporarily?02/02 01:27
SuprDewdso either some way to notify the type checker, or some kind of box I can put my thing into that the type checker can't see in02/02 01:28
subttlemudri, {AS}: Ah, yes! Excellent, thank you!02/02 09:09
lpaste“k,,” pasted “mmm” at http://lpaste.net/216419809305296896002/02 15:08
drdohttp://lpaste.net/859094192503966924802/02 18:50
drdoI don't quite understand what the problem is02/02 18:50
Caledrdo: It can't figure out that the decidable equivalence you want to use is ≡02/02 20:07
Caledrdo: But the explicit type signature for test specifies that, and helps out.02/02 20:07
drdoCale: But why can't it figure that out?02/02 20:08
CaleBecause _≟_ is polymorphic02/02 20:08
drdoThe only available instance uniquely determines that02/02 20:08
Calehm?02/02 20:09
drdoMaybe I didn't understand what you were saying02/02 20:09
CaleI don't know what reasoning Agda would have to plug in _≡_ for the implicit argument to _≟_ there, since toBool is also polymorphic in the type of Dec that it's consuming02/02 20:12
CaleMaybe I just don't understand something about Agda, but I wouldn't expect it to just guess randomly02/02 20:13
drdoCale: But it doesn't have to guess, does it? There's only one instance02/02 20:14
CaleWho says that's the right one though?02/02 20:14
drdoIt only has to check that the only available instance works02/02 20:14
CaleIt doesn't know which relation it even needs an instance for02/02 20:15
drdoCale: Note that I'm talking about the instance argument, not the implicit one02/02 20:15
CaleIt can't even start to look for a matching instance02/02 20:15
drdoIt clearly does, since it complains about it :P02/02 20:15
Calebecause it doesn't know which type _≈_ is02/02 20:15
CaleYeah, well, it's looking for an instance for this variable relation argument02/02 20:16
drdoCale: huh? It does know _≈_ : Rel ℕ ℓ02/02 20:16
CaleIt doesn't know _≈_ = _≡_02/02 20:17
CaleYou can see it found a candidate, but it can't select it while the relation argument is still polymorphic, that would be madness, wouldn't it?02/02 20:18
drdoRight, but the instance argument gives you that02/02 20:18
drdoCale: I don't see why that would be madness02/02 20:18
CaleBecause it's ambiguous which relation you want, and there's no guarantee that this is the only instance forever.02/02 20:20
drdoCale: But that's fundamentally how instance arguments work, isn't it?02/02 20:20
CaleI wouldn't expect so02/02 20:20
drdoThey depend on what is in scope, by design02/02 20:20
CaleI dunno, I suppose it's working more sensibly from my point of view than how it's actually supposed to work? :)02/02 20:23
drdoCale: I'm trying to understand what your point of view is though :P02/02 20:23
drdoWhy do you feel using context provided by the instance argument candidate to determine implicit arguments not ok?02/02 20:24
drdo*is not ok02/02 20:25
Caledrdo: From my point of view, it shouldn't be okay to make any decision regarding instance selection based on the fact that some instance *doesn't* exist.02/02 20:25
drdoCale: Then you disagree with instance arguments?02/02 20:26
CaleBecause it *may* exist in a future module, which would result in incoherent behaviour02/02 20:26
drdoThat's exactly what instance arguments are02/02 20:26
drdoThe double {{ isn't decorative :P02/02 20:26
CaleThat's not what I thought they were02/02 20:26
drdoThey are much like Haskell's type classes02/02 20:26
Caleyes, I'm describing something which holds of Haskell's type classes02/02 20:26
CaleInstance selection in Haskell *never* relies on the nonexistence of an instance.02/02 20:27
drdoIf there's only one instance, it selects that instance02/02 20:27
drdoAny other number is not ok02/02 20:27
CaleNot how it works in Haskell02/02 20:27
drdoIt isn't?02/02 20:27
CaleInstances are selected on the basis of matching the structure of the type02/02 20:27
Caleonly02/02 20:27
CaleIf more than one instance matches, it's an error. If it's ambiguous, even if there's exactly one instance of the class anywhere, you don't learn anything about what the type of your thing is.02/02 20:28
CaleBecause there could be more instances in modules that haven't been compiled yet.02/02 20:28
Caleand so committing to the one that you can see could be wrong02/02 20:29
drdoWrong in what way?02/02 20:29
CaleWell, you're not supposed to have to keep track in your head of which instances the compiler has compiled thus far when trying to figure out how it's going to deal with any particular piece of code.02/02 20:31
drdoIt's not "thus far"02/02 20:31
drdoIt's every instance in scope02/02 20:32
drdoDoes not depend on compilation order02/02 20:32
drdoThat would be very silly :P02/02 20:32
CaleWell, you're getting something which compiles here, but it compiles for the reason that there's exactly one instance of the class anywhere.02/02 20:32
Caleand then later, there are two instances02/02 20:33
drdoRight, and then later it no longer compiles02/02 20:33
drdoI don't see the issue02/02 20:33
CaleWell, what, is it going to go back and recompile all the past modules?02/02 20:33
Caleevery time a new module defines an instance?02/02 20:33
CaleAlso, that's confusing to the programmer, I feel.02/02 20:33
drdoWhenever you compile anything in agda, I'm pretty sure it looks at every module02/02 20:34
drdoCale: Why is this confusing but having two functions named "foo" isn't?02/02 20:34
drdoI was using "foo" before and my program compiled, now there's another foo in another module and it no longer compiles02/02 20:35
drdoI don't see how this is different02/02 20:35
CaleWell, not compiling is fine02/02 20:35
CaleBut compiling and doing something which is based on assumptions that are no longer true is what's questionable02/02 20:36
drdoWhat do you mean?02/02 20:36
CaleIf you commit to an instance because you only see one at the moment, and compile a bunch of let's say ultimately monomorphic code on the basis of that, and then a new module comes along and defines a second instance02/02 20:37
drdoCale: Just forget separate compilation02/02 20:37
drdo:P02/02 20:37
CaleWell, it's not just about separate compilation, but modularity02/02 20:37
drdoWell, what does "a new module comes along" mean?02/02 20:38
CaleI mean, the code under discussion is imported by some other module02/02 20:39
CaleHmm, how can I give a good example...02/02 20:39
drdoCale: You'll notice this problem also occurs in Haskell02/02 20:43
CaleWhich one?02/02 20:43
drdoThe compilation success being predicated on the non-existence of other instances02/02 20:44
CaleHaskell will never refine a type on the basis that it is looking for an instance of a type class and only one is in scope.02/02 20:44
drdoI don't think this is a problem at all, I think it's the same issue as an ordinary name clash02/02 20:44
CaleLike, if I define an  instance MyClass [Char]02/02 20:45
Caleand some MyClass [a] constraint needs satisfying02/02 20:45
CaleIt won't say "Oh, a = Char, because that's the only instance I see right now"02/02 20:45
drdoWell, I agree with that behaviour02/02 20:46
Caleokay, but that's basically what you're expecting from Agda02/02 20:47
drdoBecause instance arguments do have those semantics02/02 20:47
CaleYou want it to notice that there's only one instance of IsDecEquivalence _≈_ right now02/02 20:47
drdoAt least if I understood it correctly02/02 20:47
drdoCale: That's what instance arguments are!02/02 20:48
Caleand decide on that basis that _≈_ = _≡_02/02 20:48
CaleInstance arguments indicate that it should search for instance records of matching type02/02 20:48
drdo"In principle, an instance argument is resolved, if a unique instance of the required type can be built from declared instances and the current context."02/02 20:48
CaleBut that doesn't mean it needs to be able to refine the type which it's trying to match on the basis of what it finds in that search02/02 20:49
CaleIt finds the instance for IsDecEquivalence (_≡_)02/02 20:49
Calebut since it doesn't know that _≈_ = _≡_, it can't commit to that selection02/02 20:49
drdoBut when you select that instance, you do know that02/02 20:50
CaleYeah, it clearly doesn't select instances which might not match.02/02 20:50
drdoI thought the process would be: find matching candidates, if there's only one (or provably equal several), try to type check with it02/02 20:51
drdoI don't understand why it's an issue to infer things based on the context provided by the instance02/02 20:51
CaleWell, obviously we *could* have it work that way02/02 20:53
drdoWe could?02/02 20:53
CaleIt's just that it results in spooky and hard to predict behaviour02/02 20:53
drdoIn what way is it spooky?02/02 20:53
CaleWell, in this particular case, it's sort of obvious that only one instance exists02/02 20:53
CaleBut in general, it might involve a deeper search02/02 20:53
drdoA deeper search?02/02 20:54
drdoWhat do you mean?02/02 20:54
CaleInstances may depend on other instances, right?02/02 20:54
drdosure02/02 20:54
drdoBut what does it have to do with infering things based on the instance you found?02/02 20:54
drdoThis process is completely *after* instance search and selection02/02 20:55
drdoIt does not influence search02/02 20:55
Caleand so at the end of this search process, you find one instance, perhaps for a somewhat unexpected type, and just because it happens to be the only one, it solves what would otherwise be a type ambiguity error for you02/02 20:55
drdoCale: That's what an instance argument is!02/02 20:55
CaleI think it's okay to make the programmer be more clear about what type they want02/02 20:55
CaleNo, I don't see it that way02/02 20:55
drdoBut that's what the manual says02/02 20:55
drdohttp://agda.readthedocs.io/en/latest/language/instance-arguments.html02/02 20:55
CaleThe search is a search for the *value* of the instance argument to be used02/02 20:55
CaleIt shouldn't really be a search for the *type* of the instance argument to be used02/02 20:56
drdoCale: You're only ever searching for a value02/02 20:56
drdoWhose type must be <= the type of the instance argument02/02 20:56
Caleah, no02/02 20:57
drdoCale: Notice this though, what I want to do has nothing to do with instance search02/02 20:57
CaleWhose type must be >= the type of the instance argument :)02/02 20:57
CaleWhat you seem to want is just that they'll be able to unify somehow, and we'll learn something about both perhaps if there's a unique instance which unifies.02/02 21:00
CaleBut while that would be powerful perhaps, I think in other cases, it would result in code that you'd really want to be an error, but which compiles anyway, in a surprising way.02/02 21:00
drdoExample?02/02 21:01
drdoI don't think this is particularly powerful02/02 21:01
drdoIt's just a convenience02/02 21:01
CaleWell, it allows you to do constraint logic programming to determine types.02/02 21:02
drdoCale: what now?02/02 21:02
drdoAre we even talking about the same thing at this point?02/02 21:02
CaleBecause it's doing a recursive search for instances02/02 21:02
drdoI just want (value : Type) to be added to the context AFTER instance search is completely over02/02 21:03
CaleYou want that type there to be determined by the unification of the type at which we're searching for an instance, and the type at which we found a unique instance02/02 21:05
CaleBut the search for instances isn't just a linear search through everything that's available02/02 21:05
CaleYou can have instance functions, essentially02/02 21:05
Caleat least, I think you can02/02 21:05
Caleyeah, the Agda documentation is talking about it here02/02 21:06
Calelook for the words "proof search" on the page you linked me02/02 21:06
CaleBut you want it not only to do proof search, but theorem search :)02/02 21:07
Calei.e. it'll figure out more about what thing you wanted to prove based on the proof that it finds02/02 21:07
Calewhich... well, that might be totally okay02/02 21:07
drdoI may not understand the power of what I'm asking then02/02 21:08
CaleWell, you were basically asking it "I need some relation to have decidable equality, please prove it for me and figure out which relation I meant", not merely "I need for _≡_ to have decidable equality, please prove it for me"02/02 21:10
CaleIn your specific code, things were so simple that it's hard to see why it wouldn't just pick for you02/02 21:10
CaleBut in a really complicated setting, this sort of unification might successfully pick stuff you weren't expecting, just because things were a bit ambiguous and your code was a bit off.02/02 21:11
drdoCale: Do you have an example?02/02 21:11
drdo(Where "bad" things happen)02/02 21:12
CaleAll the examples I'm thinking of are too big to relate easily02/02 21:12
Cale(which is why you'd end up really annoyed, because the machine is doing stuff you can't do in your head)02/02 21:12
CaleOr else, maybe you'd be really happy, if you were leveraging this in a positive way02/02 21:13
Calehmm02/02 21:14
CaleWell, imagine if this were a feature, you could use it to find the unique type satisfying some property.02/02 21:16
CaleBy writing a bunch of instances for general type formers, which were dependent on other instances and conditions02/02 21:16
Caleand then simply asking for a dictionary of arbitrary type02/02 21:17
CaleIt's easy to see how that would be a positive thing02/02 21:17
CaleIt's just, when you're programming, having the type checker figuring out *both* the type and the value that you want might be a bit too error prone. Usually you expect yourself to have a pretty good idea about at least one of those two things.02/02 21:18
CaleSo in this case with the instance arguments, it expects you to pin down the type, and it finds the value for you based on a recursive search02/02 21:19
drdoCale: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments02/02 21:23
drdoScroll to the very bottom of the page02/02 21:23
drdoThe last piece of code provided there doesn't actually work02/02 21:24
drdoBut apparently someone thought it should, just like me :P02/02 21:24
CaleI seem to recall Agda being overly aggressive about selecting instances in the past, so perhaps it really used to work like that02/02 21:26
CaleI don't really know02/02 21:26
drdoIncidentally, the example on that page is really what I was trying to do02/02 21:27
CaleWell, that was a case where multiple instances would apply, and it would just select... I can't recall, it was either the first or the last one02/02 21:27
drdoGetting some sort of Eq class to actually do practical things with02/02 21:27
drdoCale: But multiple instance don't apply here02/02 21:27
Caleyeah02/02 21:27
CaleWhich is why I didn't even mention that before.02/02 21:27
drdo"Page last modified on December 05, 2014, at 05:07 PM"02/02 21:28
drdoI guess I just need to download an old version of agda!02/02 21:28
Caleheh02/02 21:28
CaleIt is kind of funny if you really think about what you're asking for though02/02 21:29
Cale"Just find me any equivalence relation which is decidable, and decide for me if these are equivalent"02/02 21:29
drdoI clearly haven't thought about it much02/02 21:29
drdoCale: I don't think that's a fair characterisation of the issue :P02/02 21:30
drdoNot even close02/02 21:30
Cale(also, make sure it's unique in my database of decidable equivalence relations)02/02 21:30
CaleSo like, for any given type, as long as you only define one equivalence relation with an instance, it'd be able to figure out which one you wanted, and apply its decision procedure, and then at the end you get a Bool which tells you whether some unspecified-but-must-have-been-unique-in-the-database equivalence relation held or not02/02 21:32
drdoI don't see the problem02/02 21:34
drdoThat seems reasonable02/02 21:34
drdoinstance arguments are always unspecified-but-must-have-been-unique-in-the-database02/02 21:34
Caleno, usually they're specified02/02 21:35
drdohmm?02/02 21:35
Calelike, I want an Eq instance for (Char, Integer)02/02 21:35
CaleWell, maybe using Eq here is confusing, but let's think of this as Haskell's Eq02/02 21:35
CaleThen it finds the instance (Eq a, Eq b) => Eq (a,b)02/02 21:36
Calecommits to that, matching a = Char, and b = Integer, and then searches for instances Eq Char and Eq Integer, which it's able to locate02/02 21:36
drdoBut this case isn't even recursive02/02 21:37
drdoIt's a single level of searching02/02 21:37
CaleWell, sure02/02 21:37
drdoIt's completely direct02/02 21:37
CaleBut the point is, it knew which type it was looking for here02/02 21:37
drdoI really truly don't see the problem02/02 21:37
Caleand deconstructing the structure of that type to pick an instance02/02 21:37
CaleWhereas in the other case, you have it discovering which type it ought to have been searcing for on the basis of which instance it finds.02/02 21:38
Calesearching*02/02 21:38
CaleWhich -- as I've mentioned, is okay, but can be a bit funny02/02 21:38
drdoI feel like that characterisation isn't fair02/02 21:39
CaleHow so?02/02 21:39
drdoThe "ought to have been searcing" part02/02 21:39
CaleMaybe... are you missing something about your own code there?02/02 21:40
drdohmm?02/02 21:40
CaleLike, you don't say anywhere in the test3 case that you want to obtain a Dec _≡_02/02 21:40
drdoIt really just has to go through everything declared as an "instance", one by one, and see if it can refine the type to match02/02 21:40
CaleSo the type of thing it's searching for is not completely specified02/02 21:41
drdoSo what?02/02 21:41
Caleand on the basis that it found an instance for a specific type02/02 21:41
Caleyou want it to refine the type for which it was meant to find an instance02/02 21:41
CaleThat's an entirely accurate characterisation of what you want, I feel.02/02 21:42
CaleNote that if you changed the type of toBool, you could also fix the ambiguity here02/02 21:42
CaletoBool : ∀ {ℓ} {P : Set ℓ} → Dec _≡_ → Bool02/02 21:42
drdoNot exactly like that, but I get your point02/02 21:43
Caleoh, sorry, I left P02/02 21:43
Caleheh02/02 21:43
drdoThat's not the issue :P02/02 21:43
CaletoBool : Dec _≡_ → Bool02/02 21:43
drdoDec _≡_ isn't what you want :P02/02 21:43
CaleIf you changed toBool to have that type signature, the problem should go away02/02 21:43
CaleAnother thing you could do is just to make the P an explicit argument02/02 21:44
CaletoBool : ∀ {ℓ} (P : Set ℓ) → Dec _≡_ → Bool02/02 21:44
Caleand then apply toBool to _≡_ when you use it02/02 21:44
Caleand it won't have a problem02/02 21:44
drdoWhich defeats the point of the instance argument thing02/02 21:44
CaleIt doesn't though02/02 21:45
CaleIt's still looking up the *value* for you02/02 21:45
CaleJust not the *type*02/02 21:45
drdoThe real solution is to package the relation and the IsDecEquivalence together02/02 21:45
drdoIn a record02/02 21:45
drdoAnd call it, let's say, Eq :P02/02 21:45
CaleWell, yeah, if it was searching for an instance for the type ℕ rather than for an instance for an unspecified relation on ℕ, it would have a lot more luck02/02 21:48
drdoConceptually what we're really looking for is the relation02/02 21:48
Cale(and then the instance could provide which relation was supposed to be used)02/02 21:48
Cale(for each type)02/02 21:48
drdoThis has been a good conversation though!02/02 21:49
CaleThe setup you have here allows for it to do searches for multiple different decidable equivalence relations on the same type02/02 21:49
drdoI was pretty confused as to why it wouldn't accept that02/02 21:49
drdoI can live with it now that I think I understand what the issue is02/02 21:50
Cale(but then it's confused if you only tell it what type you want, and not which relation)02/02 21:50
drdoWhich appears to be that implicit argument inference completely happens before any instance search02/02 21:51
CaleThat may be true -- at the very least, it doesn't use the result of instance unification to refine the variables in the type for which it was searching for an instance.02/02 21:52

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!