--- Day changed Mon Feb 13 2017 | ||

rntz | is it possible to declare infixity or syntax for something imported from another module? | 13/02 05:09 |
---|---|---|

mietek | rntz: not in my experience | 13/02 06:08 |

mietek | rntz: you can assign the thing to a new identifier and declare stuff for that… | 13/02 06:09 |

SuprDewd | ∀ {x y} → quoteTerm x ≡ quoteTerm y → x ≡ y | 13/02 11:36 |

SuprDewd | is this proved somewhere? or should I just use a postulate? | 13/02 11:36 |

SuprDewd | (or is this not true for some reason?) | 13/02 11:36 |

{AS} | SuprDewd: I am unsure whether this holds for things like coinductive terms | 13/02 11:47 |

mietek | SuprDewd: you should be suspicous | 13/02 11:48 |

mietek | SuprDewd: AFAIK, there is no rigorous theory behind Agda’s reflection | 13/02 11:48 |

mietek | SuprDewd: what are you working towards? | 13/02 11:48 |

SuprDewd | I have a datatype Expr, that you can think of as an AST | 13/02 11:49 |

SuprDewd | and I need to implement decidable equality | 13/02 11:50 |

mietek | For what notion of equality? | 13/02 11:50 |

{AS} | SuprDewd Have you looked at the one in agda-prelude? | 13/02 11:50 |

mietek | Identity? Alpha-equivalence? Alpha-beta? Alpha-beta-eta? | 13/02 11:50 |

SuprDewd | for all intents and purposes I think you can think about it as structural equality | 13/02 11:51 |

{AS} | mietek: I think the plain ol' propositional agda equality | 13/02 11:51 |

SuprDewd | but it's actually a bijection coupled with structural equality between two \NN's | 13/02 11:51 |

mietek | Conflicting data received; ignoring | 13/02 11:51 |

mietek | NNs? | 13/02 11:51 |

SuprDewd | natural numbers, sorry | 13/02 11:52 |

SuprDewd | this would be easy, however, if Expr was one of these algebraic data types, like: data Expr = zero | suc Expr | Expr + Expr | ... | 13/02 11:52 |

mietek | But? | 13/02 11:52 |

SuprDewd | this is a library, and I don't know in advance what Expr can look like | 13/02 11:53 |

SuprDewd | that is, Expr is somewhat extendible by the user | 13/02 11:53 |

mietek | Then you can’t know if your equality will be decidable | 13/02 11:53 |

SuprDewd | so Expr is currently defined as a record with some properties that the user has to provide | 13/02 11:53 |

SuprDewd | and then the user can define functions such as add : Expr -> Expr -> Expr | 13/02 11:54 |

mietek | You’re formalising a language that doesn’t have a static definition | 13/02 11:54 |

SuprDewd | but note that I'm willing to have a weaker definition of equality | 13/02 11:55 |

mietek | Well, you can always have alpha-equivalence | 13/02 11:55 |

mietek | I’m not sure if it’s more appropriate to call it weaker or strongeer | 13/02 11:56 |

mietek | I like to call it alpha-equivalence | 13/02 11:56 |

SuprDewd | (will have to google that) | 13/02 11:56 |

mietek | OK. Yes. | 13/02 11:56 |

{AS} | mietek: equivalence notions weaker/stronger is fairly standard | 13/02 11:57 |

mietek | Subjectively, I think these words are too subjective | 13/02 11:57 |

SuprDewd | but basically, I'm willing to sacrifice decidability, meanining I don't need a proof in the "no" case | 13/02 11:57 |

{AS} | ~ <= ~~ iff r ~~ r' ==> r ~ r' | 13/02 11:57 |

mietek | "weaker" usually means "the one I don’t like" | 13/02 11:57 |

SuprDewd | so a Maybe (a = b) | 13/02 11:58 |

{AS} | mietek: weaker means that you can say less things about different elements | 13/02 11:58 |

SuprDewd | but obviously I'm not looking for "return nothing" :) | 13/02 11:58 |

SuprDewd | my current workaround is to decide if quoteTerm x \== quoteTerm y | 13/02 11:59 |

SuprDewd | and in that case return just proof, otherwise nothing | 13/02 11:59 |

mietek | SuprDewd: if you’re looking at two ASTs and checking if they’re identical, variable names included, then you’re doing identity | 13/02 11:59 |

mietek | SuprDewd: if you’re disregarding variable names, then you’re doing alpha-equivalence (because you implicitly alpha-convert one term to match the other) | 13/02 12:00 |

mietek | SuprDewd: if you’re looking at two ASTs and checking if they evaluate to the same normal form, you’re doing some variant of beta-eta equivalence | 13/02 12:00 |

mietek | Depending on how you evaluate and what’s your normal form | 13/02 12:00 |

SuprDewd | I'm converting two Expr's into normal form, and this equality check I'm looking for is being used within that routine | 13/02 12:01 |

mietek | Most people here and in ##typetheory will not give you the time of day if you’re not doing at least beta | 13/02 12:01 |

SuprDewd | it's kind of weird, but I'm looking for something like identity in Agda's AST, not in my own AST | 13/02 12:03 |

SuprDewd | I guess I'm abusing Agda to make the library user's experience nicer | 13/02 12:04 |

SuprDewd | and I guess this would have worked, if not for the fact that I'm using quite a bit of coinduction in there | 13/02 12:05 |

SuprDewd | and I see what {AS} said before probably makes sense (although I'm going to double check to make sure) | 13/02 12:06 |

SuprDewd | which means I have to do something different now :( | 13/02 12:06 |

jonsterling | Does anyone have an Agda tactic for generating equality decision procedures? Curious what something like that looks like. | 13/02 12:49 |

jonsterling | Ah, I guess I should look at ulf's stuff: https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda | 13/02 12:51 |

mietek | jonsterling: Swierstra’s “Auto in Agda”? | 13/02 12:52 |

jonsterling | mietek: thanks for the reference! Does that use the modernized idris-style tactic stuff that they have in agda now? | 13/02 12:53 |

mietek | I don’t think it does, sorry | 13/02 12:53 |

jonsterling | ah, ok. | 13/02 12:53 |

mietek | I’m not sure. | 13/02 12:53 |

jonsterling | Also curious if anyone in this room has used the (current) Agda tactic system. I love agda, and sometimes tactics can be really nice for those times when you just need to grind an object into dust, so it seems like it might be a very nice combination. But I wonder how it goes in practice. | 13/02 12:54 |

mietek | What do you mean by the current Agda tactic system? | 13/02 12:54 |

mietek | Do you mean the two quotation monads? | 13/02 12:55 |

jonsterling | mietek: I believe that it was essentially rewritten this past year, modeled off David Christiansen's proof monad reflection stuff from idris. | 13/02 12:55 |

mietek | I do think something like this happened, but I’m not sure if I’d say we have tactics, except for maybe rewrite | 13/02 12:55 |

mietek | Which is special anyway | 13/02 12:56 |

jonsterling | Well, these are honest to god tactics; there is a TC monad, which lets you interact with Agda's elaborator. | 13/02 12:56 |

mietek | http://agda.readthedocs.io/en/latest/language/reflection.html | 13/02 12:56 |

mietek | “Macros lets you write tactics that can be applied without any syntactic overhead.” — well, what do I know | 13/02 12:56 |

jonsterling | I'm so out of date with this stuff... I really need to spend a weekend hacking with new agda stuff to see what can be done. | 13/02 12:56 |

jonsterling | In spite of all the French money and resources (and armies of hackers) that the Coq people have, the Agda folks are doing a shocking amount of work, and making a lot of nice scientific advances. This is a very good time for type-theoretic proof assistants! | 13/02 12:57 |

jonsterling | (btw, this is not to discount what the coq folks have been doing—the last two years have been fantastic for coq.) | 13/02 12:58 |

mietek | I believe effectfully has used the current TC system | 13/02 12:58 |

mietek | He’s been mostly offline recently though | 13/02 12:59 |

jonsterling | OK, cool. thanks! | 13/02 12:59 |

mietek | Should be some stuff in https://github.com/effectfully | 13/02 12:59 |

jonsterling | If I finish my "AI" homework early this week (sad!), I'll spend some time hacking and see what I can learn. | 13/02 12:59 |

mietek | https://github.com/effectfully/Generic looks relevant | 13/02 12:59 |

mietek | jonsterling: ^^ | 13/02 13:01 |

jonsterling | thanks! | 13/02 13:01 |

jonsterling | hmm, I also kind of wonder if it is possible to do something like the coq autosubst library for Agda. | 13/02 13:03 |

mietek | I saw something on the Agda mailing list recently | 13/02 13:03 |

mietek | “[Agda] Holes 0.1.0” and thread | 13/02 13:03 |

mietek | https://github.com/bch29/agda-holes | 13/02 13:04 |

mietek | jonsterling: this looks very relevant | 13/02 13:04 |

mietek | I think he gave a talk about it at SREPLS5 | 13/02 13:04 |

mietek | (Recent seminar in Oxford) | 13/02 13:05 |

jonsterling | that is very nice! I remember looking at that on the list. Would be interested to use the techniques in my own proofs. | 13/02 13:05 |

rntz | can anyone explain to me how I'm using equational reasoning incorrectly? this completely trivial example doesn't typecheck: http://sprunge.us/JJXB | 13/02 20:34 |

apostolis | Is there a way to point to agda that a specific case is impossible, so as not to prove that case? I suppose that during runtine it wll return an error. | 13/02 20:46 |

rntz | apostolis: yes, often. the pattern "()" can be used, and you omit the " = " and the right-hand-side | 13/02 20:47 |

rntz | unless you mean that you just want to *stipulate* that a certain case is impossible, rather than actually proving it | 13/02 20:47 |

rntz | apostolis: can you give an example of what you're trying to do? | 13/02 20:47 |

apostolis | the second. | 13/02 20:48 |

apostolis | I do not want to prove that something is impossible. | 13/02 20:48 |

rntz | ah. well. you can use "postulate" | 13/02 20:48 |

rntz | which lets you just assert anything you like | 13/02 20:48 |

rntz | postulate name : type | 13/02 20:48 |

apostolis | What will happen if one tries to execute the program and his postulation is wrong, the case is reached? | 13/02 20:49 |

rntz | I'm not sure. I think postulated terms don't reduce? | 13/02 20:49 |

rntz | so evaluation will get stuck? | 13/02 20:49 |

rntz | yeah, postulated terms don't reduce | 13/02 20:49 |

rntz | so for example if I | 13/02 20:49 |

rntz | postulate x : Nat | 13/02 20:49 |

rntz | and then try to evaluate x + 2 | 13/02 20:50 |

rntz | it'll just say "x + 2" | 13/02 20:50 |

rntz | if I evaluate (2 + x), it'll give me (suc (suc x)) | 13/02 20:50 |

rntz | if you actually want a runtime *error*, I'm not sure what you can do, but I'm not an agda expert; there might be something | 13/02 20:50 |

apostolis | I expect to see a runtime error indead. | 13/02 20:51 |

rntz | out of curiosity, may I ask what your use-case is? I think most people use agda as a theorem-prover, so introducing a "wrong" term and getting a runtime error is exactly what they don't want :P | 13/02 20:52 |

apostolis | I am not sure if postulate is easy to use to dismiss a case in a function. A specialized keyword would be much better. | 13/02 20:52 |

rntz | well, I'm not an agda language designer, but you can do: postulate undefined : forall {i}{A : Set i} -> A | 13/02 20:53 |

rntz | and then use "undefined" anywhere you like | 13/02 20:53 |

apostolis | I use agda to program software :) you know, that is a thing too. | 13/02 20:53 |

rntz | it is, for sure! I didn't realize agda could be used to do it. idris seems like it's aimed at doing that, though. | 13/02 20:54 |

rntz | I dunno how idris solves this | 13/02 20:54 |

apostolis | Idris does not provide some features that I want like Sized types, cubical type theory etc. | 13/02 20:55 |

apostolis | In idris, there is a special keyword if I remember correctly. | 13/02 20:56 |

apostolis | I will try to prove this but in any case, this undefined trick is good if it takes too much time to prove something. | 13/02 21:00 |

eze | I am getting stack overflow on emacs when loading a file, how can I increase the memory for agda? | 13/02 22:53 |

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