--- Day changed Thu May 11 2017
rgrinbergthanks gallais_ 11/05 00:07
rgrinbergwhy can't i write a type signature as follows: x : reverse [] \== []11/05 00:08
rgrinbergi know it's not a very useful type, but i'm still curious11/05 00:08
mietekwhat do you mean by "can't"?11/05 00:09
rgrinbergwell when I write that type and x = refl11/05 00:11
rgrinbergemacs highlights the type for me signaling that it's  an error11/05 00:11
mietekdid you get an error message?11/05 00:12
rgrinberghmm no. but it still gets highlighted11/05 00:13
mietekthat just means Agda couldn’t figure something out11/05 00:13
mietekwhat did you intend [] to be?11/05 00:14
rgrinbergthe empty list. i.e. the constructor from Data.List11/05 00:14
mietekwhat type, precisely?11/05 00:15
rgrinberghmm, I guess i'm not sure11/05 00:19
rgrinbergi want this to hold any list obviously, but i'm not sure how to write the type11/05 00:20
mietekwell, look how Data.List is defined11/05 00:20
mietekhttps://agda.github.io/agda-stdlib/Data.List.Base.html#111/05 00:20
mietekhttps://agda.github.io/agda-stdlib/Agda.Builtin.List.html#11711/05 00:20
mietek{a} is a universe level11/05 00:21
mietekx : forall {a} {A : Set a} -> reverse [] \== ([] {a} {A})11/05 00:22
mietekjust guessing11/05 00:22
mietekyou could also show this for the universe of small types11/05 00:22
mietekoops, there was a typo above11/05 00:23
mietekbut you’ll figure it out11/05 00:23
mietekx : forall {A : Set} -> reverse [] \== ...11/05 00:23
rgrinbergx : ∀{l}{A : Set l} -> reverse ([] {l} {A}) ≡ ([] {l} {A})11/05 00:23
rgrinbergthis works, thanks11/05 00:23
mietekyou should only need to say this on one side11/05 00:24
mietekno?11/05 00:24
rgrinbergHow would I drop something like this on lists: drop1 : ∀{l}{A : Set l}(x : A)(xs : List A) -> drop (suc zero) (x ∷ xs) ≡ xs11/05 07:25
rgrinbergI know it's trivial on vectors, but here i'm puzzled11/05 07:26
{AS}rgrinberg: Shouldn't this hold by definition of 'drop'? :)11/05 08:37
rgrinbergit should, but it doesn't :/11/05 08:38
{AS}how are you defining drop?11/05 08:41
rgrinberghttps://gist.github.com/rgrinberg/111da9db6229d23c91c93fa263639c4511/05 08:43
{AS}rgrinberg: you need to pattern match on xs11/05 08:43
{AS}in the second case11/05 08:44
rgrinberghaha yes11/05 08:44
rgrinberghitting that agda2-auto key a little fast11/05 08:44
yhhkoi'm using agda reflection. what methods are available for testing if two Terms are equal? it doesn't matter if it's not perfect11/05 12:55
gallais_yhhko: https://github.com/agda/agda-stdlib/blob/master/src/Reflection.agda#L455 ?11/05 13:50
yhhkogallais_: yes, something like that! thanks! :)11/05 13:51
yhhkodid agda ever get mutual recursion between modules?11/05 15:05
rgrinbergis it true that anything I can prove with cong, I can also prove rewrite?11/05 17:48
rgrinbergs/rewrite/with rewrite/11/05 17:48
mietekrgrinberg: perhaps you should try proving that…11/05 17:49
mietek:)11/05 17:49
rgrinbergmietek: good idea. I think I need some help with a starting point though. what would the proposition look like?11/05 17:50
mietekI would be surprised if one could express it in Agda11/05 17:50
mietekI’m not certain about the reach of Agda’s reflective capabilities11/05 17:51
rgrinbergoh, you meant the "old" way11/05 17:51
rgrinbergby hand that is :P11/05 17:51
mietekI’m actually in a discussion in another channel on the expressiveness of mathematical meta-languages11/05 17:51
mietek{AS}: ^^11/05 17:51
mietekand so, I only really mean to point out that we’re not quite there yet11/05 17:51
rgrinbergmietek: but is the statement true or not btw?11/05 17:52
mietekI don’t know11/05 17:52
mietekI would expect the converse to hold11/05 17:52
{AS}rgrinberg: rewrite is more powerful11/05 17:53
rgrinbergreally? I originally thought that rewrite is more powerful11/05 17:53
mietekhuh.11/05 17:53
rgrinberg{AS}: read my mind11/05 17:53
{AS}Rewrite is equivalent to subst11/05 17:54
mietekI thought rewrite desugars to Agda-without-rewrite11/05 17:54
mietekso it cannot be more powerful11/05 17:54
{AS}mietek: it does11/05 17:54
{AS}It's more powerful than cong, not subst :)11/05 17:54
mietekI think pgiarrusso told me once that any subst can be written as a cong11/05 17:54
{AS}It can?11/05 17:54
{AS}Hmm11/05 17:54
mietekI may be misremembering11/05 17:55
{AS}Maybe he can answer when he is here :)11/05 17:57
mietekcan’t find it in my logs so I may be wrong11/05 18:03
pgiarrussorgrinberg: for one step of cong, that's typically true11/05 18:13
pgiarrussomietek: if I said that, I forgot why11/05 18:13
rgrinbergpgiarrusso: I see, thanks.11/05 18:14
rgrinbergis there anyway to prove anything about rewrite from inside agda?11/05 18:14
pgiarrussoI'd first look at http://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html#rewrite and http://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html#technical-details11/05 18:15
pgiarrussorgrinberg, 11/05 18:15
rgrinbergOK, will check those out11/05 18:15
pgiarrussorgrinberg: that helps understanding rewrite. For proofs... I understand nobody mechanized full or core Agda anywhere, even on paper, so proofs on it might be hard...11/05 18:17
mietekhttp://agda.readthedocs.io/en/v2.5.2/language/reflection.html11/05 18:17
mietekrewrite is not mentioned11/05 18:17
mietekand the reflection machinery may or may not be sound11/05 18:18
mietek;)11/05 18:18
pgiarrussomietek: I'd wonder if reflection works on the desugared form of rewrite?11/05 18:18
mietekcould be; I don’t know11/05 18:18
pgiarrussomietek: a function is just a list of clauses, so that must be the desugared form. *If* docs are accurate and reflection works, of course :-)11/05 18:21
mietek…and if reflecting on things can happen after desugaring11/05 18:22
mietekor elaborating, or whatever it’s called11/05 18:22
mietekI mean, you could probably use reflection to prove properties of what you *think* rewrite will desugar to11/05 18:23
mietekif you state that desugared form manually11/05 18:23
mietekbut to connect to the actual `rewrite` operator in the language, I don’t know11/05 18:24
pgiarrussoexactly11/05 18:25
{AS}Hmm, but proving properties about things which use rewrite is easier than those that use subst directly?11/05 18:26
pgiarrusso{AS}: metalevel proofs on rewrite are harder, but you mean object-level right?11/05 18:29
{AS}pgiarrusso: Yeah, exactly11/05 18:30
pgiarrusso{AS}: that is, if foo is defined with rewrite, how do you do proofs on foo?11/05 18:30
{AS}So if you have a function that uses rewrite11/05 18:30
{AS}pgiarrusso: sec, I am doing an example11/05 18:30
pgiarrussothink I know what you mean11/05 18:30
pgiarrussoI expect you'll need sometimes `with` in the proof11/05 18:30
pgiarrussoas usual with functions defined with `with`11/05 18:31
{AS}pgiarrusso: So if you use subst one has to use that subst== lemma11/05 18:31
mietekpgiarrusso: yes, and that becomes really irritating fast11/05 18:31
{AS}https://github.com/agda/agda-stdlib/blob/ac6a3bd774e2d50309649090321b247aaa5c6932/Relation/Binary/PropositionalEquality.agda#L2411/05 18:32
{AS}This one11/05 18:32
pgiarrussomietek: at least Agda tells you what to match on11/05 18:32
mieteksort of11/05 18:32
{AS}I think with rewrite it will automatically rewrite, so you don't have to handle subst on the right hand side11/05 18:32
mietekyou will get holes with like "... | condition" on the right11/05 18:32
pgiarrussomietek: exactly, so add `with condition` :-)11/05 18:33
mietekand how do you write something of that type by hand?11/05 18:33
mietekwhere?11/05 18:33
mietekinside the hole?11/05 18:33
mietekno.11/05 18:33
pgiarrussoyes, left-hand side11/05 18:33
mietekleft-hand side of the equation that is the parent of the term which has a hole?11/05 18:33
pgiarrussoyes11/05 18:33
mietekI can’t recall a specific case now, but I’m not sure if this always helps11/05 18:33
pgiarrusso(a) you need to case-split on the result11/05 18:34
pgiarrusso(b) if the `with` produces ill-typed code, it's lots of fun (not sure how to deal with that)11/05 18:34
pgiarrussoI mean http://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html#ill-typed-with-abstractions11/05 18:34
pgiarrusso{AS}: `rewrite` desugars to `with` and follows the usual reduction semantics, so it depends on which actual definitional equalities you have available11/05 18:36
{AS}pgiarrusso: Ah, thanks :)11/05 18:36
pgiarrussotook me years to get why people talk about "which definitions reduce"11/05 18:37
mietekgo on?11/05 18:37
mietekpgiarrusso: you mean ones that don’t depend on postulates?11/05 18:37
pgiarrussomietek: I mean things unlike `n + 0` :-)11/05 18:38
mieteknot getting it11/05 18:38
mietekyou mean things that aren’t seen by Agda as definitionally equal?11/05 18:38
{AS}mietek: why "n+0" does not reduce unlike "0+n"11/05 18:38
pgiarrussoYes11/05 18:38
pgiarrussosorry, I should have said11/05 18:38
pgiarrusso"which *expressions* reduce"11/05 18:39
mietekhm11/05 18:39
mietekif you ask Agda explicitly to normalise "n+0" and "0+n"…11/05 18:39
mietekas I am about to11/05 18:39
pgiarrusson + 0 is a normal form11/05 18:40
pgiarrussoexercise: why?11/05 18:40
pgiarrussohint: equations are `0 + n = n` and `(S m) + n = S (m + n)`11/05 18:40
{AS}because n and 0 are neutral11/05 18:41
mietekbefore you get into that, consider your wording11/05 18:41
pgiarrussohence, think of `n + 0` as `n + 0 | n`11/05 18:41
pgiarrussolike with `with`11/05 18:41
pgiarrussoAgda can't reduce `n + 0` without knowing which `n` is11/05 18:41
pgiarrussomietek: my wording might sure be sloppy, sorry, no clue where11/05 18:42
mietekboth "n + 0" and "0 + n" reduce perfectly well if "n" is known, that is, *not a postulate*, as I’ve said11/05 18:43
mietekor assumption11/05 18:43
pgiarrussomietek: by `n` I meant an object variable11/05 18:44
pgiarrussoor an assumption, if you want :-)11/05 18:44
pgiarrussobut as {AS} said, any neutral will do11/05 18:44
mietekyes11/05 18:44
pgiarrussoBUT `0 + n` also reduces if `n` is neutral :-)11/05 18:45
{AS}I think computational systems in this case are superior 11/05 18:45
pgiarrusso{AS}: computational systems = ?11/05 18:45
{AS}I meant something like CTT11/05 18:45
mietek:)11/05 18:45
{AS}*PRL 11/05 18:46
pgiarrusso{AS}: I know SMT solvers lack this problem (but have others), but why is *PRL better?11/05 18:46
pgiarrussobecause you don't have to write `subs`?11/05 18:47
pgiarrusso* `subst` ?11/05 18:47
pgiarrussothat's the "extensional type theory" part11/05 18:47
{AS}Equality reflection11/05 18:47
mietekbecause nobody can determine for themselves whether they’re good or not11/05 18:47
pgiarrussoyes11/05 18:47
{AS}Yeah11/05 18:47
mietek;)11/05 18:47
pgiarrussomietek: ?11/05 18:47
pgiarrussobut then CTT has lots of other differences11/05 18:47
mietekpgiarrusso: poor joke; how do I run NuPRL11/05 18:48
{AS}pgiarrusso: Yeah, which is why I also said only in this case :)11/05 18:48
pgiarrussomietek: ah OK11/05 18:48
{AS}mietek: You download the virtual machine11/05 18:48
pgiarrusso{AS}: is there one? I though jonsterling tried really hard, failed, and decided to rewrite NuRPL as *PRL11/05 18:48
mietek{AS}: have you done that?11/05 18:49
{AS}mietek: I have not11/05 18:49
mietekI see http://www.nuprl.org/vms/ and it does not look inviting, but I will try11/05 18:49
pgiarrussowow hadn't seen THAT!11/05 18:49
pgiarrussothe problem, IIUC, is that NuPRL is *ALSO* a distributed systems maintaining a knowledge base11/05 18:50
pgiarrusso*Anyway*, back to Agda11/05 18:51
{AS}pgiarrusso: I think they only released it publicly recently11/05 18:51
pgiarrusso{AS}: makes sense, but that's dated 2015...11/05 18:52
mietekhttp://www.nuprl.org/FAQ/Connecting-to-nuprl-servers.html11/05 18:52
pgiarrussoanyway, JonPRL/RedPRL are probably easier to install11/05 18:52
pgiarrussomietek: yeah, found that too11/05 18:52
pgiarrusso{AS}: actually, writing untyped realizers and proving they're well-typed *can* be more flexible11/05 18:52
mietekit feels wrong11/05 18:52
mietekit feels like too much work11/05 18:53
mietekwhy do all that if you could be correct by construction?11/05 18:53
{AS}mietek: Why is *PRL not correct by construction? :)11/05 18:54
pgiarrusso{AS}: *untyped realizers* ;-)11/05 18:54
{AS}I see 11/05 18:54
pgiarrussomietek: in my PhD thesis, being correct by construction appears to add significant overhead to my proof11/05 18:54
mietekpgiarrusso: is it overhead if you wouldn’t know if you are correct otherwise?11/05 18:55
mietekI would argue the right way to move forward is to improve the language so that such overhead can be minimised11/05 18:55
mietekwithout leaving the correct-by-construction world11/05 18:55
{AS}mietek: They have build a compiler in Coq11/05 18:56
{AS}for C11/05 18:56
{AS}with multiple passes11/05 18:56
{AS}The experience I got when talking to the Coq people was this would be hard in Agda11/05 18:57
pgiarrusso{AS}: Are those Coq people also familiar with Agda?11/05 18:57
mietek{AS}: what is your point?11/05 18:57
pgiarrussomietek: maybe, eventually, but this is like postulating a sufficiently smart compiler. It's still a good eventual goal.11/05 18:57
mietekAgda runs out of CPU if I type too fast on the keyboard11/05 18:58
mietekthat may be mostly emacs fault, nevertheless11/05 18:58
mieteknobody is saying that what we have is good11/05 18:58
pgiarrusso{AS}: Coq vs agda is most often about tactics vs proof terms11/05 18:58
pgiarrussobut in both you can be "correct by construction"11/05 18:59
pgiarrussoHowever, Agda has better support for pattern matching, which sometimes compensates the lack of tactics11/05 18:59
mietekpgiarrusso: it’s more about focusing the energy of research11/05 18:59
{AS}pgiarrusso: Yeah, but I meant, they do all the proofs externally11/05 18:59
mietekpgiarrusso: but of course, people work on what interests them11/05 18:59
{AS}instead of building the right structure11/05 18:59
mietek{AS}: ?11/05 19:00
{AS}so they define ML-like programs in Coq11/05 19:00
{AS}almost no dependent types11/05 19:00
{AS}and then write the properties they want to verify externally11/05 19:00
mietek"externally" meaning what?11/05 19:00
pgiarrusso{AS}: for some reason, that's typical in Coq11/05 19:00
{AS}mietek: meaning that they write something like a sorting function returning a normal array11/05 19:01
pgiarrussomietek: separate definitions and proofs :-)11/05 19:01
{AS}and the prove something like : \forall arr -> sorted (sort arr)11/05 19:01
{AS}Yeah, what pgiarrusso said11/05 19:01
pgiarrussomietek: compare well-scoped or well-typed deBruijn indexes with raw naturals.11/05 19:01
pgiarrussoor vectors indexed by their length vs raw lists11/05 19:02
mietekthey are both internal object-level definitions formalised within Coq11/05 19:02
mietekI’m not sure why {AS} thinks that is possible in Coq and not in Agda11/05 19:02
pgiarrussomietek: yeah, another sense of "external"11/05 19:02
{AS}mietek: The tactics style of proving helps a lot11/05 19:02
pgiarrussomietek: Coq users are much more likely to use the second style and not the first11/05 19:02
mietekpgiarrusso: sure11/05 19:03
mietek{AS}: sure11/05 19:03
mietekagain, your point?11/05 19:03
mietekCoq is currently easier to use for certain tasks than Agda11/05 19:03
mietekgranted11/05 19:03
{AS}That correct by construction is fairly difficult11/05 19:03
{AS}since you have to maintain your invariants throughout11/05 19:03
pgiarrusso{AS}: agreed, sometimes.11/05 19:03
mietekbut… you are being correct by construction *by virtue of using Coq*11/05 19:03
mietekwe have a miscommunication about meta-levels11/05 19:04
mietekall confusion is meta-level confusion11/05 19:04
{AS}mietek: Prop allows you to do classical proofs11/05 19:04
pgiarrussomietek: yes, we're confusing things.11/05 19:04
pgiarrussobut what {AS} is saying is relevant to "untyped realizers"11/05 19:04
mietekbut if you use Coq to model untyped whatevers, you are still better off than if you use a *PRL (as far as I understand…)11/05 19:05
pgiarrussothere's a spectrum from "untyped lambda calculus" through "normal types" to "dependent types"11/05 19:05
mietekwhere untyped whatevers are primitive11/05 19:05
mietek(I may be wrong here as I still haven’t used *PRL)11/05 19:05
pgiarrussoto the left, you define operations and separately prove them correct11/05 19:06
pgiarrussoto the right, more of the correctness proof is embedded in the definition11/05 19:06
mietekwhat do you use to prove untyped LC programs correct?11/05 19:06
pgiarrussomietek: ?11/05 19:07
pgiarrussoall of those styles are possible in the same languag11/05 19:07
pgiarrusso*language11/05 19:07
{AS}mietek: Also, to note. I think a typical argument is that the realizers are primitive but simple to understand11/05 19:07
mietekpgiarrusso: what?11/05 19:08
{AS}While Coq/Agda/Idris's type checkers are complicated11/05 19:08
mietekpgiarrusso: you just said, there’s a spectrum.11/05 19:08
mietekpgiarrusso: let’s be concrete and say, untyped LC, STLC, MLTT11/05 19:08
mietekpgiarrusso: I can write a MLTT program and be sure that it is correct to the extend that I’ve specified in its type.11/05 19:09
{AS}mietek: You use rewriting logic :)11/05 19:09
mietekpgiarrusso: this is what I understand as correct-by-construction: because MLTT would not type-check my program otherwise.11/05 19:09
mietekpgiarrusso: how do I achieve a comparable result in untyped LC?11/05 19:10
{AS}or any computation logic11/05 19:10
mietekpgiarrusso: obviously I cannot be correct-by-construction: as you said, I have to use something external to untyped LC.11/05 19:10
mietekpgiarrusso: I’m asking, what specifically could I use?11/05 19:10
mieteks/extend/extent/11/05 19:10
pgiarrussomietek: *PRL has some dependently-typed answer11/05 19:10
pgiarrussolet me avoid debating *PRL details11/05 19:11
pgiarrussowhat I *can* say is the following11/05 19:11
pgiarrussoI love correct-by-construction11/05 19:11
pgiarrussoBut take11/05 19:12
pgiarrusso> I can write a MLTT program and be sure that it is correct to the extend that I’ve specified in its type.11/05 19:12
lambdabot <hint>:1:93: error: parse error on input ‘in’11/05 19:12
mietek:D11/05 19:12
pgiarrussoI often find that if I specify too much in the type, writing the definition becomes either impossible or harder than otherwise11/05 19:12
pgiarrusso*some* of that might be due to limited tools11/05 19:13
pgiarrussoso we should re-evaluate when we get better tools, and people are welcome to write them11/05 19:13
mietekyes.11/05 19:13
pgiarrussobut sometimes, the best way to prove "P(X)" and "P(Y)" is not a fixed set of inference rules11/05 19:14
pgiarrusso(that is, a type system)11/05 19:15
pgiarrussoin a few minutes I can maybe contribute some specific example for Agda11/05 19:15
pgiarrussotying back to our discussion11/05 19:15
pgiarrusso*PRL makes many proofs external to terms, Agda users tend to add more in their types, Coq users are in between11/05 19:16
jonsterlingI think correct by construction is the ultimate goal (and that we can in practice mitigate efficiency issues); but there are times when we do not yet know a logical explanation of some phenomenon, and it is nice to be able to resort to a computational or semantical explanation in those cases.  For instance, consider the case of computational effects...11/05 19:16
jonsterlingThe practice in prl of working mostly extrinsically is also a side effect of it's old fashioned/underpowered proof refinement apparatus. using modern techniques, we can recover a more correct-by-construction development style, but with escape hatches allowing semantical reasoning wherever it is needed.11/05 19:17
pgiarrussojonsterling: thanks for your contributions :-)11/05 19:20
pgiarrusso(and I didn't mean to be ironic, sorry if it sounded otherwise)11/05 19:22
pgiarrussomietek: on the power of `with` in practice to allow `foo | bar` to reduce, by matching on `bar`, this is an (failed) proof where `with` is very successful https://github.com/inc-lc/ilc-agda/blob/master/Thesis/FunBigStepSILR.agda#L241-L27111/05 19:22
jonsterling:)11/05 19:22
pgiarrussoOn intrinsical vs extrinsical proofs, I've failed some proofs (in part) because I used well-typed de Bruijn indexes11/05 19:23
pgiarrussoHere's an example where intrinsic typing seems to make proofs much harder in Agda: https://github.com/Blaisorblade/Agda-playground/commit/8b561f74edfc73a44b89526960fd120fc18a3af3#diff-8860ae397263a76f3e55376a6d5d32ecR18311/05 22:16
pgiarrussoI assume there's a more clever way to avoid the problem, but my point is that you need to be extremely clever11/05 22:17
pgiarrussomietek: ^^11/05 22:17
pgiarrussothis case is so bad that even in Agda I'd be ready to work on build a separate and less typed representation11/05 22:18
pgiarrussoand I haven't found solutions even in "Type-and-Scope Safe Programs and their Proofs" (I tried using simultaneous substitutions), though I haven't studied it in detail :-|11/05 22:23
pgiarrussogallais_ : some day I probably should ask you about that11/05 22:31
pgiarrussobut gotta go now :-|11/05 22:31
pgiarrussobye!11/05 22:31

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