--- Day changed Sun Jul 30 2017
akryeah, so I don't really understand how the library system works30/07 09:13
akrI have added a git submodule which points to and Agda project30/07 09:14
akr(to my project root)30/07 09:14
akrnow I have created an .agda-lib file in my project root and declared this Agda project from the submodule as a library in it30/07 09:15
akrbut when I try load one of my own files now, it says that they should reside in the library's path30/07 09:16
akrit seems like .agda-lib is used to define a library, rather than to pull in dependencies?30/07 09:16
akrbut that's not what this says: https://agda.readthedocs.io/en/v2.5.2/tools/package-system.html#using-a-library30/07 09:17
akrokay, so I suppose that I need to add an .agda-lib to this dependency that I downloaded and then make an .agda-lib in my project that depends on this dependency30/07 09:20
akrbut now it's telling me I need to add the path to this dependency to my ~/.agda/libraries30/07 09:21
akrI don't really want to do that, I wanted to make this so that you can clone my project, run `git submodule init`, and then you can compile it30/07 09:21
akrI don't really want to mess with every user's configuration in ~/.agda30/07 09:22
akrI guess I can use --library-file to point to my project's custom libraries file, but that's not that nice :|30/07 09:24
akrhmm, is there some way to pass command line options to the emacs mode by creating a file in my project's root?30/07 09:28
akreh, this library system isn't really meant to handle having dependencies somewhere other than in some global location, is it30/07 09:39
akrthere needs to be some wrapper written on top of it to facilitate automatic retrieval of libraries from github, installing them, and adding them as deps to your project's .agda-lib30/07 09:40
akr… is there such a thing already?30/07 09:48
Nik05mietek I watched a lecture from Shai Ben David, I now understand inductive types a little more. I think this will also help in understanding defining formal logics, right?30/07 11:53
Nik05And I now also understand the fundamentals of induction (not only on natural numbers)30/07 11:55
mietekhow to deal with Agda falling into an infinite loop when type-checking?30/07 17:47
mietekno postulates30/07 17:47
akrmaybe try to come up with the smallest possible example that produces this behaviour and open an issue on github?30/07 17:48
akridk30/07 17:48
akroh I see it's something in your system30/07 17:49
mietekyes, that is good general problem solving advice30/07 17:49
Nik05`mietek: does it make agda inconsistent?30/07 19:05
mietekit’s difficult to prove false when the theorem prover is stuck in a loop30/07 19:11
akrabout as difficult as it is to prove true, I suppose30/07 19:13
akrI guess if you managed to formalize the type checker in Agda and show that it loops, you should be able to show it inconsistent30/07 19:14
dolioI don't think that's how it works.30/07 19:21
akrwhich part do you mean?30/07 19:23
dolioI mean there are consistent systems where a 'type checker' can loop in some situations.30/07 19:24
akroh, hmm30/07 19:25
dolioFor instance, in false contexts, with transparent enough extensionality, you can write terms that loop.30/07 19:28
dolioThey are guarded by an unsatisfiable premise, so the system isn't inconsistent; but if your checker tries to evaluate underneath the false premise, it may loop.30/07 19:28
akrbut don't you normally only type-check closed terms?30/07 19:30
dolioType checking a lambda expression requires type checking something that isn't a closed term.30/07 19:30
akrah, true30/07 19:31
akrhmm, but you start with a closed term30/07 19:31
akrusually30/07 19:31
mietekdolio: what system would this be?30/07 19:36
mietekit sounds fishy30/07 19:36
dolioExtensional type theory.30/07 19:36
mietekright30/07 19:36
mietekthanks, that’s another great argument against extensionality 30/07 19:37
dolioThere are probably non-naive ways to check extensional type theory that don't do that.30/07 19:38
dolioBut it's one of the motivations for OTT.30/07 19:38
dolioAnd also for not trying to 'eta expand' identities to 'refl' in something like OTT.30/07 19:38
dolioBecause if you eta expand a false identity, you get the same problem.30/07 19:39
jonsterlingakr: with typechecking, you do usually start with a closed term, but you always eventually need to account for open terms. In extensional type theory, you have to let the user construct derivations by hand/interactively. Usually tactics can take care of it, but there will always be pathological cases.30/07 19:47
rntzhm, but doesn't having a typechecker that can loop put a boot in the type-systems-as-proof-systems concept, though? I wouldn't call something a proof if it's not checkable.30/07 19:56
mietekit’s a bug, plainly30/07 19:56
rntz"it's a bug" isn't really right; "bug" means "doesn't obey its specification", and the whole question here is what the specification should be :P30/07 19:57
mietekthe typechecker should not loop.30/07 19:57
rntzhaving a typechecker that can loop doesn't seem absolutely wrong to me, it just seems like you can't really call it a proof checker any more30/07 19:58
mietekthat’s the entire point of requiring totality.30/07 19:58
rntzoh, I see, I should have read backlog30/07 20:00
rntzyou've actually found a case where agda specifically loops, this isn't about considering type theories that aren't decidable in general30/07 20:00
mietekright30/07 20:01
rntzmy apologies.30/07 20:03
mietekoh, no worries :)30/07 20:03
mudriWhat brought all this up? Was mietek's advice in response to something?30/07 20:07
mietekmudri: I got Agda to loop on my latest formalisation30/07 20:07
mudriBy using postulates?30/07 20:07
mietekno postulates30/07 20:07
mudriOh, oops.30/07 20:08
mietekI suspect it’s due to using functions in constructors30/07 20:08
mietektrying to work around it by using more explicit type indices30/07 20:09
akrjonsterling: hmm, I think I'm still confused on the distinction between an extensional and intensional TT30/07 20:09
jonsterlingrntz: There are plenty of wellbehaved type theories which don't have a decidable typing relation; but the members of types can't be regarded as proofs in the currently-used sense in that case. Sometimes people describe this as a situation where "the typechecker can loop", but a better way to say it is that "there is no typechecker for this language". 30/07 20:18
jonsterlingWhich is not as bad as it sounds.30/07 20:18
mudriOh, not even a semi-checker? Interesting.30/07 20:19
rntzhm, a semi-checker would be like: if X : A, then I can determine that X : A, but if not, I might infloop rather than saying "no"?30/07 20:20
rntz(and a cosemi-checker would be: if X does *not* have type A, I will reject it, but if it's valid, I might infloop rather than saying "yes"?)30/07 20:21
mudrirntz: that's what I intended, yes.30/07 20:21
mudriI've heard arguments for semi-checkers from mathematicians, given that they're only concerned about sharing correct proofs.30/07 20:22
rntzok. I think with the example that was discussed earlier, where having a contradiction in context would let you write a looping term, you couldn't have either a semi- or a cosemi-checker?30/07 20:22
rntzalthough. I guess I hesitate to even say what the "right" answer should be in the case of shoving a looping term under a contradictory context30/07 20:23
mietekuh30/07 20:37
mietekjonsterling: not as bad as it sounds?!30/07 20:38
mietekwhat is an example use of such a theory?30/07 20:38
jonsterlingNuprl is such a type theory. You can use it to formalize most of mathematics.30/07 20:49
jonsterlingIn general, the internal type theories of many interesting categories, including toposes, are extensional30/07 20:50
jonsterlingthis just means that you have to use math to establish that some expression has some type. This is perfectly ordinary in mathematics30/07 20:50
rntzmudri: in the case of a semi-checker being useful, I guess I'd think of "the trace of the semi-checker" as being the actual proof30/07 21:31
rntzsince *that* can definitely be verified or falsified30/07 21:31
mudriAah, yeah, makes sense.30/07 21:32
mudriBut there's still a huge practical difference, given that you don't write traces directly.30/07 21:32
rntzyeah.30/07 21:32
rntzthat's true.30/07 21:32
rntzif you couldn't get your hands on an actual trace, I'd be worried about some small change in your proof search algorithm invalidating previous proofs30/07 21:33
rntzalthough actually, I think I'd be worried about that anyway30/07 21:33
mudriThe Agda is strong here. ;-)30/07 21:33
mudriBut it does sound worse if it can make your checker not terminate.30/07 21:34
mudriMaybe it depends how good feedback can be. Presumably, if you interrupt such a checker, it can tell you where it got stuck checking.30/07 21:36
mietekI’d love to know that30/07 21:37
mudriBut there is the following situation: person A writes a proof in version 1; version 2 changes something which breaks the proof and causes non-termination; person B picks up the proof and tries to check it in version 2.30/07 21:40
mudriHow should person B know to interrupt?30/07 21:40
mieteknot sure what you mean30/07 21:46
mietekif the checking is not terminating, I would certainly try to interrupt30/07 21:47
mietekugh30/07 23:47
mietekso close, and yet so far30/07 23:51
mietekhttps://gist.github.com/mietek/f05b6fadee6357bb8953b2baf6ab44cf30/07 23:51
mietekany idea how to get Agda to accept idsubstMVAR as definitional equality?30/07 23:52
mietekI can’t use REWRITE with it, because the left-hand side reduces30/07 23:52
mieteksame applies to a version of substitution defined with explicit case expressions, instead of with-abstraction30/07 23:53

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