--- Day changed Mon Jan 01 2018 | ||

robwebbjr | Hello; 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 |
---|---|---|

robwebbjr | Sorry, had a small typo in paste-bin -- fixed it now. | 01/01 00:20 |

mietek | robwebbjr: how did you come up with the type of `matrix-elt`? | 01/01 00:23 |

robwebbjr | Hi and thank you again. | 01/01 00:24 |

robwebbjr | I just thought about it? | 01/01 00:24 |

robwebbjr | I went by previous examples... | 01/01 00:25 |

mietek | oh, `tt` in this library is what’s usually written `true` | 01/01 00:26 |

robwebbjr | A good bit of trial and error, actually | 01/01 00:26 |

robwebbjr | yes | 01/01 00:26 |

mietek | well, your `matrix-elt` has 2 more arguments | 01/01 00:26 |

mietek | than what you’re passing in `matrix-elt 1 2 (zero-matrix 3 3)` | 01/01 00:27 |

robwebbjr | yes. this is how i understand hypothesis are provided as proofs -- required in the functions... | 01/01 00:28 |

mietek | so, why are you not passing in those arguments? | 01/01 00:28 |

mietek | https://github.com/williamdemeo/ial/blob/master/1.3/eq.agda#L9 | 01/01 00:29 |

mietek | there’s only one constructor for this type of equality | 01/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 |

mietek | so, why are you not passing in those arguments? | 01/01 00:30 |

mietek | https://github.com/williamdemeo/ial/blob/master/1.3/eq.agda#L9 | 01/01 00:30 |

mietek | there’s only one constructor for this type of equality | 01/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 |

mietek | you 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 context | 01/01 00:32 |

robwebbjr_ | ive only used refl in proofs of properties so far | 01/01 00:33 |

mietek | well…? | 01/01 00:33 |

robwebbjr_ | until now that is... | 01/01 00:33 |

mietek | what do you think is different? | 01/01 00:33 |

robwebbjr_ | yes it works perfectly, thank you | 01/01 00:33 |

mietek | I know it works; I’m asking why do you think this is a different situation | 01/01 00:34 |

robwebbjr_ | I can (basically) see that there is no difference, i only percieved a difference by lack of understanding | 01/01 00:34 |

robwebbjr_ | a matter of context i suppose | 01/01 00:35 |

mietek | can 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 |

mietek | let me try to clarify some things | 01/01 00:38 |

robwebbjr_ | please... | 01/01 00:39 |

mietek | it’s sometimes difficult to use the right words in a dependently typed language | 01/01 00:39 |

robwebbjr_ | YES | 01/01 00:39 |

mietek | your explanation above suggests you have a conceptual difference between “proving a property/proposition” and “writing a program/function” | 01/01 00:40 |

robwebbjr_ | ok | 01/01 00:40 |

mietek | I’m not sure what externally or internally mean to you | 01/01 00:40 |

mietek | I think it’s simplest to think of (1) types; (2) inhabitants of types. | 01/01 00:41 |

mietek | then, (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 A | 01/01 00:42 |

mietek | other people may have different views on this, but this helps me | 01/01 00:42 |

mietek | so, `rx < r ≡ tt` is a type, which we got based on the `_≡_` indexed type family | 01/01 00:43 |

mietek | in other words, `_≡_` is a function that returns a type | 01/01 00:43 |

mietek | you can see this in line 9: https://github.com/williamdemeo/ial/blob/master/1.3/eq.agda#L9 | 01/01 00:44 |

robwebbjr_ | a type like refl? | 01/01 00:44 |

mietek | `_≡_` takes an inhabitant of type `A`, and returns a type | 01/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 above | 01/01 00:45 |

mietek | in other words, `refl` is a proof of `x ≡ x`, if `x` is a proof of `A` | 01/01 00:46 |

mietek | it is the *only* proof | 01/01 00:46 |

mietek | so, 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 processing | 01/01 00:46 |

mietek | and obviously, since `refl` is the only possible proof, that’s what we need to pass there | 01/01 00:47 |

robwebbjr_ | fascinating... | 01/01 00:47 |

mietek | passing `refl` would not typecheck if `rx < r` was not in fact true | 01/01 00:47 |

robwebbjr_ | i really do love agda when i am not annoyed with it... | 01/01 00:47 |

mietek | you should read this: | 01/01 00:48 |

mietek | http://www.cse.chalmers.se/~abela/Equality.pdf | 01/01 00:48 |

robwebbjr_ | excellent | 01/01 00:49 |

robwebbjr_ | thank you for your great patience,<mietek> | 01/01 00:49 |

mietek | you’re welcome | 01/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 type | 01/01 02:03 |

mietek | mitch_: 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 however | 01/01 02:06 |

mietek | mitch_: 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 inferrable | 01/01 02:08 |

mietek | https://agda.github.io/agda-stdlib/Data.Nat.DivMod.html#1017 | 01/01 02:09 |

mietek | note the argument here is `{≢0 : False (divisor ≟ 0)}` | 01/01 02:09 |

mietek | while 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 |

mietek | but you’re using the negation of propositional equality, while the stdlib is using a converted form of decidable equality | 01/01 02:10 |

mietek | you can click the names in the HTML to see their definitions | 01/01 02:11 |

mietek | tl;dr: the argument used in the stdlib is inferable | 01/01 02:11 |

mitch_ | is it not the case that ¬ (y ≡ zero) is also inferrable? | 01/01 02:12 |

mietek | it’s a function | 01/01 02:12 |

mietek | I don’t think functions are inferable | 01/01 02:12 |

mietek | and also, what you call “weird autocomplete” is just telling you that there’s one more implicit argument that you could bind | 01/01 02:13 |

mitch_ | ah true; something like (y ≡ zero) would be inferrable. i still need to understand ¬_ better | 01/01 02:13 |

mietek | https://agda.github.io/agda-stdlib/Relation.Nullary.html#414 | 01/01 02:13 |

mietek | ¬ P = P → ⊥ | 01/01 02:13 |

mietek | it’s intuitionistic negation: P leads to absurdity | 01/01 02:14 |

mietek | or, implies absurdity | 01/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 P | 01/01 02:14 |

mietek | not quite | 01/01 02:15 |

mietek | https://agda.github.io/agda-stdlib/Data.Empty.html#360 | 01/01 02:15 |

mietek | if we already have a proof of ⊥, we can have a proof of anything, including P | 01/01 02:16 |

mietek | it should be the case that the only way we could have a proof of ⊥ is if we’ve assumed it | 01/01 02:16 |

fsestini | mitch_: that is true in the empty context | 01/01 02:16 |

mietek | where by “context” we mean all the definitions up to now | 01/01 02:17 |

mietek | `postulate oops : ⊥` | 01/01 02:18 |

mietek | we could also find another bug in Agda… | 01/01 02:19 |

mietek | https://twitter.com/i/moments/921153475836305408 | 01/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/z02e | 01/01 02:25 |

mietek | mitch_: that’s effectively what the stdlib is doing :) | 01/01 02:25 |

mietek | except 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 made | 01/01 02:26 |

mietek | indeed | 01/01 02:26 |

mitch_ | example, why an extra level is included here: https://agda.github.io/agda-stdlib/Relation.Binary.Core.html#614 | 01/01 02:27 |

mietek | excellent question; I don’t know | 01/01 02:27 |

mietek | I don’t use the stdlib | 01/01 02:27 |

mietek | except as inspiration | 01/01 02:27 |

mietek | I think it’s a very good idea to write your own analogues, keeping them as simple as possible | 01/01 02:28 |

mietek | if you simplify away something you don’t understand, make a note | 01/01 02:29 |

mietek | then, later, when you find yourself inexplicably unable to prove something… | 01/01 02:29 |

fsestini | mitch_: could be so to have REL A B polymorphic over its sort | 01/01 02:39 |

fsestini | otherwise i guess you would be stuck with the level computed from A and B’s, and lift it in other ways if you needed to | 01/01 02:40 |

fsestini | universe polymorphism is cool, but sometimes the coq/idris approach is easier to work with | 01/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 ops | 01/01 10:11 |

lambdabot | byorgey Cale conal copumpkin dcoutts dibblego dolio edwardk geekosaur glguy jmcarthur johnw monochrom quicksilver shachaf shapr ski | 01/01 10:11 |

shachaf | It's been 4 hours and that's not even the right op list. | 01/01 10:12 |

comietek | it is possible to set a flag for the channel that requires being registered with NickServ to join | 01/01 10:13 |

comietek | r on the list https://freenode.net/kb/answer/channelmodes | 01/01 10:16 |

pgiarrusso | mitch_: not sure if that’s what fsestini meant, but REL A B might need to be on a bigger level than A and B | 01/01 12:31 |

pgiarrusso | mitch_: 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 though | 01/01 12:36 |

pgiarrusso | mitch_: `StrangeEquiv (A B: Set) = \forall C: Set -> (A <-> C) <-> (B <-> C)` | 01/01 12:45 |

pgiarrusso | that lives in `Set1`, is not an overly natural idea (so maybe it’s not so good), but to me it makes *some* sense | 01/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 equivalent | 01/01 12:46 |

mitch_ | ah, i see; thanks for that pgiarrusso | 01/01 12:53 |

robwebbjr | 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: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 quit | 01/01 16:47 |

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 17:15 |

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