/home/laney/.irssi/irclogs/Freenode/2010/#epigram/August.log

--- Log opened Sun Aug 01 00:00:38 2010
pedagandSaizan, by any chance, do you know how Cabal sets the -hide-package option (in case of ambiguity)?01/08 00:11
pedagandfor example, I have mtl and monads-fd, I want to compile Epigram with mtl01/08 00:12
+SaizanCabal uses -hide-all-packages (or a similar name) and then gives -package $pkg for each $pkg in the build-depends01/08 00:12
pedagandha! 01/08 00:12
pedagandthanks!01/08 00:12
+Saizannp :)01/08 00:13
pedagandhehe, that's working. Thanks again, you saved my night ;-)01/08 00:30
pedagandthere 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
pedagandI would have expected 'cabal build' to call 'Setup.hs build', somehow01/08 00:37
pedagandwell, let's RTFM once more01/08 00:38
+Saizando you have a custom Setup.hs?01/08 00:39
+Saizanin that case you need build-type: Custom in the .cabal file01/08 00:39
+Saizanotherwise it uses the default code01/08 00:39
pedagandit's kind of custom, indeed. Let's try Custom (didn't saw that magic in the doc, tho)01/08 00:41
pedagandand that works! 01/08 00:41
pedagandvery glad to have you here :-)01/08 00:42
pedagandha, and it's in the doc actually. My bad.01/08 00:42
+Saizanit's a common gotcha, maybe the docs need some improvement..01/08 00:43
pedaganddunno, I'm an absolute beginner in ca(ni)balism, so I won't blame the docs tonight. Maybe tomorrow ;-)01/08 00:46
pedagandok, so 'cabal build' works. I'm scared of trying anything more interesting, such as 'cabal install' for instance...01/08 00:46
+Saizanit doesn't bite :)01/08 00:47
pedagandTada! "Installing executable(s) in /home/pierre/.cabal/bin"01/08 00:53
pedagandtyping "$ Pig" just works, and I still have my two arms, two legs, one head01/08 00:53
pedagandgoodo01/08 00:53
+Saizannice :)01/08 00:54
pedagandthat's rudimentary but that's a cabal package :-)01/08 00:54
pedagandyou say "nice" now, but when you see the connection cabal/Makefile, you'll cry :-)01/08 00:54
+Saizanugh01/08 00:54
+Saizanit might convince me to go back to work on build systems..01/08 00:55
pedagandwell, I would not have this cruelty01/08 00:59
pedagandnonetheless, that's an interesting (and far reaching) problem indeed01/08 01:00
+Saizanit's easy to find distractions anyway :)01/08 01:15
-!- mode/#epigram [+v dolio] by ChanServ01/08 04:06
-!- mode/#epigram [+v dolio] by ChanServ01/08 06:32
-!- mode/#epigram [+v pigworker] by ChanServ01/08 10:10
-!- mode/#epigram [+v soupdragon] by ChanServ01/08 10:37
-!- mode/#epigram [+v dolio] by ChanServ01/08 11:02
-!- mode/#epigram [+v dolio] by ChanServ01/08 13:02
-!- mode/#epigram [+v pigworker] by ChanServ01/08 13:24
-!- mode/#epigram [+v dolio] by ChanServ01/08 16:02
-!- mode/#epigram [+v pigworker] by ChanServ01/08 17:45
-!- mode/#epigram [+v dolio] by ChanServ01/08 20:06
-!- mode/#epigram [+v dolio] by ChanServ01/08 21:05
-!- mode/#epigram [+v soupdragon] by ChanServ01/08 21:50
-!- mode/#epigram [+v dolio] by ChanServ01/08 22:06
-!- mode/#epigram [+v dolio] by ChanServ01/08 23:05
-!- mode/#epigram [+v pigworker] by ChanServ01/08 23:40
--- Day changed Mon Aug 02 2010
-!- mode/#epigram [+v codolio] by ChanServ02/08 00:05
-!- mode/#epigram [+v pigworker] by ChanServ02/08 00:29
-!- mode/#epigram [+v pigworker] by ChanServ02/08 00:34
-!- mode/#epigram [+v dolio] by ChanServ02/08 01:05
-!- mode/#epigram [+v pigworker] by ChanServ02/08 01:47
-!- mode/#epigram [+v dolio] by ChanServ02/08 02:06
-!- mode/#epigram [+v pigworker] by ChanServ02/08 02:08
-!- mode/#epigram [+v dolio] by ChanServ02/08 04:02
-!- mode/#epigram [+v dolio] by ChanServ02/08 06:05
-!- mode/#epigram [+v pigworker] by ChanServ02/08 08:51
-!- mode/#epigram [+v dolio] by ChanServ02/08 09:05
-!- mode/#epigram [+v Saizan_] by ChanServ02/08 12:40
-!- Saizan_ is now known as Saizan02/08 12:40
-!- mode/#epigram [+v edwinb] by ChanServ02/08 12:42
-!- mode/#epigram [+v dolio] by ChanServ02/08 18:05
-!- mode/#epigram [+v dolio] by ChanServ02/08 20:02
-!- mode/#epigram [+v soupdragon] by ChanServ02/08 20:47
-!- mode/#epigram [+v codolio] by ChanServ02/08 21:05
-!- codolio is now known as dolio02/08 21:08
-!- mode/#epigram [+v pigworker] by ChanServ02/08 21:48
-!- copumpkin is now known as unsafePumpkin02/08 22:16
-!- unsafePumpkin is now known as copumpkin02/08 22:31
--- Day changed Tue Aug 03 2010
-!- mode/#epigram [+v dolio] by ChanServ03/08 01:33
-!- mode/#epigram [+v dolio] by ChanServ03/08 02:05
-!- mode/#epigram [+v codolio] by ChanServ03/08 04:54
-!- mode/#epigram [+v pigworker] by ChanServ03/08 09:43
-!- mode/#epigram [+v soupdragon] by ChanServ03/08 10:35
-!- codolio is now known as dolio03/08 11:28
-!- mode/#epigram [+v dolio] by ChanServ03/08 12:05
-!- mode/#epigram [+v dolio] by ChanServ03/08 13:01
-!- mode/#epigram [+v dolio] by ChanServ03/08 20:01
--- Day changed Wed Aug 04 2010
-!- mode/#epigram [+v dolio] by ChanServ04/08 03:05
-!- mode/#epigram [+v dolio] by ChanServ04/08 08:05
-!- mode/#epigram [+v soupdragon] by ChanServ04/08 10:40
-!- mode/#epigram [+v dolio] by ChanServ04/08 12:01
-!- mode/#epigram [+v soupdragon] by ChanServ04/08 13:37
-!- mode/#epigram [+v dolio] by ChanServ04/08 17:05
-!- mode/#epigram [+v dolio] by ChanServ04/08 18:01
-!- mode/#epigram [+v Saizan] by ChanServ04/08 18:38
-!- koninkje_away is now known as koninkje04/08 22:39
-!- mode/#epigram [+v dolio] by ChanServ04/08 23:04
--- Day changed Thu Aug 05 2010
Phantom_HooverFor some reason, compilation of Epigram 2 fails for me.05/08 00:09
Phantom_Hooverhttp://pastie.org/1076195 is the result of "make dep" in Pig09/src/05/08 00:10
+Saizanah, 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 will05/08 00:11
Phantom_HooverSo what do I do to fix it?05/08 00:12
pedagandyou can 'cabal build' instead of 'make'ing, I think05/08 00:13
+Saizanyeah, cabal configure first, or use "runhaskell Setup.hs" instead of cabal if you don't have the latter installed05/08 00:15
-!- mode/#epigram [+v dolio] by ChanServ05/08 03:04
-!- mode/#epigram [+v dolio] by ChanServ05/08 04:01
-!- koninkje is now known as koninkje_away05/08 04:28
-!- mode/#epigram [+v dolio] by ChanServ05/08 08:01
agundrypedagand: morning05/08 09:33
agundrywhat's going on with the cabal/make switchover?05/08 09:34
pedagandnothing is going on here :-) should there be anything going on?05/08 09:37
agundryyour latest patch seems to break make because some packages are omitted, is that intenational?05/08 09:38
pedagandkind of, yes. One should use "cabal ..." or "runhaskell Setup.hs ..." now05/08 09:38
agundryokay, but being a cabal novice, how can I can run the equivalent of "make dep" or "make profile"?05/08 09:40
agundrywe should probably also update the documentation05/08 09:40
pedagandif 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 be05/08 09:40
agundrymy plan was just not to pull your patch ;-) but I'd like to stay close to the main tree if possible05/08 09:41
pedagandas you wish05/08 09:41
agundryin other news, you've probably seen that I finally pushed my equation-smashing hammer in problem simplification05/08 09:44
agundrythis gets rid of all the "<= ship" nonsense, but seems to be rather slow05/08 09:45
pedagandwill see that when I'm back. As for now, farniente! :-)05/08 09:53
agundryfair enough05/08 09:54
pedagandall right, I've fixed the makefile, pushing in a few05/08 10:12
agundrythank you, sorry to interrupt the doing nothing!05/08 10:13
pedagandpushed my Lord05/08 10:19
agundryta05/08 10:20
-!- mode/#epigram [+v Saizan] by ChanServ05/08 10:48
-!- mode/#epigram [+v soupdragon] by ChanServ05/08 11:53
-!- copumpkin_ is now known as copumpkin05/08 13:17
-!- mode/#epigram [+v soupdragon] by ChanServ05/08 14:05
-!- mode/#epigram [+v dolio] by ChanServ05/08 18:05
-!- mode/#epigram [+v dolio] by ChanServ05/08 19:03
-!- mode/#epigram [+v codolio] by ChanServ05/08 20:04
-!- mode/#epigram [+v Saizan] by ChanServ05/08 20:40
-!- copumpkin is now known as Nu05/08 21:47
-!- Nu is now known as copumpkin05/08 21:47
-!- codolio is now known as dolio05/08 22:44
-!- koninkje_away is now known as koninkje05/08 23:14
--- Day changed Fri Aug 06 2010
-!- koninkje is now known as koninkje_away06/08 02:50
-!- mode/#epigram [+v dolio] by ChanServ06/08 03:04
-!- mode/#epigram [+v dolio] by ChanServ06/08 11:04
-!- mode/#epigram [+v soupdragon] by ChanServ06/08 13:07
-!- mode/#epigram [+v dolio] by ChanServ06/08 14:04
-!- mode/#epigram [+v dolio] by ChanServ06/08 15:04
-!- copumpkin_ is now known as copumpkin06/08 15:56
-!- mode/#epigram [+v dolio] by ChanServ06/08 20:00
-!- mode/#epigram [+v dolio] by ChanServ06/08 21:03
-!- mode/#epigram [+v dolio] by ChanServ06/08 22:04
-!- mode/#epigram [+v dolio] by ChanServ06/08 23:03
--- Day changed Sat Aug 07 2010
-!- mode/#epigram [+v dolio] by ChanServ07/08 05:53
-!- mode/#epigram [+v dolio] by ChanServ07/08 06:07
-!- mode/#epigram [+v dolio] by ChanServ07/08 06:21
-!- mode/#epigram [+v codolio] by ChanServ07/08 10:16
-!- mode/#epigram [+v dolio] by ChanServ07/08 11:18
-!- mode/#epigram [+v soupdragon] by ChanServ07/08 12:49
-!- mode/#epigram [+v dolio] by ChanServ07/08 13:21
-!- copumpkin_ is now known as copumpkin07/08 16:46
-!- mode/#epigram [+v dolio] by ChanServ07/08 21:21
-!- mode/#epigram [+v dolio] by ChanServ07/08 22:21
-!- mode/#epigram [+v dolio] by ChanServ07/08 23:17
--- Day changed Sun Aug 08 2010
-!- mode/#epigram [+v dolio] by ChanServ08/08 02:17
-!- mode/#epigram [+v dolio] by ChanServ08/08 02:47
-!- mode/#epigram [+v codolio] by ChanServ08/08 06:21
-!- codolio is now known as dolio08/08 07:22
-!- mode/#epigram [+v soupdragon] by ChanServ08/08 13:51
-!- mode/#epigram [+v pigworker] by ChanServ08/08 19:57
-!- mode/#epigram [+v pigworker] by ChanServ08/08 20:27
-!- mode/#epigram [+v pigworker] by ChanServ08/08 23:44
--- Day changed Mon Aug 09 2010
-!- mode/#epigram [+v dolio] by ChanServ09/08 04:20
-!- mode/#epigram [+v soupdragon] by ChanServ09/08 04:41
-!- mode/#epigram [+v dolio] by ChanServ09/08 05:17
-!- mode/#epigram [+v dolio] by ChanServ09/08 07:17
-!- mode/#epigram [+v pigworker] by ChanServ09/08 09:17
molerisagundry: You about?09/08 13:54
agundrymoleris: sorry, in the middle of a couple of talks; should be finished in just over an hour09/08 14:39
molerisagundry: no worries09/08 14:39
agundrymoleris: I'm back09/08 16:12
molerisagundry: Hey09/08 16:12
agundrywhat can I do you for?09/08 16:12
molerisJust wondering what I should be able to do with your new equality stuff09/08 16:13
molerisor how to make it go09/08 16:13
agundryhopefully, it should just be a case of not having to do things that were necessary before09/08 16:14
agundryif you look at Demo.pig, lots of explicit eliminations by ship have disappeared09/08 16:14
agundrythere is a new primitive substEq : (X : Set)(x : X)(y : X)(q : :- x == y)(P : X -> Set) -> P x -> P y09/08 16:15
agundryand when propositional simplification spots an equation with a variable on one side, it eliminates the variable by substEq09/08 16:16
molerisHmm09/08 16:16
molerisThis is what I thought - but earlier I had an equality in the context that was not substituted away09/08 16:18
moleristhe examples in Demo.pig work though09/08 16:18
agundry:s/propositional simplification/problem simplification09/08 16:18
agundryit's possible that it is missing some equations09/08 16:18
agundryI'm interested in examples that you think should disappear and do not09/08 16:19
molerisOK, I'll try and recreate09/08 16:19
molerisIn the meanwhile I've stopped the compiler segfaulting09/08 16:20
agundrygood09/08 16:20
agundrynow we need to stick it in the test suite so we notice if it breaks09/08 16:20
molerisThere's a problem with the operator references not being compiled properly though09/08 16:20
agundryhmm, amusingly enough I think the problem simplification only works with equations one way round (variables on the right)09/08 16:21
agundrythat needs fixing09/08 16:21
agundrywhat's wrong with operator references?09/08 16:21
molerisWhich way round do they have to be?09/08 16:24
molerisoh, var on the right09/08 16:24
molerissorry09/08 16:24
moleristhat would be the situation I find myself in09/08 16:24
agundryaha09/08 16:24
agundrysorry, I only did one case and planned to add the other once it was working09/08 16:25
agundrybut then forgot09/08 16:25
molerisrighto, I shan't worry too much then09/08 16:25
agundrygive me a few minutes to copy-paste and I can make an ugly version that works09/08 16:25
agundrybut this code really needs tidying up09/08 16:26
molerisa bit like the rest of the code, too, then09/08 16:26
agundryPropSimp.lhs is particularly horrible09/08 16:27
agundrywe need to figure out how to do everything without higher-order terms, and rewrite it to be nice09/08 16:27
molerisah yes09/08 16:28
molerisany idea on that?09/08 16:28
agundryI've not really looked at it, to be honest09/08 16:28
molerisfair enough09/08 16:28
agundryone possibility might be to add term representations of some things that are currently only stored as values09/08 16:29
agundryif I'm right in thinking that terms are now allowed in value lambdas09/08 16:29
moleristhey are09/08 16:31
moleristhe whole term/value distinction has been muddied09/08 16:31
agundryindeed09/08 16:32
agundryI think that it might be possible to produce the proof fragments required by propsimp as terms instead of values09/08 16:33
agundrythough we might just end up with horrible de Bruijn index mangling in place of the higher-order scopes09/08 16:33
molerishmm09/08 16:34
agundryah, the equation simplification fix is a bit more than I thought, because it requires symmetry to be a primitive09/08 16:44
agundryon a related note, I really want something that will give me Haskell code for an Epigram term that I've built09/08 16:45
molerisshould be reasonably straigh forward now we have FO-terms again09/08 16:47
moleris(ish)09/08 16:47
agundryyes09/08 16:49
moleriswhat is sym currently?09/08 16:51
agundryit's not built in, but various files define it manually09/08 16:52
agundrysym : :- ((X : Set)(x : X)(y : X) => x == y => y == x)09/08 16:53
agundrysym = \ X x y q -> refl (X -> Set) (\ y -> :- y == x) % x y q ! _09/08 16:53
molerisfair enough09/08 16:54
molerisI thought at one point it was an eliminator09/08 16:54
molerisprobably a long time ago09/08 16:54
agundryit may well have been once09/08 16:54
molerisright, I'm off09/08 16:56
molerismore Epigramming tomorrow09/08 16:56
agundryokay, bye for now09/08 16:56
molerischeers09/08 16:56
-!- larrytheliquid_ is now known as larrytheliquid09/08 19:25
-!- mode/#epigram [+v soupdragon] by ChanServ09/08 19:37
-!- mode/#epigram [+v dolio] by ChanServ09/08 20:20
-!- danten_ is now known as danten09/08 20:51
-!- mode/#epigram [+v dolio] by ChanServ09/08 21:20
-!- pumpkin is now known as copumpkin09/08 23:01
-!- shapr[ is now known as shapr09/08 23:10
-!- mode/#epigram [+v dolio] by ChanServ09/08 23:20
--- Day changed Tue Aug 10 2010
-!- mode/#epigram [+v dolio] by ChanServ10/08 00:20
-!- mode/#epigram [+v dolio] by ChanServ10/08 07:20
molerisagundry: Sadly, my example still only works if I turn my equations around ):10/08 12:57
agundryhmm, that's strange10/08 12:57
molerisoh, wait10/08 12:57
molerisignore that10/08 12:57
agundryis it working after all?10/08 12:58
molerisforgot to copy the replacement Pig into the right place10/08 12:59
molerissorry :$10/08 12:59
agundryno problem, glad to hear it is working10/08 12:59
agundrydoes your example do anything exciting?10/08 12:59
molerisno, just mucking about with the usual vector stuff10/08 13:00
moleristrying to get a data tactic for indexed families working too10/08 13:02
agundrythat would be very nice10/08 13:02
agundryI've been thinking about how to avoid switching on enumerations during problem simplification10/08 13:03
agundrywe need to generate induction principles with better methods (a tuple instead of a function from an enumeration)10/08 13:04
agundryI have done the construction in Epigram for Desc, but am not sure how to wire it up with the data tactic10/08 13:05
molerisI have plenty of stuff along those lines for the IDesc variant10/08 13:11
molerisI'm loathed to mess about too much with Desc, though10/08 13:12
agundrythat's fair enough10/08 13:12
agundrymostly I have been playing with Desc because I don't really understand IDesc10/08 13:12
moleris(:10/08 13:12
molerisI have a file somewhere with a `case' gadget for well-formed IDescs which you have to supply a tuple of methods10/08 13:13
moleristhat'll be what you want10/08 13:14
agundryyes, that's the sort of thing we need10/08 13:15
molerisinterestingly, I don't think that the system is clever enough to spot that a tuple of programming problems is a programming problem10/08 13:15
agundryit's not10/08 13:16
agundry(clever enough)10/08 13:17
agundrywhat kind of examples are you thinking of?10/08 13:18
molerisIt showed up while I was playing around with building the `case' and `rec' gadgets generically10/08 13:20
-!- mode/#epigram [+v soupdragon] by ChanServ10/08 16:26
molerisQuestion: is '->' not a keyword?10/08 16:39
molerisAh, 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 danten10/08 17:20
pedagandbecause 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 ChanServ10/08 18:16
-!- mode/#epigram [+v dolio] by ChanServ10/08 21:20
-!- mode/#epigram [+v dolio] by ChanServ10/08 22:19
-!- mode/#epigram [+v dolio] by ChanServ10/08 23:16
--- Day changed Wed Aug 11 2010
-!- mode/#epigram [+v dolio] by ChanServ11/08 00:16
-!- mode/#epigram [+v dolio] by ChanServ11/08 01:20
-!- mode/#epigram [+v dolio] by ChanServ11/08 02:16
-!- koninkje_away is now known as koninkje11/08 03:06
-!- mode/#epigram [+v dolio] by ChanServ11/08 03:19
-!- mode/#epigram [+v dolio] by ChanServ11/08 07:19
-!- koninkje is now known as koninkje_away11/08 09:13
pedagandagundry, will you be in the office this afternoon?11/08 12:06
-!- mode/#epigram [+v dolio] by ChanServ11/08 12:19
-!- danten_ is now known as danten11/08 12:40
agundrypedagand: yes, from now on11/08 12:44
pedagandall right. I've written some thought, I send that, eat and come at, say, 2pm.11/08 12:45
agundryokay, see you later on then11/08 12:46
molerispedagand, agundry: Plotting anything interesting?11/08 15:04
agundrymoleris: just thinking about how Epigram is going to take over the world, as usual11/08 15:06
agundrywe have been talking about how a high-level language might fit in11/08 15:07
agundrybut not in much detail as yet11/08 15:07
-!- mode/#epigram [+v dolio] by ChanServ11/08 15:19
pedagandyeah, 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 levels11/08 15:24
molerispedagand: That would be ideal11/08 15:29
-!- mode/#epigram [+v soupdragon] by ChanServ11/08 16:20
pedagandmoleris, ping?11/08 18:11
-!- mode/#epigram [+v dolio] by ChanServ11/08 18:19
pedagandping time-out, nevermind11/08 18:56
-!- mode/#epigram [+v dolio] by ChanServ11/08 20:16
-!- mode/#epigram [+v dolio] by ChanServ11/08 21:19
-!- mode/#epigram [+v dolio] by ChanServ11/08 22:16
--- Day changed Thu Aug 12 2010
-!- mode/#epigram [+v dolio] by ChanServ12/08 01:19
-!- mode/#epigram [+v dolio] by ChanServ12/08 02:19
-!- mode/#epigram [+v dolio] by ChanServ12/08 08:16
pedagandmoleris, 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 function12/08 11:22
pedagandwhat are the pro and cons?12/08 11:23
pedagandin 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
pedagandI don't think I really understand what you meant12/08 11:23
pedagandsurely, 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 language12/08 11:25
pedagandnot that I dislike this "inductive relation" presentation, but I'm curious to know the benefits/drawbacks12/08 11:27
molerisHmm, I'm not sure what I meant by that. I think that way about a lot of my thesis though :)#12/08 11:32
pedagand:-D12/08 11:33
pedagandbut is there a reason you gave this presentation back in the days and then we switched to the functional presentation?12/08 11:34
pedagandfor 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 stopper12/08 11:35
molerisis that true?12/08 11:38
moleris(necessarily)12/08 11:38
molerissorry, I'll answer your question properly in a moment - I'm just debugging some new Epigram at the same time12/08 11:39
pedagandsure, no problem12/08 11:39
pedagandthat'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
pedagandin Coq, I would abuse Prop to get my hand on the pieces without having a size explosion12/08 11:46
molerisAnd SPT is in Set1 because of the `->' constructor.. Hm12/08 11:48
pedagandyep12/08 11:49
molerisNot 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
molerisIn 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
molerisFor some reason I'm much more paranoid about bad recursive definitions than size issues.12/08 11:52
pedagandha! when you're dealing with the fix-point, right? 12/08 11:52
molerisAnd I wanted to keep the presentation of the universe as simple as possible12/08 11:52
molerisYeah, thats the one12/08 11:53
pedagandI forgot that guy, thanks. 12/08 11:53
molerisNot sure why I came up with some other weak excuse thoguh12/08 11:54
molerisI was young12/08 11:54
pedagand:-)12/08 11:54
moleriscaribou12/08 12:57
molerisoops. wrong window12/08 12:58
* moleris has good news12/08 13:29
molerismy latest patch allows one to write such things as:12/08 13:30
molerisidata Vec (A : Set) : Nat -> Set := (nil : Vec A 'zero) ; (cons : (n : Nat) -> A -> Vec A n -> Vec A ('succ n))12/08 13:30
molerisand have Epigram actually do something useful with it12/08 13:31
agundryvery nice12/08 13:31
molerisOnly for indexed families with a single index so far12/08 13:32
moleris(labels really need fixing before I attend to that shortcoming)12/08 13:32
molerisbut alpha testers are welcome to have a play12/08 13:33
pedagandgoodo12/08 13:33
agundrywhat problem are you having with labels?12/08 13:34
pedagandmoleris, are you aware (maybe you're at the origin of it) of the "universe of indexed labels"?12/08 13:35
pedagandI wasn't at pigweek, so I don't really know what was decided on that front12/08 13:35
molerisI had a conversation with pigworker on the subject of labels which went no where at the time12/08 13:36
molerisif there's a plan I'd be happy to hear about it12/08 13:37
agundryI'm not aware of such a plan12/08 13:39
pedagandwell, 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
pedagandagundry, I reckon you were here. But maybe you were working on something else12/08 13:39
agundryor possibly I've just forgotten...12/08 13:39
agundryWe talked about making a universe for programming problems12/08 13:40
pedagandwe also did that, but that was another day :-)12/08 13:40
molerisso many universes, it's hard to keep them all in ones brain12/08 13:41
pedagandanyway, it's not a turnkey solution, so I wouldn't be too hopeful now12/08 13:41
pedagandthat's why we need IIR with support for binding! Yeah!12/08 13:41
agundrySo what is the problem with the current labels setup as far as idata is concerned?12/08 13:42
agundryincidentally, I've got PropSimp to work with terms rather than values, though I still need to tidy up the code a bit12/08 13:44
molerisSo with plain ol' Mu, the label |Nat| stands for the whole of the canonical object |Mu NatD|12/08 13:45
molerisbut thats not the case with IMu, where the canonical values (for biderectional type checking purposes) include a particular index12/08 13:45
molerisyou want the label to be |Vec|, but that doesn't stand for |IMu Nat VecD n| 12/08 13:47
moleristhis causes me all sorts of problems12/08 13:47
molerisnot sure if that makes any sense12/08 13:47
molerisbut 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 good12/08 13:48
agundryI think we can pretty much get rid of them now if we want12/08 13:49
molerisTelescopes are still a blocker, but not a huge one12/08 13:49
agundryah true12/08 13:49
-!- mode/#epigram [+v soupdragon] by ChanServ12/08 13:50
agundrya quick grep suggests everything else should be fairly easy to convert to first-order12/08 13:50
molerisI might put that to the top of my in tray12/08 13:50
agundryI'm going to update Demo.pig to use idata, unless anyone is on that already?12/08 13:52
molerisgo for it12/08 13:55
agundrypedagand: ping12/08 15:32
pedagandpong12/08 15:32
agundryjust had a chat with Kirsty12/08 15:32
agundryit seems she never received your email about flights to Baltimore12/08 15:32
pedagandhaha12/08 15:33
agundrynot sure what happened there12/08 15:33
agundryI'm going to forward it and hope it gets through this time...12/08 15:33
pedagandthanks for that12/08 15:34
molerishmm12/08 15:40
molerisI need me some of those12/08 15:40
pedagandif 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
pedagandmoleris, 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
pedagandI will send it out on the mailing list when I'm confident enough that my translation is not complete bullshit12/08 16:03
moleristhey're the main 3 aren't they12/08 16:04
pedagandthey are just indexed by Nat, that's too easy :-)12/08 16:04
molerisI'm not sure I like your negativity about my demo12/08 16:05
molerisI need your help here (:12/08 16:06
moleristalking of travel though - are you guys going to come down to AIM in Nottingham?12/08 16:06
agundrywe haven't thought about it, at least I haven't12/08 16:08
agundryit's in early September, isn't it?12/08 16:08
pedagand1st to 7th, yes12/08 16:09
moleris1st to the 7th12/08 16:09
pedagandI didn't plan to go, personally12/08 16:10
molerisShame, will be fun hopefully12/08 16:11
pedagandbut maybe pigworker will give orders when he is back12/08 16:11
molerispedagand: what about:12/08 16:15
molerisdata Id (A : Set) (a : A) : A -> Set := (refl : Id A a a)12/08 16:15
pedagandthat's awful. Perfect, thanks.12/08 16:16
-!- mode/#epigram [+v dolio] by ChanServ12/08 16:20
pedagandmoleris, I've sent the agda definition on -dev12/08 16:53
-!- mode/#epigram [+v soupdragon] by ChanServ12/08 20:39
-!- mode/#epigram [+v dolio] by ChanServ12/08 22:41
-!- mode/#epigram [+v dolio] by ChanServ12/08 22:41
--- Day changed Fri Aug 13 2010
-!- koninkje_away is now known as koninkje13/08 01:48
-!- mode/#epigram [+v dolio] by ChanServ13/08 03:28
-!- mode/#epigram [+v dolio] by ChanServ13/08 05:15
-!- mode/#epigram [+v soupdragon] by ChanServ13/08 06:01
-!- mode/#epigram [+v dolio] by ChanServ13/08 06:17
-!- koninkje is now known as koninkje_away13/08 06:56
-!- mode/#epigram [+v Saizan] by ChanServ13/08 10:18
-!- moleris_ is now known as moleris13/08 10:58
molerispedagand: Your email client mangled the unicode in ILabel.agda ))): (Sent in the right channel now)13/08 11:10
pedaganddamned email client13/08 11:20
molerisstuck in the dark ages13/08 11:21
pedagandit'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
pedagandanyway, what if I push the agda code in the repos, in ./models? is that ok?13/08 11:23
pedagand(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
pedagand(I will get in touch with Al Gore, maybe we could make a convincing movie)13/08 11:25
pedagandactually, 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
pedaganddone13/08 11:31
molerisHmm, I triple checked the attachment before I accused you - I think Thunderbird is lying to you13/08 11:35
molerisI stop using thunderbird for pretty much this exact reason, btw (:13/08 11:35
moleriss/stop/stopped13/08 11:36
molerisBut thanks for putting it in the repo13/08 11:36
pedagandwhat are you using now?13/08 11:37
molerismutt13/08 11:38
-!- mode/#epigram [+v dolio] by ChanServ13/08 13:15
molerispedagand: It's a good start - but there's something I'm not getting13/08 13:23
molerisI need more think13/08 13:23
molerisin otherwords, don't worry about implementing it13/08 13:23
pedaganddid you received the picture too? does that help?13/08 13:25
molerisI got it13/08 13:27
molerisYour Agda rendering seems reasonable though13/08 13:27
molerisI think I'm worrying about scoping these labels13/08 13:27
molerisbut my brain freezes everytime I try and think about it13/08 13:28
moleris(scoping, that is)13/08 13:28
pedagandwhat do you mean by "scoping the labels"?13/08 13:28
molerisWell exactly (:13/08 13:29
pedagandha, I see :-)13/08 13:29
molerisNo really, if they are just UIds they don't fit with the module/parameter structure very well13/08 13:30
molerisso maybe they aren't UIds13/08 13:35
pedagandI see. Just stick a Name instead of an UId then?13/08 13:37
pedagandso that you can use the NameResolution machinery to disambiguate it for you13/08 13:37
molerismaybe13/08 13:38
molerisand have the type as a top level thing too13/08 13:39
molerisdunno13/08 13:39
molerisI think I might be missing the point13/08 13:42
pedagand(I'm going to the lab, see you later)13/08 13:43
+Saizan(labels are for speeding up equality tests?)13/08 14:04
pedagandmoleris,  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
agundrySaizan: they are mainly for tracking human-readable names of data types built with Mu/IMu13/08 14:10
agundryspeeding up equality checking is a useful extra13/08 14:10
+Saizanagundry: oh, right, humans :)13/08 14:17
agundryI don't think we have really figured out how the high-level language namespace should be managed13/08 14:20
agundrythis goes for both programming problems and data type labels13/08 14:22
agundryat the moment we have hacked things up on top of the ProofState namespace13/08 14:23
agundrybut maybe we should think about something more principled13/08 14:23
molerispedagand: Labels (currently) are FAKE references, with long names and global types 13/08 14:23
pedagandha! that's true, my bad.13/08 14:25
-!- mode/#epigram [+v soupdragon] by ChanServ13/08 16:41
-!- mode/#epigram [+v dolio] by ChanServ13/08 17:18
-!- pumpkin is now known as copumpkin13/08 17:54
-!- mode/#epigram [+v dolio] by ChanServ13/08 21:17
--- Day changed Sat Aug 14 2010
-!- mode/#epigram [+v dolio] by ChanServ14/08 01:18
-!- mode/#epigram [+v dolio] by ChanServ14/08 02:18
-!- mode/#epigram [+v dolio] by ChanServ14/08 04:15
-!- mode/#epigram [+v dolio] by ChanServ14/08 06:18
-!- mode/#epigram [+v dolio] by ChanServ14/08 08:15
-!- mode/#epigram [+v codolio] by ChanServ14/08 09:18
-!- mode/#epigram [+v dolio] by ChanServ14/08 10:18
-!- mode/#epigram [+v soupdragon] by ChanServ14/08 10:28
-!- mode/#epigram [+v edwinb] by ChanServ14/08 14:42
-!- mode/#epigram [+v dolio] by ChanServ14/08 18:18
-!- mode/#epigram [+v soupdragon] by ChanServ14/08 19:35
-!- mode/#epigram [+v dolio] by ChanServ14/08 22:14
* Taral waves.14/08 23:02
TaralAnyone home?14/08 23:02
* Saizan waves back14/08 23:02
TaralI think I'm going slowly stir-crazy.14/08 23:02
* copumpkin grunts14/08 23:02
TaralToo much new stuff. :P14/08 23:02
TaralOTT, and this new descriptions thing...14/08 23:03
+Saizanthey seem fun at least :)14/08 23:03
TaralDo you need to hard code observational equality for type-checking? I can't work it out from the code...14/08 23:03
TaralI'm trying to produce a "dependent core", essentially purely a type checker.14/08 23:04
TaralIdeally, it's a core small enough for a human to verify.14/08 23:04
TaralW-types were disappointing, but descriptions look promising.14/08 23:04
copumpkinde bruijn would be proud14/08 23:05
TaralHeh.14/08 23:05
+Saizani've an agda model with descriptions and OTT, which defines equality for all the description-generated datatypes14/08 23:05
TaralHm, I guess you have to have that, at least.14/08 23:05
TaralBut == can be generic over descriptions.14/08 23:05
+Saizanhttp://code.haskell.org/~Saizan/bisim/ObsEq.agda <- IDescTT is taken from the Pig09 repo14/08 23:06
TaralCould you encode generic == as a description itself?14/08 23:06
+Saizani think so14/08 23:07
TaralIs it useful? Since my type checker has to appeal to equality to start with...14/08 23:09
TaralOr does it?14/08 23:09
TaralArg... I wish I understood this stuff better. :(14/08 23:09
TaralI will say the Epitome has been useful.14/08 23:09
+Saizanthough i use a different IDesc there, which gives me the codes for the domains of sigma and pi14/08 23:09
+Saizanbut i guess from within the language it's fine to just use the primitive == for those.14/08 23:10
+SaizanObsEq is a deeper embedding than IDescTT14/08 23:11
+SaizanTaral: seen the blog, btw?14/08 23:11
TaralI read the blog.14/08 23:12
TaralThere's a lot there...14/08 23:12
TaralWhat does "deeper embedding" mean?14/08 23:14
+Saizanwell, i mean that i've represented more things using a "code" like Pi and Sigma rather than simply using Agda's ones14/08 23:15
TaralAh.14/08 23:15
TaralWell, if one doesn't assume that the underlying language has these things... (e.g. C)14/08 23:15
+Saizanyeah, 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
Taral*nod*14/08 23:19
-!- mode/#epigram [+v dolio] by ChanServ14/08 23:19
Taralok, I found it.14/08 23:25
TaralPig uses a definitional equality separate from observational equality to feed the type checker.14/08 23:25
TaralHence the need for an explicit coercion operator.14/08 23:25
TaralGot it!14/08 23:25
+Saizanah, 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 language14/08 23:27
--- Day changed Sun Aug 15 2010
-!- mode/#epigram [+v dolio] by ChanServ15/08 00:15
TaralIt 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
TaralOh, I see. An artifact of the functional representation of closures.15/08 01:21
+soupdragonhave you read the paper15/08 01:29
+soupdragonI am not a number I am a free variable15/08 01:29
TaralNo, I don't think I've read that one.15/08 01:33
TaralInteresting.15/08 01:34
TaralSo part of the quotation process is to replace functional closures with deBruijn indices.15/08 01:35
+dolioAre we talking about the Scope stuff?15/08 01:35
+dolioBecause I thought they got rid of functional closures.15/08 01:36
TaralNot in the Epitome that I'm reading.15/08 01:36
TaralIt's possible that it needs regenerating.15/08 01:36
+dolioHow old is it?15/08 01:36
Taral2010/08/1315/08 01:36
+dolioThen again, I don't know if they changed the description.15/08 01:36
TaralThe HF constructor is still present15/08 01:36
TaralAlthough there's a comment in heere...15/08 01:37
+dolioYes, but it's no longer a higher-order function.15/08 01:37
TaralHF :: String ! (VAL ! Tm {In, VV} x ) ! Scope p {-VV -} x15/08 01:37
Taraler, ! is ->15/08 01:37
TaralLooks higher-order to me.15/08 01:37
TaralConor has a comment: I’min themiddle ofmessing this bit about. The plan is tomake scopes syntactic again,15/08 01:37
Taralbut also to ensure that values can be embedded in terms. Step one is to whistle innocently and15/08 01:37
Taralallow both syntactic and functional scopes in both places.15/08 01:37
+dolioOh, I'm wrong.15/08 01:38
Taral:)15/08 01:38
+dolioI guess they haven't completely eliminated it yet.15/08 01:38
TaralIt's quite brain-bending for m.e15/08 01:38
+dolioIt's kind of a shame, because the higher-order stuff is so easy when you can use it.15/08 01:38
+dolioBut I guess it's got performance problems.15/08 01:39
TaralHonestly, programming with de Bruijn indices is a lot like programming a stack-based language like Forth.15/08 01:39
TaralNot too hard once you bend your brain around it.15/08 01:40
+dolioUsing the right higher-order representation has more advantages than just being able to use names.15/08 01:40
TaralAs per the HOAS papers?15/08 01:41
+dolioI quite like parametric HOAS. I rewrote an interpreter I have to use it not too long ago.15/08 01:41
TaralGiven 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
TaralYes, PHOAS is lovely.15/08 01:41
TaralI wouldn't be surprised if it had negative impact on performance, though.15/08 01:41
+dolioIt 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
+dolioYes, no doubt.15/08 01:42
Taralok, dinner soon. Talk to you all later.15/08 01:42
+dolioFor instance, I was able to write a Show instance that produces valid Haskell source for my terms. :)15/08 01:43
Taralo.O nice15/08 01:43
+dolioLambdas and all.15/08 01:43
+dolioOf course, that wouldn't be at all surprising if it weren't higher-order.15/08 01:44
Taral:)15/08 01:47
Taralttyl :D15/08 01:47
-!- mode/#epigram [+v dolio] by ChanServ15/08 02:15
-!- mode/#epigram [+v dolio] by ChanServ15/08 03:18
Taralwhen did the levitation paper get the set-stratification added?15/08 06:36
+dolioWhen they were revising the paper due to comments from reviewers, I think.15/08 06:42
TaralBother, now I have to print a new copy.15/08 06:54
Taral:P15/08 06:54
TaralAlthough it makes the need for switchD/switchID much clearer.15/08 06:54
TaralSo who came up with extending descriptions with a nu operator for coinduction?15/08 06:58
+dolioIt's a pretty straight-forward idea, isn't it?15/08 06:58
TaralYeah, but I'm willing to bet there's a catch.15/08 06:58
TaralCoinduction is never straightforward in my experience.15/08 06:59
+dolioThe descriptions don't actually have internal mu and nu yet anyway, though.15/08 06:59
TaralHm.15/08 06:59
+dolioI don't think coinduction is that hard, either, except people have been messing up the interface for it.15/08 07:01
+dolioAgda and Coq implement something that isn't exactly categorical coinduction with their productivity checkers, for instance.15/08 07:03
TaralHmm...15/08 07:04
TaralI always associated coinduction with laziness.15/08 07:04
TaralIt's technically just the result of taking the greatest fixpoint of an endofunctor, yes?15/08 07:04
+dolioFor instance, in Agda, you can get away with a single coinductive datatype.15/08 07:04
+dolio'codata Delay (A : Set) : Set where d : A -> Delay A'15/08 07:05
+dolioYes.15/08 07:05
TaralI see.15/08 07:05
+dolioBut it makes no sense for you to be able to use that for all coinduction.15/08 07:05
+dolioDelay is just the identity functor.15/08 07:05
+dolioBut it doesn't work that way.15/08 07:06
TaralThe fixpoints of identity are... oh.15/08 07:06
TaralNot exactly categorical coinduction.15/08 07:06
+dolioBecause 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
Taral*nod*15/08 07:07
TaralAs will coq's.15/08 07:07
+dolioYeah.15/08 07:07
TaralBecause that's "good enough".15/08 07:07
TaralAnd it appeals to the idea of coinduction as "selectively lazy evaluation"15/08 07:08
+dolioAnd Coq also has the weirdness of values of a coinductive type being/evaluating to constructors of said type.15/08 07:08
TaralWhich mixes up evaluation semantics and categories.15/08 07:08
+dolioWhich isn't really justified by the underlying theory.15/08 07:08
TaralCoq is very hacky in various ways. Which is why I'm looking so hard at epigram.15/08 07:09
+dolioAgda used to have that, too, of course.15/08 07:09
Taralbrb - getting drink15/08 07:09
Taralback15/08 07:10
+dolioCharity 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
+dolioAlthough, being directly category-theory-based, you'd expect it to be right.15/08 07:11
TaralI'm not entirely clear on what's required to get it right.15/08 07:11
TaralObviously "lazy evaluation" is only one piece of the puzzle.15/08 07:11
+dolioIntroduction via unfold, elimination via single-step observations.15/08 07:12
+dolioOf 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
Taral*nod*15/08 07:12
TaralAlways a catch... :)15/08 07:12
-!- mode/#epigram [+v dolio] by ChanServ15/08 07:14
Taraloh!15/08 07:19
TaralIntroduction via coind, elimination via cocon. Ahaha.15/08 07:19
TaralOf course.15/08 07:19
+dolioRight.15/08 07:20
TaralSorry, real coinduction always makes me think. Gotta remember it's purely dual to induction.15/08 07:20
+dolioAnd as far as equality is concerned, proof by coinduction should get you some kind of bisimulation.15/08 07:25
+dolioBut that doesn't gel well with intensional equality.15/08 07:25
+dolioOr maybe we just haven't figured out how it fits in well with dependent types yet.15/08 07:26
+dolioI 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
+dolioAnd 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
+dolioBecause they're not built exactly the same.15/08 07:29
-!- mode/#epigram [+v soupdragon] by ChanServ15/08 07:32
TaralDidn't I see something about that on the blog?15/08 07:47
TaralYes, I did: http://www.e-pig.org/epilogue/?p=41815/08 07:47
Taral"Or, in other words, it works."15/08 07:48
TaralSaizan 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.agda15/08 07:48
+SaizanTaral: that file i linked is doing the same thing as that blog post but using descriptions instead of Cont15/08 07:57
TaralYes, I noticed the parallels.15/08 07:57
TaralStill over my head for now.15/08 07:57
TaralNice to know that, when I need it, it will be there.15/08 07:57
Taralnini15/08 08:30
-!- mode/#epigram [+v soupdragon] by ChanServ15/08 09:08
-!- mode/#epigram [+v dolio] by ChanServ15/08 09:18
pedagandfrom Evidences.Tm: "[...] neutral application of a fake reference --- a definition whose hysterectomy stops it computing"15/08 10:52
pedagandI had to look up a dictionary15/08 10:52
pedagandneedless to say, that didn't really helped...15/08 10:52
+Saizan"\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 compute15/08 11:07
pedagandthanks, Doctor :-)15/08 11:08
pedagandmoleris, 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
pedagandit's not really important nor urgent, just fyi.15/08 11:43
-!- mode/#epigram [+v dolio] by ChanServ15/08 13:14
-!- mode/#epigram [+v dolio] by ChanServ15/08 14:14
-!- mode/#epigram [+v dolio] by ChanServ15/08 17:17
-!- mode/#epigram [+v dolio] by ChanServ15/08 19:18
-!- pumpkin is now known as copumpkin15/08 19:37
-!- mode/#epigram [+v soupdragon] by ChanServ15/08 20:31
-!- pumpkin is now known as copumpkin15/08 23:58
--- Day changed Mon Aug 16 2010
-!- mode/#epigram [+v dolio] by ChanServ16/08 03:17
-!- mode/#epigram [+v dolio] by ChanServ16/08 08:17
-!- mode/#epigram [+v dolio] by ChanServ16/08 10:14
-!- mode/#epigram [+v dolio] by ChanServ16/08 12:18
-!- mode/#epigram [+v soupdragon] by ChanServ16/08 12:27
molerispedagand: upload should work now16/08 13:17
-!- mode/#epigram [+v dolio] by ChanServ16/08 17:14
pedagandmoleris, thanks. I've fixed the post, at last.16/08 19:05
-!- mode/#epigram [+v dolio] by ChanServ16/08 20:14
-!- mode/#epigram [+v dolio] by ChanServ16/08 21:14
-!- mode/#epigram [+v dolio] by ChanServ16/08 23:33
--- Day changed Tue Aug 17 2010
-!- mode/#epigram [+v dolio] by ChanServ17/08 01:17
-!- mode/#epigram [+v dolio] by ChanServ17/08 02:14
Taralok, I have a new problem.17/08 04:17
TaralWhat is the type of % (out)?17/08 04:17
Taralit doesn't actually seem to have an expressible type. :/17/08 04:18
-!- mode/#epigram [+v soupdragon] by ChanServ17/08 04:26
Taralhm, apparently it can't have an expressible type. :(17/08 04:27
TaralIs it necessary? Can I hack it up with "ind"?17/08 04:27
TaralI think so...17/08 04:27
TaralOh! I think it can have a type...17/08 04:28
TaralJust have to have a proper constructor?17/08 04:28
Taral... noep.17/08 04:35
Taral*nope17/08 04:35
Taralok.17/08 04:35
-!- mode/#epigram [+v dolio] by ChanServ17/08 07:17
-!- mode/#epigram [+v codolio] by ChanServ17/08 11:17
molerismount17/08 13:50
-!- mode/#epigram [+v dolio] by ChanServ17/08 14:14
-!- copumpkin is now known as snowboard17/08 14:58
-!- snowboard is now known as copumpkin17/08 15:00
-!- mode/#epigram [+v dolio] by ChanServ17/08 15:17
-!- mode/#epigram [+v codolio] by ChanServ17/08 16:17
-!- codolio is now known as dolio17/08 17:27
-!- mode/#epigram [+v dolio] by ChanServ17/08 20:17
-!- mode/#epigram [+v dolio] by ChanServ17/08 22:13
--- Day changed Wed Aug 18 2010
-!- mode/#epigram [+v dolio] by ChanServ18/08 00:17
-!- mode/#epigram [+v soupdragon] by ChanServ18/08 01:10
-!- mode/#epigram [+v dolio] by ChanServ18/08 04:14
-!- koninkje_away is now known as koninkje18/08 05:08
-!- mode/#epigram [+v dolio] by ChanServ18/08 07:17
-!- koninkje is now known as koninkje_away18/08 08:05
-!- mode/#epigram [+v dolio] by ChanServ18/08 10:17
-!- mode/#epigram [+v dolio] by ChanServ18/08 12:13
-!- mode/#epigram [+v soupdragon] by ChanServ18/08 12:24
-!- mode/#epigram [+v codolio] by ChanServ18/08 13:17
-!- mode/#epigram [+v pigworker] by ChanServ18/08 13:46
-!- mode/#epigram [+v pigworker_] by ChanServ18/08 17:03
-!- pigworker_ is now known as pigworker18/08 17:03
-!- mode/#epigram [+v dolio] by ChanServ18/08 17:17
dantenHello 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.org18/08 18:01
-!- mode/#epigram [+v soupdragon] by ChanServ18/08 21:06
-!- mode/#epigram [+v dolio] by ChanServ18/08 21:17
--- Day changed Thu Aug 19 2010
-!- mode/#epigram [+v soupdragon] by ChanServ19/08 03:47
-!- ServerMode/#epigram [+vvvv edwinb dolio soupdragon codolio] by holmes.freenode.net19/08 10:19
-!- ServerMode/#epigram [+v Saizan] by holmes.freenode.net19/08 10:19
-!- ServerMode/#epigram [+vvv codolio soupdragon edwinb] by holmes.freenode.net19/08 10:35
-!- mode/#epigram [+v Saizan] by ChanServ19/08 11:12
molerisdanten: If you really want Epigram1 I've got the old binaries19/08 11:54
dantenI just want to test it some :)19/08 11:54
molerishttp://www.cs.nott.ac.uk/~pwm/epigram1-linux.tar.gz19/08 11:54
dantenthanks19/08 11:54
molerishttp://www.cs.nott.ac.uk/~pwm/epigram1-windows.zip19/08 11:55
molerisyou'll need xemacs19/08 11:55
dantenok19/08 11:56
-!- mode/#epigram [+v dolio] by ChanServ19/08 13:17
-!- mode/#epigram [+v soupdragon] by ChanServ19/08 16:35
-!- mode/#epigram [+v dolio] by ChanServ19/08 19:22
-!- mode/#epigram [+v dolio] by ChanServ19/08 22:21
-!- mode/#epigram [+v dolio] by ChanServ19/08 23:13
-!- koninkje_away is now known as koninkje19/08 23:29
--- Day changed Fri Aug 20 2010
-!- pumpkin is now known as copumpkin20/08 00:00
-!- mode/#epigram [+v dolio] by ChanServ20/08 01:13
-!- mode/#epigram [+v soupdragon] by ChanServ20/08 06:00
-!- koninkje is now known as koninkje_away20/08 09:47
-!- mode/#epigram [+v dolio] by ChanServ20/08 12:12
-!- mode/#epigram [+v soupdragon] by ChanServ20/08 14:54
roconnoron 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
agundryroconnor: yes, it should20/08 15:47
agundryin fact, maybe I should just fix that typo20/08 15:47
agundrydone20/08 15:50
roconnorah, 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 ChanServ20/08 18:57
-!- mode/#epigram [+v dolio] by ChanServ20/08 19:16
-!- mode/#epigram [+v dolio] by ChanServ20/08 20:12
-!- mode/#epigram [+v dolio] by ChanServ20/08 22:12
-!- mode/#epigram [+v dolio] by ChanServ20/08 23:16
--- Day changed Sat Aug 21 2010
-!- mode/#epigram [+v dolio] by ChanServ21/08 00:16
-!- mode/#epigram [+v soupdragon] by ChanServ21/08 05:35
-!- mode/#epigram [+v dolio] by ChanServ21/08 07:15
-!- mode/#epigram [+v dolio] by ChanServ21/08 16:16
-!- mode/#epigram [+v dolio] by ChanServ21/08 17:15
-!- mode/#epigram [+v dolio] by ChanServ21/08 20:12
-!- mode/#epigram [+v dolio] by ChanServ21/08 23:16
--- Day changed Sun Aug 22 2010
-!- mode/#epigram [+v dolio] by ChanServ22/08 02:12
-!- mode/#epigram [+v codolio] by ChanServ22/08 08:15
-!- mode/#epigram [+v soupdragon] by ChanServ22/08 09:24
-!- codolio is now known as dolio22/08 10:30
-!- mode/#epigram [+v dolio] by ChanServ22/08 13:15
-!- soupdragon is now known as Grass-Mud-Horse22/08 13:34
-!- mode/#epigram [+v dolio] by ChanServ22/08 17:15
-!- mode/#epigram [+v Grass-Mud-Horse] by ChanServ22/08 17:36
-!- mode/#epigram [+v dolio] by ChanServ22/08 20:15
-!- mode/#epigram [+v dolio] by ChanServ22/08 21:12
-!- koninkje_away is now known as koninkje22/08 23:26
--- Day changed Mon Aug 23 2010
-!- mode/#epigram [+v dolio] by ChanServ23/08 00:15
-!- mode/#epigram [+v dolio] by ChanServ23/08 02:15
-!- mode/#epigram [+v dolio] by ChanServ23/08 04:15
-!- koninkje is now known as koninkje_away23/08 05:14
-!- mode/#epigram [+v dolio] by ChanServ23/08 09:15
-!- mode/#epigram [+v Grass-Mud-Horse] by ChanServ23/08 09:55
-!- mode/#epigram [+v Saizan] by ChanServ23/08 11:13
-!- mode/#epigram [+v codolio] by ChanServ23/08 11:15
-!- mode/#epigram [+v Saizan] by ChanServ23/08 11:32
molerispedagand: hola23/08 11:43
pedagandhello23/08 11:45
pedagandwhat's up?23/08 11:45
molerisJust thought I'd reply here to at least one of your emails23/08 11:45
molerisWould be good to do some Epigram while you are around next week23/08 11:46
moleristhough what we can usefully do is up for debate23/08 11:46
pedagandall right! Do you want to give the demo with Cochon or a more "high-level" system?23/08 11:47
molerisI was hoping to do as much as possible without really talking about the proofstate as such23/08 11:50
moleriswhether thats a case of using cochon's `programming' tactics, or something else, I do not know23/08 11:50
pedagandyeah, the problem is "time". I don't know how much we can do before ICFP23/08 11:52
pedagandI've been experimenting with various high-level interfaces (that is, dropping Cochon out of the way)23/08 11:53
pedagandthe elaboration problem is not too hard, but distillation (from proofstate to the high-level system) is quite fiddly23/08 11:53
pedagandanother angle of attack would be to try implementing a serious demo and get it to work as we go 23/08 11:55
pedagandwe probably will need to implement the "with" gadget on our way there23/08 11:55
molerisshouldn't be a massive problem that, really (with)23/08 11:56
pedagand(also, improve our induction principles, and remove the sigma-splitting madness, something we've discussed on Friday here)23/08 11:57
molerisoh, cool23/08 11:57
molerisimprove ind how?23/08 11:57
pedagandyeah, I hope so23/08 11:57
pedagandright 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 splitting23/08 11:59
pedagandbecause Enum splitting triggers everywhere, not just when you're in a Description. That's annoying (and incorrect).23/08 11:59
molerisindeed, eliminating a list of bools and getting two cons cases is just odd :)23/08 12:00
pedagandexactly :-)23/08 12:01
-!- mode/#epigram [+v Saizan] by ChanServ23/08 12:03
pedagandso, 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
pedagandI suspect, starting from basic stuffs, going crazy on stuff that only us can do, such as OTTism, Desc-ism, etc.23/08 12:04
molerisIndeed23/08 12:05
molerisI'd like to show pigworkers FreeIMonad stuff from FitA Standard Chartered if possible23/08 12:06
molerisI plan to write that feature file this week23/08 12:06
pedagand"FitA Standard Chartered"?23/08 12:06
pedagandwhat's this?23/08 12:07
molerishmm, actually that was a she talk wasn't it23/08 12:07
pedagandoh, I understand23/08 12:07
molerisignore me23/08 12:07
pedagandsorry, got confused by the acronym23/08 12:07
pedagandwhy do you want to implement it as a Feature? You plan to use the simplification rules?23/08 12:08
molerisYeah, that would be good :) 23/08 12:10
pedagandI see, that would be good indeed23/08 12:11
molerisShame that your talk is after the demo - but still23/08 12:12
molerisgoing to grab something to eat - chat in a bit23/08 12:12
pedagandsee ya23/08 12:12
molerisQ: Whats the status of the implicit syntax mechanism and the spotting of recursive calls?23/08 15:45
pedagandI think it just works, isn't it?23/08 15:57
pedagandfor example, in List.pig23/08 15:58
pedagandyou do your recursive call, the machinery tries to find the corresponding programming problem in the context23/08 15:59
molerisHmm, 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 context23/08 16:07
pedagandha, this is a bug then, no?23/08 16:18
molerisI guess so23/08 16:19
pedagandis the programming problem mentioning the implicit argument?23/08 16:19
pedagandprobably, it should (even if not displaying it in Cochon)23/08 16:20
molerisIt doesn't, but I think that's ok23/08 16:23
pedagandha? then I don't see how to fix the bug, you have an idea?23/08 16:24
moleriswell, the thing we want to use currently has this type:23/08 16:28
molerisxf : ((a : A) -> < snoc^1 A xf^1 a : List A >)23/08 16:28
moleriswhere A is fixed by the sub-list (xf^1 : List A) - so I don't see how we do anything else23/08 16:29
molerisbut then I don't know the code in question well enough to suggest another path forward23/08 16:29
pedagandin these examples, you add defined snoc with {A : Set}, right?23/08 16:40
pedagandnevermind, I'll try defining it on my side and see if I can have a clue23/08 16:42
-!- codolio is now known as dolio23/08 17:11
molerisany luck?23/08 17:37
-!- mode/#epigram [+v codolio] by ChanServ23/08 20:15
--- Day changed Tue Aug 24 2010
-!- codolio is now known as dolio24/08 00:45
-!- pumpkin is now known as copumpkin24/08 06:30
-!- xa is now known as xarch24/08 09:39
xarchhi24/08 09:40
+Saizanhi24/08 09:41
pedagandmoleris, so, I took snoc in List.pig, replace (A : Set) by {A : Set}, replace the recursive call "snoc A ..." by "snoc ..." and it just works24/08 09:57
pedagandso, I guess, I don't understand the point you raised yesterday...24/08 09:57
pedagandxarch, 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
pedagandlooks like I won't make career as a doorman, or the nightclub will be empty :-(24/08 10:20
xarchoops, sorry24/08 10:25
xarchso, how do you want me to prove I'm human ? 24/08 10:25
pedagandkind of, you just did, isn't it? :-)24/08 10:27
pedagandhere you go, "approved" human being :-)24/08 10:28
xarchthanks :)24/08 10:28
molerispedagand: Really? What do you mean by 'just works'?24/08 10:29
pedagandmoleris, it is accepted and there is no subgoal left24/08 10:29
pedagandwait a sec, I copy it on pastebin24/08 10:30
pedagandhttp://pastebin.com/L4cen0My24/08 10:31
pedagandand if I do "prev" or "next", there is no subgoal24/08 10:31
molerisLet me just check this without my unrecorded changes to the tree24/08 10:36
pedagand(go to go (to work), will be back soon)24/08 10:46
molerispedagand: I agree that it works now (:24/08 11:41
pedagandall right, perfect then. Was it not-working because of your local change?24/08 11:42
molerisI don't think so, it's possible that agundry fixed it24/08 11:42
moleristhere were some patches I had to leave on the server because of my changes conflicting with them24/08 11:43
pedagandoh, you were on a old tree. Then, yes, that's likely24/08 11:43
molerisnot that old, a few days24/08 11:43
molerisanyway, I'm happy it works24/08 11:44
molerisI'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 way24/08 11:45
molerisusing agundry's 'haskell' tactic to write a kind of data prelude24/08 11:47
molerismeans you can turn off that Enum simplification and still write programs24/08 11:47
xarchwhy does Epigram use its own parser combinators library instead of, for example, Parsec ?24/08 12:03
pedagandxarch, 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
pedagandmoleris, 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
pedagandI think, what you did was what Adam initially suggested. What pigworker wanted was to generate this principle directly inside Epigram24/08 12:30
pedaganddo you think it would be difficult to follow the suggestion of our Supreme Leader?24/08 12:34
xarchso if i rewrote Parsley so that it uses Parsec, my patch would be accepted ?24/08 12:37
xarch*rewrite24/08 12:37
xarchhey but24/08 12:40
xarchyou're french ?24/08 12:40
pedagandyeah,  but I promise, I didn't meant to be French. I just happen to be born there, silly mistake :-)24/08 12:44
xarchwell24/08 12:44
xarchI'm french too :)24/08 12:44
pedagandif 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
pedagandI saw that :-)24/08 12:45
pedagandthat's why I was wondering if you knew the risks you're taking, being there and not on #coq :-)24/08 12:47
pedagandRoms has been deported for less than that, you know24/08 12:48
pedagandha, you're on #coq now, well done ;-)24/08 12:51
molerispedagand: Sorry, I should look at the bug tracker more often |:24/08 12:53
pedagandno problem24/08 12:54
molerisI pretty much did what pigworker suggests24/08 12:54
pedagandyou can follow it by RSS, if you like this technology24/08 12:54
pedagandoh, that's perfect then. Out of curiosity, why do you need the haskell tactic to do that?24/08 12:55
moleristhe 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 type24/08 12:55
pedagandall right. When you're happy with it, please commit, I'm curious to see that.24/08 12:56
molerisI'll what I have, but with the enum simplification switched on still - since I haven't done anything to the ol' Desc stuff24/08 12:58
pedagandif we could get some form of labelling on IDesc, we could remove Desc probably24/08 12:59
molerisThat's the dream.24/08 13:00
molerisWell, we have some form of labelling. We need a better one24/08 13:01
pedagandI'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
molerisI have bits of the picture, but I'm no less bamboozled24/08 13:03
molerisOK, it's on blinky24/08 13:03
molerisI should add the original epigram definitions to the test suite too24/08 13:04
pedagandgreat, 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
pedagandback from the 70's, hurrah.24/08 13:12
pedagandxarch, out of curiosity, what got you interested in the parser? A long struggle with it?24/08 13:23
xarchno24/08 13:24
xarchthat's because rewriting Parsley to use Parsec doesn't seem to be really hard24/08 13:25
xarchbut now i have made a change to the code that is even cooler24/08 13:26
xarchCochon's prompt is now λ instead of >24/08 13:26
pedagandhaha24/08 13:26
xarchthat's so cool24/08 13:26
pedagandrewriting 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
pedagandthis is due to the absence of support of left-recursion, plus various hack (in the syntax) to solve performance issues24/08 13:35
pedagandParsec would give clean error report, tho. 24/08 13:36
pedagandmoleris, had a look at the new IDesc: haha! :-) I love ity and friends.24/08 13:45
xarchif I improve Cochon prompt so that there's an history of typed commands, would you accept my patch ?24/08 13:51
xarch*Cochon's24/08 13:51
pedagandwe use "rlwrap" for that. Also, work on Cochon is suspended because it must disappear24/08 13:51
pedagandCochon will become a "ProofState explorer", no more. 24/08 13:52
xarchah, ok24/08 13:52
pedagandright now, it is abused as a theorem prover, but this is really an abuse24/08 13:52
pedagandrlwrap or a shell in emacs do the trick usually24/08 13:53
pedagandbut don't misread me, I'm not "rejecting/accepting patches", just avoiding you wasting your time24/08 13:55
molerispedagand: it's horrible, I know. Please don't hate me24/08 14:00
molerisI've updated the bug tracker24/08 14:01
pedagandthat'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 ChanServ24/08 18:14
-!- mode/#epigram [+v dolio] by ChanServ24/08 21:11
-!- mode/#epigram [+v dolio] by ChanServ24/08 22:15
-!- mode/#epigram [+v dolio] by ChanServ24/08 23:11
--- Day changed Wed Aug 25 2010
-!- mode/#epigram [+v dolio] by ChanServ25/08 00:14
-!- mode/#epigram [+v dolio] by ChanServ25/08 03:14
-!- mode/#epigram [+v dolio] by ChanServ25/08 08:14
pedagandxarch, 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 parser25/08 10:22
pedagandI'm still wading through Parsec API but I believe I can give this information25/08 10:22
pedagandhowever, I really like uu-parsinglib...25/08 10:24
pedagandyeah, uu-parsinglib is really close to what we want in the end, in term of implementation25/08 10:27
+Saizanwhat does it lack?25/08 11:20
pedagandpigworker has a very special "automaton-based parser" in mind25/08 11:32
pedagandit's not that uu-parsinglib lacks something, it just a different implementation25/08 11:39
+Saizana 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
pedagandmy 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
pedagandI 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
pedagandnow, 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
+Saizanah, it has some similarity with iteratees, though those have a way to refuse to accept more input25/08 12:00
pedagandthat's interesting25/08 12:08
xarchwell, if you explain it more precisely I'd maybe like to try to implement it :-)25/08 13:19
xarch(and sorry, I was away)25/08 13:19
pedagandno 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
pedagandthis 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, somehow25/08 13:33
pedagandI'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
pedagandfinally, 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 does25/08 13:34
xarchok25/08 13:37
-!- jjc_ is now known as jcapper25/08 14:58
-!- mode/#epigram [+v dolio] by ChanServ25/08 15:09
-!- mode/#epigram [+v pigworker] by ChanServ25/08 16:41
+pigworkerJust checking... does Agda from darcs need ghc >= 6.12 these days?25/08 16:43
+pigworkerI 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
+pigworkerhow embarrassing; I meant to ask that in #Agda..25/08 16:47
pedagandpigworker, you know you're on #epigram, right? #agda is the next door25/08 16:47
pedagandok25/08 16:47
+pigworkerin other news, Dr Oury will be visiting Glasgow tomorrow, which sounds like an excuse for a free lunch25/08 16:48
pedagandgoodo25/08 16:48
pedagandout of curiosity, is he coming back in type theory-land? or he still enjoys dissecting rats with computers?25/08 16:49
pedagandI guess, I could ask tomorrow... curiosity killed the rat25/08 16:49
+pigworkerhe's keen to do a little coinduction on the side, anyhow25/08 16:50
pedagandall 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
xarchuh, the parseBrackets needed refactoring25/08 17:32
xarch+parser25/08 17:32
pedagandhaha25/08 17:34
xarchand I think the parseIdent parser should juste be parseWord25/08 17:35
xarchbecuase, in parseToken, parseKeyword is before25/08 17:35
xarchparseIdent25/08 17:35
pedagandbut sometimes parseIdent is used alone, I suspect, and you want to parse a keyword as an ident25/08 17:36
xarchoh, ok25/08 17:36
pedagandbut, in whatever library you use, you should probably be able to define keywords as a separate entity, isn't it?25/08 17:36
pedagandin which case, your suggestion is the right thing to do25/08 17:36
xarchoh, I'm so stupid25/08 17:36
xarchi should have used parsec's tools to make the lexer25/08 17:37
pedagandas I told you, this thing is massively over-engineered to do one thing and to do it very badly25/08 17:37
pedagandmaybe, 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
pedagandwhich library are you using/planning to use?25/08 17:39
xarchI currently only now how to use Parsec25/08 17:39
xarchbut I will look at uu-parsinglib25/08 17:39
pedagandyeah, no worries.25/08 17:41
pedagandcouldn't you make use of the makeTokenParser thingie?25/08 17:42
xarchyes25/08 17:42
pedagandI have used that thing in the past, that worked quite well25/08 17:43
+pigworkerI'm trying to make Pig and tome; what the frel is manfnt.sty?25/08 17:48
pedagandno clue25/08 17:50
pedagandI'm investigating the case25/08 17:50
pedagandyou can just 'make Pig' if you want just to make Pig25/08 17:50
pedagand'make clean dep && make Pig' actually25/08 17:51
+pigworkerI ain't got it, so no tome for me. Probable fix: add to repo.25/08 17:51
pedagandout of curiosity, what is the name of the TeX distribution on MacOS? It seems rather poor, isn't it?25/08 17:52
pedagandha, manfnt is the thing that gives the cute "Danger" diagram :-)25/08 17:52
pedagandit has been a long time since you've compiled the Epitome25/08 17:53
+pigworkerI'm using tetex, from macports. It's bloody awful, as is macports.25/08 17:53
pedagandindeed, that's quite light. In FreeBSD, they have at least tetex-extras25/08 17:54
copumpkinI use MacTeX25/08 17:54
copumpkinand don't mind it25/08 17:54
copumpkinbut I mostly use XeTeX and haven't used many exotic packages25/08 17:55
+pigworkerMaybe I just need to port install tetex-extras, or maybe I need to fumigate macports off my machine for good.25/08 17:55
copumpkinyeah, I used to like macports, but homebrew seems nicer now25/08 17:56
copumpkinif not as complete25/08 17:56
pedagandanyway, I pushed manfnt into the wild25/08 17:57
+pigworkerpedagand: thanks; having another go, fingers crossed...25/08 17:59
pedagandat worst, the Epitome is linked in the Epilogue25/08 18:00
+pigworkerI 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
xarchdo you want nested comments ?25/08 18:02
pedagandxarch, yep25/08 18:03
xarchok25/08 18:03
pedagandor is it a hassle? I mean, in a first instance, we can live without them25/08 18:03
+pigworkerwe've been debating the lexical structure of comments quite a bit recently; it's fascinating25/08 18:03
xarchpedagand: it's only a matter of setting nestedComments = True or False :)25/08 18:04
pedagandyeah, that's what I thought too but I wasn't sure you followed this path :-)25/08 18:05
+pigworkerpedagand: 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
+pigworkerIt's not an urgent problem.25/08 18:09
pedagandyeah. Strangely enough, I'm not too worried that you do a dangerous thing :-)25/08 18:09
pedagandfor instance, there is one top of p.1325/08 18:10
-!- mode/#epigram [+v dolio] by ChanServ25/08 18:10
+pigworkerGoodness 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 ChanServ25/08 18:20
-!- pigworker_ is now known as pigworker25/08 18:22
-!- mode/#epigram [+v dolio] by ChanServ25/08 19:10
-!- mode/#epigram [+v dolio] by ChanServ25/08 20:14
-!- mode/#epigram [+v pigworker] by ChanServ25/08 23:26
--- Day changed Thu Aug 26 2010
-!- mode/#epigram [+v dolio] by ChanServ26/08 04:10
-!- mode/#epigram [+v pigworker] by ChanServ26/08 09:03
pedagandmoleris, what is the plan for Telescopes (in Evidences.Tm)?26/08 12:30
-!- mode/#epigram [+v Saizan] by ChanServ26/08 12:31
-!- mode/#epigram [+v pigworker] by ChanServ26/08 12:32
+pigworkerpedagand: hungry?26/08 12:32
pedagandpigworker, always26/08 12:32
+pigworkerpedagand: 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 out26/08 12:34
pedagandall right. So, shall I come now or you're in the middle of something?26/08 12:35
+pigworkernow's good26/08 12:36
+pigworkerunless you're in the middle of something26/08 12:36
pedagandbtw, bringing 2 French hosts on WELLINGTON street... That's perverse.26/08 12:36
pedagandI'm in the middle of nowhere. Will be here in a few minutes.26/08 12:37
-!- mode/#epigram [+v dolio] by ChanServ26/08 14:14
-!- mode/#epigram [+v dolio] by ChanServ26/08 17:10
-!- mode/#epigram [+v dolio] by ChanServ26/08 18:13
--- Day changed Fri Aug 27 2010
-!- mode/#epigram [+v dolio] by ChanServ27/08 01:10
-!- pumpkin is now known as copumpkin27/08 04:01
-!- mode/#epigram [+v dolio] by ChanServ27/08 06:13
pedaganddear 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 ChanServ27/08 10:15
-!- mode/#epigram [+v dolio] by ChanServ27/08 10:30
-!- mode/#epigram [+v pigworker_] by ChanServ27/08 11:30
-!- pigworker_ is now known as pigworker27/08 11:30
molerispedagand: What time of day are you leaving?27/08 13:12
pedagandmoleris, in the morning of the 8th 27/08 13:18
pedagandI thought, sometime around 827/08 13:18
molerisThen your life is probably not in danger27/08 13:25
molerisThe change in Manchester Picadilly is a long walk, but doable27/08 13:26
pedagandok, thanks27/08 13:35
+pigworkerYeah, 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
pedagandso, you don't advise NOT -> Derby -> Crewe -> GLC27/08 14:02
+pigworkerService Derby-Crewe is infrequent.27/08 14:08
pedagandooh27/08 14:09
pedagandthanks27/08 14:09
-!- mode/#epigram [+v dolio] by ChanServ27/08 14:09
Laneymoleris: pub?27/08 15:57
-!- mode/#epigram [+v codolio] by ChanServ27/08 16:13
-!- mode/#epigram [+v pigworker] by ChanServ27/08 18:02
-!- mode/#epigram [+v dolio] by ChanServ27/08 19:13
-!- mode/#epigram [+v pigworker_] by ChanServ27/08 21:46
-!- pigworker_ is now known as pigworker27/08 21:47
-!- mode/#epigram [+v dolio] by ChanServ27/08 22:13
--- Day changed Sat Aug 28 2010
-!- mode/#epigram [+v dolio] by ChanServ28/08 01:38
-!- mode/#epigram [+v dolio] by ChanServ28/08 02:13
-!- mode/#epigram [+v dolio] by ChanServ28/08 07:13
-!- mode/#epigram [+v dolio] by ChanServ28/08 13:09
-!- mode/#epigram [+v dolio] by ChanServ28/08 16:12
pedagandshapr, the +v mode seems to be scaring people from #epigram: with your Superpowers, can you disable that?28/08 16:22
pedagandI mean, I'm expecting people to be scared of Epigram, but they have to look at the code for that28/08 16:23
pedagandnow, we are scaring people even before they read any single line of code28/08 16:23
pedagandthat's no fun :-)28/08 16:23
pedagandwhat's the point of writing code then..28/08 16:23
shaprsure28/08 16:33
shaprbonjour pedagand, talar du svenska? :-)28/08 16:34
pedagandthanks!28/08 16:34
pedagandI understand the first half of this sentence, but the second half is out of my (Swedish, I suspect) reach :-)28/08 16:35
shaprGood guess.28/08 16:35
pedagandha, Google tells me that I answered your question without knowing what the question was :-)28/08 16:36
shaprYup, pretty much.28/08 16:36
shaprHm, I've forgotten how to use my irc Superpowers...28/08 16:39
pedagandthere must be some Kryptonite in the room then, be careful!28/08 16:40
-!- roconnor_ is now known as roconnor28/08 21:54
-!- mode/#epigram [+v pigworker] by ChanServ28/08 22:48
--- Day changed Sun Aug 29 2010
-!- mode/#epigram [+v dolio] by ChanServ29/08 00:13
-!- mode/#epigram [+v pigworker] by ChanServ29/08 09:53
-!- mode/#epigram [+v dolio] by ChanServ29/08 12:09
-!- mode/#epigram [+v pigworker_] by ChanServ29/08 13:47
-!- pigworker_ is now known as pigworker29/08 13:49
-!- mode/#epigram [+v dolio] by ChanServ29/08 14:12
-!- mode/#epigram [+v pigworker] by ChanServ29/08 15:33
Phantom_HooverEpigram 2 has a completely different syntax to Epigram 1, yes?29/08 16:08
+Saizanquite different afaik, there are examples in the test directory29/08 16:10
Phantom_HooverAww, I liked the Epigram 1 syntax..29/08 16:10
Phantom_HooverI never learnt it, but it looked very pretty.29/08 16:10
+Saizanwell, 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
Phantom_Hoover:)29/08 16:15
Phantom_HooverThis makes me happy.29/08 16:16
Phantom_HooverSo it doesn't have nice pattern matching and such?29/08 16:18
+Saizanit kind of does, but you've to explicitly call an eliminator29/08 16:20
Phantom_HooverDoes Epigram have the termination restriction Coq etc. have?29/08 16:21
+Saizanhttp://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
+Saizani think normal functions are supposed to be total but they are also going to embed general recursion via something like a monad29/08 16:23
Phantom_HooverWhen you say monad-like...29/08 16:24
+Saizanthe 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 termination29/08 16:27
Phantom_HooverAh.29/08 16:30
pedagandyeah, 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 interfaces29/08 16:42
+Saizan"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
pedagandI think so, yes29/08 17:19
pedagandthe compiler takes the proofstate and generates a binary29/08 17:19
-!- mode/#epigram [+v dolio] by ChanServ29/08 19:09
-!- mode/#epigram [+v dolio] by ChanServ29/08 20:13
-!- mode/#epigram [+v dolio] by ChanServ29/08 22:09
-!- mode/#epigram [+v pigworker] by ChanServ29/08 22:13
-!- mode/#epigram [+v dolio] by ChanServ29/08 23:12
--- Day changed Mon Aug 30 2010
-!- mode/#epigram [+v dolio] by ChanServ30/08 00:12
-!- mode/#epigram [+v pigworker] by ChanServ30/08 00:34
-!- mode/#epigram [+v pigworker] by ChanServ30/08 00:50
-!- mode/#epigram [+v dolio] by ChanServ30/08 01:12
-!- mode/#epigram [+v pigworker] by ChanServ30/08 01:17
-!- mode/#epigram [+v dolio] by ChanServ30/08 02:12
-!- mode/#epigram [+v dolio] by ChanServ30/08 03:12
-!- mode/#epigram [+v pigworker] by ChanServ30/08 09:40
-!- mode/#epigram [+v pigworker] by ChanServ30/08 11:45
-!- mode/#epigram [+v dolio] by ChanServ30/08 15:56
-!- mode/#epigram [+v pigworker] by ChanServ30/08 17:00
-!- mode/#epigram [+v pigworker] by ChanServ30/08 17:22
-!- mode/#epigram [+v dolio] by ChanServ30/08 18:26
-!- mode/#epigram [+v dolio] by ChanServ30/08 18:51
-!- mode/#epigram [+v pigworker] by ChanServ30/08 19:33
-!- copumpkin is now known as NaturalTransform30/08 20:27
-!- NaturalTransform is now known as NattransSalad30/08 20:27
-!- NattransSalad is now known as copumpkin30/08 20:29
-!- mode/#epigram [+v dolio] by ChanServ30/08 21:48
-!- mode/#epigram [+v pigworker] by ChanServ30/08 21:57
-!- mode/#epigram [+v pigworker] by ChanServ30/08 22:35
-!- mode/#epigram [+v pigworker] by ChanServ30/08 23:04
--- Day changed Tue Aug 31 2010
-!- mode/#epigram [+v dolio] by ChanServ31/08 02:51
-!- mode/#epigram [+v dolio] by ChanServ31/08 07:51
-!- mode/#epigram [+v pigworker] by ChanServ31/08 09:02
tsapigreetings sports fans.31/08 10:41
tsapi > 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
tsapiParse failure: end of parser.31/08 10:44
agundryhmm, that's strange31/08 10:56
tsapi > idata One : Set := (void : One) ;31/08 10:56
tsapiParse failure: end of parser.31/08 10:56
agundryI think the index set is compulsory at the moment, but even with one, idata doesn't seem to parse anything31/08 10:57
agundryit wasn't me, guv, I was on holiday...31/08 10:58
tsapime too :) back to work yesterday31/08 10:58
agundrythere have been a lot of changes recently, but I can't see any that have touched the idata parser31/08 10:59
agundrymoleris, any ideas?31/08 10:59
agundryah, I think I see it31/08 11:03
agundrythe 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
agundryhurrah, fixed31/08 11:09
agundrywell, fixed the parser anyway31/08 11:12
agundryit now turns out that the anchors code doesn't work with idata (idesc?) so the Pig just crashes instead31/08 11:13
tsapiagundry: thanks!31/08 11:37
agundryhmm, the new problem seems to be that the idesc bootstrapping code hasn't been updated since anchors were introduced31/08 11:40
* tsapi reads about anchors31/08 11:40
agundryI don't know much about them31/08 11:41
agundrywe really need a nice way to bootstrap some kind of prelude without converting Cochon code to Haskell manually31/08 11:41
tsapidoesn'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
molerisagundry: Agreed31/08 13:39
molerisI've fixed the idata tactic, and now I'm going to go find something tall to jump off31/08 13:39
-!- mode/#epigram [+v dolio] by ChanServ31/08 14:51
-!- mode/#epigram [+v dolio] by ChanServ31/08 16:55
-!- mode/#epigram [+v dolio] by ChanServ31/08 17:51
-!- mode/#epigram [+v dolio] by ChanServ31/08 18:51
-!- mode/#epigram [+v pigworker] by ChanServ31/08 20:48
-!- mode/#epigram [+v dolio] by ChanServ31/08 21:51
-!- mode/#epigram [+v pigworker] by ChanServ31/08 23:05

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