--- Day changed Thu May 11 2017 | ||

rgrinberg | thanks gallais_ | 11/05 00:07 |
---|---|---|

rgrinberg | why can't i write a type signature as follows: x : reverse [] \== [] | 11/05 00:08 |

rgrinberg | i know it's not a very useful type, but i'm still curious | 11/05 00:08 |

mietek | what do you mean by "can't"? | 11/05 00:09 |

rgrinberg | well when I write that type and x = refl | 11/05 00:11 |

rgrinberg | emacs highlights the type for me signaling that it's an error | 11/05 00:11 |

mietek | did you get an error message? | 11/05 00:12 |

rgrinberg | hmm no. but it still gets highlighted | 11/05 00:13 |

mietek | that just means Agda couldn’t figure something out | 11/05 00:13 |

mietek | what did you intend [] to be? | 11/05 00:14 |

rgrinberg | the empty list. i.e. the constructor from Data.List | 11/05 00:14 |

mietek | what type, precisely? | 11/05 00:15 |

rgrinberg | hmm, I guess i'm not sure | 11/05 00:19 |

rgrinberg | i want this to hold any list obviously, but i'm not sure how to write the type | 11/05 00:20 |

mietek | well, look how Data.List is defined | 11/05 00:20 |

mietek | https://agda.github.io/agda-stdlib/Data.List.Base.html#1 | 11/05 00:20 |

mietek | https://agda.github.io/agda-stdlib/Agda.Builtin.List.html#117 | 11/05 00:20 |

mietek | {a} is a universe level | 11/05 00:21 |

mietek | x : forall {a} {A : Set a} -> reverse [] \== ([] {a} {A}) | 11/05 00:22 |

mietek | just guessing | 11/05 00:22 |

mietek | you could also show this for the universe of small types | 11/05 00:22 |

mietek | oops, there was a typo above | 11/05 00:23 |

mietek | but you’ll figure it out | 11/05 00:23 |

mietek | x : forall {A : Set} -> reverse [] \== ... | 11/05 00:23 |

rgrinberg | x : ∀{l}{A : Set l} -> reverse ([] {l} {A}) ≡ ([] {l} {A}) | 11/05 00:23 |

rgrinberg | this works, thanks | 11/05 00:23 |

mietek | you should only need to say this on one side | 11/05 00:24 |

mietek | no? | 11/05 00:24 |

rgrinberg | How would I drop something like this on lists: drop1 : ∀{l}{A : Set l}(x : A)(xs : List A) -> drop (suc zero) (x ∷ xs) ≡ xs | 11/05 07:25 |

rgrinberg | I know it's trivial on vectors, but here i'm puzzled | 11/05 07:26 |

{AS} | rgrinberg: Shouldn't this hold by definition of 'drop'? :) | 11/05 08:37 |

rgrinberg | it should, but it doesn't :/ | 11/05 08:38 |

{AS} | how are you defining drop? | 11/05 08:41 |

rgrinberg | https://gist.github.com/rgrinberg/111da9db6229d23c91c93fa263639c45 | 11/05 08:43 |

{AS} | rgrinberg: you need to pattern match on xs | 11/05 08:43 |

{AS} | in the second case | 11/05 08:44 |

rgrinberg | haha yes | 11/05 08:44 |

rgrinberg | hitting that agda2-auto key a little fast | 11/05 08:44 |

yhhko | i'm using agda reflection. what methods are available for testing if two Terms are equal? it doesn't matter if it's not perfect | 11/05 12:55 |

gallais_ | yhhko: https://github.com/agda/agda-stdlib/blob/master/src/Reflection.agda#L455 ? | 11/05 13:50 |

yhhko | gallais_: yes, something like that! thanks! :) | 11/05 13:51 |

yhhko | did agda ever get mutual recursion between modules? | 11/05 15:05 |

rgrinberg | is it true that anything I can prove with cong, I can also prove rewrite? | 11/05 17:48 |

rgrinberg | s/rewrite/with rewrite/ | 11/05 17:48 |

mietek | rgrinberg: perhaps you should try proving that… | 11/05 17:49 |

mietek | :) | 11/05 17:49 |

rgrinberg | mietek: good idea. I think I need some help with a starting point though. what would the proposition look like? | 11/05 17:50 |

mietek | I would be surprised if one could express it in Agda | 11/05 17:50 |

mietek | I’m not certain about the reach of Agda’s reflective capabilities | 11/05 17:51 |

rgrinberg | oh, you meant the "old" way | 11/05 17:51 |

rgrinberg | by hand that is :P | 11/05 17:51 |

mietek | I’m actually in a discussion in another channel on the expressiveness of mathematical meta-languages | 11/05 17:51 |

mietek | {AS}: ^^ | 11/05 17:51 |

mietek | and so, I only really mean to point out that we’re not quite there yet | 11/05 17:51 |

rgrinberg | mietek: but is the statement true or not btw? | 11/05 17:52 |

mietek | I don’t know | 11/05 17:52 |

mietek | I would expect the converse to hold | 11/05 17:52 |

{AS} | rgrinberg: rewrite is more powerful | 11/05 17:53 |

rgrinberg | really? I originally thought that rewrite is more powerful | 11/05 17:53 |

mietek | huh. | 11/05 17:53 |

rgrinberg | {AS}: read my mind | 11/05 17:53 |

{AS} | Rewrite is equivalent to subst | 11/05 17:54 |

mietek | I thought rewrite desugars to Agda-without-rewrite | 11/05 17:54 |

mietek | so it cannot be more powerful | 11/05 17:54 |

{AS} | mietek: it does | 11/05 17:54 |

{AS} | It's more powerful than cong, not subst :) | 11/05 17:54 |

mietek | I think pgiarrusso told me once that any subst can be written as a cong | 11/05 17:54 |

{AS} | It can? | 11/05 17:54 |

{AS} | Hmm | 11/05 17:54 |

mietek | I may be misremembering | 11/05 17:55 |

{AS} | Maybe he can answer when he is here :) | 11/05 17:57 |

mietek | can’t find it in my logs so I may be wrong | 11/05 18:03 |

pgiarrusso | rgrinberg: for one step of cong, that's typically true | 11/05 18:13 |

pgiarrusso | mietek: if I said that, I forgot why | 11/05 18:13 |

rgrinberg | pgiarrusso: I see, thanks. | 11/05 18:14 |

rgrinberg | is there anyway to prove anything about rewrite from inside agda? | 11/05 18:14 |

pgiarrusso | I'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-details | 11/05 18:15 |

pgiarrusso | rgrinberg, | 11/05 18:15 |

rgrinberg | OK, will check those out | 11/05 18:15 |

pgiarrusso | rgrinberg: 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 |

mietek | http://agda.readthedocs.io/en/v2.5.2/language/reflection.html | 11/05 18:17 |

mietek | rewrite is not mentioned | 11/05 18:17 |

mietek | and the reflection machinery may or may not be sound | 11/05 18:18 |

mietek | ;) | 11/05 18:18 |

pgiarrusso | mietek: I'd wonder if reflection works on the desugared form of rewrite? | 11/05 18:18 |

mietek | could be; I don’t know | 11/05 18:18 |

pgiarrusso | mietek: 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 desugaring | 11/05 18:22 |

mietek | or elaborating, or whatever it’s called | 11/05 18:22 |

mietek | I mean, you could probably use reflection to prove properties of what you *think* rewrite will desugar to | 11/05 18:23 |

mietek | if you state that desugared form manually | 11/05 18:23 |

mietek | but to connect to the actual `rewrite` operator in the language, I don’t know | 11/05 18:24 |

pgiarrusso | exactly | 11/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, exactly | 11/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 rewrite | 11/05 18:30 |

{AS} | pgiarrusso: sec, I am doing an example | 11/05 18:30 |

pgiarrusso | think I know what you mean | 11/05 18:30 |

pgiarrusso | I expect you'll need sometimes `with` in the proof | 11/05 18:30 |

pgiarrusso | as usual with functions defined with `with` | 11/05 18:31 |

{AS} | pgiarrusso: So if you use subst one has to use that subst== lemma | 11/05 18:31 |

mietek | pgiarrusso: yes, and that becomes really irritating fast | 11/05 18:31 |

{AS} | https://github.com/agda/agda-stdlib/blob/ac6a3bd774e2d50309649090321b247aaa5c6932/Relation/Binary/PropositionalEquality.agda#L24 | 11/05 18:32 |

{AS} | This one | 11/05 18:32 |

pgiarrusso | mietek: at least Agda tells you what to match on | 11/05 18:32 |

mietek | sort of | 11/05 18:32 |

{AS} | I think with rewrite it will automatically rewrite, so you don't have to handle subst on the right hand side | 11/05 18:32 |

mietek | you will get holes with like "... | condition" on the right | 11/05 18:32 |

pgiarrusso | mietek: exactly, so add `with condition` :-) | 11/05 18:33 |

mietek | and how do you write something of that type by hand? | 11/05 18:33 |

mietek | where? | 11/05 18:33 |

mietek | inside the hole? | 11/05 18:33 |

mietek | no. | 11/05 18:33 |

pgiarrusso | yes, left-hand side | 11/05 18:33 |

mietek | left-hand side of the equation that is the parent of the term which has a hole? | 11/05 18:33 |

pgiarrusso | yes | 11/05 18:33 |

mietek | I can’t recall a specific case now, but I’m not sure if this always helps | 11/05 18:33 |

pgiarrusso | (a) you need to case-split on the result | 11/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 |

pgiarrusso | I mean http://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html#ill-typed-with-abstractions | 11/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 available | 11/05 18:36 |

{AS} | pgiarrusso: Ah, thanks :) | 11/05 18:36 |

pgiarrusso | took me years to get why people talk about "which definitions reduce" | 11/05 18:37 |

mietek | go on? | 11/05 18:37 |

mietek | pgiarrusso: you mean ones that don’t depend on postulates? | 11/05 18:37 |

pgiarrusso | mietek: I mean things unlike `n + 0` :-) | 11/05 18:38 |

mietek | not getting it | 11/05 18:38 |

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

pgiarrusso | Yes | 11/05 18:38 |

pgiarrusso | sorry, I should have said | 11/05 18:38 |

pgiarrusso | "which *expressions* reduce" | 11/05 18:39 |

mietek | hm | 11/05 18:39 |

mietek | if you ask Agda explicitly to normalise "n+0" and "0+n"… | 11/05 18:39 |

mietek | as I am about to | 11/05 18:39 |

pgiarrusso | n + 0 is a normal form | 11/05 18:40 |

pgiarrusso | exercise: why? | 11/05 18:40 |

pgiarrusso | hint: equations are `0 + n = n` and `(S m) + n = S (m + n)` | 11/05 18:40 |

{AS} | because n and 0 are neutral | 11/05 18:41 |

mietek | before you get into that, consider your wording | 11/05 18:41 |

pgiarrusso | hence, think of `n + 0` as `n + 0 | n` | 11/05 18:41 |

pgiarrusso | like with `with` | 11/05 18:41 |

pgiarrusso | Agda can't reduce `n + 0` without knowing which `n` is | 11/05 18:41 |

pgiarrusso | mietek: my wording might sure be sloppy, sorry, no clue where | 11/05 18:42 |

mietek | both "n + 0" and "0 + n" reduce perfectly well if "n" is known, that is, *not a postulate*, as I’ve said | 11/05 18:43 |

mietek | or assumption | 11/05 18:43 |

pgiarrusso | mietek: by `n` I meant an object variable | 11/05 18:44 |

pgiarrusso | or an assumption, if you want :-) | 11/05 18:44 |

pgiarrusso | but as {AS} said, any neutral will do | 11/05 18:44 |

mietek | yes | 11/05 18:44 |

pgiarrusso | BUT `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 CTT | 11/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 |

pgiarrusso | because you don't have to write `subs`? | 11/05 18:47 |

pgiarrusso | * `subst` ? | 11/05 18:47 |

pgiarrusso | that's the "extensional type theory" part | 11/05 18:47 |

{AS} | Equality reflection | 11/05 18:47 |

mietek | because nobody can determine for themselves whether they’re good or not | 11/05 18:47 |

pgiarrusso | yes | 11/05 18:47 |

{AS} | Yeah | 11/05 18:47 |

mietek | ;) | 11/05 18:47 |

pgiarrusso | mietek: ? | 11/05 18:47 |

pgiarrusso | but then CTT has lots of other differences | 11/05 18:47 |

mietek | pgiarrusso: poor joke; how do I run NuPRL | 11/05 18:48 |

{AS} | pgiarrusso: Yeah, which is why I also said only in this case :) | 11/05 18:48 |

pgiarrusso | mietek: ah OK | 11/05 18:48 |

{AS} | mietek: You download the virtual machine | 11/05 18:48 |

pgiarrusso | {AS}: is there one? I though jonsterling tried really hard, failed, and decided to rewrite NuRPL as *PRL | 11/05 18:48 |

mietek | {AS}: have you done that? | 11/05 18:49 |

{AS} | mietek: I have not | 11/05 18:49 |

mietek | I see http://www.nuprl.org/vms/ and it does not look inviting, but I will try | 11/05 18:49 |

pgiarrusso | wow hadn't seen THAT! | 11/05 18:49 |

pgiarrusso | the problem, IIUC, is that NuPRL is *ALSO* a distributed systems maintaining a knowledge base | 11/05 18:50 |

pgiarrusso | *Anyway*, back to Agda | 11/05 18:51 |

{AS} | pgiarrusso: I think they only released it publicly recently | 11/05 18:51 |

pgiarrusso | {AS}: makes sense, but that's dated 2015... | 11/05 18:52 |

mietek | http://www.nuprl.org/FAQ/Connecting-to-nuprl-servers.html | 11/05 18:52 |

pgiarrusso | anyway, JonPRL/RedPRL are probably easier to install | 11/05 18:52 |

pgiarrusso | mietek: yeah, found that too | 11/05 18:52 |

pgiarrusso | {AS}: actually, writing untyped realizers and proving they're well-typed *can* be more flexible | 11/05 18:52 |

mietek | it feels wrong | 11/05 18:52 |

mietek | it feels like too much work | 11/05 18:53 |

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

pgiarrusso | mietek: in my PhD thesis, being correct by construction appears to add significant overhead to my proof | 11/05 18:54 |

mietek | pgiarrusso: is it overhead if you wouldn’t know if you are correct otherwise? | 11/05 18:55 |

mietek | I would argue the right way to move forward is to improve the language so that such overhead can be minimised | 11/05 18:55 |

mietek | without leaving the correct-by-construction world | 11/05 18:55 |

{AS} | mietek: They have build a compiler in Coq | 11/05 18:56 |

{AS} | for C | 11/05 18:56 |

{AS} | with multiple passes | 11/05 18:56 |

{AS} | The experience I got when talking to the Coq people was this would be hard in Agda | 11/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 |

pgiarrusso | mietek: maybe, eventually, but this is like postulating a sufficiently smart compiler. It's still a good eventual goal. | 11/05 18:57 |

mietek | Agda runs out of CPU if I type too fast on the keyboard | 11/05 18:58 |

mietek | that may be mostly emacs fault, nevertheless | 11/05 18:58 |

mietek | nobody is saying that what we have is good | 11/05 18:58 |

pgiarrusso | {AS}: Coq vs agda is most often about tactics vs proof terms | 11/05 18:58 |

pgiarrusso | but in both you can be "correct by construction" | 11/05 18:59 |

pgiarrusso | However, Agda has better support for pattern matching, which sometimes compensates the lack of tactics | 11/05 18:59 |

mietek | pgiarrusso: it’s more about focusing the energy of research | 11/05 18:59 |

{AS} | pgiarrusso: Yeah, but I meant, they do all the proofs externally | 11/05 18:59 |

mietek | pgiarrusso: but of course, people work on what interests them | 11/05 18:59 |

{AS} | instead of building the right structure | 11/05 18:59 |

mietek | {AS}: ? | 11/05 19:00 |

{AS} | so they define ML-like programs in Coq | 11/05 19:00 |

{AS} | almost no dependent types | 11/05 19:00 |

{AS} | and then write the properties they want to verify externally | 11/05 19:00 |

mietek | "externally" meaning what? | 11/05 19:00 |

pgiarrusso | {AS}: for some reason, that's typical in Coq | 11/05 19:00 |

{AS} | mietek: meaning that they write something like a sorting function returning a normal array | 11/05 19:01 |

pgiarrusso | mietek: 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 said | 11/05 19:01 |

pgiarrusso | mietek: compare well-scoped or well-typed deBruijn indexes with raw naturals. | 11/05 19:01 |

pgiarrusso | or vectors indexed by their length vs raw lists | 11/05 19:02 |

mietek | they are both internal object-level definitions formalised within Coq | 11/05 19:02 |

mietek | I’m not sure why {AS} thinks that is possible in Coq and not in Agda | 11/05 19:02 |

pgiarrusso | mietek: yeah, another sense of "external" | 11/05 19:02 |

{AS} | mietek: The tactics style of proving helps a lot | 11/05 19:02 |

pgiarrusso | mietek: Coq users are much more likely to use the second style and not the first | 11/05 19:02 |

mietek | pgiarrusso: sure | 11/05 19:03 |

mietek | {AS}: sure | 11/05 19:03 |

mietek | again, your point? | 11/05 19:03 |

mietek | Coq is currently easier to use for certain tasks than Agda | 11/05 19:03 |

mietek | granted | 11/05 19:03 |

{AS} | That correct by construction is fairly difficult | 11/05 19:03 |

{AS} | since you have to maintain your invariants throughout | 11/05 19:03 |

pgiarrusso | {AS}: agreed, sometimes. | 11/05 19:03 |

mietek | but… you are being correct by construction *by virtue of using Coq* | 11/05 19:03 |

mietek | we have a miscommunication about meta-levels | 11/05 19:04 |

mietek | all confusion is meta-level confusion | 11/05 19:04 |

{AS} | mietek: Prop allows you to do classical proofs | 11/05 19:04 |

pgiarrusso | mietek: yes, we're confusing things. | 11/05 19:04 |

pgiarrusso | but what {AS} is saying is relevant to "untyped realizers" | 11/05 19:04 |

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

pgiarrusso | there's a spectrum from "untyped lambda calculus" through "normal types" to "dependent types" | 11/05 19:05 |

mietek | where untyped whatevers are primitive | 11/05 19:05 |

mietek | (I may be wrong here as I still haven’t used *PRL) | 11/05 19:05 |

pgiarrusso | to the left, you define operations and separately prove them correct | 11/05 19:06 |

pgiarrusso | to the right, more of the correctness proof is embedded in the definition | 11/05 19:06 |

mietek | what do you use to prove untyped LC programs correct? | 11/05 19:06 |

pgiarrusso | mietek: ? | 11/05 19:07 |

pgiarrusso | all of those styles are possible in the same languag | 11/05 19:07 |

pgiarrusso | *language | 11/05 19:07 |

{AS} | mietek: Also, to note. I think a typical argument is that the realizers are primitive but simple to understand | 11/05 19:07 |

mietek | pgiarrusso: what? | 11/05 19:08 |

{AS} | While Coq/Agda/Idris's type checkers are complicated | 11/05 19:08 |

mietek | pgiarrusso: you just said, there’s a spectrum. | 11/05 19:08 |

mietek | pgiarrusso: let’s be concrete and say, untyped LC, STLC, MLTT | 11/05 19:08 |

mietek | 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:09 |

{AS} | mietek: You use rewriting logic :) | 11/05 19:09 |

mietek | pgiarrusso: this is what I understand as correct-by-construction: because MLTT would not type-check my program otherwise. | 11/05 19:09 |

mietek | pgiarrusso: how do I achieve a comparable result in untyped LC? | 11/05 19:10 |

{AS} | or any computation logic | 11/05 19:10 |

mietek | pgiarrusso: obviously I cannot be correct-by-construction: as you said, I have to use something external to untyped LC. | 11/05 19:10 |

mietek | pgiarrusso: I’m asking, what specifically could I use? | 11/05 19:10 |

mietek | s/extend/extent/ | 11/05 19:10 |

pgiarrusso | mietek: *PRL has some dependently-typed answer | 11/05 19:10 |

pgiarrusso | let me avoid debating *PRL details | 11/05 19:11 |

pgiarrusso | what I *can* say is the following | 11/05 19:11 |

pgiarrusso | I love correct-by-construction | 11/05 19:11 |

pgiarrusso | But take | 11/05 19:12 |

pgiarrusso | > I can write a MLTT program and be sure that it is correct to the extend that Ive specified in its type. | 11/05 19:12 |

lambdabot | <hint>:1:93: error: parse error on input ‘in’ | 11/05 19:12 |

mietek | :D | 11/05 19:12 |

pgiarrusso | I often find that if I specify too much in the type, writing the definition becomes either impossible or harder than otherwise | 11/05 19:12 |

pgiarrusso | *some* of that might be due to limited tools | 11/05 19:13 |

pgiarrusso | so we should re-evaluate when we get better tools, and people are welcome to write them | 11/05 19:13 |

mietek | yes. | 11/05 19:13 |

pgiarrusso | but sometimes, the best way to prove "P(X)" and "P(Y)" is not a fixed set of inference rules | 11/05 19:14 |

pgiarrusso | (that is, a type system) | 11/05 19:15 |

pgiarrusso | in a few minutes I can maybe contribute some specific example for Agda | 11/05 19:15 |

pgiarrusso | tying back to our discussion | 11/05 19:15 |

pgiarrusso | *PRL makes many proofs external to terms, Agda users tend to add more in their types, Coq users are in between | 11/05 19:16 |

jonsterling | I 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 |

jonsterling | The 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 |

pgiarrusso | jonsterling: 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 |

pgiarrusso | mietek: 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-L271 | 11/05 19:22 |

jonsterling | :) | 11/05 19:22 |

pgiarrusso | On intrinsical vs extrinsical proofs, I've failed some proofs (in part) because I used well-typed de Bruijn indexes | 11/05 19:23 |

pgiarrusso | Here's an example where intrinsic typing seems to make proofs much harder in Agda: https://github.com/Blaisorblade/Agda-playground/commit/8b561f74edfc73a44b89526960fd120fc18a3af3#diff-8860ae397263a76f3e55376a6d5d32ecR183 | 11/05 22:16 |

pgiarrusso | I assume there's a more clever way to avoid the problem, but my point is that you need to be extremely clever | 11/05 22:17 |

pgiarrusso | mietek: ^^ | 11/05 22:17 |

pgiarrusso | this case is so bad that even in Agda I'd be ready to work on build a separate and less typed representation | 11/05 22:18 |

pgiarrusso | and 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 |

pgiarrusso | gallais_ : some day I probably should ask you about that | 11/05 22:31 |

pgiarrusso | but gotta go now :-| | 11/05 22:31 |

pgiarrusso | bye! | 11/05 22:31 |

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