/home/laney/.irssi/irclogs/Freenode/2010/#agda/November.log

--- Log opened Mon Nov 01 00:00:26 2010
leoHi ! A simple question, on the stdlib , where is the associativity or commutativity of integers ?01/11 20:53
dolioI'd expect it to be in Data.Integer.Properties, but that module looks pretty light.01/11 20:55
leono está ahi. mmm :'(01/11 20:56
leois not there. mmm: '(01/11 20:56
Spockzpumpkin: hi01/11 21:13
Spockzleo: Relation.Binary?01/11 21:13
pumpkinhi01/11 21:14
pumpkinyay, new laptop01/11 21:14
pumpkinI put 6.12 on it so I could use agda again :P01/11 21:14
Spockza MBA? :P01/11 21:15
pumpkinof course :P01/11 21:15
pumpkinit's the nicest laptop I've owned yet01/11 21:15
Spockz\o/ how is it?01/11 21:15
pumpkinfrom the first few hours of use01/11 21:15
pumpkinfeels solid, very zippy, and the batt seems to be lasting forever01/11 21:15
SpockzI'm so restraining myself to not get a 13"01/11 21:16
pumpkinthat's the one I have01/11 21:17
pumpkinalthough 11 looked pretty sweet too01/11 21:17
pumpkinI had to wait a while cause you can only get 4GB of RAM with a custom order01/11 21:17
pumpkinand I need moar RAM for agda :P01/11 21:17
pumpkinI'd have liked 8 but they didn't offer it :(01/11 21:17
djahandariemoar01/11 21:17
pumpkinNEED MOAR01/11 21:18
Spockzyes but that one has a slower proc + less battery + a lower resolution than I have now01/11 21:18
pumpkinyeah01/11 21:18
Spockzindeed :)01/11 21:18
pumpkinbut it's so cute01/11 21:18
Spockzsure, but a 13" is also cute01/11 21:18
Spockzbtw, can you really cut yourself on the front part of the MBA?01/11 21:18
pumpkinI just tried, and no01/11 21:19
Spockznice :)01/11 21:19
pumpkinthe screen is even thinner than the one on my old mba01/11 21:19
pumpkinalso, this one hasn't overheated once01/11 21:19
pumpkinunlike the other one01/11 21:19
Spockzbut you don't have it as long as the other ;)01/11 21:22
pumpkintrue01/11 21:23
Spockzpumpkin: are you going to be in Ghent with the hackathon?01/11 21:31
pumpkinI wish :P01/11 21:54
pumpkinI just left europe a few weeks ago01/11 21:54
Spockzwhy?!01/11 21:59
pumpkinto get a job in the US :P01/11 22:00
Spockzok ok :P01/11 22:03
SpockzI'm going to get some much needed sleep01/11 22:03
Spockzgood night01/11 22:04
pumpkingood night :)01/11 22:06
--- Day changed Tue Nov 02 2010
pumpkinagda is wonderfully fast02/11 03:22
pumpkinon this new laptop02/11 03:22
Saizanram++02/11 03:35
djahandarieIt's interesting that Agda is judged by how fast its compiler runs, while Haskell is judged by how fast its compiled programs run02/11 03:36
djahandarieI've heard rumors that dolio doesn't even run his programs!02/11 03:38
* Saizan neither02/11 03:40
* djahandarie gasps02/11 03:40
pumpkinyeah, most people don't :)02/11 03:40
penelopeI've been trying to teach myself Agda, but I'm afraid I don't quite get the theorem proving aspects.02/11 03:53
penelopeFor instance, in Dependently Typed Programs in Agda,02/11 03:54
penelopeI was able to do the matix transposition exercise without trouble02/11 03:55
penelopeBut, the lem-!-tab exercise leaves me mystified as to where to begin02/11 03:55
penelopeI get that it should work with a base step along with an induction step.02/11 03:56
* Saizan fetches the article02/11 03:56
penelopeBut I feel like I'm missing something important.02/11 03:56
penelopeSaizan: Exercise 2.202/11 03:57
Saizanfound02/11 03:58
Saizanso, over what are you doing the induction?02/11 03:59
pumpkinpenelope: just to check, do you understand the curry-howard correspondence?02/11 04:00
penelopeOver finite numbers?02/11 04:00
penelopeI've encounterd the term, but I'm not from a comp sci background...02/11 04:01
pumpkinpenelope: I'd read the wikipedia article on it first02/11 04:01
penelopeI'll have to look it up...02/11 04:01
pumpkinit's a pretty simple concept and it underpins all of agda (and even haskell)02/11 04:01
pumpkinbut basically, types are logical statements, programs are proofs of the statements corresponding to their types02/11 04:01
penelopeHaskell makes more sense than agda, at this point...02/11 04:01
penelopeNo, I get that.02/11 04:02
penelopeBut02/11 04:02
Saizangood start, but when you see induction as a program it becomes a recursive function that pattern matches against one of its arguments02/11 04:02
pumpkinpenelope: so you understand that Either is like or, and (,) is like and, and so on?02/11 04:02
penelopeetc.02/11 04:03
penelopewell, I might say (,) is more like cartesian plus...02/11 04:03
Saizanfrom the set perspective, (,) is cartesian product, and Either is disjoint union02/11 04:04
Saizananyhow, if we start with "lem-!-tab : forall {A n} (f : Fin n -> A)(i : Fin n) ->02/11 04:05
Saizan"lem-!-tab : forall {A n} (f : Fin n -> A)(i : Fin n) -> tabulate f ! i == f i02/11 04:05
Saizanlem-!-tab f i = ?02/11 04:05
Saizanour best shot is to pattern match against i02/11 04:06
penelopeI'd approach that from matching against i == 002/11 04:06
penelopelem-!-tab f fzero    = refl02/11 04:07
Saizanright02/11 04:07
Saizanbecause from the definition of tabulate and ! we immediately see that "tabulate f ! fzero" reduces to "f fzero"02/11 04:08
Saizanbut now we have the other case to fill too02/11 04:08
penelopeBut 1) I'm not sure what I'm doing there--I'm asserting that? Whether true or false in reality?02/11 04:08
penelopeI'm just jumping from an idea to an assertion?02/11 04:09
pumpkinyou've proved your base case. Now you want to say "for all i > 0, tabulate f ! i == f i"02/11 04:09
penelopeCan I just assert anything that typechecks? True or False?02/11 04:10
Saizanwriting refl there you're sort of asserting that "tabulate f ! fzero" is obviously equal to "f i"02/11 04:10
Saizanbut the fact that it typechecks means you're right02/11 04:10
Saizanyou're using the emacs mode, right?02/11 04:10
pumpkinpenelope: you can assert that 1 == 2 (i.e., write the type), but you will never be able to prove it (assuming agda isn't broken, which it often is)02/11 04:11
penelopeYes :)02/11 04:11
penelopeI guess I'm just not seeing the equivalence of what seem to me to be assertions, from what I remember from proofs in math.02/11 04:12
Saizanif you replace refl with ?, load the file, you'll see that the goal type there will be "f fzero == f fzero" and refl fits nicely there because it has forall {x} -> x == x as type, so you can just take x = f fzero02/11 04:13
pumpkinpenelope: what do you mean by an assertion? the refl you wrote in there, or the type of lem-!-tab?02/11 04:13
penelopeYeah, I get that.02/11 04:13
pumpkinpenelope: how did you do induction proofs in math?02/11 04:13
Saizanah, then you really need to understand the curry-howard correspondence :)02/11 04:13
dolioIn math, you frequently write only the propositions down.02/11 04:13
dolioIn type theory, we have names for the proofs of each proposition.02/11 04:14
penelopeNo, your right. I'm just having trouble translating...02/11 04:14
dolioSo 'refl' is the name of the proof that 'x == x'.02/11 04:14
penelopeIs it a proof?02/11 04:15
penelopeIt seems more like a statement?02/11 04:15
penelopeI mean, that's an axiom? no?02/11 04:15
Saizanwell, an axiom is the simplest form of proof02/11 04:16
dolioAxioms are propositions. So 'x == x' is an axiom.02/11 04:16
doliorefl is the proof of that axiom.02/11 04:16
Saizanyeah, my bad02/11 04:16
dolioIf you've ever seen proof trees, you could think of the proof names as being written next to the line, for the rule you're using.02/11 04:17
dolio----- refl02/11 04:17
doliox == x02/11 04:17
penelopeThis might be over my head, but I always thought that axioms were unproved, assumed statesments. Atoms.02/11 04:17
lispypenelope: I think dolio just explained it best02/11 04:18
pumpkinpenelope: they are, but you still give them names02/11 04:18
lispydolio: particularly, the statement, "Axioms are propositions."02/11 04:18
Saizanpenelope: from the outside they look like that, but from the inside they simply look as very easy statements to prove02/11 04:18
penelope(without proof?)02/11 04:18
penelopeBut we don't even now which axioms to select from?02/11 04:19
lispypenelope: an axiom may not have a proof.  Sometimes they are just rules to be followed.02/11 04:19
lispyaxiomatizing a subject generally means describing the rules that are used when reasoning from first principles02/11 04:19
penelopeI mean, math is kind of confused about what would make physics work?02/11 04:19
Saizanpenelope: well, if you wanted a complete list you could look at the typing rules02/11 04:19
penelopeOk. I'll grant that the axioms should be obvious.02/11 04:20
penelopeBut aren't they always without proof?02/11 04:20
Saizanbut that's a bit like learning a programming language by reading only the specification02/11 04:20
pumpkinpenelope: consider the proof of an axiom to be equivalent to something like "it is obvious"02/11 04:21
pumpkinrefl is basically like saying "it is obvious"02/11 04:21
pumpkinbut we still consider it a proof for consistency02/11 04:21
pumpkinyou still need to say that, though02/11 04:21
penelopeOk. So that's something that goes on in my head, an not in compiling agda.02/11 04:21
SaizanAgda's type system doesn't pretend to describe reality, btw, it's one formal system among many, it hopes to be consistent within itself at least yough02/11 04:22
Saizan*tough02/11 04:22
penelopeLike haskell's type system.02/11 04:22
lispypenelope: Depending on the axiomatization, some axioms may be provable from other axioms.02/11 04:23
Saizanyeah, except haskell's type system is incositent by design, and it's less expressive02/11 04:23
lispypenelope: In cases like that, we tend to want minimal sets of axioms, so we label some of the axioms as lemmas02/11 04:23
penelopeHey--then they would be theorms!02/11 04:23
lispypenelope: a risk that arises from too many axioms is inconsistency02/11 04:24
penelopeI remember my Godel.02/11 04:24
pumpkinpenelope: anyway, going back to your lem-!-tab, when you pattern matched on the i, you're saying you're doing induction on i. When you wrote the zero case, you wrote the base case of your induction, and by writing refl you wrote "it is obvious for i = zero". Now you need to write the inductive case, which ideally should refer to an earlier case02/11 04:25
penelopeSo, I want to express that, given tabulate f ! (fsuc n) == f (fsuc n) =>02/11 04:25
Saizanto understand how a program can be considered a proof of a proposition we could start with some simple ones from propositional logic, if you want02/11 04:26
penelopetabulate f ! (fsuc (fsuc n)) == f (fsuc (fsuc n))02/11 04:26
pumpkinpenelope: yeah, you want to show it in terms of a smaller case02/11 04:26
pumpkinso ideally if you have i = fsuc n, you want to reduce it to the same statement about n02/11 04:27
Saizanthe usual inductive step would be to assume "tabulate f ! n == f n" and prove "tabulate f ! (fsuc n) == f (fsuc n)", actually02/11 04:27
pumpkinand transform the result of that a bit after recursing02/11 04:27
penelopeI get this. But I'm not able to take the next step. Do you know any good books, or maybe some examples?02/11 04:28
Saizanso you can complete the proof but you're not sure about what it really means?02/11 04:29
penelopeI've tried a number of attemps at expressing a solution, but they tend to fail the type check.02/11 04:30
penelopeI'm still trying to visualize it as a program, but I'm not able to synchronize the visualization as a proof.02/11 04:31
penelopeEven though I know I'm just doing a recursive program.02/11 04:31
pumpkinI'd try with a simpler proof then02/11 04:32
pumpkinI mean, of a simpler statement02/11 04:32
penelopeWould you know a simpler exercise?02/11 04:32
* pumpkin tries to think of something decent02/11 04:32
pumpkinhow about proofs about Bool operations, like demorgan's laws?02/11 04:34
pumpkinon actual data Bool : Set where true false : Bool02/11 04:34
pumpkinthey're fairly simple, and aren't recursive02/11 04:34
penelopeI think -- were I doing it mathmatically -- I'd attempt to take apart tabulet f ! (fsuc n) == f (fsuc n)02/11 04:34
pumpkinin fact, they're obvious to agda :P02/11 04:34
pumpkinso maybe not such a good idea02/11 04:34
penelopeand reduce it to a form where we got to tabulate f ! n == f n02/11 04:35
penelopeBut I think I'm somehow supposed to express this in the form of lem-!-tab f n02/11 04:36
penelope(that being the recursive call)02/11 04:36
pumpkinthat is how you want to do it in agda too02/11 04:36
Saizanthe most simple proof doesn't involve "lem-!-tab f n" actually02/11 04:37
penelope?02/11 04:37
penelopeHow is that possible?02/11 04:37
Saizanpenelope: first look at what "tabulate f ! (fsuc n)" reduces to02/11 04:37
Saizanyou can actually ask agda, if you put your cursor over the hole and use "C-c C-," you'll get the normal form of the goal type (and the variables in scope below it)02/11 04:40
SaizanGoal: tabulate (λ x → f (fsuc x)) ! n == f (fsuc n)02/11 04:40
penelopeBy the way, thanks.02/11 04:41
Saizan(which is "obviously" (to agda) the same as the original "tabulate f ! (fsuc n) == f (fsuc n)" because it just applied the function definitions)02/11 04:41
Saizanpenelope: np :)02/11 04:42
Saizanif you look at that goal type you should spot that it has a familiar structure02/11 04:42
penelopeah02/11 04:43
penelopeso we can do02/11 04:43
penelope(λ x → f (fsuc x)) ! n == (λ x → f (fsuc x)) n02/11 04:45
penelopeoops02/11 04:46
Saizanwell, assuming you forgot a tabulate at that start, that is indeed equivalent to our goal type02/11 04:46
Saizanand we already know how to prove a goal of that form, right?02/11 04:47
penelopeC-c C-, is very interesting!02/11 04:47
Saizanyep, it's probably the most useful command :)02/11 04:48
penelopeGoal: tabulate ((λ {.x} → f) ∘ fsuc) ! m == f (fsuc m)02/11 04:49
Saizanyou can ignore the "λ {.x} →" part02/11 04:50
penelopeI'm wondering about that?02/11 04:50
Saizanit's there to compensate the fact that _∘_ is overly general for our purpouses02/11 04:50
penelopef is already a monadic function...02/11 04:50
penelopeah02/11 04:51
Saizanso, anyhow "tabulate (λ x → f (fsuc x)) ! m == (λ x → f (fsuc x)) m" matches exactly the type of "lem-!-tab (f ∘ fsuc) m"02/11 04:52
Saizanso we can just use that02/11 04:52
Saizanwhich corresponds to appealing to the inductive hypothesis02/11 04:52
penelopeI will have to spend some time thinking about this..02/11 04:53
penelopebut it would not match the type of..02/11 04:54
Saizanof?02/11 04:54
penelopetabulate (λ x → f x) ! m == (λ x  → f x) m02/11 04:55
Saizanright02/11 04:55
penelopeOk. So I think I can probably put together a proof for lem-!-tab.02/11 04:56
penelopeBut02/11 04:56
penelopeI still feel like I'm waving in the dark.02/11 04:56
penelopeLet me play with this for a bit, and I'd hope to chat later.02/11 04:57
Saizanok :)02/11 04:57
penelopeAnd if you know any good text books, or a page with some exercises, wow. Anyway, I really appreciate your patience. I don't know why I'm so dense. I feel as stupid as when I was first doing FP.02/11 04:59
Saizantbc, our reasoning about the equivalent goal types that we did above doesn't have to be explicit in the proof, which in fact looks very simple02/11 04:59
Saizanyou shouldn't feel dense, it really is like learning a new paradigm, anyhow i was just as much confused at the start02/11 05:00
pumpkinyeah, same here02/11 05:00
penelopeIt seems, if I understand correctly, to make QuickCheck look as crude as unit testing.02/11 05:01
Saizanyeah :)02/11 05:01
penelopewow.02/11 05:01
pumpkinyep, but I actually would appreciate quickcheck in agda02/11 05:01
pumpkinor something similar to it02/11 05:01
penelopeNo randoms?02/11 05:01
penelopeOr no library?02/11 05:01
pumpkinsort of as a meta-tool in agda-mode, simply because sometimes I set out to prove something that isn't obviously false (to dumb me)02/11 05:02
Saizanthe downside is that proof can require much more effort than just running quickCheck02/11 05:02
pumpkinbut has a simple counterexample02/11 05:02
Saizanbut then they also let you know much more02/11 05:02
pumpkinand it'd be nice if when I set out to prove something, agda would search for simple counterexamples and tell me I'm dumb02/11 05:02
Saizan(*proofs)02/11 05:02
pumpkinrather than have me slave away for half an hour and then figuring out my statement was wrong02/11 05:02
penelopeAh. Too bad agda-mode is written in emacs-lisp.02/11 05:03
penelopeYeah, that would be nice.02/11 05:03
penelopeAnyway, thank you all so much! You've been tremendously helpful. xoxo!02/11 05:04
Saizancheers :)02/11 05:04
pumpkinpenelope: we look forward to more questions!02/11 05:04
Spockzpumpkin: how are you with the agda highlighting api thingy?02/11 22:12
pumpkinbeen wrapped up with other stuff, sorry :/02/11 22:12
Spockzno problem :p02/11 22:13
--- Day changed Wed Nov 03 2010
pumpkinwhat's the heaviest module in the standard library?03/11 04:38
pumpkin(the most painful to typecheck)03/11 04:38
Saizanwhen typechecking the whole stdlib i often get an overflow at ..BagAndSetEquality, but i'm not sure if it's singularly heavy03/11 04:40
pumpkinI'm just stress testing my laptop03/11 04:44
pumpkin:P03/11 04:44
dolioWhy not just load Everything or whatever it's called?03/11 04:45
pumpkinmostly cause it's not in my search path03/11 04:45
pumpkinand in a hidden dir :P03/11 04:45
pumpkinbut I might just d othat03/11 04:45
pumpkinyeah, BagAndSetEquality is pretty heavy03/11 04:46
pumpkinfan hasn't come on yet, but it's using 700MB of RAM03/11 04:46
djahandarieMy thinkpad tends to overheat if I'm not careful03/11 04:46
pumpkinmy old laptop did even if I was careful03/11 04:46
pumpkinI am madly in love with this new one though03/11 04:47
djahandarieThere needs to be more noob questions in here03/11 04:47
pumpkinhow come?03/11 04:47
pumpkin(but it'd be nice, I agree)03/11 04:47
djahandarieSo I can learn by proximity03/11 04:47
pumpkinlol03/11 04:47
djahandarieI don't want to provide them because I like looking smart03/11 04:48
djahandarie:P03/11 04:48
pumpkinhave you read the tutorial? it's very accessible03/11 04:48
djahandarieTo be honest I haven't put in very much effort into learn Agda03/11 04:48
djahandarieOne day I'll try it and get really focused and learn it though03/11 04:48
djahandarieThat's how things tend to be with me...03/11 04:48
djahandarieI'll continue watching videos of this crossdressing guy covering Japanese songs on the bass in the meantime03/11 04:50
pumpkinlol03/11 04:51
pumpkinokay, here goes03/11 04:51
pumpkinopen import Everything03/11 04:51
djahandarieNever to be heard from again03/11 04:55
pumpkinno, I'm still alive :P03/11 04:56
pumpkinit crashed though03/11 04:56
pumpkinat about 2.5GB of RAM03/11 04:56
Saizanheap overflow?03/11 04:57
pumpkinnot sure, emacs started pegging my CPU when GHCi died03/11 04:58
Saizanah, yeah, that's quite annoying03/11 04:59
Saizani usually stress test with the agda excutable03/11 04:59
--- Day changed Thu Nov 04 2010
cadshey, how easy is it to adjoin haskell with agda to provide things like for instance a proof that a given functor instance really represents a functor?04/11 23:30
cadsare there facilities for reasoning about haskell code in agda?04/11 23:33
--- Day changed Fri Nov 05 2010
copumpkincads: nope05/11 00:16
stevani wish one could inject some html thru comments into the html output, e.g. -- some comment bla bla <some url> bla bla, and in the html output it would actually be come a link. likewise it would be nice to be able to refere to functions in comments, but i guess that is harder. images would be nice too.05/11 14:01
Spockzstevan: hasn't that already be done thousand times over?05/11 14:12
stevanit has, but not in this context? :-)05/11 14:14
stevanwhile on it, one might as well add latex injection via js or whatever. that would make the html output superior to literate agda in many ways imo.05/11 14:24
Spockzhi copumpkinhow are you?05/11 14:39
Spockzlatex injection via JS?05/11 14:39
stevane.g. mathoverflow and other mathy blogs do05/11 14:41
stevandoing it statically would be even better i guess05/11 14:42
Spockzyou mean that something between $$ is send to the server and it returns an image or something?05/11 14:42
stevanyea05/11 14:42
--- Day changed Sat Nov 06 2010
syntaxglitchI don't know if anyone's even watching this channel, but... is there any easier way to write bindings to Haskell modules? All the boilerplate is pretty tedious, especially for types with lots of nullary data constructors...06/11 19:57
dolioI don't think so.06/11 20:25
syntaxglitchhm06/11 20:26
syntaxglitchin that case, any advice on the easiest way to parse Haskell code? is the haskell-src package the best option?06/11 20:29
syntaxglitchor would there be a better way to generate bindings for agda? all I really need are data declarations and type signatures, I suppose06/11 20:30
dolioAgda uses haskell-src in some capacity, although I don't know what.06/11 20:31
doliohaskell-src-exts is more actively developed, I think.06/11 20:31
dolioAnd parses more of what GHC parses.06/11 20:31
syntaxglitchactually, shouldn't the .hi file have everything that the agda bindings needs? that might be easier.06/11 20:32
dolioI don't really know.06/11 20:32
syntaxglitch'k, thanks anyway06/11 20:32
--- Day changed Sun Nov 07 2010
danris there a way to see the code the rewrite keyword produces?07/11 15:19
Associ8orjoinx #haskell07/11 19:00
Associ8orsorry forgot the slash07/11 19:00
Spockzwho knows where the HOL irc channel is? (The theorem prover)07/11 21:29
dolioHow do you know there is one?07/11 21:30
SpockzI'm merely wishing there is one :)07/11 21:30
Spockzhowever, the problems I'm having finding it suggest otherwise07/11 21:30
--- Day changed Mon Nov 08 2010
roconnordoes agda support non-uniform recursive data types?08/11 21:24
copumpkinhow do you mean?08/11 21:27
ccasinroconnor: well, yes, in the sense that indices don't have to be uniform08/11 21:42
ccasinbut I don't think it supports non-uniform parameters, like coq08/11 21:42
ccasinnon-uniform parameters have always been a little bit of a mystery to me, in coq.  I always thought that the whole point of parameters is you get a better induction principle exactly because they are uniform08/11 21:44
ccasinThey tell me, though, that even though non-uniform parameters get treated like indices for the elimination principles, they are still useful to avoid bumping up the universe level of a datatype08/11 21:44
dolioYes, it supports non-uniform parameters.08/11 21:45
ccasinI haven't fully grokked the examples of this08/11 21:45
ccasinagda does?08/11 21:45
dolioYes.08/11 21:45
ccasindo you need a special flag?08/11 21:46
ccasinthe example I am trying doesn't work08/11 21:46
dolioI don't think so.08/11 21:46
ccasinhttp://hpaste.org/41299/nonuniform_parameters08/11 21:47
ccasinthat gets rejected08/11 21:47
dolioThat's trying to use a parameter as an index.08/11 21:48
dolioNon-uniform parameters let you take Foo Bool as an inductive argument.08/11 21:48
ccasinah, right, my mistake08/11 21:48
ccasinand that goes through08/11 21:48
ccasinsilly me08/11 21:49
dolioI don't really understand the underlying theory of that, either.08/11 21:49
ccasinanyway, can you enlighten me about why these are useful?08/11 21:49
dolioOne of the justifications of parameters (and their not affecting size) is that you can pull them out of the datatype and stick them in, say, a parameterized module.08/11 21:49
dolioBut obviously you can't do that with non-uniform parameters.08/11 21:49
dolioWell, there's a nice formulation of debruijn-indexed lambda terms as a nested type.08/11 21:50
ccasinthere is this thread:08/11 21:50
ccasinhttp://thread.gmane.org/gmane.science.mathematics.logic.coq.club/492008/11 21:51
ccasinI thought I understood the examples at the time, but I don't really remember any of it now08/11 21:51
ccasinalas08/11 21:51
doliohttp://hpaste.org/paste/41299/lambda_terms_with_de_bruijn_in#p4130008/11 21:52
ccasinoh my08/11 21:55
ccasindolio: that's really nifty08/11 21:55
ccasinthanks for the example08/11 21:55
ccasinI wonder what the type-theoretic difference is that makes this OK, but not if V is an index08/11 21:56
dolioI'm not sure that's nicer than using a Nat-indexed type and finite sets as variables in a dependently typed language, though. It's more useful when nested types are all you have (like, pre-GADT Haskell).08/11 21:56
ccasinyeah, it's still pretty cool though08/11 21:56
dolioYes.08/11 21:57
dolioAgda doesn't actually make things bigger with large indices automatically.08/11 21:57
dolioIt only happens if you quantify over them in constructors.08/11 21:57
ccasinyeah, I think coq is the same?08/11 21:57
ccasinof course, here one would need to08/11 21:57
dolioYeah.08/11 21:57
dolioYou can argue that's impredicative.08/11 21:57
ccasinSure, but "some" impredicativity should be OK08/11 21:58
dolioYeah, unless you're a real hard-liner.08/11 21:58
ccasinI discovered the other day that if you turn on impredicative set in coq08/11 21:58
dolioNested parameters sometimes seem like they're a little more lax than large indices even.08/11 21:58
ccasinand define a datatype exploiting it08/11 21:58
ccasincoq will stop you from doing large eliminations from that datatype08/11 21:59
ccasinthe error message just says "this would cause inconsistency"08/11 21:59
ccasinbut in the user manual, all the references are in french :(08/11 21:59
dolioHeh.08/11 21:59
ccasinso I wonder if impredicativity is just incompatible with large eliminations in general08/11 21:59
dolioIt may be. But I don't know much about impredicativity in inductive datatypes.08/11 22:00
dolioAnyhow, I've got to go for a bit.08/11 22:00
--- Day changed Tue Nov 09 2010
dolioBah, ccasin needs to come back so I can tell him the stuff I remembered.09/11 01:13
pumpkinwe could join lambdabot here and use @tell09/11 01:32
--- Log closed Tue Nov 09 06:34:19 2010
--- Log opened Tue Nov 09 06:40:58 2010
-!- Irssi: #agda: Total of 28 nicks [0 ops, 0 halfops, 0 voices, 28 normal]09/11 06:40
-!- Irssi: Join to #agda was synced in 85 secs09/11 06:42
Saizanwhy is it always a pain to prove things about concat?09/11 17:29
SpockzSaizan: is it?09/11 18:14
dolioccasin: Ping.09/11 20:04
ccasindolio: hi09/11 20:12
dolioSo, I remembered something important shortly after I left yesterday. But you were gone by the time I got back.09/11 20:12
ccasinalas09/11 20:12
dolioAnd that is: strong, impredicative sums are inconsistent.09/11 20:12
ccasinyes, this much I know09/11 20:12
ccasinthough, I don't know why09/11 20:12
dolioBecause you can have: (Σ (Set i) ⊤) : Set₀09/11 20:13
dolioFor any i.09/11 20:13
ccasinah, makes perfect sense09/11 20:13
dolioAnd if you can project out the first component, you essentially have Set0 : Set 0.09/11 20:13
ccasinI knew that coq gives you weak elimination principles for impredicatively defined Sets, but wasn't sure why09/11 20:14
ccasinthe references are from the 70s/80s and in french :)09/11 20:14
dolioAnyhow, the same would happen with impredicative quantification in inductive types. But, if you don't allow large elimination, you can't project out the large part, so you avoid the inconsistency (presumably).09/11 20:14
ccasinyeah, that is just what coq does09/11 20:15
ccasincool, I'm really glad to have an example of this09/11 20:15
ccasinwe have been having some fighting about this subject on the internal trellys mailing list :)09/11 20:16
dolioThere are other ways to make the sums effectively weak. Like modal type theory.09/11 20:17
dolioBut that's another story, I guess.09/11 20:18
ccasinHmm, actually, I'm having trouble with your example09/11 20:22
ccasinI want to get to Set 0 : Set 009/11 20:23
dolioYou don't literally get Set 0 : Set 0.09/11 20:23
ccasinyeah, OK09/11 20:24
ccasinbut you're saying this weird pair which contains Set 0 and has type Set 0 - that should be enough to get to a girard's paradox-like situation09/11 20:24
dolioHowever, you get (Σ (Set 0) ⊤) : Set 0, and inj : Set 0 -> (Σ (Set 0) ⊤), proj : (Σ (Set 0) ⊤) -> Set 0, proj . inj = inj . proj = id.09/11 20:24
dolioYes. Although I haven't worked it out for myself. I'm just citing Luo.09/11 20:25
ccasinwhich luo?09/11 20:25
ccasinI have his book here09/11 20:25
ccasin(which reference, I mean)09/11 20:25
dolioIt's in there somewhere. If you're talking A Type Theory for Computer Science.09/11 20:25
ccasinyes09/11 20:25
dolioI don't think he actually works it out, either.09/11 20:26
ccasinexcellent, thanks09/11 20:26
dolioBut he explains why he's disallowing strong sums from the lowest level.09/11 20:26
ccasinit's good enough just to have an english-language reference that gives a specific example09/11 20:26
ccasinThanks for your help!  Luo references a tech report called "Impredicative Strong Existential Equivalent to Type:Type" which promises to go into some detail09/11 20:34
dolioAh, yeah, that sounds good.09/11 20:35
stevani found some new utf8 symbols i'd like to share: http://hpaste.org/41324/utf8s   :-)09/11 21:59
pumpkinooh, I like ↻ and ↺09/11 21:59
Adamantclockwise and counter-clockwise symbol, huh09/11 22:10
stevanhttp://www.fileformat.info/info/charset/UTF-8/list.htm   premature optimisation agda-style09/11 22:14
--- Day changed Wed Nov 10 2010
danrWhere is the IsEquivalence for _\==_ lurking?10/11 13:46
SaizanRelation.Binary.PropositionalEquality.isEquivalence10/11 14:15
Saizanre-exported from ....Core10/11 14:15
danrSaizan: thanks :)10/11 14:24
--- Day changed Thu Nov 11 2010
dolioWow, Agda now uses haskell-src-exts.11/11 01:20
Saizandoes it also build on ghc 7?11/11 07:29
dolioNot sure, but they've been working on that.11/11 07:31
dolioI guess they weren't confident that haskell-src would be made to work.11/11 07:31
Saizanneeded darcs haskeline but it went through11/11 08:01
SpockzI'm having trouble compiling this in 2.2.6: https://gist.github.com/672654 It works in 2.2.8 though11/11 15:48
Spockzif I case split on the first parameter, it first comes up with refl and then gives the given error11/11 15:50
SaizanSpockz: what error do you get in with 2.2.6 ?11/11 15:50
SpockzSaizan: I added it to the gist, refresh :)11/11 15:50
Saizanhttps://gist.github.com/672654#comments <- meh, got mangled by the comment system, but i think that should work in both 2.2.6 and 2.2.8 if you can see what i tried to do11/11 15:54
SpockzSaizan: unfortunately, no: https://gist.github.com/672654#gistcomment-1383611/11 15:57
SpockzSaizan: well, it works in 2.2.8 but not in 2.2.611/11 15:57
Saizanah11/11 15:59
Saizandoes "pairing-inj eq = cong proj1 eq , cong proj2 eq" work?11/11 16:00
Spockzyes, that compiles :)11/11 16:00
Spockzthanks Saizan :D11/11 16:23
Saizannp11/11 16:24
--- Day changed Sun Nov 14 2010
Saizanwhat would be a good way to gain some intuition on realizability?14/11 12:55
--- Day changed Tue Nov 16 2010
Saizanis there an implementation of Pure Type Systems in Agda?16/11 12:29
Saizanit seems it's impossible to have a shallow embedding16/11 12:30
--- Day changed Thu Nov 18 2010
edskoanybody here?18/11 10:11
edskono?18/11 10:13
Saizanhi18/11 10:18
edskohi18/11 10:19
edskoare you an Agda user?18/11 10:19
Saizanyep18/11 10:19
edskocan I ask a very basic question?18/11 10:19
Saizansure18/11 10:19
edsko(I started learning Agda yesterday, having used Coq for years)18/11 10:19
edskohere is an extremely simple lemma:18/11 10:20
edskobar : {A : Set} {n : Nat} {x y : A} {xs ys : Vec A n} -> x == y -> xs == ys -> x :: xs == y :: ys18/11 10:20
edskobar {A} {n} {x} {.x} {xs} {.xs} refl refl = refl18/11 10:20
edskoAgda however complains that there are unresolved implicit variables18/11 10:21
edskopresumably because it doesn't know whether the :: in the conclusion18/11 10:21
edskorefers to the list constructor or the vector constructor18/11 10:21
edskoI can fix it as follows:18/11 10:21
edskobar : {A : Set} {n : Nat} {x y : A} {xs ys : Vec A n} -> x == y -> xs == ys -> x :: xs == y :: ys let xs' : Vec A (succ n) ; xs' = x :: xs in  let ys' : Vec A (succ n) ; ys' = y :: ys in xs' == ys'18/11 10:21
edskobar {A} {n} {x} {.x} {xs} {.xs} refl refl = reflbut that's rather ugly!18/11 10:21
edskosurely there must be a better way?18/11 10:22
Saizanyeah18/11 10:23
Saizanlet me find the operator for type annotations in the stdlib18/11 10:24
Saizanotherwise you could use Vec._::_ x xs == y :: ys18/11 10:24
edskoah, I had been looking for a type annotation18/11 10:24
edskobut couldn't find anything in the language18/11 10:24
Saizanthere's the ∶ operator/syntax defined in the Function module18/11 10:26
edskoI'm not using the stdlib at the moment, following the AFP08 tutorial.18/11 10:26
edskobut ok, I'll have a look18/11 10:26
edskothanks.18/11 10:26
edskothe absence of tactics is wrecking my head :)18/11 10:27
Saizanas a simple operator you can define _∶_ : (A : Set) -> A -> A, but then you've to place the type on the left, the new syntax mechanism let you reverse the order of the arguments18/11 10:28
edskook, cool18/11 10:29
Saizananyhow it's just the identity function in the end18/11 10:29
edsko_:_ is you mean?18/11 10:29
Saizanyep18/11 10:30
edskosure, of course18/11 10:30
edskoI had just assumed it would have been in the language18/11 10:30
edskobut it makes sense to define it within the language18/11 10:30
Saizanthe only downside is that you can't reuse : because that's taken as a keyword, but unicode is large enough to contain another :)18/11 10:31
edskoah, I had been wondering about that overloading18/11 10:32
edskofair enough18/11 10:32
edskoright, one more question and I'll stop disturing you :)18/11 10:32
edskothis lemma I mentioned above18/11 10:32
edskobasically, :: is injective18/11 10:32
edskois that a useful one?18/11 10:32
edskoas in, should I need to define it?18/11 10:32
edskolem-::-inj : {A : Set} {n : Nat} {x y : A} {xs ys : Vec A n} -> x == y -> xs == ys -> Vec._::_ x xs == y :: ys18/11 10:33
edskolem-::-inj {A} {n} {x} {.x} {xs} {.xs} refl refl = refl18/11 10:33
edskolem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs18/11 10:33
edskolem-tab-! {n = zero} [] = refl18/11 10:33
edskolem-tab-! {n = succ m} (x :: xs) with lem-tab-! xs18/11 10:33
Saizanit's sometimes useful, but in those cases you can just use cong _::_18/11 10:33
edsko... | p = lem-::-inj refl p18/11 10:33
edskoin Coq I would do two rewrites in the proof of lem-tab-!18/11 10:34
Saizanthere you could've pattern matched on p, i think18/11 10:34
edskowell, if I leave a hold, I get18/11 10:34
edskoGoal: x :: tabulate ((λ {.x} → _!_ (x :: xs)) ◦ fsucc) == x :: xs18/11 10:34
edskothe tails are equal by p18/11 10:35
edskothe heads are already the same18/11 10:35
edskoso hence my use of lem-::-inj18/11 10:35
Saizanright, and if you put refl as a pattern for p the tails should be equal too18/11 10:35
edskoyou mean:18/11 10:36
edskolem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs18/11 10:36
edskolem-tab-! {n = zero} [] = refl18/11 10:36
edskolem-tab-! {n = succ m} (x :: xs) with lem-tab-! xs18/11 10:36
edsko... | refl = {! !}18/11 10:36
edsko?18/11 10:36
Saizanyes18/11 10:36
edsko/Users/edsko/svn/globalcomputing/code/agda/AgdaBasics.agda:341,7-1118/11 10:36
edskotabulate (_!_ xs) != xs of type Vec A m18/11 10:36
edskowhen checking that the pattern refl has type18/11 10:36
edskotabulate (_!_ xs) == xs18/11 10:36
edskooh, perhaps I have to dot some arguments?18/11 10:37
Saizanah, maybe it doesn't refine because xs appears on both sides18/11 10:37
edskoI don't really understand the error message18/11 10:38
Saizanwell, it's trying to typecheck the refl pattern18/11 10:39
edskomust succeed though right18/11 10:39
edskoonly one way to construct == :)18/11 10:39
Saizanheh, but that way carries a constraint on the two indexes, they must be equal18/11 10:40
Saizanso when pattern matching it has to find a substitution of the context that makes them equal18/11 10:40
Saizanit won't just leave that constraint dangling18/11 10:40
edskoand it's unable to unify tabulate (_!_ xs) and xs you mean?18/11 10:41
Saizanthat's what i'm guessing18/11 10:41
edskoof course, then lem-::-inj goes right ahead and does a pattern match on it anyhow..18/11 10:41
edskowell, anyway. I have *a* proof for the exercise now. fun to learn something new. but confusing for a Coq user :)18/11 10:42
edskothanks for the help18/11 10:42
Saizannp18/11 10:42
Saizananyhow, your lem-::-inj doesn't seem a proof of the injectivity of ::, in fact a similar thing holds for every function18/11 10:43
edskoer18/11 10:44
Saizancong₂ : {A : Set} {B : Set} {C : Set} (f : A → B → C) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v -- you can prove this18/11 10:44
edskosorry18/11 10:44
edskoyes18/11 10:44
edskoof course18/11 10:44
edskoyou'r right18/11 10:44
Saizan(and the unary version too)18/11 10:44
edskosome sort of Leibniz law I guess18/11 10:46
Saizancong is short for congruence i think18/11 10:47
edskois that a function from the stdlib?18/11 10:47
Saizanyep18/11 10:49
Saizanin Relation.Binary.PropositionalEquality18/11 10:49
edskook, must make a point of studying that18/11 10:49
Saizanhttp://hpaste.org/41603/lemtab <- another way to prove the lemma18/11 10:50
Saizanwhich is the same as "lem-tab-! {A} {suc n} (x :: xs) rewrite lem-tab-! xs = refl" with a recent enough agda18/11 10:51
Saizanthough maybe the tutorial introduces with later?18/11 10:51
edskono, it's introduced with18/11 10:51
edskosure, I used it in my proof too18/11 10:51
edskoto get the induction hypothesis18/11 10:52
Saizanah, true18/11 10:52
Saizanbtw, you didn't need it18/11 10:52
edskoyeah, because I didn't pattern match on it I guess18/11 10:52
Saizanyeah18/11 10:52
edskobut I couldn't figure out *why* I couldn't pattern match on it18/11 10:53
edskoah, you are introducing tabulate (_!_ xs) as a variable, enabling unification?18/11 10:53
edskosomething along those lines?18/11 10:53
Saizanight18/11 10:53
Saizan*exactly that18/11 10:53
edskoih, Agda doesn't seem to like it..18/11 10:56
Saizanit typechecks here, but i'm using the darcs version18/11 10:57
edskoyes, me too18/11 10:57
edskohold on18/11 10:57
edskonot sure that your definitions of tabulate etc correspond to mine; they come from the tutorial18/11 10:58
edskobut if I change the last line to18/11 10:58
edskolem-tab-! {A} {succ _} (x :: xs) | .xs | refl = {! !}18/11 10:58
edskoI get18/11 10:58
edskoGoal: x :: tabulate ((λ {.x} → _!_ (x :: xs)) ◦ fsucc) == x :: xs18/11 10:58
edskooh, perhaps I need to change the line above to make it match?18/11 10:59
edskonot sure why it's not reducing it further18/11 10:59
Saizanhttp://hpaste.org/paste/41603/a#p41605 <- these are the definitions i'm using18/11 11:02
edskoyeah, exactly the same18/11 11:07
edskohm.18/11 11:07
edskoif you do18/11 11:07
edskohttp://hpaste.org/paste/41603/a#p4160518/11 11:08
edskowhoops, sorry18/11 11:08
edskolem-tab-! {A} {succ _} (x :: xs) | .xs | refl = {! !}18/11 11:08
edskowhat goal do you get?18/11 11:08
edsko(I get Goal: x :: tabulate ((λ {.x} → _!_ (x :: xs)) ◦ fsucc) == x :: xs )18/11 11:08
Saizani get  x :: xs == x :: xs18/11 11:09
Saizanas a goal18/11 11:10
edskooh.18/11 11:10
Saizanyou've "lem-tab-! {A} {succ n} (x :: xs) with tabulate (_!_ xs) | lem-tab-! xs" on the line above, right?18/11 11:10
edskoyes18/11 11:12
edskolet me remove everything in my file18/11 11:12
edskoexcept the essentials18/11 11:12
edskosee what's going on18/11 11:12
edskohttp://hpaste.org/paste/41603/full_file#p4160618/11 11:19
edskois my entire file18/11 11:19
edskono stdlib18/11 11:19
edskoAgda 2.2.918/11 11:20
edskofrom darcs18/11 11:20
Saizanwi get the same goal as you there18/11 11:25
edskoso what is the difference?18/11 11:26
edskoam I doing something stupid somewhere :-/18/11 11:26
Saizanit seems the difference is in the definition of the composition function18/11 11:29
edskoreally? wow18/11 11:31
edskolet me replace it with the version from the stdlib18/11 11:32
Saizanyeah, replace "(f ◦ g) x = f (g x)" with "(f ◦ g) = \ x -> f (g x)" and it works18/11 11:32
edskopffffff18/11 11:32
edskowow.18/11 11:32
edskothat's weird.18/11 11:32
Saizanyeah, you'd expect those to be equivalent..18/11 11:33
edskosure would18/11 11:34
edskoI'm guessing because ana rgument is missing it doesn't unroll18/11 11:34
edskoor something like that18/11 11:34
Saizanyeah, i'm guessing the same18/11 11:34
edskowell, I guess every system has its quirks18/11 11:34
Saizani wonder if it qualifies as a bug..18/11 11:34
edskowas just thinking the same myself. however, having been using agda for two days, I don't feel qualified to say :)18/11 11:34
Saizanmatters are probably more complex than one would think due to implicit arguments, even if in this specific case there are none between g and x18/11 11:39
Saizanat least worth asking on the ml, anyhow :)18/11 11:40
edskook18/11 11:42
edskowill I send an email?18/11 11:42
Saizansince you found the problem it's probably more appropriate, if it's not a problem :)18/11 11:46
edskosure, no problem18/11 11:46
edskois Saizan your real name or an IRC nickname only?18/11 11:47
Saizanirc nickname18/11 11:47
Saizanthe real one is Andrea Vezzosi18/11 11:48
edskook, well, thanks for the help Andrea :)18/11 11:48
Saizannp :)18/11 11:48
edskoanybody here still?18/11 20:55
copumpkinyep18/11 20:55
edskodo you have time for a quick Agda beginner question?18/11 20:55
copumpkinsure18/11 20:55
edskook. going through the AGP'08 tutorial, and there is a question at some point to prove:18/11 20:56
edskolem-filter-sat : {A : Set} (p : A -> Bool) (xs : List A) -> All (satisfies p) (filter p xs)18/11 20:56
edskothe tutorial explains (later) to use the 'inspect' datatype to pattern match on p x and get a proof that p x is true (or false)18/11 20:56
edskoso, I do18/11 20:56
edskolem-filter-sat p [] = all[]18/11 20:56
edskolem-filter-sat p (x :: xs) with inspect (p x)18/11 20:56
edsko... | it true  prf = {! !}18/11 20:56
edsko... | it false prf = {! !}18/11 20:56
edskoin the first hole, I now know that18/11 20:57
edskoprf : p x = true18/11 20:57
edskohowever, the goal is18/11 20:57
edskoGoal: All (satisfies p) (filter p (x :: xs) | p x)18/11 20:57
edskoi.e., it's clear to Agda that p x is in fact true18/11 20:57
edskoand filter p (x :: xs) does not get unrolled to x :: filter p xs18/11 20:57
edskohow do I fix that?18/11 20:57
edsko*not clear to Agda, I mean18/11 20:59
dantenis prf a proof that p x = true ?18/11 21:11
dantenin that case, does pattern matching on prf work?18/11 21:11
edskoGoal: All (satisfies p) (filter p (x :: xs) | p x)18/11 21:12
edsko————————————————————————————————————————————————————————————18/11 21:12
edskoxs  : List .A18/11 21:12
edskoprf : p x == true18/11 21:12
edskox   : .A18/11 21:12
edskop   : .A → Bool18/11 21:12
edsko.A  : Set18/11 21:12
edskobut I need the proof to construct the proof of (satisfies p)18/11 21:12
edskofirst of all18/11 21:12
edskoand second, if I try to pattern match on it, I get18/11 21:12
edsko/Users/edsko/svn/globalcomputing/code/agda/AgdaBasics.agda:475,16-2018/11 21:13
edskop x != true of type Bool18/11 21:13
edskowhen checking that the pattern refl has type p x == true18/11 21:13
copumpkinoh18/11 21:13
edskowhich I don't really understand18/11 21:13
copumpkinpattern match refl on it, and then write .true in the other one18/11 21:13
copumpkinthe dot means that it's fully determined by another pattern match (the refl in this case)18/11 21:13
edskoif I change it to18/11 21:14
edsko... | it .true refl = {! !}18/11 21:14
edskoI get18/11 21:14
edsko/Users/edsko/svn/globalcomputing/code/agda/AgdaBasics.agda:475,11-1518/11 21:14
edskotrue != p x of type Bool18/11 21:14
edskowhen checking that the given dot pattern true matches the inferred18/11 21:14
edskovalue p x18/11 21:14
edskoI'm not pattern matching on p x though right, I'm pattern matching on (inspect (p x)). And if I change that to refl, don't I loose the proof that p x = true, which I need to construct the (satisfies p) bit?18/11 21:15
copumpkinby matching refl on it, you're "telling agda"18/11 21:16
dantenyou could probably add p x to the with clause also and pattern match on it (using dot pattern on one of them)18/11 21:16
edskoyes, I tried that:18/11 21:17
edskolem-filter-sat p (x :: xs) with inspect (p x) | p x18/11 21:17
edsko... | it .true prf | true = {! !}18/11 21:17
edsko... | it false prf = {! !}18/11 21:17
edskobut that gives:18/11 21:17
edsko/Users/edsko/svn/globalcomputing/code/agda/AgdaBasics.agda:475,10-1518/11 21:17
edskoFailed to infer the value of dotted pattern18/11 21:17
edskowhen checking that the pattern .true has type Bool18/11 21:17
copumpkinhere, try something else18/11 21:18
edsko(and likewise when I dot the other one)18/11 21:18
copumpkinit true prf rewrite prf = ...18/11 21:18
dantencan you have that and also match prf against refl?18/11 21:18
edskooh, haven't come across 'rewrite' yet :)18/11 21:19
copumpkinrewrite is equivalent to matching against refl18/11 21:19
danrI have been using quite a lot of rewrite, but I only understand it intuitively. Does someone knows where it is explained a bit in detail?18/11 21:20
edskoah, that works actually18/11 21:20
edskonow I have the proof *and* it's unrolled18/11 21:21
edskook, now I need to understand what rewrite does :)18/11 21:21
edskothanks18/11 21:21
dantenhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-6 the second item18/11 21:21
danrdanten: thanks18/11 21:22
danten:)18/11 21:22
danri thought it did something more clever than just pattern match on it :P18/11 21:23
copumpkinwell18/11 21:23
copumpkinit pattern matches on it and takes care of putting the dots in :)18/11 21:23
dantendanr: our agda compiler now can compile fac, and it translates Nat to nice GMP integers :) I have to show you sometime18/11 21:24
danrdanten: sure, can't we meet at the uni some time next week?18/11 21:24
dantenthat would be nice, we programmed alot today and now we also have some IO18/11 21:25
edskook, thanks guys, I'm off18/11 21:29
edskoappreciated the help18/11 21:29
--- Day changed Sat Nov 20 2010
edskoanyone around?20/11 16:37
* Saizan waves his hand20/11 16:38
edskovery quick question about syntax, if you don't mind20/11 16:38
edskoif I dot a pttern like20/11 16:38
edsko.(x :: xs)20/11 16:38
edskothen it interprets it as if the whole thing is dotted20/11 16:39
edskowhat if I want to say that it must be of the form (somethnig :: something else)20/11 16:39
edskobut the something and somethnig else aren't "dotted" themselves?20/11 16:39
edskoI tried (x .:: xs)20/11 16:39
edskoand (.List._::_ x xs)20/11 16:39
edskobut neither works20/11 16:39
Saizani don't think you can20/11 16:39
edskooh20/11 16:40
edskobummer :)20/11 16:40
Saizanyeah, it's a bit annoying20/11 16:41
edskook, well, at least I know not to look for it so :)20/11 16:42
edskothanks20/11 16:42
Saizanoften you have 'x' and 'xs' in scope from your proof that it's a cons though20/11 16:42
edskoyes, I guess I had that here too20/11 16:43
edskoas implicit arguments20/11 16:43
edskowhich is why I didn't realize it at first20/11 16:43
edskolem-filter-complete p x {.(y :: xs)} (tl {y} {xs} p∈) psat = {! !}20/11 16:43
edskoworks nicely20/11 16:43
edskoand makes sense20/11 16:43
edskothanks20/11 16:58
Saizannp20/11 17:01
--- Day changed Sun Nov 21 2010
copumpkinanyone ever see an "incomplete pattern matching" error in agda? :P21/11 16:04
copumpkinI must say, agda was the last place I'd expect to see that21/11 16:04
copumpkinI get it when trying to normalize an expression21/11 16:06
Saizanhah21/11 16:11
Saizanno, i don't think i've seen one :)21/11 16:11
copumpkinI just translated oleg's symantics approach to a HOAS GADT to agda21/11 16:13
byorgeyI'm confused, why would you not expect to see such an error in agda?21/11 16:13
copumpkinbecause it forces you to pattern match on everything or it won't typecheck?21/11 16:14
copumpkinthis module typechecks fine21/11 16:14
copumpkinbut C-c C-n reveals "incomplete pattern matching"21/11 16:14
copumpkinhere, try it: http://hpaste.org/41677/incomplete_pattern_matching_x321/11 16:14
byorgeyoh, I see, that is strange21/11 16:15
copumpkinwhat's neat is that evalR x2 actually prints a lambda term when normalized, though21/11 16:17
copumpkinbug?21/11 16:35
dolioCan you paste what the error says?21/11 16:37
copumpkinit's pretty short21/11 16:38
copumpkinhttp://snapplr.com/f3z421/11 16:38
dolioIt sounds like a GHC error is propagating up to display in the Agda buffer somehow.21/11 16:38
copumpkinI'll look at the ghci buffer21/11 16:39
copumpkinhmm, that didn't reveal much21/11 16:39
dolioBecause there's not pattern matching in that module except 'yes' and 'no'.21/11 16:39
copumpkinyeah, and that part isn't even used in the failing case21/11 16:39
copumpkinhttp://hpaste.org/41678/incomplete_pattern_matching21/11 16:40
copumpkinit seems like it'd be a reasonably pleasant way of representing terms in agda, if it worked21/11 16:40
dolioWell, that stuff doesn't mean much to me.21/11 16:41
copumpkinyeah21/11 16:41
dolioMy bet is on incomplete pattern matching in the Agda implementation, though.21/11 16:41
copumpkinyeah21/11 16:41
copumpkinany incomplete pattern matching in agda should result in a typechecking error, anyway21/11 16:41
copumpkinin .agda code, that is21/11 16:41
dolioRight.21/11 16:43
--- Day changed Mon Nov 22 2010
copumpkinyay22/11 01:33
copumpkinsymantics works now22/11 01:33
dolioWhat was it?22/11 01:38
copumpkinan eta contraction around records bug22/11 01:39
--- Day changed Tue Nov 23 2010
nappingI'd like to learn more about the metatheory of dependent type systems. I've started reading Luo's book. What else should I read?23/11 00:00
rjsimmonSo I've got an Agda development, medium-sized cut elimination argument, totally chokes the termination checker which is tragic but not unexpected. What's unusual is that, if there's an unresolved meta anywhere in the file it takes about 180x longer to load.23/11 20:51
rjsimmonHas anyone else encountered this?23/11 20:51
copumpkinI've noticed unresolved metas slowing things down in some contexts, yeah23/11 20:51
copumpkinnever really explored it much23/11 20:51
rjsimmonNo, it's their *absence*23/11 20:51
copumpkinhm?23/11 20:51
rjsimmonIt happens even if the unresolved meta is an irrelevant one like x : Set x = ? at the end of the file. If I have "x : Set x = ?" it takes 5 seconds to load the file.23/11 20:51
rjsimmonIf I remove those two lines it takes about 15 minutes.23/11 20:52
copumpkinoh that's weird23/11 20:52
rjsimmonthis is with the termination checker *already off*23/11 20:52
copumpkincan you reduce it to something else?23/11 20:52
copumpkinoh, I've never turned it off before23/11 20:52
copumpkinthere be the dragons23/11 20:52
copumpkinyou can't rephrase your algorithm in a form the termination checker likes?23/11 20:52
copumpkinor turn up the termination depth checking?23/11 20:52
rjsimmonWell, on this file the termination checker uses >3GB of memory and then GHC kills itself. I believe that it's a terminating function.23/11 20:53
copumpkin(you should still submit a bug for the weird meta behavior)23/11 20:53
rjsimmonBut it's a cut elimination argument, so it's 1) formula 2) 2 cut formulas over 7 mutually inductive lemmas. Like I said, that Agda can't infer this termination ordering automatically is not at all shocking.23/11 20:54
copumpkinsure, but most of the time things can be rephrased in such a way that does pass the checker23/11 20:55
copumpkinbut they become a hell of a lot less readable sometimes23/11 20:55
copumpkinanyway, not really the issue here23/11 20:55
rjsimmonWell, you're right that it's not the real issue (submitting bug report) but I'm curious about this comment. The argument *is* (I believe) structurally inductive.23/11 20:57
copumpkinif it is structural recursion but you just happen to peel off more than one layer at a time, you can just turn up the termination depth and it'll realize you're right23/11 20:57
copumpkinor rather, peel off more than one layer at a time, and then stick fewer layers back on before recursing23/11 20:58
rjsimmonEither the cut formula gets smaller or it stays the same size and one both of the two derivations gets smaller. And by one step, so I don't think what you're describing is the issue. It doesn't say "this doesn't terminate," it says "ACK I AM OUT OF MEMORY NOW"23/11 20:58
copumpkinI see :/23/11 20:59
copumpkinanother thing you might want to try23/11 20:59
copumpkinis to mark irrelevant things as such23/11 20:59
copumpkinto try to economize on memory23/11 20:59
rjsimmonHmm... unfortunately, everything is, I believe, computationally relevant in this case. What I think I actually need is the twelf-like ability to say "hey, I bet if you check *this* termination ordering it'll work." I stay comfortably within 500mb of memory until checking termination, at which point 3GB isn't enough.23/11 21:05
rjsimmonInlining some of the mutually recursive bits would probably help too.23/11 21:05
rjsimmonSmaller versions pass, with time.23/11 21:06
copumpkinaw :/23/11 21:07
copumpkinonly solution is to SSH into a box with craploads of RAM23/11 21:07
copumpkin:P23/11 21:07
rjsimmonand wait23/11 21:07
copumpkinI imagine it wouldn't be 15 minutes if you had enough RAM to stop it from swapping23/11 21:07
rjsimmonI'm fine with going on my own authority for this termination argument, honestly.23/11 21:07
rjsimmonNo, RAM swapping doesn't start until about minute 7.23/11 21:08
copumpkinoh wow :(23/11 21:08
rjsimmonMy officemates mock me with their "%total {A [D E]} (cut A D E F)." declarations :-)23/11 21:08
rjsimmon(that's Twelf for lexicographic termination on A, followed by simultaneous termination on D and E)23/11 21:09
copumpkininteresting23/11 21:10
rjsimmonalright: http://code.google.com/p/agda/issues/detail?id=36723/11 21:12
rjsimmonSo the ticket was closed as invalid, "The difference is that it doesn't write out the interface when there are unsolved metas."23/11 21:37
--- Day changed Wed Nov 24 2010
* sully wonders how hard it would be to extend agda with the ability to give hints to the termination checker24/11 01:26
Saizanseen sized types?24/11 01:27
sullyI should also point out that I basically don't know agda24/11 01:28
Saizanrjsimmon: i think using bove's technique to encode general recursion would also effectivelly allow to give that sort of hint to the termination checker http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.662624/11 01:41
Saizanor this http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.183124/11 01:41
rjsimmonAah, that's an interesting point - it would just be a single termination argument that Agda would need to synthesize instead of a lexicographic one. The theory here being that agda tries all the straightforward termination arguments before any of the composite ones.24/11 01:57
Saizanyeah, that's the conjecture :)24/11 01:58
Saizanthough maybe we've just shifted the problem to the function that builds the inhabitants of the relation?24/11 01:59
rjsimmonOh, that's fine24/11 02:00
rjsimmonBecause the problem is the seven mutually-inductive... oh yeah it would be almost as bad.24/11 02:00
rjsimmonI don't have a feel for how reliable sized types are in Agda.24/11 02:00
rjsimmonAnother conjecture would be that, by indexing derivations by a structural metric (I do this here http://requestforlogic.blogspot.com/2010/11/totally-nameless-representation.html) the "correct" things to induct over could be placed further to the left (since the structural metric isn't dependent on say, the context).24/11 02:01
rjsimmonThough honestly, I'm fine with cut being "on me" in these situations, and I'm more perturbed about the 12 minutes it takes to produce an interface file.24/11 02:02
Saizanheh, true24/11 02:02
rjsimmonThe old ticket about that issue has an outstanding request for a smaller example (http://code.google.com/p/agda/issues/detail?id=294&q=interface) but the problem is the time to produce .agdai seems to get exponentially worse with complexity (and, conversely, exponentially better with a simplified example)24/11 02:04
* Saizan has no idea how interface files are created24/11 02:08
rjsimmonblack magic, is my guess24/11 02:10
* copumpkin catches liyang 24/11 22:37
--- Day changed Thu Nov 25 2010
benk_Hi anyone around?25/11 05:09
benk_I'm running 2.2.8 with libs 0.4. I'm trying to load pouillard/potttier notsofresh implementation. They have an import "open import Function using (_∘_;_∶_)" which fails as it says Function.agda doesn't export _∶_. This operator is defined as syntax. Is there a simple workaround?25/11 05:14
copumpkinI want quotients25/11 06:00
cads__hola25/11 19:44
Saizanhi25/11 19:44
--- Day changed Sat Nov 27 2010
cadshey, anyone know good software for keeping files on people?27/11 17:41
cadssay you'd like to know all your important contacts and business partners, and have a place to put important info about them27/11 17:41
Saizanwrong channel?:)27/11 17:42
cadsoh yeah27/11 17:42
cadsit should be dependently typed!27/11 17:42
cadsheh,  whoops27/11 17:43
cadshow are you today saizan?27/11 17:43
Saizanfine, i guess27/11 17:44
cadsonly fine?27/11 17:49
Spockzcopumpkin: hi, did you have a look at Agda highlighting already? :-D *hopeful*27/11 17:56
--- Log closed Sat Nov 27 19:02:37 2010
--- Log opened Sat Nov 27 19:02:48 2010
-!- Irssi: #agda: Total of 32 nicks [0 ops, 0 halfops, 0 voices, 32 normal]27/11 19:02
-!- Irssi: Join to #agda was synced in 89 secs27/11 19:04
--- Day changed Mon Nov 29 2010
Saizanwhat's an elegant way to express in types that a function (nu F -> Bool) can only observe a finite number of layers of its argument?29/11 20:07
--- Log closed Tue Nov 30 01:58:43 2010
--- Log opened Tue Nov 30 01:58:50 2010
-!- Irssi: #agda: Total of 33 nicks [0 ops, 0 halfops, 0 voices, 33 normal]30/11 01:58
-!- Irssi: Join to #agda was synced in 78 secs30/11 02:00
freiksenetwhy are types for function uninferable in Agda like they are in haskell? is that a limitation of all dependently typed language?30/11 11:21
freiksenetat least Agda "tutorial" said that you need to always declare type for a function30/11 11:22
Saizansometimes you can get away with just providing _ as the type if there's enough context and you're not pattern matching or using with30/11 11:52
Saizanthe fundamental problem is that type inference is undecidable for dependent types30/11 11:53
freiksenetok30/11 11:55
Saizanwith extensions even the type system of GHC is undecidable, but since most haskell code doesn't use them ghc can still default to something similar to Hindley-Milner when there's no type signature30/11 11:55
Saizanthe downside of GHC's strategy is that it might report as a type error something that's just a failure of type inference30/11 11:56
freiksenetso you can't reliable tell type error and undecidable type from each other?30/11 11:56
freiksenetreliably*30/11 11:56
freiksenets/tell/differentiate30/11 11:57
Saizanright, though you can get pretty close if you're familiar with the limitations of ghc's type inference30/11 11:57
freiksenetisn't "undecidable type" just an infinite recursion at the end?30/11 11:57
Saizani meant undecidable type inference, above30/11 11:58
Saizanand "undecidable type" just some type that can't be inferred30/11 11:58
freiksenetyeah30/11 11:58
Saizanin fact "undecidable type" is not a good term at all30/11 11:58
freiksenetok, undecidable type inference30/11 11:58
Saizanand no, it's not just an infinite recursion, ghc's type inference results in false negatives30/11 11:58
Saizane.g. when you're using higher-rank polymorphism without a type signature30/11 11:59
freiksenetis inference for dependent types always undecidable?30/11 12:00
Saizanthat happens because it assumes things that aren't necessarily true about your code30/11 12:00
freiksenetlike I think Cayenne paper said something about it being decidable in many (some?) cases?30/11 12:01
freiksenetand it just terminated when inference went into infinite loop30/11 12:01
Saizanyou can do some type inference, and in fact Agda does, but it'll never add extra assumptions hoping your code falls into those inferrable cases, it'll just work with what's actually deducible from the code30/11 12:01
freiksenetI see.30/11 12:01
freiksenetcan one tell type erros from undecidable inference in this kind of model?30/11 12:02
Saizanyes30/11 12:02
freiksenetok, great30/11 12:03
freiksenethave you seen PiSigma paper?30/11 12:03
Saizanwhen type inference fails it'll just show you which parts of the types it couldn't deduce30/11 12:03
Saizannever read it30/11 12:03
freiksenetok. it presents minimal language with dependent types, which is supposed to be a base for languages like agda30/11 12:04
freiksenetone limitation that they have is that their types are not total30/11 12:04
Saizan(i think the cayenne paper is referring to type checking, since cayenne is not strong normalizing even that is undecidable for it)30/11 12:04
Saizan(while type checking for Agda is decidable)30/11 12:05
freiksenetI am quite confused about type totality, what does type totality means?30/11 12:05
freiksenetand what implications does not having type totality holds for a language?30/11 12:05
Saizani'm not familiar with that term30/11 12:05
Saizanthough "total function" means a function that's defined for every input30/11 12:06
Saizantype totality might mean that all your type expressions have a normal form? so you don't have any loops?30/11 12:06
freiksenetI am not sure. it mentions taht Cayenne is a "partial", so a non-total language30/11 12:07
freiksenetyeah, it seems that non-terminating types are not total30/11 12:08
Saizanthe usual consequences are that type checking becomes undecidable (since you need to do evaluation during typechecking and evaluation might loop forever), and that you can't trust proofs without first normalizing them30/11 12:10
freiksenetI see.30/11 12:11
freiksenetthanks for the help )30/11 12:12
Saizannp :)30/11 12:14
freiksenetSaizan: what would you advice as a reference for type checking rules for dependent types?30/11 14:12
freiksenet(reference implementation)30/11 14:17
Saizanfreiksene: http://lambda-the-ultimate.org/node/234030/11 14:43

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