--- Day changed Mon Mar 06 2017
snow_lemurianHey, I just have a question06/03 01:36
snow_lemurianIs agda proved the same way Coq is? With a small kernel that enhances itself?06/03 01:37
byorgeyI can't seem to prove that 'just' (from Data.Maybe) is injective.  What am I missing?06/03 04:00
byorgeyI tried writing  just-inj : {A : Set} (x y : A) → just x ≡ just y → x ≡ y06/03 04:00
byorgeybut I get some kind of weird unsolved metas on the  'just x \== just y' part, i.e. it is highlighted in yellow06/03 04:01
byorgeyand pattern-matching on the given equality with 'refl' doesn't reduce the goal at all.06/03 04:02
byorgeyrelatedly, I found 'drop-just' in the standard library but I am unsure how to use it.06/03 04:03
ezyangI think you probably want to case on the value of type just x 06/03 04:04
byorgeyeh? just x is not a type06/03 04:05
ezyangoh oops 06/03 04:06
lpaste_byorgey pasted “just is injective” at http://lpaste.net/35325406/03 04:13
byorgeyhuh, I finally got it to work, but I had to write this ^^^   I still don't understand why I need to explicitly give that implicit parameter to _≡_06/03 04:14
qmmhttps://stackoverflow.com/questions/4713906/purely-functional-equivalent-of-weakhashmap06/03 06:33
qmmwrong channel06/03 06:36
comietekbyorgey: I think it's not the Maybe A that you need to provide, but the A06/03 08:59
comietekbyorgey: note you're assuming A is a small set (level 0)06/03 08:59
comietekbyorgey: you could probably show the same for all levels (A : Set l)06/03 09:00
byorgeycomietek: yes, it works for all levels, but that doesn't change the fact that I need to provide the implicit argument to \==06/03 15:08
byorgeycomietek: I'm not sure what you mean about needing to provide the A rather than the Maybe A06/03 15:08
{AS}byorgey: it's most likely not inferring the type of just x and just y06/03 15:10
{AS}byorgey: oh, it seems that Maybe is level polymorphic06/03 15:11
{AS}so it may not infer the level06/03 15:12
{AS}in any case try writing just {?} x 06/03 15:12
{AS}and see whether there is something missing06/03 15:12
mietekActually it’s just overloading06/03 15:18
{AS}mietek: there is something else called just?06/03 15:19
mietekWait.06/03 15:19
mietekThis is weird.06/03 15:19
mietekThis might be an Agda bug.06/03 15:19
mietek{AS}, byorgey: https://gist.github.com/mietek/65f9d88492f0495965f34d6dcd9a54b406/03 15:20
{AS}mietek: hmm06/03 15:21
{AS}that seems buggy indeed06/03 15:21
{AS}mietek: 06/03 15:21
{AS}https://www.irccloud.com/pastebin/BHUpkr3t/06/03 15:21
{AS}byorgey: as well06/03 15:21
{AS}I get this error06/03 15:21
mietekAnd there’s nothing else that can possibly be named "just" because I import explicitly06/03 15:23
mietekI noticed this before when I had overloaded zero/suc06/03 15:23
mietekBut there is no overloading here06/03 15:23
{AS}mietek: it seems it can't infer the type for some reason06/03 15:23
{AS}if you just prefix any of them with Maybe06/03 15:24
{AS}it works06/03 15:24
mietekWell, that’s the difference between good and bad ;p06/03 15:24
mietekin my gist06/03 15:24
{AS}mietek: yeah, but you don't need to prefix both06/03 15:24
mietekAh, yeah06/03 15:24
{AS}definitely a bug06/03 15:24
mietekhmhm06/03 15:26
mietekInlining Maybe into the file helps06/03 15:26
mietekdoh06/03 15:26
mietekIt *is* overloaded06/03 15:26
mietekdata Any {a p} {A : Set a} (P : A → Set p) : Maybe A → Set (a ⊔ p) where06/03 15:26
mietek  just : ∀ {x} (px : P x) → Any P (just x)06/03 15:26
mietekdata All {a p} {A : Set a} (P : A → Set p) : Maybe A → Set (a ⊔ p) where06/03 15:26
mietek  just    : ∀ {x} (px : P x) → All P (just x)06/03 15:26
mietek  nothing : All P nothing06/03 15:26
mietekThat is OBVIOUSLY in Data.Maybe06/03 15:26
{AS}mietek: oh06/03 15:26
* mietek glares at agda-stdlib06/03 15:27
{AS}so it can't infer that they have the _same_ type 06/03 15:27
mietekIt just doesn’t know what we mean by "just"06/03 15:27
mietekUnless we give it a hint06/03 15:28
mietekThat’s perfectly reasonable06/03 15:28
mietekThe design of the stdlib is less so06/03 15:28
{AS}mietek: Yeah, maybe the error message should be something easier to understand06/03 15:28
{AS}usually it complains when overloading06/03 15:28
mietekbyorgey: got it?06/03 15:29
mietekbyorgey: overloading. Sufficient to say Maybe.just and avoid the other noise.06/03 15:29
byorgeyhaha, I see, thanks!06/03 15:30
byorgeyperhaps I would have thought of that eventually but I'm not so sure =)06/03 15:30
mietekYou’re welcome. This should indeed be handled better 06/03 15:30
mietekMaybe open an issue on GitHub?06/03 15:30
mietekI think they’re sick of my issues by now06/03 15:30
byorgeyhttps://github.com/agda/agda-stdlib/issues/13306/03 16:20
byorgeySo do I understand correctly that Agda is willing to do type-based disambiguation of overloaded identifiers, but it just doesn't work here because it has no way to infer which 'just' we want?06/03 16:22
mietekYep06/03 16:23
mietekIdentifiers — no06/03 16:23
mietekJust constructors06/03 16:23
mietekI wish it did functions, too06/03 16:23
byorgeyah, got it06/03 16:25
rntzis there a way to quantify over strictly positive functions in agda?06/03 19:17
rntz(and use this when constructing inductive types?)06/03 19:18

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