--- Day changed Mon Jan 01 2018
robwebbjrHello; back again... Would you please help me with another exercise from stump's text? My question is here: http://lpaste.net/360556 Thank you.01/01 00:17
robwebbjrSorry, had a small typo in paste-bin -- fixed it now.01/01 00:20
mietekrobwebbjr: how did you come up with the type of `matrix-elt`?01/01 00:23
robwebbjrHi and thank you again.01/01 00:24
robwebbjrI just thought about it?01/01 00:24
robwebbjrI went by previous examples...01/01 00:25
mietekoh, `tt` in this library is what’s usually written `true`01/01 00:26
robwebbjrA good bit of trial and error, actually01/01 00:26
robwebbjryes01/01 00:26
mietekwell, your `matrix-elt` has 2 more arguments01/01 00:26
mietekthan what you’re passing in `matrix-elt 1 2 (zero-matrix 3 3)`01/01 00:27
robwebbjryes. this is how i understand hypothesis are provided as proofs -- required in the functions...01/01 00:28
mietekso, why are you not passing in those arguments?01/01 00:28
mietekhttps://github.com/williamdemeo/ial/blob/master/1.3/eq.agda#L901/01 00:29
mietekthere’s only one constructor for this type of equality01/01 00:29
mietek`matrix-elt 1 2 (zero-matrix 3 3) refl refl`01/01 00:30
robwebbjr_sorry, im on public wifi...where were we?01/01 00:30
mietekso, why are you not passing in those arguments?01/01 00:30
mietekhttps://github.com/williamdemeo/ial/blob/master/1.3/eq.agda#L901/01 00:30
mietekthere’s only one constructor for this type of equality01/01 00:31
mietek`matrix-elt 1 2 (zero-matrix 3 3) refl refl`01/01 00:31
robwebbjr_oh, ok, I didn't know that...01/01 00:31
robwebbjr_let me try it...01/01 00:32
robwebbjr_YEAAAHHHH!!01/01 00:32
mietekyou didn’t know how to give an inhabitant of the equality type?01/01 00:32
robwebbjr_right. I didn't understand to pass refl in this context01/01 00:32
robwebbjr_ive only used refl in proofs of properties so far01/01 00:33
mietekwell…?01/01 00:33
robwebbjr_until now that is...01/01 00:33
mietekwhat do you think is different?01/01 00:33
robwebbjr_yes it works perfectly, thank you01/01 00:33
mietekI know it works; I’m asking why do you think this is a different situation01/01 00:34
robwebbjr_I can (basically) see that there is no difference, i only percieved a difference by lack of understanding01/01 00:34
robwebbjr_a matter of context i suppose01/01 00:35
mietekcan you say what made you think there was a difference?01/01 00:35
robwebbjr_ok, so in proving an property externally, i was equating some statement with the value refl, whille here, internal to a function i was not doing that so i made no connection. MORE..01/01 00:37
robwebbjr_however, now i see that i am not eguating as refl is not a value, but rather giving a justification for the proposition being true.01/01 00:38
mieteklet me try to clarify some things01/01 00:38
robwebbjr_please...01/01 00:39
mietekit’s sometimes difficult to use the right words in a dependently typed language01/01 00:39
robwebbjr_YES01/01 00:39
mietekyour explanation above suggests you have a conceptual difference between “proving a property/proposition” and “writing a program/function”01/01 00:40
robwebbjr_ok01/01 00:40
mietekI’m not sure what externally or internally mean to you01/01 00:40
mietekI think it’s simplest to think of (1) types; (2) inhabitants of types.01/01 00:41
mietekthen, (1) a type is equivalent to a proposition; (2) a program with the type A is equivalent to a proof of the proposition equivalent to A01/01 00:42
mietekother people may have different views on this, but this helps me01/01 00:42
mietekso, `rx < r ≡ tt` is a type, which we got based on the `_≡_` indexed type family01/01 00:43
mietekin other words, `_≡_` is a function that returns a type01/01 00:43
mietekyou can see this in line 9: https://github.com/williamdemeo/ial/blob/master/1.3/eq.agda#L901/01 00:44
robwebbjr_a type like refl?01/01 00:44
mietek`_≡_` takes an inhabitant of type `A`, and returns a type01/01 00:45
mietek`refl` is an inhabitant of `x ≡ x`, where `x` is the inhabitant of `A` that I just mentioned in the line above01/01 00:45
mietekin other words, `refl` is a proof of `x ≡ x`, if `x` is a proof of `A`01/01 00:46
mietekit is the *only* proof01/01 00:46
mietekso, in your invocation of `matrix-elt`, you’re supposed to supply proofs of `rx < r ≡ tt` and `cx < c ≡ tt`01/01 00:46
robwebbjr_ok processing01/01 00:46
mietekand obviously, since `refl` is the only possible proof, that’s what we need to pass there01/01 00:47
robwebbjr_fascinating...01/01 00:47
mietekpassing `refl` would not typecheck if `rx < r` was not in fact true01/01 00:47
robwebbjr_i really do love agda when i am not annoyed with it...01/01 00:47
mietekyou should read this:01/01 00:48
mietekhttp://www.cse.chalmers.se/~abela/Equality.pdf01/01 00:48
robwebbjr_excellent01/01 00:49
robwebbjr_thank you for your great patience,<mietek>01/01 00:49
mietekyou’re welcome01/01 00:49
robwebbjr_ok, i'll go have a look at all you've provided.01/01 00:50
mitch_could someone help me to understand why this definition for nat. modulus doesnt work? http://termbin.com/kbg5 due to the weird autocomplete for (x mod zero) im guessing it must be related to the type01/01 02:03
mietekmitch_: did you write it yourself?01/01 02:05
mitch_mietek, that is my attempt at writing a proper modulus function, yes; i did have a peek through some other code from stdlib however01/01 02:06
mietekmitch_: can you say why did you use two explicit arguments and one implicit argument?01/01 02:06
mitch_implicit was actually due to noticing that in Data.Nat.DivMod (from stdlib), implicit was used there; that, and i thought that it should be inferrable01/01 02:08
mietekhttps://agda.github.io/agda-stdlib/Data.Nat.DivMod.html#101701/01 02:09
mieteknote the argument here is `{≢0 : False (divisor ≟ 0)}`01/01 02:09
mietekwhile you’ve used `{≠0 : ¬ (y ≡ zero)}`01/01 02:09
mietek`0` is the same as `zero`01/01 02:10
mitch_im not super well versed w/ stdlib, but ≟ is a decidable, right?01/01 02:10
mietekbut you’re using the negation of propositional equality, while the stdlib is using a converted form of decidable equality01/01 02:10
mietekyou can click the names in the HTML to see their definitions01/01 02:11
mietektl;dr: the argument used in the stdlib is inferable01/01 02:11
mitch_is it not the case that ¬ (y ≡ zero) is also inferrable?01/01 02:12
mietekit’s a function01/01 02:12
mietekI don’t think functions are inferable01/01 02:12
mietekand also, what you call “weird autocomplete” is just telling you that there’s one more implicit argument that you could bind01/01 02:13
mitch_ah true; something like (y ≡ zero) would be inferrable. i still need to understand ¬_ better01/01 02:13
mietekhttps://agda.github.io/agda-stdlib/Relation.Nullary.html#41401/01 02:13
mietek¬ P = P → ⊥01/01 02:13
mietekit’s intuitionistic negation: P leads to absurdity01/01 02:14
mietekor, implies absurdity01/01 02:14
mitch_so, if you had a proof of P, you could construct a proof of ⊥, hence you can't produce a proof of P01/01 02:14
mieteknot quite01/01 02:15
mietekhttps://agda.github.io/agda-stdlib/Data.Empty.html#36001/01 02:15
mietekif we already have a proof of ⊥, we can have a proof of anything, including P01/01 02:16
mietekit should be the case that the only way we could have a proof of ⊥ is if we’ve assumed it01/01 02:16
fsestinimitch_: that is true in the empty context01/01 02:16
mietekwhere by “context” we mean all the definitions up to now01/01 02:17
mietek`postulate oops : ⊥`01/01 02:18
mietekwe could also find another bug in Agda…01/01 02:19
mietekhttps://twitter.com/i/moments/92115347583630540801/01 02:19
mitch_mietek, thanks for the help; i think i just need to avoid trying to use more complex constructs before i properly understand them. i dropped back to a more simple approach and it seems to be working alright: http://termbin.com/z02e01/01 02:25
mietekmitch_: that’s effectively what the stdlib is doing :)01/01 02:25
mietekexcept as the stdlib usually does, it goes through multiple layers of functions…01/01 02:25
mitch_it is quite difficult to follow through at times. i've been toying around with writing my own analogues to stdlib-provided types/functions to try to understand it better, but its often quite difficult to understand exactly why some choices were made01/01 02:26
mietekindeed01/01 02:26
mitch_example, why an extra level is included here: https://agda.github.io/agda-stdlib/Relation.Binary.Core.html#61401/01 02:27
mietekexcellent question; I don’t know01/01 02:27
mietekI don’t use the stdlib01/01 02:27
mietekexcept as inspiration01/01 02:27
mietekI think it’s a very good idea to write your own analogues, keeping them as simple as possible01/01 02:28
mietekif you simplify away something you don’t understand, make a note01/01 02:29
mietekthen, later, when you find yourself inexplicably unable to prove something…01/01 02:29
fsestinimitch_: could be so to have REL A B polymorphic over its sort01/01 02:39
fsestiniotherwise i guess you would be stuck with the level computed from A and B’s, and lift it in other ways if you needed to01/01 02:40
fsestiniuniverse polymorphism is cool, but sometimes the coq/idris approach is easier to work with01/01 02:42
loyaldeath893▄▄▄▄▄▄▄▄▄▄▄▄▄▄ A DISCUSSION IS GOING ON ABOUT TO TO RE-ENSLAVE NIGGERS IN #/JOIN IF THIS GETS YOUR DICK HARD JOIN IN (MESSAGE VAP0R FOR HELP) bsqcmb: milessabin adamse {AS} ▄▄▄▄▄▄▄▄▄▄▄▄▄▄01/01 06:15
comietek@where ops01/01 10:11
lambdabotbyorgey Cale conal copumpkin dcoutts dibblego dolio edwardk geekosaur glguy jmcarthur johnw monochrom quicksilver shachaf shapr ski01/01 10:11
shachafIt's been 4 hours and that's not even the right op list.01/01 10:12
comietekit is possible to set a flag for the channel that requires being registered with NickServ to join01/01 10:13
comietekr on the list https://freenode.net/kb/answer/channelmodes01/01 10:16
pgiarrussomitch_:  not sure if that’s what fsestini meant, but REL A B might need to be on a bigger level than A and B01/01 12:31
pgiarrussomitch_: for instance, if `A` and `B` are on level `l`, and a relation between them quantifies over all `C : Set l`, that relation will be at level `suc l`01/01 12:32
mitch_pgiarrusso, understandable; i think i just need to see an example of a relation in which the result needs to be on a bigger level than any of the two inputs. im sure i'll eventually come across it while reading through the stdlib though01/01 12:36
pgiarrussomitch_: `StrangeEquiv (A B: Set) = \forall C: Set -> (A <-> C) <-> (B <-> C)`01/01 12:45
pgiarrussothat lives in `Set1`, is not an overly natural idea (so maybe it’s not so good), but to me it makes *some* sense01/01 12:45
pgiarrusso`A` and `B` are “equivalent” if for all `C`, `A` and `C` are equivalent if and only if `B` and `C` are equivalent01/01 12:46
mitch_ah, i see; thanks for that pgiarrusso 01/01 12:53
robwebbjrHello. Would you please help me with an exercise from stump's text? My question is here: http://lpaste.net/360556 and has to do with making an identity matrix. Thank you. Please note that I have a sketchy internet connection, but if I get dropped, I will be back. Thanks.01/01 16:34
robwebbjr_Sorry, I got dropped. Reposting: Hello. Would you please help me with an exercise from stump's text? My question is here: http://lpaste.net/360556 and has to do with making an identity matrix. Thank you. Please note that I have a sketchy internet connection, but if I get dropped, I will be back. Thanks.01/01 16:43
robwebbjr_i did not quit01/01 16:47
robwebbjrSorry, I got dropped. Reposting: Hello. Would you please help me with an exercise from stump's text? My question is here: http://lpaste.net/360556 and has to do with making an identity matrix. Thank you. Please note that I have a sketchy internet connection, but if I get dropped, I will be back. Thanks.01/01 17:15

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