pedagand pedagand +Saizan --- Log opened Sun Aug 01 00:00:38 2010 Saizan, by any chance, do you know how Cabal sets the -hide-package option (in case of ambiguity)? 01/08 00:11 for example, I have mtl and monads-fd, I want to compile Epigram with mtl 01/08 00:12 Cabal uses -hide-all-packages (or a similar name) and then gives -package $pkg for each$pkg in the build-depends 01/08 00:12 ha! 01/08 00:12 thanks! 01/08 00:12 np :) 01/08 00:13 hehe, that's working. Thanks again, you saved my night ;-) 01/08 00:30 there is something I haven't figured out yet, tho. Why do 'runhaskell Setup.hs build' works fine while 'cabal build' tries to compile Epigram's "Main.lhs" 01/08 00:37 I would have expected 'cabal build' to call 'Setup.hs build', somehow 01/08 00:37 well, let's RTFM once more 01/08 00:38 do you have a custom Setup.hs? 01/08 00:39 in that case you need build-type: Custom in the .cabal file 01/08 00:39 otherwise it uses the default code 01/08 00:39 it's kind of custom, indeed. Let's try Custom (didn't saw that magic in the doc, tho) 01/08 00:41 and that works! 01/08 00:41 very glad to have you here :-) 01/08 00:42 ha, and it's in the doc actually. My bad. 01/08 00:42 it's a common gotcha, maybe the docs need some improvement.. 01/08 00:43 dunno, I'm an absolute beginner in ca(ni)balism, so I won't blame the docs tonight. Maybe tomorrow ;-) 01/08 00:46 ok, so 'cabal build' works. I'm scared of trying anything more interesting, such as 'cabal install' for instance... 01/08 00:46 it doesn't bite :) 01/08 00:47 Tada! "Installing executable(s) in /home/pierre/.cabal/bin" 01/08 00:53 typing "$Pig" just works, and I still have my two arms, two legs, one head 01/08 00:53 goodo 01/08 00:53 nice :) 01/08 00:54 that's rudimentary but that's a cabal package :-) 01/08 00:54 you say "nice" now, but when you see the connection cabal/Makefile, you'll cry :-) 01/08 00:54 ugh 01/08 00:54 it might convince me to go back to work on build systems.. 01/08 00:55 well, I would not have this cruelty 01/08 00:59 nonetheless, that's an interesting (and far reaching) problem indeed 01/08 01:00 it's easy to find distractions anyway :) 01/08 01:15 -!- mode/#epigram [+v dolio] by ChanServ 01/08 04:06 -!- mode/#epigram [+v dolio] by ChanServ 01/08 06:32 -!- mode/#epigram [+v pigworker] by ChanServ 01/08 10:10 -!- mode/#epigram [+v soupdragon] by ChanServ 01/08 10:37 -!- mode/#epigram [+v dolio] by ChanServ 01/08 11:02 -!- mode/#epigram [+v dolio] by ChanServ 01/08 13:02 -!- mode/#epigram [+v pigworker] by ChanServ 01/08 13:24 -!- mode/#epigram [+v dolio] by ChanServ 01/08 16:02 -!- mode/#epigram [+v pigworker] by ChanServ 01/08 17:45 -!- mode/#epigram [+v dolio] by ChanServ 01/08 20:06 -!- mode/#epigram [+v dolio] by ChanServ 01/08 21:05 -!- mode/#epigram [+v soupdragon] by ChanServ 01/08 21:50 -!- mode/#epigram [+v dolio] by ChanServ 01/08 22:06 -!- mode/#epigram [+v dolio] by ChanServ 01/08 23:05 -!- mode/#epigram [+v pigworker] by ChanServ 01/08 23:40 --- Day changed Mon Aug 02 2010 -!- mode/#epigram [+v codolio] by ChanServ 02/08 00:05 -!- mode/#epigram [+v pigworker] by ChanServ 02/08 00:29 -!- mode/#epigram [+v pigworker] by ChanServ 02/08 00:34 -!- mode/#epigram [+v dolio] by ChanServ 02/08 01:05 -!- mode/#epigram [+v pigworker] by ChanServ 02/08 01:47 -!- mode/#epigram [+v dolio] by ChanServ 02/08 02:06 -!- mode/#epigram [+v pigworker] by ChanServ 02/08 02:08 -!- mode/#epigram [+v dolio] by ChanServ 02/08 04:02 -!- mode/#epigram [+v dolio] by ChanServ 02/08 06:05 -!- mode/#epigram [+v pigworker] by ChanServ 02/08 08:51 -!- mode/#epigram [+v dolio] by ChanServ 02/08 09:05 -!- mode/#epigram [+v Saizan_] by ChanServ 02/08 12:40 -!- Saizan_ is now known as Saizan 02/08 12:40 -!- mode/#epigram [+v edwinb] by ChanServ 02/08 12:42 -!- mode/#epigram [+v dolio] by ChanServ 02/08 18:05 -!- mode/#epigram [+v dolio] by ChanServ 02/08 20:02 -!- mode/#epigram [+v soupdragon] by ChanServ 02/08 20:47 -!- mode/#epigram [+v codolio] by ChanServ 02/08 21:05 -!- codolio is now known as dolio 02/08 21:08 -!- mode/#epigram [+v pigworker] by ChanServ 02/08 21:48 -!- copumpkin is now known as unsafePumpkin 02/08 22:16 -!- unsafePumpkin is now known as copumpkin 02/08 22:31 --- Day changed Tue Aug 03 2010 -!- mode/#epigram [+v dolio] by ChanServ 03/08 01:33 -!- mode/#epigram [+v dolio] by ChanServ 03/08 02:05 -!- mode/#epigram [+v codolio] by ChanServ 03/08 04:54 -!- mode/#epigram [+v pigworker] by ChanServ 03/08 09:43 -!- mode/#epigram [+v soupdragon] by ChanServ 03/08 10:35 -!- codolio is now known as dolio 03/08 11:28 -!- mode/#epigram [+v dolio] by ChanServ 03/08 12:05 -!- mode/#epigram [+v dolio] by ChanServ 03/08 13:01 -!- mode/#epigram [+v dolio] by ChanServ 03/08 20:01 --- Day changed Wed Aug 04 2010 -!- mode/#epigram [+v dolio] by ChanServ 04/08 03:05 -!- mode/#epigram [+v dolio] by ChanServ 04/08 08:05 -!- mode/#epigram [+v soupdragon] by ChanServ 04/08 10:40 -!- mode/#epigram [+v dolio] by ChanServ 04/08 12:01 -!- mode/#epigram [+v soupdragon] by ChanServ 04/08 13:37 -!- mode/#epigram [+v dolio] by ChanServ 04/08 17:05 -!- mode/#epigram [+v dolio] by ChanServ 04/08 18:01 -!- mode/#epigram [+v Saizan] by ChanServ 04/08 18:38 -!- koninkje_away is now known as koninkje 04/08 22:39 -!- mode/#epigram [+v dolio] by ChanServ 04/08 23:04 --- Day changed Thu Aug 05 2010 For some reason, compilation of Epigram 2 fails for me. 05/08 00:09 http://pastie.org/1076195 is the result of "make dep" in Pig09/src/ 05/08 00:10 ah, yeah, the cabalization patch added -hide-all-packages directly in the Makefile, but that doesn't work if you don't also pass the -package ... like Setup.hs will 05/08 00:11 So what do I do to fix it? 05/08 00:12 you can 'cabal build' instead of 'make'ing, I think 05/08 00:13 yeah, cabal configure first, or use "runhaskell Setup.hs" instead of cabal if you don't have the latter installed 05/08 00:15 -!- mode/#epigram [+v dolio] by ChanServ 05/08 03:04 -!- mode/#epigram [+v dolio] by ChanServ 05/08 04:01 -!- koninkje is now known as koninkje_away 05/08 04:28 -!- mode/#epigram [+v dolio] by ChanServ 05/08 08:01 pedagand: morning 05/08 09:33 what's going on with the cabal/make switchover? 05/08 09:34 nothing is going on here :-) should there be anything going on? 05/08 09:37 your latest patch seems to break make because some packages are omitted, is that intenational? 05/08 09:38 kind of, yes. One should use "cabal ..." or "runhaskell Setup.hs ..." now 05/08 09:38 okay, but being a cabal novice, how can I can run the equivalent of "make dep" or "make profile"? 05/08 09:40 we should probably also update the documentation 05/08 09:40 if you want to fix the makefile, tho, it's easy as well: on the HC_PACKAGE thing, you add "-package foo" for all packages there used to be 05/08 09:40 my plan was just not to pull your patch ;-) but I'd like to stay close to the main tree if possible 05/08 09:41 as you wish 05/08 09:41 in other news, you've probably seen that I finally pushed my equation-smashing hammer in problem simplification 05/08 09:44 this gets rid of all the "<= ship" nonsense, but seems to be rather slow 05/08 09:45 will see that when I'm back. As for now, farniente! :-) 05/08 09:53 fair enough 05/08 09:54 all right, I've fixed the makefile, pushing in a few 05/08 10:12 thank you, sorry to interrupt the doing nothing! 05/08 10:13 pushed my Lord 05/08 10:19 ta 05/08 10:20 -!- mode/#epigram [+v Saizan] by ChanServ 05/08 10:48 -!- mode/#epigram [+v soupdragon] by ChanServ 05/08 11:53 -!- copumpkin_ is now known as copumpkin 05/08 13:17 -!- mode/#epigram [+v soupdragon] by ChanServ 05/08 14:05 -!- mode/#epigram [+v dolio] by ChanServ 05/08 18:05 -!- mode/#epigram [+v dolio] by ChanServ 05/08 19:03 -!- mode/#epigram [+v codolio] by ChanServ 05/08 20:04 -!- mode/#epigram [+v Saizan] by ChanServ 05/08 20:40 -!- copumpkin is now known as Nu 05/08 21:47 -!- Nu is now known as copumpkin 05/08 21:47 -!- codolio is now known as dolio 05/08 22:44 -!- koninkje_away is now known as koninkje 05/08 23:14 --- Day changed Fri Aug 06 2010 -!- koninkje is now known as koninkje_away 06/08 02:50 -!- mode/#epigram [+v dolio] by ChanServ 06/08 03:04 -!- mode/#epigram [+v dolio] by ChanServ 06/08 11:04 -!- mode/#epigram [+v soupdragon] by ChanServ 06/08 13:07 -!- mode/#epigram [+v dolio] by ChanServ 06/08 14:04 -!- mode/#epigram [+v dolio] by ChanServ 06/08 15:04 -!- copumpkin_ is now known as copumpkin 06/08 15:56 -!- mode/#epigram [+v dolio] by ChanServ 06/08 20:00 -!- mode/#epigram [+v dolio] by ChanServ 06/08 21:03 -!- mode/#epigram [+v dolio] by ChanServ 06/08 22:04 -!- mode/#epigram [+v dolio] by ChanServ 06/08 23:03 --- Day changed Sat Aug 07 2010 -!- mode/#epigram [+v dolio] by ChanServ 07/08 05:53 -!- mode/#epigram [+v dolio] by ChanServ 07/08 06:07 -!- mode/#epigram [+v dolio] by ChanServ 07/08 06:21 -!- mode/#epigram [+v codolio] by ChanServ 07/08 10:16 -!- mode/#epigram [+v dolio] by ChanServ 07/08 11:18 -!- mode/#epigram [+v soupdragon] by ChanServ 07/08 12:49 -!- mode/#epigram [+v dolio] by ChanServ 07/08 13:21 -!- copumpkin_ is now known as copumpkin 07/08 16:46 -!- mode/#epigram [+v dolio] by ChanServ 07/08 21:21 -!- mode/#epigram [+v dolio] by ChanServ 07/08 22:21 -!- mode/#epigram [+v dolio] by ChanServ 07/08 23:17 --- Day changed Sun Aug 08 2010 -!- mode/#epigram [+v dolio] by ChanServ 08/08 02:17 -!- mode/#epigram [+v dolio] by ChanServ 08/08 02:47 -!- mode/#epigram [+v codolio] by ChanServ 08/08 06:21 -!- codolio is now known as dolio 08/08 07:22 -!- mode/#epigram [+v soupdragon] by ChanServ 08/08 13:51 -!- mode/#epigram [+v pigworker] by ChanServ 08/08 19:57 -!- mode/#epigram [+v pigworker] by ChanServ 08/08 20:27 -!- mode/#epigram [+v pigworker] by ChanServ 08/08 23:44 --- Day changed Mon Aug 09 2010 -!- mode/#epigram [+v dolio] by ChanServ 09/08 04:20 -!- mode/#epigram [+v soupdragon] by ChanServ 09/08 04:41 -!- mode/#epigram [+v dolio] by ChanServ 09/08 05:17 -!- mode/#epigram [+v dolio] by ChanServ 09/08 07:17 -!- mode/#epigram [+v pigworker] by ChanServ 09/08 09:17 agundry: You about? 09/08 13:54 moleris: sorry, in the middle of a couple of talks; should be finished in just over an hour 09/08 14:39 agundry: no worries 09/08 14:39 moleris: I'm back 09/08 16:12 agundry: Hey 09/08 16:12 what can I do you for? 09/08 16:12 Just wondering what I should be able to do with your new equality stuff 09/08 16:13 or how to make it go 09/08 16:13 hopefully, it should just be a case of not having to do things that were necessary before 09/08 16:14 if you look at Demo.pig, lots of explicit eliminations by ship have disappeared 09/08 16:14 there is a new primitive substEq : (X : Set)(x : X)(y : X)(q : :- x == y)(P : X -> Set) -> P x -> P y 09/08 16:15 and when propositional simplification spots an equation with a variable on one side, it eliminates the variable by substEq 09/08 16:16 Hmm 09/08 16:16 This is what I thought - but earlier I had an equality in the context that was not substituted away 09/08 16:18 the examples in Demo.pig work though 09/08 16:18 :s/propositional simplification/problem simplification 09/08 16:18 it's possible that it is missing some equations 09/08 16:18 I'm interested in examples that you think should disappear and do not 09/08 16:19 OK, I'll try and recreate 09/08 16:19 In the meanwhile I've stopped the compiler segfaulting 09/08 16:20 good 09/08 16:20 now we need to stick it in the test suite so we notice if it breaks 09/08 16:20 There's a problem with the operator references not being compiled properly though 09/08 16:20 hmm, amusingly enough I think the problem simplification only works with equations one way round (variables on the right) 09/08 16:21 that needs fixing 09/08 16:21 what's wrong with operator references? 09/08 16:21 Which way round do they have to be? 09/08 16:24 oh, var on the right 09/08 16:24 sorry 09/08 16:24 that would be the situation I find myself in 09/08 16:24 aha 09/08 16:24 sorry, I only did one case and planned to add the other once it was working 09/08 16:25 but then forgot 09/08 16:25 righto, I shan't worry too much then 09/08 16:25 give me a few minutes to copy-paste and I can make an ugly version that works 09/08 16:25 but this code really needs tidying up 09/08 16:26 a bit like the rest of the code, too, then 09/08 16:26 PropSimp.lhs is particularly horrible 09/08 16:27 we need to figure out how to do everything without higher-order terms, and rewrite it to be nice 09/08 16:27 ah yes 09/08 16:28 any idea on that? 09/08 16:28 I've not really looked at it, to be honest 09/08 16:28 fair enough 09/08 16:28 one possibility might be to add term representations of some things that are currently only stored as values 09/08 16:29 if I'm right in thinking that terms are now allowed in value lambdas 09/08 16:29 they are 09/08 16:31 the whole term/value distinction has been muddied 09/08 16:31 indeed 09/08 16:32 I think that it might be possible to produce the proof fragments required by propsimp as terms instead of values 09/08 16:33 though we might just end up with horrible de Bruijn index mangling in place of the higher-order scopes 09/08 16:33 hmm 09/08 16:34 ah, the equation simplification fix is a bit more than I thought, because it requires symmetry to be a primitive 09/08 16:44 on a related note, I really want something that will give me Haskell code for an Epigram term that I've built 09/08 16:45 should be reasonably straigh forward now we have FO-terms again 09/08 16:47 (ish) 09/08 16:47 yes 09/08 16:49 what is sym currently? 09/08 16:51 it's not built in, but various files define it manually 09/08 16:52 sym : :- ((X : Set)(x : X)(y : X) => x == y => y == x) 09/08 16:53 sym = \ X x y q -> refl (X -> Set) (\ y -> :- y == x) % x y q ! _ 09/08 16:53 fair enough 09/08 16:54 I thought at one point it was an eliminator 09/08 16:54 probably a long time ago 09/08 16:54 it may well have been once 09/08 16:54 right, I'm off 09/08 16:56 more Epigramming tomorrow 09/08 16:56 okay, bye for now 09/08 16:56 cheers 09/08 16:56 -!- larrytheliquid_ is now known as larrytheliquid 09/08 19:25 -!- mode/#epigram [+v soupdragon] by ChanServ 09/08 19:37 -!- mode/#epigram [+v dolio] by ChanServ 09/08 20:20 -!- danten_ is now known as danten 09/08 20:51 -!- mode/#epigram [+v dolio] by ChanServ 09/08 21:20 -!- pumpkin is now known as copumpkin 09/08 23:01 -!- shapr[ is now known as shapr 09/08 23:10 -!- mode/#epigram [+v dolio] by ChanServ 09/08 23:20 --- Day changed Tue Aug 10 2010 -!- mode/#epigram [+v dolio] by ChanServ 10/08 00:20 -!- mode/#epigram [+v dolio] by ChanServ 10/08 07:20 agundry: Sadly, my example still only works if I turn my equations around ): 10/08 12:57 hmm, that's strange 10/08 12:57 oh, wait 10/08 12:57 ignore that 10/08 12:57 is it working after all? 10/08 12:58 forgot to copy the replacement Pig into the right place 10/08 12:59 sorry :$ 10/08 12:59 no problem, glad to hear it is working 10/08 12:59 does your example do anything exciting? 10/08 12:59 no, just mucking about with the usual vector stuff 10/08 13:00 trying to get a data tactic for indexed families working too 10/08 13:02 that would be very nice 10/08 13:02 I've been thinking about how to avoid switching on enumerations during problem simplification 10/08 13:03 we need to generate induction principles with better methods (a tuple instead of a function from an enumeration) 10/08 13:04 I have done the construction in Epigram for Desc, but am not sure how to wire it up with the data tactic 10/08 13:05 I have plenty of stuff along those lines for the IDesc variant 10/08 13:11 I'm loathed to mess about too much with Desc, though 10/08 13:12 that's fair enough 10/08 13:12 mostly I have been playing with Desc because I don't really understand IDesc 10/08 13:12 (: 10/08 13:12 I have a file somewhere with a case' gadget for well-formed IDescs which you have to supply a tuple of methods 10/08 13:13 that'll be what you want 10/08 13:14 yes, that's the sort of thing we need 10/08 13:15 interestingly, I don't think that the system is clever enough to spot that a tuple of programming problems is a programming problem 10/08 13:15 it's not 10/08 13:16 (clever enough) 10/08 13:17 what kind of examples are you thinking of? 10/08 13:18 It showed up while I was playing around with building the case' and rec' gadgets generically 10/08 13:20 -!- mode/#epigram [+v soupdragon] by ChanServ 10/08 16:26 Question: is '->' not a keyword? 10/08 16:39 Ah, found it... So supplementary question: Why on Earth is it only introduced by the Prop feature? 10/08 16:44 -!- danten_ is now known as danten 10/08 17:20 because the parser is bloated anyway, so nobody wants to touch it. You could move '->' in a better place, but the parser would still be massively bloated... 10/08 17:59 -!- mode/#epigram [+v dolio] by ChanServ 10/08 18:16 -!- mode/#epigram [+v dolio] by ChanServ 10/08 21:20 -!- mode/#epigram [+v dolio] by ChanServ 10/08 22:19 -!- mode/#epigram [+v dolio] by ChanServ 10/08 23:16 --- Day changed Wed Aug 11 2010 -!- mode/#epigram [+v dolio] by ChanServ 11/08 00:16 -!- mode/#epigram [+v dolio] by ChanServ 11/08 01:20 -!- mode/#epigram [+v dolio] by ChanServ 11/08 02:16 -!- koninkje_away is now known as koninkje 11/08 03:06 -!- mode/#epigram [+v dolio] by ChanServ 11/08 03:19 -!- mode/#epigram [+v dolio] by ChanServ 11/08 07:19 -!- koninkje is now known as koninkje_away 11/08 09:13 agundry, will you be in the office this afternoon? 11/08 12:06 -!- mode/#epigram [+v dolio] by ChanServ 11/08 12:19 -!- danten_ is now known as danten 11/08 12:40 pedagand: yes, from now on 11/08 12:44 all right. I've written some thought, I send that, eat and come at, say, 2pm. 11/08 12:45 okay, see you later on then 11/08 12:46 pedagand, agundry: Plotting anything interesting? 11/08 15:04 moleris: just thinking about how Epigram is going to take over the world, as usual 11/08 15:06 we have been talking about how a high-level language might fit in 11/08 15:07 but not in much detail as yet 11/08 15:07 -!- mode/#epigram [+v dolio] by ChanServ 11/08 15:19 yeah, I was trying to make the point that we need to stabilise the code (that is, get clear, documented APIs with quickcheck ideally) so that we can smoothly move to higher levels 11/08 15:24 pedagand: That would be ideal 11/08 15:29 -!- mode/#epigram [+v soupdragon] by ChanServ 11/08 16:20 moleris, ping? 11/08 18:11 -!- mode/#epigram [+v dolio] by ChanServ 11/08 18:19 ping time-out, nevermind 11/08 18:56 -!- mode/#epigram [+v dolio] by ChanServ 11/08 20:16 -!- mode/#epigram [+v dolio] by ChanServ 11/08 21:19 -!- mode/#epigram [+v dolio] by ChanServ 11/08 22:16 --- Day changed Thu Aug 12 2010 -!- mode/#epigram [+v dolio] by ChanServ 12/08 01:19 -!- mode/#epigram [+v dolio] by ChanServ 12/08 02:19 -!- mode/#epigram [+v dolio] by ChanServ 12/08 08:16 moleris, in your definition of SPTs (in your thesis for instance, p.41), you define the interpretation function as a data-type, whereas we have been defining it purely as a function 12/08 11:22 what are the pro and cons? 12/08 11:23 in your thesis, top of p.39, you hint that "it is preferable to define the family inductively so that the syntax of types and values is always available" 12/08 11:23 I don't think I really understand what you meant 12/08 11:23 surely, if you interpret codes to types (with a pure function), you also get the syntax of values, excepted that you're using the one of the host language 12/08 11:25 not that I dislike this "inductive relation" presentation, but I'm curious to know the benefits/drawbacks 12/08 11:27 Hmm, I'm not sure what I meant by that. I think that way about a lot of my thesis though :)# 12/08 11:32 :-D 12/08 11:33 but is there a reason you gave this presentation back in the days and then we switched to the functional presentation? 12/08 11:34 for what I see, the interpretation function goes to Set while the inductive relation builds into Set1. But I need to go further to see if it's a show stopper 12/08 11:35 is that true? 12/08 11:38 (necessarily) 12/08 11:38 sorry, I'll answer your question properly in a moment - I'm just debugging some new Epigram at the same time 12/08 11:39 sure, no problem 12/08 11:39 that's true in Agda, because the SPT n is Set1 (function space) and the inductive relation takes an SPT *not* as a parameter: "data ⟦_⟧_ {n : ℕ} : SPT n -> ... -> Set1 where " 12/08 11:45 in Coq, I would abuse Prop to get my hand on the pieces without having a size explosion 12/08 11:46 And SPT is in Set1 because of the ->' constructor.. Hm 12/08 11:48 yep 12/08 11:49 Not much you can do about it in agda, but I'd argue that the inductive interpretation should be small. I'd never really thought about it that way, though. 12/08 11:50 In answer to your original question though, it was definitely on my mind that the naive recursive definition is not structurally recursive. 12/08 11:51 For some reason I'm much more paranoid about bad recursive definitions than size issues. 12/08 11:52 ha! when you're dealing with the fix-point, right? 12/08 11:52 And I wanted to keep the presentation of the universe as simple as possible 12/08 11:52 Yeah, thats the one 12/08 11:53 I forgot that guy, thanks. 12/08 11:53 Not sure why I came up with some other weak excuse thoguh 12/08 11:54 I was young 12/08 11:54 :-) 12/08 11:54 caribou 12/08 12:57 oops. wrong window 12/08 12:58 * moleris has good news 12/08 13:29 my latest patch allows one to write such things as: 12/08 13:30 idata Vec (A : Set) : Nat -> Set := (nil : Vec A 'zero) ; (cons : (n : Nat) -> A -> Vec A n -> Vec A ('succ n)) 12/08 13:30 and have Epigram actually do something useful with it 12/08 13:31 very nice 12/08 13:31 Only for indexed families with a single index so far 12/08 13:32 (labels really need fixing before I attend to that shortcoming) 12/08 13:32 but alpha testers are welcome to have a play 12/08 13:33 goodo 12/08 13:33 what problem are you having with labels? 12/08 13:34 moleris, are you aware (maybe you're at the origin of it) of the "universe of indexed labels"? 12/08 13:35 I wasn't at pigweek, so I don't really know what was decided on that front 12/08 13:35 I had a conversation with pigworker on the subject of labels which went no where at the time 12/08 13:36 if there's a plan I'd be happy to hear about it 12/08 13:37 I'm not aware of such a plan 12/08 13:39 well, I wasn't there, so I cannot tell. The day after, in 5 minutes, pigworker thrown us a universe of labels that he said would solve your misery. I might have a whiteboard picture of it, if so I'll transcribe it and forward to the list. 12/08 13:39 agundry, I reckon you were here. But maybe you were working on something else 12/08 13:39 or possibly I've just forgotten... 12/08 13:39 We talked about making a universe for programming problems 12/08 13:40 we also did that, but that was another day :-) 12/08 13:40 so many universes, it's hard to keep them all in ones brain 12/08 13:41 anyway, it's not a turnkey solution, so I wouldn't be too hopeful now 12/08 13:41 that's why we need IIR with support for binding! Yeah! 12/08 13:41 So what is the problem with the current labels setup as far as idata is concerned? 12/08 13:42 incidentally, I've got PropSimp to work with terms rather than values, though I still need to tidy up the code a bit 12/08 13:44 So with plain ol' Mu, the label |Nat| stands for the whole of the canonical object |Mu NatD| 12/08 13:45 but thats not the case with IMu, where the canonical values (for biderectional type checking purposes) include a particular index 12/08 13:45 you want the label to be |Vec|, but that doesn't stand for |IMu Nat VecD n| 12/08 13:47 this causes me all sorts of problems 12/08 13:47 not sure if that makes any sense 12/08 13:47 but good news on the prop simp stuff :) 12/08 13:48 * moleris wonders how close we are to getting rid of higer order values for good 12/08 13:48 I think we can pretty much get rid of them now if we want 12/08 13:49 Telescopes are still a blocker, but not a huge one 12/08 13:49 ah true 12/08 13:49 -!- mode/#epigram [+v soupdragon] by ChanServ 12/08 13:50 a quick grep suggests everything else should be fairly easy to convert to first-order 12/08 13:50 I might put that to the top of my in tray 12/08 13:50 I'm going to update Demo.pig to use idata, unless anyone is on that already? 12/08 13:52 go for it 12/08 13:55 pedagand: ping 12/08 15:32 pong 12/08 15:32 just had a chat with Kirsty 12/08 15:32 it seems she never received your email about flights to Baltimore 12/08 15:32 haha 12/08 15:33 not sure what happened there 12/08 15:33 I'm going to forward it and hope it gets through this time... 12/08 15:33 thanks for that 12/08 15:34 hmm 12/08 15:40 I need me some of those 12/08 15:40 if I were going to Baltimore to give an Epigram demo, I would very carefully remember to forget to book a flight... :-) 12/08 15:50 moleris, I've transcribed pigworker's PhD code into Agda. I've written down the labels for Nat, Vec, and Fin. Do you have any other interesting example to test the thing? 12/08 16:03 I will send it out on the mailing list when I'm confident enough that my translation is not complete bullshit 12/08 16:03 they're the main 3 aren't they 12/08 16:04 they are just indexed by Nat, that's too easy :-) 12/08 16:04 I'm not sure I like your negativity about my demo 12/08 16:05 I need your help here (: 12/08 16:06 talking of travel though - are you guys going to come down to AIM in Nottingham? 12/08 16:06 we haven't thought about it, at least I haven't 12/08 16:08 it's in early September, isn't it? 12/08 16:08 1st to 7th, yes 12/08 16:09 1st to the 7th 12/08 16:09 I didn't plan to go, personally 12/08 16:10 Shame, will be fun hopefully 12/08 16:11 but maybe pigworker will give orders when he is back 12/08 16:11 pedagand: what about: 12/08 16:15 data Id (A : Set) (a : A) : A -> Set := (refl : Id A a a) 12/08 16:15 that's awful. Perfect, thanks. 12/08 16:16 -!- mode/#epigram [+v dolio] by ChanServ 12/08 16:20 moleris, I've sent the agda definition on -dev 12/08 16:53 -!- mode/#epigram [+v soupdragon] by ChanServ 12/08 20:39 -!- mode/#epigram [+v dolio] by ChanServ 12/08 22:41 -!- mode/#epigram [+v dolio] by ChanServ 12/08 22:41 --- Day changed Fri Aug 13 2010 -!- koninkje_away is now known as koninkje 13/08 01:48 -!- mode/#epigram [+v dolio] by ChanServ 13/08 03:28 -!- mode/#epigram [+v dolio] by ChanServ 13/08 05:15 -!- mode/#epigram [+v soupdragon] by ChanServ 13/08 06:01 -!- mode/#epigram [+v dolio] by ChanServ 13/08 06:17 -!- koninkje is now known as koninkje_away 13/08 06:56 -!- mode/#epigram [+v Saizan] by ChanServ 13/08 10:18 -!- moleris_ is now known as moleris 13/08 10:58 pedagand: Your email client mangled the unicode in ILabel.agda ))): (Sent in the right channel now) 13/08 11:10 damned email client 13/08 11:20 stuck in the dark ages 13/08 11:21 it's a fairly standard thunderbird, I'm disappointed. utf8 was supposed to solve all encoding problems, yet we have found a way to implement it in so many incompatible ways.. 13/08 11:23 anyway, what if I push the agda code in the repos, in ./models? is that ok? 13/08 11:23 (I suggest that before we attack the global warming problem, we first solve the utf8 problem. If we cannot agree a character set, there is no hope to solve any larger-scale problem) 13/08 11:25 (I will get in touch with Al Gore, maybe we could make a convincing movie) 13/08 11:25 actually, if I download the attached file, it's all right on my machine. Now, let me blame your email client, your OS, etc. :-) I push it in the repos... 13/08 11:29 done 13/08 11:31 Hmm, I triple checked the attachment before I accused you - I think Thunderbird is lying to you 13/08 11:35 I stop using thunderbird for pretty much this exact reason, btw (: 13/08 11:35 s/stop/stopped 13/08 11:36 But thanks for putting it in the repo 13/08 11:36 what are you using now? 13/08 11:37 mutt 13/08 11:38 -!- mode/#epigram [+v dolio] by ChanServ 13/08 13:15 pedagand: It's a good start - but there's something I'm not getting 13/08 13:23 I need more think 13/08 13:23 in otherwords, don't worry about implementing it 13/08 13:23 did you received the picture too? does that help? 13/08 13:25 I got it 13/08 13:27 Your Agda rendering seems reasonable though 13/08 13:27 I think I'm worrying about scoping these labels 13/08 13:27 but my brain freezes everytime I try and think about it 13/08 13:28 (scoping, that is) 13/08 13:28 what do you mean by "scoping the labels"? 13/08 13:28 Well exactly (: 13/08 13:29 ha, I see :-) 13/08 13:29 No really, if they are just UIds they don't fit with the module/parameter structure very well 13/08 13:30 so maybe they aren't UIds 13/08 13:35 I see. Just stick a Name instead of an UId then? 13/08 13:37 so that you can use the NameResolution machinery to disambiguate it for you 13/08 13:37 maybe 13/08 13:38 and have the type as a top level thing too 13/08 13:39 dunno 13/08 13:39 I think I might be missing the point 13/08 13:42 (I'm going to the lab, see you later) 13/08 13:43 (labels are for speeding up equality tests?) 13/08 14:04 moleris,  for Desc labels, we don't go through the hoops of defining the label wrt. to scopes or anything like that. Why would we have to do that in IDesc? 13/08 14:09 Saizan: they are mainly for tracking human-readable names of data types built with Mu/IMu 13/08 14:10 speeding up equality checking is a useful extra 13/08 14:10 agundry: oh, right, humans :) 13/08 14:17 I don't think we have really figured out how the high-level language namespace should be managed 13/08 14:20 this goes for both programming problems and data type labels 13/08 14:22 at the moment we have hacked things up on top of the ProofState namespace 13/08 14:23 but maybe we should think about something more principled 13/08 14:23 pedagand: Labels (currently) are FAKE references, with long names and global types 13/08 14:23 ha! that's true, my bad. 13/08 14:25 -!- mode/#epigram [+v soupdragon] by ChanServ 13/08 16:41 -!- mode/#epigram [+v dolio] by ChanServ 13/08 17:18 -!- pumpkin is now known as copumpkin 13/08 17:54 -!- mode/#epigram [+v dolio] by ChanServ 13/08 21:17 --- Day changed Sat Aug 14 2010 -!- mode/#epigram [+v dolio] by ChanServ 14/08 01:18 -!- mode/#epigram [+v dolio] by ChanServ 14/08 02:18 -!- mode/#epigram [+v dolio] by ChanServ 14/08 04:15 -!- mode/#epigram [+v dolio] by ChanServ 14/08 06:18 -!- mode/#epigram [+v dolio] by ChanServ 14/08 08:15 -!- mode/#epigram [+v codolio] by ChanServ 14/08 09:18 -!- mode/#epigram [+v dolio] by ChanServ 14/08 10:18 -!- mode/#epigram [+v soupdragon] by ChanServ 14/08 10:28 -!- mode/#epigram [+v edwinb] by ChanServ 14/08 14:42 -!- mode/#epigram [+v dolio] by ChanServ 14/08 18:18 -!- mode/#epigram [+v soupdragon] by ChanServ 14/08 19:35 -!- mode/#epigram [+v dolio] by ChanServ 14/08 22:14 * Taral waves. 14/08 23:02 Anyone home? 14/08 23:02 * Saizan waves back 14/08 23:02 I think I'm going slowly stir-crazy. 14/08 23:02 * copumpkin grunts 14/08 23:02 Too much new stuff. :P 14/08 23:02 OTT, and this new descriptions thing... 14/08 23:03 they seem fun at least :) 14/08 23:03 Do you need to hard code observational equality for type-checking? I can't work it out from the code... 14/08 23:03 I'm trying to produce a "dependent core", essentially purely a type checker. 14/08 23:04 Ideally, it's a core small enough for a human to verify. 14/08 23:04 W-types were disappointing, but descriptions look promising. 14/08 23:04 de bruijn would be proud 14/08 23:05 Heh. 14/08 23:05 i've an agda model with descriptions and OTT, which defines equality for all the description-generated datatypes 14/08 23:05 Hm, I guess you have to have that, at least. 14/08 23:05 But == can be generic over descriptions. 14/08 23:05 http://code.haskell.org/~Saizan/bisim/ObsEq.agda <- IDescTT is taken from the Pig09 repo 14/08 23:06 Could you encode generic == as a description itself? 14/08 23:06 i think so 14/08 23:07 Is it useful? Since my type checker has to appeal to equality to start with... 14/08 23:09 Or does it? 14/08 23:09 Arg... I wish I understood this stuff better. :( 14/08 23:09 I will say the Epitome has been useful. 14/08 23:09 though i use a different IDesc there, which gives me the codes for the domains of sigma and pi 14/08 23:09 but i guess from within the language it's fine to just use the primitive == for those. 14/08 23:10 ObsEq is a deeper embedding than IDescTT 14/08 23:11 Taral: seen the blog, btw? 14/08 23:11 I read the blog. 14/08 23:12 There's a lot there... 14/08 23:12 What does "deeper embedding" mean? 14/08 23:14 well, i mean that i've represented more things using a "code" like Pi and Sigma rather than simply using Agda's ones 14/08 23:15 Ah. 14/08 23:15 Well, if one doesn't assume that the underlying language has these things... (e.g. C) 14/08 23:15 yeah, the main point here is that Set represents "epigram" types, so we know what we're dealing with when we define == 14/08 23:18 *nod* 14/08 23:19 -!- mode/#epigram [+v dolio] by ChanServ 14/08 23:19 ok, I found it. 14/08 23:25 Pig uses a definitional equality separate from observational equality to feed the type checker. 14/08 23:25 Hence the need for an explicit coercion operator. 14/08 23:25 Got it! 14/08 23:25 ah, yeah, OTT is all about separating the judgemental equality from the propositional one, i.e. the one used by the typechecker and the one exposed in the language 14/08 23:27 --- Day changed Sun Aug 15 2010 -!- mode/#epigram [+v dolio] by ChanServ 15/08 00:15 It seems a lot of the Pig core is made more complex by the need for names. Could a core execute some kind of name erasure and still be able to type check? "equal" wants a name supply... 15/08 01:18 Oh, I see. An artifact of the functional representation of closures. 15/08 01:21 have you read the paper 15/08 01:29 I am not a number I am a free variable 15/08 01:29 No, I don't think I've read that one. 15/08 01:33 Interesting. 15/08 01:34 So part of the quotation process is to replace functional closures with deBruijn indices. 15/08 01:35 Are we talking about the Scope stuff? 15/08 01:35 Because I thought they got rid of functional closures. 15/08 01:36 Not in the Epitome that I'm reading. 15/08 01:36 It's possible that it needs regenerating. 15/08 01:36 How old is it? 15/08 01:36 2010/08/13 15/08 01:36 Then again, I don't know if they changed the description. 15/08 01:36 The HF constructor is still present 15/08 01:36 Although there's a comment in heere... 15/08 01:37 Yes, but it's no longer a higher-order function. 15/08 01:37 HF :: String ! (VAL ! Tm {In, VV} x ) ! Scope p {-VV -} x 15/08 01:37 er, ! is -> 15/08 01:37 Looks higher-order to me. 15/08 01:37 Conor has a comment: I’min themiddle ofmessing this bit about. The plan is tomake scopes syntactic again, 15/08 01:37 but also to ensure that values can be embedded in terms. Step one is to whistle innocently and 15/08 01:37 allow both syntactic and functional scopes in both places. 15/08 01:37 Oh, I'm wrong. 15/08 01:38 :) 15/08 01:38 I guess they haven't completely eliminated it yet. 15/08 01:38 It's quite brain-bending for m.e 15/08 01:38 It's kind of a shame, because the higher-order stuff is so easy when you can use it. 15/08 01:38 But I guess it's got performance problems. 15/08 01:39 Honestly, programming with de Bruijn indices is a lot like programming a stack-based language like Forth. 15/08 01:39 Not too hard once you bend your brain around it. 15/08 01:40 Using the right higher-order representation has more advantages than just being able to use names. 15/08 01:40 As per the HOAS papers? 15/08 01:41 I quite like parametric HOAS. I rewrote an interpreter I have to use it not too long ago. 15/08 01:41 Given that I'm hoping to target C as my language for the core implementation, I won't be able to use HOAS anyway. :) 15/08 01:41 Yes, PHOAS is lovely. 15/08 01:41 I wouldn't be surprised if it had negative impact on performance, though. 15/08 01:41 It lets you write down a lot of useful functions on your terms just by filling in the right bound variable type. 15/08 01:41 Yes, no doubt. 15/08 01:42 ok, dinner soon. Talk to you all later. 15/08 01:42 For instance, I was able to write a Show instance that produces valid Haskell source for my terms. :) 15/08 01:43 o.O nice 15/08 01:43 Lambdas and all. 15/08 01:43 Of course, that wouldn't be at all surprising if it weren't higher-order. 15/08 01:44 :) 15/08 01:47 ttyl :D 15/08 01:47 -!- mode/#epigram [+v dolio] by ChanServ 15/08 02:15 -!- mode/#epigram [+v dolio] by ChanServ 15/08 03:18 when did the levitation paper get the set-stratification added? 15/08 06:36 When they were revising the paper due to comments from reviewers, I think. 15/08 06:42 Bother, now I have to print a new copy. 15/08 06:54 :P 15/08 06:54 Although it makes the need for switchD/switchID much clearer. 15/08 06:54 So who came up with extending descriptions with a nu operator for coinduction? 15/08 06:58 It's a pretty straight-forward idea, isn't it? 15/08 06:58 Yeah, but I'm willing to bet there's a catch. 15/08 06:58 Coinduction is never straightforward in my experience. 15/08 06:59 The descriptions don't actually have internal mu and nu yet anyway, though. 15/08 06:59 Hm. 15/08 06:59 I don't think coinduction is that hard, either, except people have been messing up the interface for it. 15/08 07:01 Agda and Coq implement something that isn't exactly categorical coinduction with their productivity checkers, for instance. 15/08 07:03 Hmm... 15/08 07:04 I always associated coinduction with laziness. 15/08 07:04 It's technically just the result of taking the greatest fixpoint of an endofunctor, yes? 15/08 07:04 For instance, in Agda, you can get away with a single coinductive datatype. 15/08 07:04 'codata Delay (A : Set) : Set where d : A -> Delay A' 15/08 07:05 Yes. 15/08 07:05 I see. 15/08 07:05 But it makes no sense for you to be able to use that for all coinduction. 15/08 07:05 Delay is just the identity functor. 15/08 07:05 But it doesn't work that way. 15/08 07:06 The fixpoints of identity are... oh. 15/08 07:06 Not exactly categorical coinduction. 15/08 07:06 Because the agda productivity checker will accept any definition where the corecursive call is guarded by constructors, at least one of which is coinductive. 15/08 07:07 *nod* 15/08 07:07 As will coq's. 15/08 07:07 Yeah. 15/08 07:07 Because that's "good enough". 15/08 07:07 And it appeals to the idea of coinduction as "selectively lazy evaluation" 15/08 07:08 And Coq also has the weirdness of values of a coinductive type being/evaluating to constructors of said type. 15/08 07:08 Which mixes up evaluation semantics and categories. 15/08 07:08 Which isn't really justified by the underlying theory. 15/08 07:08 Coq is very hacky in various ways. Which is why I'm looking so hard at epigram. 15/08 07:09 Agda used to have that, too, of course. 15/08 07:09 brb - getting drink 15/08 07:09 back 15/08 07:10 Charity might be the only language that's gotten it right so far (of course, it's the only other one I know of that's tried), but I can't actually confirm that, because I haven't used it. 15/08 07:11 Although, being directly category-theory-based, you'd expect it to be right. 15/08 07:11 I'm not entirely clear on what's required to get it right. 15/08 07:11 Obviously "lazy evaluation" is only one piece of the puzzle. 15/08 07:11 Introduction via unfold, elimination via single-step observations. 15/08 07:12 Of course, Charity isn't dependently typed, so it doesn't have to worry about equality at all, which is a big issue. 15/08 07:12 *nod* 15/08 07:12 Always a catch... :) 15/08 07:12 -!- mode/#epigram [+v dolio] by ChanServ 15/08 07:14 oh! 15/08 07:19 Introduction via coind, elimination via cocon. Ahaha. 15/08 07:19 Of course. 15/08 07:19 Right. 15/08 07:20 Sorry, real coinduction always makes me think. Gotta remember it's purely dual to induction. 15/08 07:20 And as far as equality is concerned, proof by coinduction should get you some kind of bisimulation. 15/08 07:25 But that doesn't gel well with intensional equality. 15/08 07:25 Or maybe we just haven't figured out how it fits in well with dependent types yet. 15/08 07:26 I don't think anyone's figured out a good dependently typed 'coinduction principle' similar to the induction principles you get for datatypes. 15/08 07:27 And the induction principles let you prove things like 'x + (y + z) = (x + y) + z' even though, if you're really strict in your intensionality, they'd be unequal. 15/08 07:29 Because they're not built exactly the same. 15/08 07:29 -!- mode/#epigram [+v soupdragon] by ChanServ 15/08 07:32 Didn't I see something about that on the blog? 15/08 07:47 Yes, I did: http://www.e-pig.org/epilogue/?p=418 15/08 07:47 "Or, in other words, it works." 15/08 07:48 Saizan linked to an interesting agda file with the coinduction stuff in it. It's a bit over my head, though: http://code.haskell.org/~Saizan/bisim/ObsEq.agda 15/08 07:48 Taral: that file i linked is doing the same thing as that blog post but using descriptions instead of Cont 15/08 07:57 Yes, I noticed the parallels. 15/08 07:57 Still over my head for now. 15/08 07:57 Nice to know that, when I need it, it will be there. 15/08 07:57 nini 15/08 08:30 -!- mode/#epigram [+v soupdragon] by ChanServ 15/08 09:08 -!- mode/#epigram [+v dolio] by ChanServ 15/08 09:18 from Evidences.Tm: "[...] neutral application of a fake reference --- a definition whose hysterectomy stops it computing" 15/08 10:52 I had to look up a dictionary 15/08 10:52 needless to say, that didn't really helped... 15/08 10:52 "\item |FAKE|: a hysterectomized definition, used to make labels.", so i think it means that a fake reference is a definition without a body, hence it can't compute 15/08 11:07 thanks, Doctor :-) 15/08 11:08 moleris, I was uploading the missing pictures to the EPIG post, got that: "Unable to create directory /var/www/html/epigram/epilogue/wp-content/uploads/2010/05. Is its parent directory writable by the server?" 15/08 11:42 it's not really important nor urgent, just fyi. 15/08 11:43 -!- mode/#epigram [+v dolio] by ChanServ 15/08 13:14 -!- mode/#epigram [+v dolio] by ChanServ 15/08 14:14 -!- mode/#epigram [+v dolio] by ChanServ 15/08 17:17 -!- mode/#epigram [+v dolio] by ChanServ 15/08 19:18 -!- pumpkin is now known as copumpkin 15/08 19:37 -!- mode/#epigram [+v soupdragon] by ChanServ 15/08 20:31 -!- pumpkin is now known as copumpkin 15/08 23:58 --- Day changed Mon Aug 16 2010 -!- mode/#epigram [+v dolio] by ChanServ 16/08 03:17 -!- mode/#epigram [+v dolio] by ChanServ 16/08 08:17 -!- mode/#epigram [+v dolio] by ChanServ 16/08 10:14 -!- mode/#epigram [+v dolio] by ChanServ 16/08 12:18 -!- mode/#epigram [+v soupdragon] by ChanServ 16/08 12:27 pedagand: upload should work now 16/08 13:17 -!- mode/#epigram [+v dolio] by ChanServ 16/08 17:14 moleris, thanks. I've fixed the post, at last. 16/08 19:05 -!- mode/#epigram [+v dolio] by ChanServ 16/08 20:14 -!- mode/#epigram [+v dolio] by ChanServ 16/08 21:14 -!- mode/#epigram [+v dolio] by ChanServ 16/08 23:33 --- Day changed Tue Aug 17 2010 -!- mode/#epigram [+v dolio] by ChanServ 17/08 01:17 -!- mode/#epigram [+v dolio] by ChanServ 17/08 02:14 ok, I have a new problem. 17/08 04:17 What is the type of % (out)? 17/08 04:17 it doesn't actually seem to have an expressible type. :/ 17/08 04:18 -!- mode/#epigram [+v soupdragon] by ChanServ 17/08 04:26 hm, apparently it can't have an expressible type. :( 17/08 04:27 Is it necessary? Can I hack it up with "ind"? 17/08 04:27 I think so... 17/08 04:27 Oh! I think it can have a type... 17/08 04:28 Just have to have a proper constructor? 17/08 04:28 ... noep. 17/08 04:35 *nope 17/08 04:35 ok. 17/08 04:35 -!- mode/#epigram [+v dolio] by ChanServ 17/08 07:17 -!- mode/#epigram [+v codolio] by ChanServ 17/08 11:17 mount 17/08 13:50 -!- mode/#epigram [+v dolio] by ChanServ 17/08 14:14 -!- copumpkin is now known as snowboard 17/08 14:58 -!- snowboard is now known as copumpkin 17/08 15:00 -!- mode/#epigram [+v dolio] by ChanServ 17/08 15:17 -!- mode/#epigram [+v codolio] by ChanServ 17/08 16:17 -!- codolio is now known as dolio 17/08 17:27 -!- mode/#epigram [+v dolio] by ChanServ 17/08 20:17 -!- mode/#epigram [+v dolio] by ChanServ 17/08 22:13 --- Day changed Wed Aug 18 2010 -!- mode/#epigram [+v dolio] by ChanServ 18/08 00:17 -!- mode/#epigram [+v soupdragon] by ChanServ 18/08 01:10 -!- mode/#epigram [+v dolio] by ChanServ 18/08 04:14 -!- koninkje_away is now known as koninkje 18/08 05:08 -!- mode/#epigram [+v dolio] by ChanServ 18/08 07:17 -!- koninkje is now known as koninkje_away 18/08 08:05 -!- mode/#epigram [+v dolio] by ChanServ 18/08 10:17 -!- mode/#epigram [+v dolio] by ChanServ 18/08 12:13 -!- mode/#epigram [+v soupdragon] by ChanServ 18/08 12:24 -!- mode/#epigram [+v codolio] by ChanServ 18/08 13:17 -!- mode/#epigram [+v pigworker] by ChanServ 18/08 13:46 -!- mode/#epigram [+v pigworker_] by ChanServ 18/08 17:03 -!- pigworker_ is now known as pigworker 18/08 17:03 -!- mode/#epigram [+v dolio] by ChanServ 18/08 17:17 Hello I was thinking of testing Epigram a little but I can't find where to download it. Only Epigram2 seems to be on e-pig.org 18/08 18:01 -!- mode/#epigram [+v soupdragon] by ChanServ 18/08 21:06 -!- mode/#epigram [+v dolio] by ChanServ 18/08 21:17 --- Day changed Thu Aug 19 2010 -!- mode/#epigram [+v soupdragon] by ChanServ 19/08 03:47 -!- ServerMode/#epigram [+vvvv edwinb dolio soupdragon codolio] by holmes.freenode.net 19/08 10:19 -!- ServerMode/#epigram [+v Saizan] by holmes.freenode.net 19/08 10:19 -!- ServerMode/#epigram [+vvv codolio soupdragon edwinb] by holmes.freenode.net 19/08 10:35 -!- mode/#epigram [+v Saizan] by ChanServ 19/08 11:12 danten: If you really want Epigram1 I've got the old binaries 19/08 11:54 I just want to test it some :) 19/08 11:54 http://www.cs.nott.ac.uk/~pwm/epigram1-linux.tar.gz 19/08 11:54 thanks 19/08 11:54 http://www.cs.nott.ac.uk/~pwm/epigram1-windows.zip 19/08 11:55 you'll need xemacs 19/08 11:55 ok 19/08 11:56 -!- mode/#epigram [+v dolio] by ChanServ 19/08 13:17 -!- mode/#epigram [+v soupdragon] by ChanServ 19/08 16:35 -!- mode/#epigram [+v dolio] by ChanServ 19/08 19:22 -!- mode/#epigram [+v dolio] by ChanServ 19/08 22:21 -!- mode/#epigram [+v dolio] by ChanServ 19/08 23:13 -!- koninkje_away is now known as koninkje 19/08 23:29 --- Day changed Fri Aug 20 2010 -!- pumpkin is now known as copumpkin 20/08 00:00 -!- mode/#epigram [+v dolio] by ChanServ 20/08 01:13 -!- mode/#epigram [+v soupdragon] by ChanServ 20/08 06:00 -!- koninkje is now known as koninkje_away 20/08 09:47 -!- mode/#epigram [+v dolio] by ChanServ 20/08 12:12 -!- mode/#epigram [+v soupdragon] by ChanServ 20/08 14:54 on http://www.e-pig.org/epilogue/?p=657 where it says "We get from values to types by quotation.", should it instead read "We get from values to terms by quotation."? 20/08 15:46 roconnor: yes, it should 20/08 15:47 in fact, maybe I should just fix that typo 20/08 15:47 done 20/08 15:50 ah, I see the comments at the end shows that I'm not the only one caught by this. 20/08 16:41 -!- mode/#epigram [+v dolio] by ChanServ 20/08 18:57 -!- mode/#epigram [+v dolio] by ChanServ 20/08 19:16 -!- mode/#epigram [+v dolio] by ChanServ 20/08 20:12 -!- mode/#epigram [+v dolio] by ChanServ 20/08 22:12 -!- mode/#epigram [+v dolio] by ChanServ 20/08 23:16 --- Day changed Sat Aug 21 2010 -!- mode/#epigram [+v dolio] by ChanServ 21/08 00:16 -!- mode/#epigram [+v soupdragon] by ChanServ 21/08 05:35 -!- mode/#epigram [+v dolio] by ChanServ 21/08 07:15 -!- mode/#epigram [+v dolio] by ChanServ 21/08 16:16 -!- mode/#epigram [+v dolio] by ChanServ 21/08 17:15 -!- mode/#epigram [+v dolio] by ChanServ 21/08 20:12 -!- mode/#epigram [+v dolio] by ChanServ 21/08 23:16 --- Day changed Sun Aug 22 2010 -!- mode/#epigram [+v dolio] by ChanServ 22/08 02:12 -!- mode/#epigram [+v codolio] by ChanServ 22/08 08:15 -!- mode/#epigram [+v soupdragon] by ChanServ 22/08 09:24 -!- codolio is now known as dolio 22/08 10:30 -!- mode/#epigram [+v dolio] by ChanServ 22/08 13:15 -!- soupdragon is now known as Grass-Mud-Horse 22/08 13:34 -!- mode/#epigram [+v dolio] by ChanServ 22/08 17:15 -!- mode/#epigram [+v Grass-Mud-Horse] by ChanServ 22/08 17:36 -!- mode/#epigram [+v dolio] by ChanServ 22/08 20:15 -!- mode/#epigram [+v dolio] by ChanServ 22/08 21:12 -!- koninkje_away is now known as koninkje 22/08 23:26 --- Day changed Mon Aug 23 2010 -!- mode/#epigram [+v dolio] by ChanServ 23/08 00:15 -!- mode/#epigram [+v dolio] by ChanServ 23/08 02:15 -!- mode/#epigram [+v dolio] by ChanServ 23/08 04:15 -!- koninkje is now known as koninkje_away 23/08 05:14 -!- mode/#epigram [+v dolio] by ChanServ 23/08 09:15 -!- mode/#epigram [+v Grass-Mud-Horse] by ChanServ 23/08 09:55 -!- mode/#epigram [+v Saizan] by ChanServ 23/08 11:13 -!- mode/#epigram [+v codolio] by ChanServ 23/08 11:15 -!- mode/#epigram [+v Saizan] by ChanServ 23/08 11:32 pedagand: hola 23/08 11:43 hello 23/08 11:45 what's up? 23/08 11:45 Just thought I'd reply here to at least one of your emails 23/08 11:45 Would be good to do some Epigram while you are around next week 23/08 11:46 though what we can usefully do is up for debate 23/08 11:46 all right! Do you want to give the demo with Cochon or a more "high-level" system? 23/08 11:47 I was hoping to do as much as possible without really talking about the proofstate as such 23/08 11:50 whether thats a case of using cochon's `programming' tactics, or something else, I do not know 23/08 11:50 yeah, the problem is "time". I don't know how much we can do before ICFP 23/08 11:52 I've been experimenting with various high-level interfaces (that is, dropping Cochon out of the way) 23/08 11:53 the elaboration problem is not too hard, but distillation (from proofstate to the high-level system) is quite fiddly 23/08 11:53 another angle of attack would be to try implementing a serious demo and get it to work as we go 23/08 11:55 we probably will need to implement the "with" gadget on our way there 23/08 11:55 shouldn't be a massive problem that, really (with) 23/08 11:56 (also, improve our induction principles, and remove the sigma-splitting madness, something we've discussed on Friday here) 23/08 11:57 oh, cool 23/08 11:57 improve ind how? 23/08 11:57 yeah, I hope so 23/08 11:57 right now, we rely on Enum splitting to give access to branches per constructor. Instead, given a TaggedDesc, we should generate the induction principle that does this constructor splitting 23/08 11:59 because Enum splitting triggers everywhere, not just when you're in a Description. That's annoying (and incorrect). 23/08 11:59 indeed, eliminating a list of bools and getting two cons cases is just odd :) 23/08 12:00 exactly :-) 23/08 12:01 -!- mode/#epigram [+v Saizan] by ChanServ 23/08 12:03 so, if you like the targeted approach, we should come up with a list of things you would like to show off. 23/08 12:03 I suspect, starting from basic stuffs, going crazy on stuff that only us can do, such as OTTism, Desc-ism, etc. 23/08 12:04 Indeed 23/08 12:05 I'd like to show pigworkers FreeIMonad stuff from FitA Standard Chartered if possible 23/08 12:06 I plan to write that feature file this week 23/08 12:06 "FitA Standard Chartered"? 23/08 12:06 what's this? 23/08 12:07 hmm, actually that was a she talk wasn't it 23/08 12:07 oh, I understand 23/08 12:07 ignore me 23/08 12:07 sorry, got confused by the acronym 23/08 12:07 why do you want to implement it as a Feature? You plan to use the simplification rules? 23/08 12:08 Yeah, that would be good :) 23/08 12:10 I see, that would be good indeed 23/08 12:11 Shame that your talk is after the demo - but still 23/08 12:12 going to grab something to eat - chat in a bit 23/08 12:12 see ya 23/08 12:12 Q: Whats the status of the implicit syntax mechanism and the spotting of recursive calls? 23/08 15:45 I think it just works, isn't it? 23/08 15:57 for example, in List.pig 23/08 15:58 you do your recursive call, the machinery tries to find the corresponding programming problem in the context 23/08 15:59 Hmm, but if (for instance) you make the type of snoc {A : Set} -> ... rather than (A : Set) -> ... it won't fill in A and then spot the programming prob in the context 23/08 16:07 ha, this is a bug then, no? 23/08 16:18 I guess so 23/08 16:19 is the programming problem mentioning the implicit argument? 23/08 16:19 probably, it should (even if not displaying it in Cochon) 23/08 16:20 It doesn't, but I think that's ok 23/08 16:23 ha? then I don't see how to fix the bug, you have an idea? 23/08 16:24 well, the thing we want to use currently has this type: 23/08 16:28 xf : ((a : A) -> < snoc^1 A xf^1 a : List A >) 23/08 16:28 where A is fixed by the sub-list (xf^1 : List A) - so I don't see how we do anything else 23/08 16:29 but then I don't know the code in question well enough to suggest another path forward 23/08 16:29 in these examples, you add defined snoc with {A : Set}, right? 23/08 16:40 nevermind, I'll try defining it on my side and see if I can have a clue 23/08 16:42 -!- codolio is now known as dolio 23/08 17:11 any luck? 23/08 17:37 -!- mode/#epigram [+v codolio] by ChanServ 23/08 20:15 --- Day changed Tue Aug 24 2010 -!- codolio is now known as dolio 24/08 00:45 -!- pumpkin is now known as copumpkin 24/08 06:30 -!- xa is now known as xarch 24/08 09:39 hi 24/08 09:40 hi 24/08 09:41 moleris, so, I took snoc in List.pig, replace (A : Set) by {A : Set}, replace the recursive call "snoc A ..." by "snoc ..." and it just works 24/08 09:57 so, I guess, I don't understand the point you raised yesterday... 24/08 09:57 xarch, would you mind re-subscribing to -discuss, filling in your name in the appropriate field? It's just to avoid spam bots. Or you could prove your belonging to the human race right here and I just approve the subscription as it is :-) 24/08 10:12 looks like I won't make career as a doorman, or the nightclub will be empty :-( 24/08 10:20 oops, sorry 24/08 10:25 so, how do you want me to prove I'm human ? 24/08 10:25 kind of, you just did, isn't it? :-) 24/08 10:27 here you go, "approved" human being :-) 24/08 10:28 thanks :) 24/08 10:28 pedagand: Really? What do you mean by 'just works'? 24/08 10:29 moleris, it is accepted and there is no subgoal left 24/08 10:29 wait a sec, I copy it on pastebin 24/08 10:30 http://pastebin.com/L4cen0My 24/08 10:31 and if I do "prev" or "next", there is no subgoal 24/08 10:31 Let me just check this without my unrecorded changes to the tree 24/08 10:36 (go to go (to work), will be back soon) 24/08 10:46 pedagand: I agree that it works now (: 24/08 11:41 all right, perfect then. Was it not-working because of your local change? 24/08 11:42 I don't think so, it's possible that agundry fixed it 24/08 11:42 there were some patches I had to leave on the server because of my changes conflicting with them 24/08 11:43 oh, you were on a old tree. Then, yes, that's likely 24/08 11:43 not that old, a few days 24/08 11:43 anyway, I'm happy it works 24/08 11:44 I'm not sure exactly what you guys were planning to do about induction principles but I've got something that does the trick in a slightly hacky way 24/08 11:45 using agundry's 'haskell' tactic to write a kind of data prelude 24/08 11:47 means you can turn off that Enum simplification and still write programs 24/08 11:47 why does Epigram use its own parser combinators library instead of, for example, Parsec ? 24/08 12:03 xarch, masochism is the only reasonable answer I found. There used to be a plan to develop a fancy parser (that nobody else provides as of today), but most of us are just scared by parsers now, so we are stuck with this one. 24/08 12:29 moleris, sorry, pigworker came in. I've detailed the plan for induction here [http://code.google.com/p/epigram/issues/detail?id=48] 24/08 12:30 I think, what you did was what Adam initially suggested. What pigworker wanted was to generate this principle directly inside Epigram 24/08 12:30 do you think it would be difficult to follow the suggestion of our Supreme Leader? 24/08 12:34 so if i rewrote Parsley so that it uses Parsec, my patch would be accepted ? 24/08 12:37 *rewrite 24/08 12:37 hey but 24/08 12:40 you're french ? 24/08 12:40 yeah,  but I promise, I didn't meant to be French. I just happen to be born there, silly mistake :-) 24/08 12:44 well 24/08 12:44 I'm french too :) 24/08 12:44 if you rewrote it, well, and it's clean, it would be accepted, yeah. But, honestly, don't bother: we need to drop that stuff one day or another, the sooner the better. 24/08 12:45 I saw that :-) 24/08 12:45 that's why I was wondering if you knew the risks you're taking, being there and not on #coq :-) 24/08 12:47 Roms has been deported for less than that, you know 24/08 12:48 ha, you're on #coq now, well done ;-) 24/08 12:51 pedagand: Sorry, I should look at the bug tracker more often |: 24/08 12:53 no problem 24/08 12:54 I pretty much did what pigworker suggests 24/08 12:54 you can follow it by RSS, if you like this technology 24/08 12:54 oh, that's perfect then. Out of curiosity, why do you need the haskell tactic to do that? 24/08 12:55 the Haskell bit only comes in because I don't know a decent way of bootstrapping the prelude, so I can specialise the generated induction principle when the user defines a new data type 24/08 12:55 all right. When you're happy with it, please commit, I'm curious to see that. 24/08 12:56 I'll what I have, but with the enum simplification switched on still - since I haven't done anything to the ol' Desc stuff 24/08 12:58 if we could get some form of labelling on IDesc, we could remove Desc probably 24/08 12:59 That's the dream. 24/08 13:00 Well, we have some form of labelling. We need a better one 24/08 13:01 I've thought about it and I just don't see a nice way. I think I don't understand the big picture, so I really need to spend some time studying the code. 24/08 13:02 I have bits of the picture, but I'm no less bamboozled 24/08 13:03 OK, it's on blinky 24/08 13:03 I should add the original epigram definitions to the test suite too 24/08 13:04 great, thanks. I'm away to fax a few things for ICFP. Yes, you read correctly: to fax things. Will be back shortly. 24/08 13:05 back from the 70's, hurrah. 24/08 13:12 xarch, out of curiosity, what got you interested in the parser? A long struggle with it? 24/08 13:23 no 24/08 13:24 that's because rewriting Parsley to use Parsec doesn't seem to be really hard 24/08 13:25 but now i have made a change to the code that is even cooler 24/08 13:26 Cochon's prompt is now λ instead of > 24/08 13:26 haha 24/08 13:26 that's so cool 24/08 13:26 rewriting Parsley to use Parsec is not hard, but doesn't solve the real problem, which is in DisplayLang.TmParse: the term parser is a nightmare. 24/08 13:33 this is due to the absence of support of left-recursion, plus various hack (in the syntax) to solve performance issues 24/08 13:35 Parsec would give clean error report, tho. 24/08 13:36 moleris, had a look at the new IDesc: haha! :-) I love ity and friends. 24/08 13:45 if I improve Cochon prompt so that there's an history of typed commands, would you accept my patch ? 24/08 13:51 *Cochon's 24/08 13:51 we use "rlwrap" for that. Also, work on Cochon is suspended because it must disappear 24/08 13:51 Cochon will become a "ProofState explorer", no more. 24/08 13:52 ah, ok 24/08 13:52 right now, it is abused as a theorem prover, but this is really an abuse 24/08 13:52 rlwrap or a shell in emacs do the trick usually 24/08 13:53 but don't misread me, I'm not "rejecting/accepting patches", just avoiding you wasting your time 24/08 13:55 pedagand: it's horrible, I know. Please don't hate me 24/08 14:00 I've updated the bug tracker 24/08 14:01 that's all right, introducing code means increasing entropy. As soon as this is documented, that's under control. In this case, that's well done, imho. 24/08 14:03 -!- mode/#epigram [+v dolio] by ChanServ 24/08 18:14 -!- mode/#epigram [+v dolio] by ChanServ 24/08 21:11 -!- mode/#epigram [+v dolio] by ChanServ 24/08 22:15 -!- mode/#epigram [+v dolio] by ChanServ 24/08 23:11 --- Day changed Wed Aug 25 2010 -!- mode/#epigram [+v dolio] by ChanServ 25/08 00:14 -!- mode/#epigram [+v dolio] by ChanServ 25/08 03:14 -!- mode/#epigram [+v dolio] by ChanServ 25/08 08:14 xarch, I had a chat with our Supreme Leader yesterday: if Parsec can give us precise (line, column) information, we would favourably move to a saner, Parsec parser 25/08 10:22 I'm still wading through Parsec API but I believe I can give this information 25/08 10:22 however, I really like uu-parsinglib... 25/08 10:24 yeah, uu-parsinglib is really close to what we want in the end, in term of implementation 25/08 10:27 what does it lack? 25/08 11:20 pigworker has a very special "automaton-based parser" in mind 25/08 11:32 it's not that uu-parsinglib lacks something, it just a different implementation 25/08 11:39 a more proper question would have been, what would be the advantages of this automaton-based parser over uu-parsinglib? but i guess it'd require a lengthy explanation and your time might be needed elsewhere :) 25/08 11:47 my time is not needed anywhere, you cannot imagine how useless I am :-) Here is the data-type of this automaton: newtype Parser t x = Parser (Maybe x, t -> Maybe (Parser t x)) 25/08 11:51 I think the advantage is that it's "resumable": you can parse a bit, stop and think, then re-parse a bit, etc. 25/08 11:52 now, the drawback is that it's not implemented and nobody wants to do it :-) When it comes to parsers, I've more trust in Doaitse than in ourselves. 25/08 11:53 ah, it has some similarity with iteratees, though those have a way to refuse to accept more input 25/08 12:00 that's interesting 25/08 12:08 well, if you explain it more precisely I'd maybe like to try to implement it :-) 25/08 13:19 (and sorry, I was away) 25/08 13:19 no problem. So, we would be glad to replace Parsley by some other parser combinator library. However, we need to be careful to be able to get the line-column information of the tokens. 25/08 13:32 this information is not needed in the very short term, so, as a first step, we could ignore that. But, eventually, we want this information so the parser combinators must let us get this information, somehow 25/08 13:33 I'm pretty sure any decent combinator library would provide that, but it's better to be sure before moving on using it.. 25/08 13:34 finally, instead of parsec, I was wondering if uu-parsinglib is not better. But I don't have much experience with it, just happen to know Doaitse and like what he does 25/08 13:34 ok 25/08 13:37 -!- jjc_ is now known as jcapper 25/08 14:58 -!- mode/#epigram [+v dolio] by ChanServ 25/08 15:09 -!- mode/#epigram [+v pigworker] by ChanServ 25/08 16:41 Just checking... does Agda from darcs need ghc >= 6.12 these days? 25/08 16:43 I might be teaching an Agda course in Edinburgh, early 2011. I suppose we'll be lucky if 6.12 cuts it by then... 25/08 16:46 how embarrassing; I meant to ask that in #Agda.. 25/08 16:47 pigworker, you know you're on #epigram, right? #agda is the next door 25/08 16:47 ok 25/08 16:47 in other news, Dr Oury will be visiting Glasgow tomorrow, which sounds like an excuse for a free lunch 25/08 16:48 goodo 25/08 16:48 out of curiosity, is he coming back in type theory-land? or he still enjoys dissecting rats with computers? 25/08 16:49 I guess, I could ask tomorrow... curiosity killed the rat 25/08 16:49 he's keen to do a little coinduction on the side, anyhow 25/08 16:50 all right, will be in the lab tomorrow then. Going back home now, watch out the streets for a right-leaning cyclist. 25/08 16:57 uh, the parseBrackets needed refactoring 25/08 17:32 +parser 25/08 17:32 haha 25/08 17:34 and I think the parseIdent parser should juste be parseWord 25/08 17:35 becuase, in parseToken, parseKeyword is before 25/08 17:35 parseIdent 25/08 17:35 but sometimes parseIdent is used alone, I suspect, and you want to parse a keyword as an ident 25/08 17:36 oh, ok 25/08 17:36 but, in whatever library you use, you should probably be able to define keywords as a separate entity, isn't it? 25/08 17:36 in which case, your suggestion is the right thing to do 25/08 17:36 oh, I'm so stupid 25/08 17:36 i should have used parsec's tools to make the lexer 25/08 17:37 as I told you, this thing is massively over-engineered to do one thing and to do it very badly 25/08 17:37 maybe, I don't know which way is best. I did that for this lexer, before me, pigworker wrote the lexer within the State monad. 25/08 17:38 which library are you using/planning to use? 25/08 17:39 I currently only now how to use Parsec 25/08 17:39 but I will look at uu-parsinglib 25/08 17:39 yeah, no worries. 25/08 17:41 couldn't you make use of the makeTokenParser thingie? 25/08 17:42 yes 25/08 17:42 I have used that thing in the past, that worked quite well 25/08 17:43 I'm trying to make Pig and tome; what the frel is manfnt.sty? 25/08 17:48 no clue 25/08 17:50 I'm investigating the case 25/08 17:50 you can just 'make Pig' if you want just to make Pig 25/08 17:50 'make clean dep && make Pig' actually 25/08 17:51 I ain't got it, so no tome for me. Probable fix: add to repo. 25/08 17:51 out of curiosity, what is the name of the TeX distribution on MacOS? It seems rather poor, isn't it? 25/08 17:52 ha, manfnt is the thing that gives the cute "Danger" diagram :-) 25/08 17:52 it has been a long time since you've compiled the Epitome 25/08 17:53 I'm using tetex, from macports. It's bloody awful, as is macports. 25/08 17:53 indeed, that's quite light. In FreeBSD, they have at least tetex-extras 25/08 17:54 I use MacTeX 25/08 17:54 and don't mind it 25/08 17:54 but I mostly use XeTeX and haven't used many exotic packages 25/08 17:55 Maybe I just need to port install tetex-extras, or maybe I need to fumigate macports off my machine for good. 25/08 17:55 yeah, I used to like macports, but homebrew seems nicer now 25/08 17:56 if not as complete 25/08 17:56 anyway, I pushed manfnt into the wild 25/08 17:57 pedagand: thanks; having another go, fingers crossed... 25/08 17:59 at worst, the Epitome is linked in the Epilogue 25/08 18:00 I know I'm a bit of a spare part, but I still like to be able to make on my computer. 25/08 18:02 do you want nested comments ? 25/08 18:02 xarch, yep 25/08 18:03 ok 25/08 18:03 or is it a hassle? I mean, in a first instance, we can live without them 25/08 18:03 we've been debating the lexical structure of comments quite a bit recently; it's fascinating 25/08 18:03 pedagand: it's only a matter of setting nestedComments = True or False :) 25/08 18:04 yeah, that's what I thought too but I wasn't sure you followed this path :-) 25/08 18:05 pedagand: Thanks to your patch, make works. But when I build the tome, nothing is dangerous. I guess there's a font file I also need. 25/08 18:07 It's not an urgent problem. 25/08 18:09 yeah. Strangely enough, I'm not too worried that you do a dangerous thing :-) 25/08 18:09 for instance, there is one top of p.13 25/08 18:10 -!- mode/#epigram [+v dolio] by ChanServ 25/08 18:10 Goodness me! I take it back. So there is. Why didn't I see it a moment ago? 25/08 18:11 -!- mode/#epigram [+v pigworker_] by ChanServ 25/08 18:20 -!- pigworker_ is now known as pigworker 25/08 18:22 -!- mode/#epigram [+v dolio] by ChanServ 25/08 19:10 -!- mode/#epigram [+v dolio] by ChanServ 25/08 20:14 -!- mode/#epigram [+v pigworker] by ChanServ 25/08 23:26 --- Day changed Thu Aug 26 2010 -!- mode/#epigram [+v dolio] by ChanServ 26/08 04:10 -!- mode/#epigram [+v pigworker] by ChanServ 26/08 09:03 moleris, what is the plan for Telescopes (in Evidences.Tm)? 26/08 12:30 -!- mode/#epigram [+v Saizan] by ChanServ 26/08 12:31 -!- mode/#epigram [+v pigworker] by ChanServ 26/08 12:32 pedagand: hungry? 26/08 12:32 pigworker, always 26/08 12:32 pedagand: I was thinking of Osteria Piero, Wellington St; my place is on the way; if you ring my doorbell Dr O and I will come out 26/08 12:34 all right. So, shall I come now or you're in the middle of something? 26/08 12:35 now's good 26/08 12:36 unless you're in the middle of something 26/08 12:36 btw, bringing 2 French hosts on WELLINGTON street... That's perverse. 26/08 12:36 I'm in the middle of nowhere. Will be here in a few minutes. 26/08 12:37 -!- mode/#epigram [+v dolio] by ChanServ 26/08 14:14 -!- mode/#epigram [+v dolio] by ChanServ 26/08 17:10 -!- mode/#epigram [+v dolio] by ChanServ 26/08 18:13 --- Day changed Fri Aug 27 2010 -!- mode/#epigram [+v dolio] by ChanServ 27/08 01:10 -!- pumpkin is now known as copumpkin 27/08 04:01 -!- mode/#epigram [+v dolio] by ChanServ 27/08 06:13 dear Brits, which one of these combinations has the highest chance to bring me home (alive), in your opinion: {Nottingham -> Derby -> Crewe -> Glasgow}  or {Nottingham -> Manchester Picadilly -> Preston -> Glasgow}? 27/08 09:39 -!- mode/#epigram [+v dolio] by ChanServ 27/08 10:15 -!- mode/#epigram [+v dolio] by ChanServ 27/08 10:30 -!- mode/#epigram [+v pigworker_] by ChanServ 27/08 11:30 -!- pigworker_ is now known as pigworker 27/08 11:30 pedagand: What time of day are you leaving? 27/08 13:12 moleris, in the morning of the 8th 27/08 13:18 I thought, sometime around 8 27/08 13:18 Then your life is probably not in danger 27/08 13:25 The change in Manchester Picadilly is a long walk, but doable 27/08 13:26 ok, thanks 27/08 13:35 Yeah, the Manchester way is probably more reliable. Worth checking if you could actually change at Manchester Oxford Road instead of Picc. 27/08 13:52 so, you don't advise NOT -> Derby -> Crewe -> GLC 27/08 14:02 Service Derby-Crewe is infrequent. 27/08 14:08 ooh 27/08 14:09 thanks 27/08 14:09 -!- mode/#epigram [+v dolio] by ChanServ 27/08 14:09 moleris: pub? 27/08 15:57 -!- mode/#epigram [+v codolio] by ChanServ 27/08 16:13 -!- mode/#epigram [+v pigworker] by ChanServ 27/08 18:02 -!- mode/#epigram [+v dolio] by ChanServ 27/08 19:13 -!- mode/#epigram [+v pigworker_] by ChanServ 27/08 21:46 -!- pigworker_ is now known as pigworker 27/08 21:47 -!- mode/#epigram [+v dolio] by ChanServ 27/08 22:13 --- Day changed Sat Aug 28 2010 -!- mode/#epigram [+v dolio] by ChanServ 28/08 01:38 -!- mode/#epigram [+v dolio] by ChanServ 28/08 02:13 -!- mode/#epigram [+v dolio] by ChanServ 28/08 07:13 -!- mode/#epigram [+v dolio] by ChanServ 28/08 13:09 -!- mode/#epigram [+v dolio] by ChanServ 28/08 16:12 shapr, the +v mode seems to be scaring people from #epigram: with your Superpowers, can you disable that? 28/08 16:22 I mean, I'm expecting people to be scared of Epigram, but they have to look at the code for that 28/08 16:23 now, we are scaring people even before they read any single line of code 28/08 16:23 that's no fun :-) 28/08 16:23 what's the point of writing code then.. 28/08 16:23 sure 28/08 16:33 bonjour pedagand, talar du svenska? :-) 28/08 16:34 thanks! 28/08 16:34 I understand the first half of this sentence, but the second half is out of my (Swedish, I suspect) reach :-) 28/08 16:35 Good guess. 28/08 16:35 ha, Google tells me that I answered your question without knowing what the question was :-) 28/08 16:36 Yup, pretty much. 28/08 16:36 Hm, I've forgotten how to use my irc Superpowers... 28/08 16:39 there must be some Kryptonite in the room then, be careful! 28/08 16:40 -!- roconnor_ is now known as roconnor 28/08 21:54 -!- mode/#epigram [+v pigworker] by ChanServ 28/08 22:48 --- Day changed Sun Aug 29 2010 -!- mode/#epigram [+v dolio] by ChanServ 29/08 00:13 -!- mode/#epigram [+v pigworker] by ChanServ 29/08 09:53 -!- mode/#epigram [+v dolio] by ChanServ 29/08 12:09 -!- mode/#epigram [+v pigworker_] by ChanServ 29/08 13:47 -!- pigworker_ is now known as pigworker 29/08 13:49 -!- mode/#epigram [+v dolio] by ChanServ 29/08 14:12 -!- mode/#epigram [+v pigworker] by ChanServ 29/08 15:33 Epigram 2 has a completely different syntax to Epigram 1, yes? 29/08 16:08 quite different afaik, there are examples in the test directory 29/08 16:10 Aww, I liked the Epigram 1 syntax.. 29/08 16:10 I never learnt it, but it looked very pretty. 29/08 16:10 well, the current epigram 2 one is just an interface to the proof state, the high level one doesn't exist yet :) 29/08 16:13 :) 29/08 16:15 This makes me happy. 29/08 16:16 So it doesn't have nice pattern matching and such? 29/08 16:18 it kind of does, but you've to explicitly call an eliminator 29/08 16:20 Does Epigram have the termination restriction Coq etc. have? 29/08 16:21 http://www.e-pig.org/darcs/Pig09/test/Demo.pig <- the demo is a nice tour of syntax, see the lines with "define" 29/08 16:21 i think normal functions are supposed to be total but they are also going to embed general recursion via something like a monad 29/08 16:23 When you say monad-like... 29/08 16:24 the main point is to somehow tag the fact they are using general recursion in the type system, and allow a "normal" function to be projected out only if you additionally prove termination 29/08 16:27 Ah. 29/08 16:30 yeah, right now, we have some kind of kernel for writing an interactive programming system. The actual interface for programming is up for grab, and actually there could well be many interfaces 29/08 16:42 "A separate (or at least separable) component, ...,  can generate a \texttt{.gram} file from an executable." <- isn't this backwards? (from notes/Epigram2/Epigram2.tex) 29/08 17:12 I think so, yes 29/08 17:19 the compiler takes the proofstate and generates a binary 29/08 17:19 -!- mode/#epigram [+v dolio] by ChanServ 29/08 19:09 -!- mode/#epigram [+v dolio] by ChanServ 29/08 20:13 -!- mode/#epigram [+v dolio] by ChanServ 29/08 22:09 -!- mode/#epigram [+v pigworker] by ChanServ 29/08 22:13 -!- mode/#epigram [+v dolio] by ChanServ 29/08 23:12 --- Day changed Mon Aug 30 2010 -!- mode/#epigram [+v dolio] by ChanServ 30/08 00:12 -!- mode/#epigram [+v pigworker] by ChanServ 30/08 00:34 -!- mode/#epigram [+v pigworker] by ChanServ 30/08 00:50 -!- mode/#epigram [+v dolio] by ChanServ 30/08 01:12 -!- mode/#epigram [+v pigworker] by ChanServ 30/08 01:17 -!- mode/#epigram [+v dolio] by ChanServ 30/08 02:12 -!- mode/#epigram [+v dolio] by ChanServ 30/08 03:12 -!- mode/#epigram [+v pigworker] by ChanServ 30/08 09:40 -!- mode/#epigram [+v pigworker] by ChanServ 30/08 11:45 -!- mode/#epigram [+v dolio] by ChanServ 30/08 15:56 -!- mode/#epigram [+v pigworker] by ChanServ 30/08 17:00 -!- mode/#epigram [+v pigworker] by ChanServ 30/08 17:22 -!- mode/#epigram [+v dolio] by ChanServ 30/08 18:26 -!- mode/#epigram [+v dolio] by ChanServ 30/08 18:51 -!- mode/#epigram [+v pigworker] by ChanServ 30/08 19:33 -!- copumpkin is now known as NaturalTransform 30/08 20:27 -!- NaturalTransform is now known as NattransSalad 30/08 20:27 -!- NattransSalad is now known as copumpkin 30/08 20:29 -!- mode/#epigram [+v dolio] by ChanServ 30/08 21:48 -!- mode/#epigram [+v pigworker] by ChanServ 30/08 21:57 -!- mode/#epigram [+v pigworker] by ChanServ 30/08 22:35 -!- mode/#epigram [+v pigworker] by ChanServ 30/08 23:04 --- Day changed Tue Aug 31 2010 -!- mode/#epigram [+v dolio] by ChanServ 31/08 02:51 -!- mode/#epigram [+v dolio] by ChanServ 31/08 07:51 -!- mode/#epigram [+v pigworker] by ChanServ 31/08 09:02 greetings sports fans. 31/08 10:41 > idata Vec (A : Set) : Nat -> Set := (nil : Vec A 'zero) ; (cons : A -> (n : Nat) -> Vec A n -> Vec A ('suc n)) ; 31/08 10:44 Parse failure: end of parser. 31/08 10:44 hmm, that's strange 31/08 10:56 > idata One : Set := (void : One) ; 31/08 10:56 Parse failure: end of parser. 31/08 10:56 I think the index set is compulsory at the moment, but even with one, idata doesn't seem to parse anything 31/08 10:57 it wasn't me, guv, I was on holiday... 31/08 10:58 me too :) back to work yesterday 31/08 10:58 there have been a lot of changes recently, but I can't see any that have touched the idata parser 31/08 10:59 moleris, any ideas? 31/08 10:59 ah, I think I see it 31/08 11:03 the parser for the |Ix -> Set| bit is parsing |Ix| at the wrong size, so it eats |-> Set| as well, then can't find another |-> Set| (surprise surprise) 31/08 11:06 hurrah, fixed 31/08 11:09 well, fixed the parser anyway 31/08 11:12 it now turns out that the anchors code doesn't work with idata (idesc?) so the Pig just crashes instead 31/08 11:13 agundry: thanks! 31/08 11:37 hmm, the new problem seems to be that the idesc bootstrapping code hasn't been updated since anchors were introduced 31/08 11:40 * tsapi reads about anchors 31/08 11:40 I don't know much about them 31/08 11:41 we really need a nice way to bootstrap some kind of prelude without converting Cochon code to Haskell manually 31/08 11:41 doesn't bother me :) I wonder how many times I've defined the natural numbers in Agda... I realise this isn't sensible behaviour though. 31/08 11:46 agundry: Agreed 31/08 13:39 I've fixed the idata tactic, and now I'm going to go find something tall to jump off 31/08 13:39 -!- mode/#epigram [+v dolio] by ChanServ 31/08 14:51 -!- mode/#epigram [+v dolio] by ChanServ 31/08 16:55 -!- mode/#epigram [+v dolio] by ChanServ 31/08 17:51 -!- mode/#epigram [+v dolio] by ChanServ 31/08 18:51 -!- mode/#epigram [+v pigworker] by ChanServ 31/08 20:48 -!- mode/#epigram [+v dolio] by ChanServ 31/08 21:51 -!- mode/#epigram [+v pigworker] by ChanServ 31/08 23:05