--- Day changed Mon Feb 13 2017
rntzis it possible to declare infixity or syntax for something imported from another module?13/02 05:09
mietekrntz: not in my experience13/02 06:08
mietekrntz: 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 ≡ y13/02 11:36
SuprDewdis 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 terms13/02 11:47
mietekSuprDewd: you should be suspicous13/02 11:48
mietekSuprDewd: AFAIK, there is no rigorous theory behind Agda’s reflection13/02 11:48
mietekSuprDewd: what are you working towards?13/02 11:48
SuprDewdI have a datatype Expr, that you can think of as an AST13/02 11:49
SuprDewdand I need to implement decidable equality13/02 11:50
mietekFor what notion of equality?13/02 11:50
{AS} SuprDewd Have you looked at the one in agda-prelude?13/02 11:50
mietekIdentity? Alpha-equivalence? Alpha-beta? Alpha-beta-eta?13/02 11:50
SuprDewdfor all intents and purposes I think you can think about it as structural equality13/02 11:51
{AS}mietek: I think the plain ol' propositional agda equality13/02 11:51
SuprDewdbut it's actually a bijection coupled with structural equality between two \NN's13/02 11:51
mietekConflicting data received; ignoring13/02 11:51
mietekNNs?13/02 11:51
SuprDewdnatural numbers, sorry13/02 11:52
SuprDewdthis 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
mietekBut?13/02 11:52
SuprDewdthis is a library, and I don't know in advance what Expr can look like13/02 11:53
SuprDewdthat is, Expr is somewhat extendible by the user13/02 11:53
mietekThen you can’t know if your equality will be decidable13/02 11:53
SuprDewdso Expr is currently defined as a record with some properties that the user has to provide13/02 11:53
SuprDewdand then the user can define functions such as add : Expr -> Expr -> Expr13/02 11:54
mietekYou’re formalising a language that doesn’t have a static definition13/02 11:54
SuprDewdbut note that I'm willing to have a weaker definition of equality13/02 11:55
mietekWell, you can always have alpha-equivalence13/02 11:55
mietekI’m not sure if it’s more appropriate to call it weaker or strongeer13/02 11:56
mietekI like to call it alpha-equivalence13/02 11:56
SuprDewd(will have to google that)13/02 11:56
mietekOK. Yes.13/02 11:56
{AS}mietek: equivalence notions weaker/stronger is fairly standard13/02 11:57
mietekSubjectively, I think these words are too subjective 13/02 11:57
SuprDewdbut basically, I'm willing to sacrifice decidability, meanining I don't need a proof in the "no" case13/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
SuprDewdso a Maybe (a = b)13/02 11:58
{AS}mietek: weaker means that you can say less things about different elements13/02 11:58
SuprDewdbut obviously I'm not looking for "return nothing"  :)13/02 11:58
SuprDewdmy current workaround is to decide if quoteTerm x \== quoteTerm y13/02 11:59
SuprDewdand in that case return just proof, otherwise nothing13/02 11:59
mietekSuprDewd: if you’re looking at two ASTs and checking if they’re identical, variable names included, then you’re doing identity13/02 11:59
mietekSuprDewd: 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
mietekSuprDewd: 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 equivalence13/02 12:00
mietekDepending on how you evaluate and what’s your normal form13/02 12:00
SuprDewdI'm converting two Expr's into normal form, and this equality check I'm looking for is being used within that routine13/02 12:01
mietekMost people here and in ##typetheory will not give you the time of day if you’re not doing at least beta13/02 12:01
SuprDewdit's kind of weird, but I'm looking for something like identity in Agda's AST, not in my own AST13/02 12:03
SuprDewdI guess I'm abusing Agda to make the library user's experience nicer13/02 12:04
SuprDewdand I guess this would have worked, if not for the fact that I'm using quite a bit of coinduction in there13/02 12:05
SuprDewdand I see what {AS} said before probably makes sense (although I'm going to double check to make sure)13/02 12:06
SuprDewdwhich means I have to do something different now :(13/02 12:06
jonsterlingDoes anyone have an Agda tactic for generating equality decision procedures? Curious what something like that looks like.13/02 12:49
jonsterlingAh, I guess I should look at ulf's stuff: https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda13/02 12:51
mietekjonsterling: Swierstra’s “Auto in Agda”?13/02 12:52
jonsterlingmietek: thanks for the reference! Does that use the modernized idris-style tactic stuff that they have in agda now?13/02 12:53
mietekI don’t think it does, sorry13/02 12:53
jonsterlingah, ok.13/02 12:53
mietekI’m not sure.13/02 12:53
jonsterlingAlso 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
mietekWhat do you mean by the current Agda tactic system?13/02 12:54
mietekDo you mean the two quotation monads?13/02 12:55
jonsterlingmietek: 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
mietekI do think something like this happened, but I’m not sure if I’d say we have tactics, except for maybe rewrite13/02 12:55
mietekWhich is special anyway13/02 12:56
jonsterlingWell, these are honest to god tactics; there is a TC monad, which lets you interact with Agda's elaborator.13/02 12:56
mietekhttp://agda.readthedocs.io/en/latest/language/reflection.html13/02 12:56
mietek“Macros lets you write tactics that can be applied without any syntactic overhead.” — well, what do I know13/02 12:56
jonsterlingI'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
jonsterlingIn 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
mietekI believe effectfully has used the current TC system13/02 12:58
mietekHe’s been mostly offline recently though13/02 12:59
jonsterlingOK, cool. thanks!13/02 12:59
mietekShould be some stuff in https://github.com/effectfully13/02 12:59
jonsterlingIf 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
mietekhttps://github.com/effectfully/Generic looks relevant13/02 12:59
mietekjonsterling: ^^13/02 13:01
jonsterlingthanks!13/02 13:01
jonsterlinghmm, I also kind of wonder if it is possible to do something like the coq autosubst library for Agda.13/02 13:03
mietekI saw something on the Agda mailing list recently13/02 13:03
mietek“[Agda] Holes 0.1.0” and thread13/02 13:03
mietekhttps://github.com/bch29/agda-holes13/02 13:04
mietekjonsterling: this looks very relevant13/02 13:04
mietekI think he gave a talk about it at SREPLS513/02 13:04
mietek(Recent seminar in Oxford)13/02 13:05
jonsterlingthat 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
rntzcan anyone explain to me how I'm using equational reasoning incorrectly? this completely trivial example doesn't typecheck: http://sprunge.us/JJXB13/02 20:34
apostolisIs 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
rntzapostolis: yes, often. the pattern "()" can be used, and you omit the " = " and the right-hand-side13/02 20:47
rntzunless you mean that you just want to *stipulate* that a certain case is impossible, rather than actually proving it13/02 20:47
rntzapostolis: can you give an example of what you're trying to do?13/02 20:47
apostolisthe second.13/02 20:48
apostolisI do not want to prove that something is impossible.13/02 20:48
rntzah. well. you can use "postulate"13/02 20:48
rntzwhich lets you just assert anything you like13/02 20:48
rntzpostulate name : type13/02 20:48
apostolisWhat will happen if one tries to execute the program and his postulation is wrong, the case is reached?13/02 20:49
rntzI'm not sure. I think postulated terms don't reduce?13/02 20:49
rntzso evaluation will get stuck?13/02 20:49
rntzyeah, postulated terms don't reduce13/02 20:49
rntzso for example if I13/02 20:49
rntzpostulate x : Nat13/02 20:49
rntzand then try to evaluate x + 213/02 20:50
rntzit'll just say "x + 2"13/02 20:50
rntzif I evaluate (2 + x), it'll give me (suc (suc x))13/02 20:50
rntzif you actually want a runtime *error*, I'm not sure what you can do, but I'm not an agda expert; there might be something13/02 20:50
apostolisI expect to see a runtime error indead.13/02 20:51
rntzout 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 :P13/02 20:52
apostolisI 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
rntzwell, I'm not an agda language designer, but you can do: postulate undefined : forall {i}{A : Set i} -> A13/02 20:53
rntzand then use "undefined" anywhere you like13/02 20:53
apostolisI use agda to program software :) you know, that is a thing too.13/02 20:53
rntzit 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
rntzI dunno how idris solves this13/02 20:54
apostolisIdris does not provide some features that I want like Sized types, cubical type theory etc.13/02 20:55
apostolisIn idris, there is a special keyword if I remember correctly.13/02 20:56
apostolisI 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
ezeI 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!