::= epsilon | '('

')'

08/01 15:06 is that the one for well parenthesized expressions? 08/01 15:06 depends on what you mean i suppose 08/01 15:06 hehe 08/01 15:06 if you consider stuff like ()() valid, than yeah 08/01 15:06 s/than/then 08/01 15:06 it's called Dyck iirc 08/01 15:07 ah yes, for all "balanced" parenthesis 08/01 15:07 copumpkin: yeah, im actually working on the permise that combining two AGs, such that one is used for parsing and the second for generation, forms an unrestricted grammar (for which recognition is undecidable) 08/01 15:14 ah 08/01 15:14 what are you going to prove? 08/01 15:15 nothing actually, i'm only constructing a mathematically-founded counterexample for pattern-based computer virus detection 08/01 15:18 based on this paper: http://www.waset.org/journals/waset/v26/v26-1.pdf 08/01 15:19 having such a system turns out to have a lot of other applications, but that was the initial inspiration anyway 08/01 15:19 (err, by system i mean a system where you can easily syntactically rewrite a string while preserving its semantic equivalence) 08/01 15:21 but i suppose if i can't find a proof that i can reference for my premise, i may attempt to tackle that 08/01 15:22

::= epsilon | '('

')'

08/01 15:22 yeah 08/01 15:23 guerrilla: interesting 08/01 15:23 09:07 < copumpkin> it's called Dyck iirc 08/01 15:23 09:07 < guerrilla> ah yes, for all "balanced" parenthesis 08/01 15:23 http://en.wikipedia.org/wiki/Dyck_language 08/01 15:23 so a derivation for this is going to be 08/01 15:23 hm 08/01 15:24 copumpkin: yeah. i'm just kind of tired of antivirus and other post-hoc security measures. thought i'd start here since some work on it has already been done 08/01 15:24 well either 08/01 15:24 :) 08/01 15:24 data Dyck : String -> Set where 08/01 15:24 empty : Dyck [] 08/01 15:24 wrappend : Dyck m -> Dyck n -> Dyck ("("++m++")"++n) 08/01 15:24 or the same thing without the String index 08/01 15:25 copumpkin: plus, its an area where one can combine a lot of different fields of math and learn quite a bit. also a rather challenging engineering problem (for me anyway) 08/01 15:25 doesn't really matter 08/01 15:25 guerrilla: sounds great 08/01 15:25 or does it? 08/01 15:25 I don't think it does 08/01 15:25 anyway the point is:  Here's just one CFG -- what you are doing is programming in a generic way, over all CFGs 08/01 15:26 that's all I wanted to say :) 08/01 15:28 Incidentally, the difference between foo_ and foo is that the latter has a precedence higher than any operator can, and the former's precedence is adjustable. 08/01 15:29 simple expressions without binding (but with some finite set of variables) like "("++m++")"++n might be replaced by "("++#0++")"++#1 08/01 15:30 opdolio: that's great to know, thanks 08/01 15:30 (where #0 and #1 are shorthand for fz and fs fz : Fin 2 which I should not have bothered to introduce) 08/01 15:30 -!- opdolio is now known as dolio 08/01 15:30 I hope that I have said something meaningful 08/01 15:33 I know it made sense inside my head 08/01 15:33 I think I get it 08/01 15:34 the set theoretic definitions of CFG are probably very awkward in the type theory 08/01 15:36 although, it's going to be really difficult no matter what 08/01 15:36 at least I don't really have the hang of this programming stuff yet 08/01 15:36 nor I 08/01 15:37 soupdragon: yeah, i spent a few days looking into it from a pure set-theoretic view 08/01 15:37 it's not that bad 08/01 15:37 it's just not very convenient 08/01 15:37 data Dyck : Set where 08/01 15:39 empty : Dyck 08/01 15:39 wrappend : Dyck -> Dyck -> Dyck 08/01 15:39 that's okay but for something like 08/01 15:40 ::= epsilon | 'a' 'a' 08/01 15:40 ::= epsilon | 'b' 'b' 08/01 15:40 mutual 08/01 15:41 data A : Set where emptyA : A ; wrapA : B -> A 08/01 15:41 data B : Set where emptyB : B ; wrapA : A -> B 08/01 15:41 * guerrilla doesn't know what mutual means yet 08/01 15:42 ? 08/01 15:42 it means they are both defined together 08/01 15:42 oops 08/01 15:42 data B : Set where emptyB : B ; wrapB* : A -> B 08/01 15:42 correction 08/01 15:42 Without mutual, you can only refer to things that come prior in the source file. 08/01 15:42 right, that makes total sense 08/01 15:42 got it 08/01 15:42 but it will be easier to use, 08/01 15:43 data AB : Fin 2 -> Set where 08/01 15:43 emptyA : AB #0 ; wrapA : AB #1 -> AB #0 08/01 15:43 emptyB : AB #1 ; wrapB : AB #0 -> AB #1 08/01 15:43 it says here Fin 2 meaning we have 2 different rules 08/01 15:43 (A and B) 08/01 15:43 you can see in general.. for n rules it's just Fin n 08/01 15:43 so that's nicer 08/01 15:44 ah 08/01 15:44 AB = Fin 2 * Nat 08/01 15:44 you might also find the pattern in the constructors 08/01 15:44 it's just a list of lists of Fin 2's 08/01 15:44 [#0], [#1,#0], [#1], [#0,#1] 08/01 15:45 we see there are 4 rules so Fin 4 can index a rule 08/01 15:45 ok 08/01 15:45 maybe some kind f generic tree type, which takes {2,4,[#0], [#1,#0], [#1], [#0,#1]} as signature 08/01 15:45 er 08/01 15:45 {2,4,{[#0], [#1,#0], [#1], [#0,#1]}} that's better 08/01 15:45 but this loses the information about the strings 08/01 15:46 this seems like a rather awkward system to encode stuff in :\ 08/01 15:46 or? 08/01 15:47 guerrilla that's hard to say 08/01 15:55 about if it's awkward to encode stuff in 08/01 15:55 rather subjective 08/01 15:55 if you know of some other generic notations then we could consider the complexity of conversions between them 08/01 15:55 but if i may digress a little bit, i can show you an example of the ideal input and state some facts about it 08/01 15:56 yes 08/01 15:56 using an ascii version of extended attribute grammar syntax: 08/01 15:57 p = -> 08/01 15:57 add and addb are nonterminals 08/01 15:58 generated by a disassembler, lets supppose 08/01 15:58 now 08/01 15:58 wait, actually 08/01 15:58 this is a terrible example 08/01 15:59 hehe 08/01 15:59 don't rush :) 08/01 15:59 ok, lemi just write this. 1sec 08/01 15:59 here, this is much better 08/01 16:04 thunkers.net/~guerrilla/eag.pdf 08/01 16:04 err, http://thunkers.net/~guerrilla/eag.pdf 08/01 16:04 <- meaning assignment and = meaning value equality 08/01 16:04 proper nonterminals in bold 08/01 16:04 addl.v means the attribute names v of the symbol named addl 08/01 16:04 this is confusing me 08/01 16:04 ok? 08/01 16:05 what are the up arrows? 08/01 16:05 if you think in terms of a parse tree, its essentially propogating that semantic information (that attribute) "upwards" 08/01 16:06 \up e denots a synthesized attribute with an expression e 08/01 16:06 okay 08/01 16:06 so like --> is like saying B.b <- A.a 08/01 16:07 this should be familiar if you ever used Yacc, bison, antlr, or any of those parser generators 08/01 16:07 it's a generalisation of that same method of passing up information when doing parsing 08/01 16:08 so, in essence it gives you context-sensitivity without needing to abandon context-free grammar's notation completely 08/01 16:08 anyway 08/01 16:09 my main points are: 1. that the metagrammar is a formal language in and of itself and 2. its "easy" to encode transformations over another language in this language 3. is equivalent to a form of PDA 08/01 16:10 point 1, i suppose i didn't mention before - that the language should be able to operate on itself. sorry about that 08/01 16:11 that's i think why i got put off by the Fin version 08/01 16:11 woah 08/01 16:11 can you tell me more about that 08/01 16:11 which part 08/01 16:11 it can operate on itself 08/01 16:11 ah 08/01 16:11 one central point of what i'm doing is that the system should not only be able to transform strings (syntax diff, semant. equiv) but it should also be able to transform its own rules 08/01 16:12 that sounds really cool 08/01 16:13 its the only theoretical counterexample of a undecidable metamorphic function that doesn't involve including the antirivurs software in the virus itself (that i've ever seen since Cohen's original paper anyway) 08/01 16:14 s/counter// 08/01 16:14 it moves the problem of detection from NP to undecidable 08/01 16:15 and in fact, is the only theory that means "metamorphic" like we mean in english 08/01 16:15 other so-called metamorphic viruses are just extremely coplex polymorphic viruses if you go by the dictionary definitions anyway 08/01 16:16 wow 08/01 16:16 so how does it operate on itsself are there examples? 08/01 16:16 yeah, lemi see. i just saw an example in my notes 08/01 16:17 the main of the grammar essentially denotes an assembly language, the assembly language in question (x86) has instructions (or sequences thereof) that are syntactically diff. but sem. equiv anyway (the point of all this from the start).. so the grammar must account for these. and since we have this information readily availible and the instructions are part of some of the more of the abstract rules, we can treat the rule bodies themselves as if they were 08/01 16:19 so 08/01 16:19 for example 08/01 16:19 We can change the rule 08/01 16:19 sorry, it uses the stupid ascii version of EAG-syntax 08/01 16:19 p0 = -> 08/01 16:19 to be 08/01 16:19 p0 = -> 08/01 16:19 but \syn = uparrow 08/01 16:19 i added type annotations in this case for other purposes (:val32) but you can ignore that 08/01 16:19 the idea stands 08/01 16:19 you can replace the rule with a new rule that is sem. equiv 08/01 16:19 just in the same way you can replace seq.s of instructions 08/01 16:20 how is that semantically equivalent? 08/01 16:20 adding a value to a register is the same as subtracting that value negated from a register 08/01 16:20 oh 08/01 16:20 I didn't notice it went from addl to subl, I see 08/01 16:20 right 08/01 16:20 but there's an AG which expresses that transform? 08/01 16:21 that would be a rule in an AG 08/01 16:21 an attributed context-free prod. rule 08/01 16:21 (btw, im not a logician or ontologist here, but i think it should be obvious that there are different levels of sem.equiv. here, where we just mean that the grammar can never corrupt the input program no matter what level sem.equiv. or syn.diff. we're talking about) 08/01 16:22 oh wait, i missed what you asked 08/01 16:23 yes 08/01 16:23 there would be other rules to do those type of transforms 08/01 16:23 in a second grammar 08/01 16:23 (or if you wana go insane, part of the same grammar) 08/01 16:24 :D 08/01 16:24 but essentially you have G1 which can manipulate instrs, G2 which can manipulate grammars. so G2 can manipulate G1 and G2 08/01 16:24 since both G1 and G2 are grammars 08/01 16:24 meh 08/01 16:24 * guerrilla done wasting channel bandwidth 08/01 16:25 hehe 08/01 16:25 no this is good 08/01 16:25 hehe ok 08/01 16:25 I am just trying to keep up 08/01 16:25 so the way it operates on other grammars imposes some particular structure/representation of these grammars? 08/01 16:29 yes 08/01 16:29 sorry i have to afk for a while (real work calls) 08/01 16:31 -!- mak__ is now known as comak 08/01 16:44 -!- lpsmith_ is now known as lpsmith 08/01 16:48 larrytheliquid: Any luck getting categories stuff into Agda? 08/01 18:11 solidsnack: there have been several attempts to do it as far as I know, but agda tends to gobble up all your memory to typecheck them 08/01 18:12 copumpkin: What kind of stuff are you talking about? 08/01 18:12 solidsnack: just working through exercises in the barr book 08/01 18:13 just basic CT definitions and theorems, as far as I know 08/01 18:13 copumpkin: Hmm. 08/01 18:13 I know that dolio tried it and ccasin did too 08/01 18:13 barr book ?? 08/01 18:13 I wrote something really basic a while back too 08/01 18:13 i could contribute some stuff back to the standard library maybe if anyone were interested (there already is some categories stuff in there im using too) 08/01 18:13 Memory starts getting tight around products, for me. 08/01 18:13 soupdragon: barr+wells notes? 08/01 18:13 soupdragon: Category Theory for Computing Science 08/01 18:13 ah 08/01 18:13 We have a groud reading it in in San Francisco. 08/01 18:14 solidsnack: ah who are you? 08/01 18:14 larrytheliquid: I am Jason Dusek. 08/01 18:14 cool 08/01 18:14 dude category theory is too hard 08/01 18:14 lol 08/01 18:14 * copumpkin goes shopping 08/01 18:15 soupdragon: I fear we have no choice. 08/01 18:15 soupdragon: There is no alternative. 08/01 18:15 solidsnack: have you seen the curry-howard <-> categories <-> quantum computing paper? 08/01 18:15 I'll just grow my own potatos and live in the mountains if ti comes to that 08/01 18:15 larrytheliquid: No. 08/01 18:15 What is the name of the paper? 08/01 18:15 i want to see that lol 08/01 18:15 maybe through curry-howard-lambek? 08/01 18:16 http://math.ucr.edu/home/baez/rosetta.pdf 08/01 18:16 someone made some sort of quantum CCC? 08/01 18:16 ah 08/01 18:16 i didnt expect to get interested in physics again haha 08/01 18:17 Don't forget the <-> logic <-> topology. 08/01 18:17 yup 08/01 18:17 I'm reading this, in and around other things: http://docs.google.com/viewer?url=http://www.dpmms.cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf 08/01 18:17 the chart at the end of the paper is a nice one-slide summary 08/01 18:17 "‘cartesian closed categories’ — where ‘cartesian’ can be seen, roughly, as an antonym of ‘quantum’." I guess not what I was saying :) 08/01 18:18 nice to have lots more activity in this channel even if I don't know what the hell anyone is talking about 08/01 18:18 copumpkin: Why is Cartesian an antonym of quantum? 08/01 18:18 solidsnack: just a quote from the paper, beats me :) 08/01 18:19 also, a nice little slide summary: http://www.google.com/url?sa=t&source=web&ct=res&cd=2&ved=0CA8QFjAB&url=http%3A%2F%2Fmath.ucr.edu%2F~mike%2Frosettaslides.pdf&ei=DXdHS4yBFp2ssQOyw8imBQ&usg=AFQjCNG6RSafce7gcTqyRxsK1Sg9p5lqhQ&sig2=JDdCHfOyiN3ZBCx5hxzNNQ 08/01 18:19 grr google links 08/01 18:19 math.ucr.edu/~mike/rosettaslides.pdf 08/01 18:19 there 08/01 18:19 I seem to recall seeing something about categories related to physical theories not being cartesian. 08/01 18:19 Braided monoidal closed or something. 08/01 18:19 I may be making things up, though. 08/01 18:20 Maybe it was that paper, even. I haven't looked at it in a while. 08/01 18:20 larrytheliquid: That's pretty neat. 08/01 18:21 one day I shall understand all this crap 08/01 18:21 * copumpkin changes his nick to CTLove 08/01 18:21 I am rather pleased by the recent streams combinator package and the new regions package on Hackage. 08/01 18:21 They seem to be bringing a lot of nice formal stuff to shell scripting and file-fiddling. 08/01 18:22 -!- copumpkin is now known as CategoryLove 08/01 18:22 Heh. 08/01 18:22 I shall read all the books and tomorrow I'll know it all 08/01 18:22 Help me complete project Euler with categories! 08/01 18:22 CategoryLove: You are Wolfram now. 08/01 18:23 -!- CategoryLove is now known as copumpkin 08/01 18:23 dolio I started doing project euler in http://esolangs.org/wiki/IRP 08/01 18:24 http://projecteuler.net/index.php?section=profile&profile=InternetRelayProgrammer 08/01 18:24 basically you ask people on IRC to solve problems for you 08/01 18:24 oh wow, that sounds like HaskellLove (and me) 08/01 18:24 it's remarkably difficult compared to just writin programs to do it :P 08/01 18:24 annoying thing about HaskellLove is he seems really into a whole load of interesting stuff but he is pretty rude so I find it hard to bother to talk to him (yeah yeah double standards) 08/01 18:25 Who is HaskellLove? 08/01 18:25 soupdragon: :) 08/01 18:25 soupdragon: you pay attention to #haskell still? 08/01 18:26 WAT? 08/01 18:26 i thought it would be neat to try collaborative theorem proving via agda's goal system + making a googlewave bot that ran the compiler 08/01 18:26 no 08/01 18:26 larrytheliquid: LOLz 08/01 18:26 solidsnack: a kid (not terribly young) who wants to learn everything yesterday in #haskell 08/01 18:26 ##algorithms #math #lisp #coq 08/01 18:26 Is doing categories stuff in other theorem provers easier/better? 08/01 18:26 I would like to know more about efforts to automate one's category theory homework, basically. 08/01 18:27 larrytheliquid: I like the idea of an wiki style library of formal mathematics, but I wouldn't want to use agda for it 08/01 18:27 copumpkin: Not young is like 25? 08/01 18:27 solidsnack: he's 21 08/01 18:27 or claims o be 08/01 18:27 copumpkin: Oh, okay. 08/01 18:27 it's always depressing when you find people that (1) you can't get along with (2) love the same things as you 08/01 18:28 Inasmuch as they let you do bigger proofs without bringing your computer to its knees, probably. 08/01 18:28 Or more proofs, rather than bigger ones. 08/01 18:28 What is too much RAM, then? 08/01 18:31 larrytheliquid: there's a couple projects like this cropping up but not sure if they're like, good, yet 08/01 18:31 nice, any links? 08/01 18:31 I have 2 GB. 08/01 18:31 Like, all the RAM on your laptop or all the RAM on a 16 core box at a math department? 08/01 18:31 Oh, I see. 08/01 18:32 http://prover.cs.ru.nl/login.php 08/01 18:47 I can't remember the other one :/ 08/01 18:49 cool thx 08/01 18:50 it's a great idea though 08/01 18:50 it'd be nice to have a builtin notation for fractional numbers 08/01 21:50 and a way to display values at compile time 08/01 21:51 unsafePerformIO from Template Haskell? 08/01 21:52 well I mean if someone wrote a real module 08/01 21:52 great idea lpsmith :P 08/01 21:52 that is R 08/01 21:52 we'd need a "show instance" for it 08/01 21:52 When haskell programmers are confronted with a problem, they think "I know, I'll use unsafePerformIO." Now they have no problems. 08/01 21:53 * copumpkin wants an infinite colist of naturals 08/01 23:11 seems hard to convince agda that it terminates without doing that nasty type thing 08/01 23:11 and there's no unfold 08/01 23:12 of all the naturals? 08/01 23:12 yep 08/01 23:12 all 1001 of them 08/01 23:12 i'm quite surprised that it's not straightforward 08/01 23:12 http://snapplr.com/3ryz 08/01 23:13 not many utility functions in Colist 08/01 23:13 what about natlist n = n :: \# natlist (n + 1); naturals = natlist 0 ? 08/01 23:14 that works :) 08/01 23:15 i wonder if the termination checker is on par with the state of the art for coinductives 08/01 23:18 * copumpkin is trying to figure out how to do left induction over colists 08/01 23:37 I wonder if I could do it as a foldl 08/01 23:38 probably not, eh 08/01 23:40 left induction? 08/01 23:42 I have an infinite list of squares and I want to prove that they're all squares :) 08/01 23:43 just to play with more coinduction 08/01 23:43 i think you've to define a coinductive version of All 08/01 23:44 yeah, there is one in Colist already 08/01 23:44 allSquares : All square squares 08/01 23:44 pretty nice eh 08/01 23:44 heh, a bit lolcat-like :) 08/01 23:45 I think he left out foldr from Colist because it's pink 08/01 23:45 well, yeah, foldr it's definitely unsafe, you'd need to have a guarantee the folding function ignores its arguments at some point 08/01 23:46 yep 08/01 23:46 but unfoldr? 08/01 23:47 you mean to unfold an All value? 08/01 23:48 no on Colist, you said earlier there's no unfoldr 08/01 23:50 yeah, but what would I be unfolding? 08/01 23:50 I need an All square squares 08/01 23:50 I already have squares 08/01 23:50 ah, true, i was just disconnectly wondering why it's missing :) 08/01 23:51 ah 08/01 23:51 how is squares defined? 08/01 23:51 scanl _+_ 0 odds 08/01 23:51 that was my first encounter with induction a million years ago so I'm attached 08/01 23:52 hah 08/01 23:52 --- Day changed Sat Jan 09 2010 ah, it's probably smarter to use Stream for this 09/01 00:02 rather than colist 09/01 00:03 but then it's missing an All type 09/01 00:03 *sigh* 09/01 00:03 copumpkin: What do the #' and |' do in this code? 09/01 00:13 solidsnack: the | is just my cursor 09/01 00:14 # lifts you into codata! 09/01 00:14 Interesting. 09/01 00:14 it's just a one-constructor data type 09/01 00:14 or codata type 09/01 00:14 the type itself is \inf 09/01 00:14 In Agda, ::' is cons', right? 09/01 00:14 usually 09/01 00:14 Well, it doesn't mean has type' in this case, right? 09/01 00:15 yeah, agda uses a single colon for type 09/01 00:15 *zonk* 09/01 00:25 zonk! 09/01 00:25 indeed 09/01 00:28 I think we have just finished a productive PigWeek 09/01 00:29 it is possible that when we get home we will figure out exactly where it is we've got to 09/01 00:29 -!- solidsnack is now known as Guest49122 09/01 01:55 -!- Saizan_ is now known as Saizan 09/01 03:46 I don't actually understand just what structure the self applicability critea imposes onto the representation 09/01 07:53 Was that in reference to something? 09/01 07:58 yeah 09/01 07:58 the attribute grammar stuff 09/01 07:58 Oh. 09/01 07:58 They've got something to do with comonads. 09/01 08:00 oh god 09/01 08:01 only with memoization :) 09/01 08:04 I don't know I'm starting to think this programming stuff is just ridiculously difficult beyond all comprehension 09/01 08:04 http://code.haskell.org/~dolio/agda-share/html/ZigZag.html now with stream proofs. 09/01 10:21 All pairs of naturals are enumerable. 09/01 10:21 mh, c.h.o is not responding 09/01 10:46 It's back up. 09/01 11:10 -!- opdolio is now known as dolio 09/01 11:10 dolio: very nice 09/01 13:34 now you can show that crank that N x N is countable 09/01 13:36 is there any work on extracting code from agda to haskell or something? 09/01 16:38 copumpkin: doesn't one of the compilers do that? 09/01 17:04 the MAlonzo compiler, no? 09/01 17:06 -!- copumpkin is now known as palomer 09/01 21:27 -!- palomer is now known as copumpkin 09/01 21:27 --- Day changed Sun Jan 10 2010 hello Saizan 10/01 09:47 hi 10/01 09:47 something like:  e1{x -> e2} => v  <-> (\x. e1) e2 => v 10/01 09:47 "Substitution Commutes" 10/01 09:47 [e]{x → [e']} = [e{x → e'}] 10/01 09:48 oh, right 10/01 09:49 which works well with an AST with named variables, so that \x. is trivial 10/01 09:50 would it still make sense if you use substitution to implement [_] or _=>_ ? 10/01 09:54 I think that you must :S 10/01 09:55 * soupdragon gets angry at /haskell/ 10/01 09:59 "I have to admit that part of me has a strong dislike for mechanized proofs; for example, I consider the proof of the 4-color theorem an atrocity. The purpose of a proof is to explain why a theorem holds, not that it merely happens to be true. A machine telling me that a completely undecipherable proof is true would not satisfy me one bit, to the contrary." 10/01 09:59 crazy people 10/01 10:04 What do you think proofs are for? 10/01 10:05 heh, he could look at the algorithm, and the proof of why the algorithm gives you a proof of the theorem 10/01 10:05 from a CS pov, i just want to know if my documentation matches my implementation, though it is indeed nice to derive which changes would break it 10/01 10:07 I mean, there are several uses for proofs. 10/01 10:07 If you have a proof about some property of your program, and it's machine checked, that might be good enough if what you care about is correctness of the program. 10/01 10:08 For math proofs, you might use the proof to gain insight as to why the theorem is true. 10/01 10:08 And coq proof scripts appear to suck for the latter, on their own at least. 10/01 10:09 http://www.reddit.com/r/coding/comments/ajk0p/a_haskell_program_to_solve_a_sudoku_puzzle_pdf/ 10/01 10:09 At the very least, you'd need to have a replay of what each line of the script does to the proof goals and such. 10/01 10:09 and i guess the generated proof terms aren't much better 10/01 10:12 Probably not. 10/01 10:12 well Ltac is TC so 10 lines of proof script can produce busybeaver(10) pages of lambda terms :D 10/01 10:12 That's why the PreorderReasoning module is nice. You can see all the intermediate results, even though they're irrelevant to the proof term. 10/01 10:13 yeah reflective proofs in general are great 10/01 10:13 Instead of "trans (trans (sym (cong (\x -> ...) foo)) (cong (\y -> ...) bar)) baz" 10/01 10:14 http://www.reddit.com/r/programming/comments/9sgw1/proof_driven_development_sudoku_pdf/ 10/01 10:15 bleck!!! this is not "proof driven developmen" 10/01 10:15 grrrr!! 10/01 10:21 why not? 10/01 10:22 because it's program derivation 10/01 10:22 apfelmus admits "Ah, yes, of course. "Proof Driven Design" is a deliberate buzzword for those who have only heard of "Test Driven Design". ;-)" 10/01 10:29 dolio: i wonder if the lisp/scheme people have tackled this problem for macros 10/01 10:38 What problem? 10/01 10:38 of understanding generated code 10/01 10:39 You don't need to be able to understand the proof term to understand the proof. 10/01 10:40 Just what it's doing at a reasonable level of abstraction. 10/01 10:40 sure, i guess i should have said "code that uses generated code", or "programs that use macros" 10/01 10:41 Coq proofs tell you all the proof strategies that are executed and in what order, but it doesn't show you what that does to the various subgoals and stuff. 10/01 10:41 Or why you'd use each strategy when it is used. 10/01 10:41 strategies are mostly searches, right? 10/01 10:44 i wasn't considering that 10/01 10:44 proof scripts in coq are usually just someone hacking away to make the blooding thing say "proof completed" 10/01 10:46 no matter HOW just get it done 10/01 10:46 They can be, certainly. 10/01 10:50 The ring solver module in agda was ported from coq. 10/01 10:50 And you can just tell it to prove arbitrary stuff involving operations on rings. 10/01 10:50 yeah, and that's pretty deterministic, it just normalizes 10/01 10:51 it could be made so that it logs the equalities used, to form an PreorderReasoning style proof, if one wants to know why that specific equality on rings work 10/01 10:54 whcih might not be at a sufficiently high level of abstraction either.. 10/01 10:56 mathematicians are warped :L 10/01 11:05 Implement an Agda-like language on top of ΠΣ. 10/01 11:40 ΠΣ in ΠΣ. 10/01 11:40 Optimizing compiler. 10/01 11:40 ? 10/01 11:40 "what's next" regarding pi-sigma 10/01 11:41 -!- jfredett_ is now known as jfredett 10/01 17:02 --- Day changed Mon Jan 11 2010 TacticalGrace: so you're going to teach an agda course? :) 11/01 01:21 copumpkin: I wouldn't call it an Agda course 11/01 01:25 a course using agda, I meant :) 11/01 01:25 The course is on formal methods and tools for software design, implementation, and testing 11/01 01:26 ooh 11/01 01:26 So, I plan to talk about formal specifications and proofs against such specifications 11/01 01:26 cool 11/01 01:27 and this is what I want to use Agda for 11/01 01:27 but the course will also use Haskell and tools, such as QuickCheck and HPC 11/01 01:27 nice :) I wish we had courses like that 11/01 01:27 it's an existing course that was taught in an imho somewhat misguided way 11/01 01:28 what did it use before? 11/01 01:28 basically fancy tricks using C++ and working from somewhat mathematical, but not at all rigorous specs 11/01 01:29 I don't think it met the aim of the official course description at all 11/01 01:29 ah 11/01 01:30 the classical thing to do would probably be Hoare calculus and/or WP and fuzz around with Java 11/01 01:30 but I think that's boring ;) 11/01 01:30 :) 11/01 01:30 so, I'm going to do the FP high-assurance thing 11/01 01:30 but most students will not know Haskell or FP 11/01 01:31 and as I don't think we'll get far with pen-and-paper proofs in such a class 11/01 01:31 oh I thought you taught that early on there? 11/01 01:31 I want something that is close to Haskell (which they'll learn anyway), but allows me to do rigorous specs and proofs 11/01 01:32 Agda seems to fit that pretty well 11/01 01:32 we used to 11/01 01:32 oh :( 11/01 01:32 since the CS intro was unified with the EE intro, not nymore 11/01 01:33 anymore* 11/01 01:33 (our CS school is part of the engineering faculty, and it was a faculty thing) 11/01 01:33 ah 11/01 01:33 can't you just put a haskell course as a prereq? 11/01 01:34 nah 11/01 01:35 this course now is a compulsory course for our CS and SE degrees 11/01 01:35 oh 11/01 01:35 so, this is where they are gonna learn Haskell now ;) 11/01 01:35 will be interesting 11/01 01:36 this sounds like it'll be interesting 11/01 01:36 I think it is not bad to tie it to the whole correctness thing 11/01 01:36 I mean, tie FP to it 11/01 01:36 will make it much easier to motivate 11/01 01:36 yeah :) reminds me of a course here where we were told to learn c in the first week and get on with the assignments 11/01 01:36 but c is pretty easy to pick up :) 11/01 01:36 edwinb: yeah, I hope it'll also work! ;) 11/01 01:36 indeed 11/01 01:37 I'm not worried about them picking up Haskell 11/01 01:37 I taught Concepts of Programming Languages the last two years in that way 11/01 01:37 I even refused to teach it in class (well, I had one quick intro) 11/01 01:37 :) 11/01 01:37 but I gave them exercises and Real World Haskell 11/01 01:38 I got some students writing an interpreter in Haskell once after one quick intro 11/01 01:38 worked just fine 11/01 01:38 they didn't seem to find it that hard to pick up, with enough pointers in the right direction 11/01 01:38 ah, so that's where all those clueless newbies came from? j/k :) 11/01 01:38 lol 11/01 01:38 Haskell is actually pretty easy to pick up if you put aside any prejudice 11/01 01:38 Saizan_: hehehe 11/01 01:38 I'll be interested to hear what they think of correctness in the context of a tool that allows them to prove stuff about actual programs... 11/01 01:38 yeah, I forgot that I also tell them about #haskell 11/01 01:39 that sorts them out ;) 11/01 01:39 heh 11/01 01:39 edwinb: yep, my main gripe as a student when it came to verification was that the pen-and-paper Hoare proofs seemed to have little to do with actual programming practice 11/01 01:40 exactly 11/01 01:40 so, I think, tool support is crucial 11/01 01:40 and using code that you actual might consider to run is crucial 11/01 01:40 yup, same here wrt mu-calculus and concurrent systems 11/01 01:40 actually* 11/01 01:40 I think, dependent types might be a way to deliver that 11/01 01:41 I'm going to test that hypothesis! ;) 11/01 01:41 (of course, you could use Isabelle and use the C frontend and fuzz around with that, but that would be a very steep learning curve and not integrate with the other material in the course) 11/01 01:43 When teaching Haskell to first-years, I found one big benefit was that you could get to interesting assignments much more quickly than in an imperative language. 11/01 01:44 So, hopefully Agda can be a fast-path to more interesting verification problems. 11/01 01:45 (interesting assignments => better motivtation => happy students) 11/01 01:45 yes, we have some good first year students who end up thinking CS is too easy because the first assignments are so trivial 11/01 01:46 it's a pity we don't teach them any functional programming at all really... 11/01 01:46 well, not officially 11/01 01:46 edwinb: doesn't your group have courses where you could use it 11/01 01:53 yes, we can sneak it in 11/01 01:53 but it'd be so much easier if we could assume more about what they know 11/01 01:54 yes, but it works fine for us in Concepts of Programming Languages 11/01 01:54 sure, the students need to learn the language 11/01 01:54 but because it's a languages course that's easily motivated 11/01 01:54 so in the compiling course and the logic course, say, they get functional programming, but you have to spend time teaching some basics 11/01 01:54 and the pay of comes in the assignments 11/01 01:54 and actually also the lectures 11/01 01:54 -!- opdolio is now known as dolio 11/01 04:39 -!- opdolio is now known as dolio 11/01 19:50 --- Day changed Tue Jan 12 2010 -!- opdolio is now known as dolio 12/01 04:38 -!- EnglishGent is now known as EnglishGent^afk 12/01 13:51 goorilla did you read about the x86 12/01 22:11 http://www.cl.cam.ac.uk/~mom22/jit/jit.pdf 12/01 22:11 self modification 12/01 22:11 --- Day changed Wed Jan 13 2010 are there proper dependently typed languages where you can write a function on types by case analysis? 13/01 00:22 you could do something similar to extensible variants, i'd think 13/01 00:23 as in f : Set -> Nat; f Void = 0; f Unit = 1; f Bool = 2 ? 13/01 00:27 seems unnatural 13/01 00:27 + a catchall 13/01 00:28 f _ = 3 13/01 00:28 e.g. type families in GHC kind of do this 13/01 00:29 except that they are open instead 13/01 00:29 in Agda you've to use an "universe" 13/01 00:29 to reify the types 13/01 00:30 yeah 13/01 00:33 * copumpkin isn't sure how typecase breaks parametricity but our open typecase through typeclasses doesn't 13/01 00:34 Type classes do it, too. 13/01 00:55 ah okay 13/01 00:56 And it doesn't break parametricity because it shows up in the type. 13/01 00:56 'forall a. a -> a' doesn't use type case. 13/01 00:56 oh, that's the secret ingredient! 13/01 00:56 well, don't gadts break parametricity by themselves? 13/01 00:56 I wouldn't say so off the top of my head, but I'm not really sure. 13/01 00:58 i just mean that when you see a function of type forall a. F a -> G a, you're not sure if it's guaranteed to be a natural transformation until you check the definition of F 13/01 00:59 Yeah. 13/01 00:59 So, you may well be able to write 'forall a. F a -> G a' that isn't 'natural', but I think in cases like that, F may not be a functor, either. 13/01 02:22 So whether you still have parametricity may be open. 13/01 02:25 i was thinking of "data F : Set -> Set where FInt : Int -> F Int; FOther : a -> F a" but then it's hard to write a fmap respecting fmap id = id 13/01 02:27 Yes. In the FInt case you're forced to return an FOther. 13/01 02:28 Because you don't know the return type. 13/01 02:28 Woo! 13/01 19:35 you didn't?? 13/01 19:36 "Ulf and I have optimised the handling of records. If you have encountered performance problems when, say, formalising category theory,you may want to try again. For one example we measured a speedup of ∼5 ..." 13/01 19:36 Hmm... Should I install GHC 6.12 before upgrading... 13/01 19:39 Ooo, pattern matching on records, too. 13/01 19:40 aw i thouhght you hit false 13/01 19:41 (again) 13/01 19:41 No, I'm just excited that I might be able to prove more than 5 theorems about categorical products without exhausting all my memory. 13/01 19:41 I guess I should get 6.12 since I have a patch sitting around to update bytestring-show for it. 13/01 19:46 nice! 13/01 19:53 mmm category theory 13/01 19:54 -!- Saizan_ is now known as Saizan 13/01 21:30 -!- lpsmith_ is now known as lpsmith 13/01 22:48 --- Day changed Thu Jan 14 2010 Time to play with Agda again! 14/01 03:08 What's the typecheck-and-all-that-jazz command? 14/01 03:08 C-c C-l 14/01 03:18 -!- opdolio is now known as dolio 14/01 17:01 -!- dolio is now known as codolio 14/01 17:07 -!- codolio is now known as dolio 14/01 17:07 -!- dolio is now known as codolio 14/01 17:08 -!- codolio is now known as dolio 14/01 17:08 --- Day changed Fri Jan 15 2010 -!- opdolio is now known as dolio 15/01 05:01 Does anyone know a way to buy printed copies of "Programming in Martin-Lof's Type Theory"? (the out of print edition seems to be rather expensive) 15/01 10:13 Probably downloading it and taking it to a printing shop is the easiest... 15/01 10:23 yeah, i suppose so 15/01 10:30 Is agda likely to get a tactic based theorem prover at some point? 15/01 10:38 -!- Berengal_ is now known as Berengal 15/01 12:00 -!- ksf_ is now known as ksf 15/01 22:41 -!- Berengal_ is now known as Berengal 15/01 22:41 -!- solidsnack_ is now known as solidsnack 15/01 23:24 -!- whoppix_ is now known as whoppix 15/01 23:24 --- Day changed Sat Jan 16 2010 what is this sized type stuff? 16/01 01:24 ah, found a paper 16/01 01:24 or slides, at least 16/01 01:24 can't actually find much on them 16/01 01:28 It's like indexing your type by a natural number to more easily prove termination, only there's some kind of built-in support for figuring out how the indices work out with a constraint solver of some sort. 16/01 01:30 And there's some kind of infinity when x = S x is inferred. 16/01 01:31 aha 16/01 01:31 in the slides it says it's equivalent to the ordinals though 16/01 01:31 not naturals :o 16/01 01:31 which seems strange 16/01 01:31 Okay. 16/01 01:31 anyway, that doesn't change the basic point 16/01 01:32 which ordinals? 16/01 01:32 just wondering how you'd write down inductive ordinals 16/01 01:32 the set of ordinals --> BOOM 16/01 01:32 dolio: btw, you were trying to prove stuff about sorting a while ago: http://www.iis.sinica.edu.tw/~scm/2007/agda-exercise-length-indexed-mergesort/ and http://www.iis.sinica.edu.tw/~scm/2007/agda-exercise-proving-that-mergesort-returns-ordered-list/ are interesting 16/01 01:32 My problem was proving transitivity for permutation proofs that didn't simply assume transitivity. 16/01 01:34 ah 16/01 01:35 Anyhow, the usual inductive ordinal definition is: data O : Set where zero : O ; suc : O -> O ; lim : (Nat -> O) -> O 16/01 01:42 oh, hm 16/01 01:43 Although you can get fancier from there. 16/01 01:43 this goes up to e^e^...^e? 16/01 01:43 err 16/01 01:44 is that all of them? 16/01 01:44 s/e/w/g 16/01 01:44 All of them? 16/01 01:44 copumkin (BOOM!) 16/01 01:44 I think O has the strength of epsilon_0 = w^w^...^w 16/01 01:45 (nice to be able to check somehow..) 16/01 01:45 GOT EPIGRAM WORKING! 16/01 19:47 Which one? 16/01 19:47 Pig09 16/01 19:48 So you can write cryptic programs in some core language? 16/01 20:02 I haven't tried 16/01 20:05 I think I need to get TeX to build some documentation 16/01 20:05 this is what .pig files look like 16/01 20:06 make Nat := (Mu con ['arg (Enum ['zero 'suc]) [ (con ['done]) (con ['ind1 con ['done]]) ] ] ) : Set ; 16/01 20:06 module Vec ; 16/01 20:06 lambda A : Set ; 16/01 20:06 make Vec : Nat -> Set ; 16/01 20:06 make VecD := (\ n -> IArg (Enum ['nil 'cons]) [ (IDone ((n : Nat) == (zero : Nat))) (IArg Nat (\ m -> IArg A (\ a -> IInd1 m (IDone ((n : Nat) == (suc m : Nat)))))) ]) : Nat -> IDesc Nat ; 16/01 20:06 make vnil := con [ 0 , [] ] : Vec zero ; 16/01 20:06 make vcons := (\ n a as -> con [ 1 n a as , [] ]) : (n : Nat) -> A -> Vec n -> Vec (suc n) ; 16/01 20:06 and it's got quotients! 16/01 20:07 It does? 16/01 20:12 I didn't realize that. 16/01 20:12 better than setoidsa 16/01 20:12 -a 16/01 20:12 Yeah, you don't have to tell me that. :) 16/01 20:13 have you looked at the epigram impl. it's all crazy 16/01 20:13 they use aspect oriented program 16/01 20:13 I have a little. I have a lot of trouble figuring it out. 16/01 20:13 I wanted to see where they went with their locally nameless stuff, but it's far beyond what's in the paper on it. 16/01 20:14 oh really 16/01 20:14 With all kinds of riffing on applicative stuff. 16/01 20:14 And I don't understand much of it. 16/01 20:14 Plus, the SHE stuff makes it kind of difficult to read, since they import parts of data definitions from other files and stuff. 16/01 20:17 ah that's she doing that 16/01 20:17 last time I looked it was higgelty piggelty or something 16/01 20:18 I think it's meant to be easier to read in this style though... 16/01 20:18 I'm also not entirely clear what red and green types are, although it seems like I've heard of those before. 16/01 20:19 Or red and green terms. I forget. 16/01 20:21 Maybe the red/green stuff is from older repositories. I don't see it anymore. 16/01 20:24 I've never been entirely clear on how you define functions on quotient types. I guess I should read up some. 16/01 20:29 That is, how you define them without excessively burdensome proofs. 16/01 20:29 dolio it looks like the eliminator you get requires the burdensome proof 16/01 20:30 Ah. :) 16/01 20:30 but you know that MOST functions you write are probaby just compositions of other programs 16/01 20:30 Yeah, I guess providing the API for using the quotient type would be expected to fulfill the proof obligations. 16/01 20:31 I can't seem to pull from the repository. 16/01 20:37 dolio that's weird 16/01 20:39 Pulling from "http://www.e-pig.org/darcs/Pig09"... 16/01 20:39 I just pulled 16/01 20:39 Ah, my repository was pointed at sneezy.cs.nott.ac.uk 16/01 20:41 Hey, it's got coinductive types, too. 16/01 20:56 \o/ 16/01 20:57 but does it have equality on them 16/01 20:57 I think that's in the TODO 16/01 20:57 I thought their plan was to encode them using inductive types. 16/01 20:57 Do they still have Set : Set? 16/01 20:59 Oh, the colors are back in the equality module. 16/01 21:00 Only it's green and blue instead of green and red. 16/01 21:00 Ill try and check Set : Set 16/01 21:00 Oh, I think I know what the colors mean. 16/01 21:00 hehe Pig told me "I'm sorry, Dave. I'm afraid I can't do that." 16/01 21:01 > make Foo := Set : Set ; 16/01 21:01 Made. 16/01 21:01 > make Bar := Foo : Foo ; 16/01 21:02 Made. 16/01 21:02 Heh. 16/01 21:02 How'd you build this? Just make in the src directory? 16/01 21:03 yes but I had to get GHC 6.12 and darcs She 16/01 21:04 I have 6.12. 16/01 21:04 Guess I made the right decision when re-installing Agda the other day. 16/01 21:05 Huh, I don't have lhs2TeX. 16/01 21:08 you don't need it 16/01 21:10 try ./Pig 16/01 21:11 make Pig 16/01 21:11 You should install lhs2TeX. The output is pretty impressive. 16/01 21:16 okay 16/01 21:16 how do you run lhs2Tex on it? 16/01 22:47 * edwinb spots people playing with the Pig 16/01 22:58 make Epitome will run lhs2Tex 16/01 22:59 hi edwin!! 16/01 22:59 hello world 16/01 22:59 thanks :) 16/01 23:04 so whats everyone wrote in epirgam 16/01 23:53 we have added two and two 16/01 23:53 did you get five? 16/01 23:53 and taken the first few things from a stream 16/01 23:53 I don't think we ever got five 16/01 23:53 I'm fairly sure we got two at one point 16/01 23:54 > compile x foo 16/01 23:58 /bin/sh: epic: command not found 16/01 23:58 Pig: user error (EPIC FAIL) 16/01 23:58 * soupdragon snorts 16/01 23:58 cabal install epic, no problem ;) 16/01 23:58 I knew it wouldn't be that easy 16/01 23:59 I'll need to install bohm and gmp I guess 16/01 23:59 --- Day changed Sun Jan 17 2010 you probably have gmp already 17/01 00:00 but you will need boehm, yes 17/01 00:00 not that any epigram programs actually need garbage collection yet 17/01 00:00 boehm gc is a pretty painless install, fortunately 17/01 00:00 unless you're on a weird system 17/01 00:00 yikes 17/01 00:01 edwinb have you seen this? 17/01 00:02 *** This will be an error in GHC 6.14! Fix your code now! 17/01 00:02 Yes, it's from happy generated code though 17/01 00:02 so it's just noise 17/01 00:02 ghc is getting very snappy 17/01 00:02 err 17/01 00:02 bossy 17/01 00:02 I blame Simon M ;) 17/01 00:02 Pig doesn't seem to like much of what I'm typing. 17/01 01:42 I'm gonna read the sources a bit more carefully before pulling on its tail 17/01 01:43 tommorow :[ 17/01 01:43 parse \ x -> x works, but asking it to infer gives me a parse error. 17/01 01:45 no wonder 17/01 01:45 hmm 17/01 01:46 maybe not what I thought it was 17/01 01:46 > make f := (\ x -> x) : Set -> Set ; 17/01 01:50 Made. 17/01 01:50 > infer f 17/01 01:50 Set -> Set 17/01 01:50 \o/ 17/01 01:50 forgetting about proofs, I wonder how nice a SQL library in agda would be nice :) 17/01 01:53 -nice 17/01 01:53 or maybe +nice 17/01 01:53 How nice it would be nice nice? 17/01 01:54 SQL kicks ass 17/01 01:54 Anything to do with SQL is pure win 17/01 01:54 you being sarcastic? :) 17/01 01:54 Anything to do with Joe Celko is pure win. 17/01 01:54 no I love SQL 17/01 01:54 it'd be nice to guarantee that types passed to compiled queries match what's expected 17/01 01:55 I submit SQL scripts to rosettacode sometimes 17/01 01:55 it's a seriously cool language 17/01 01:55 :) 17/01 01:55 I don't like what oracle did to it 17/01 01:55 also I have a thing for expressive subturings 17/01 01:55 they have a certain je ne calculer pas 17/01 01:56 :) 17/01 01:56 http://rosettacode.org/wiki/Look-and-say_sequence#SQL 17/01 01:56 wow 17/01 01:56 that's pretty intense :) 17/01 01:57 Joe Celko is also intense. 17/01 01:59 yeah? 17/01 02:00 Who else has written a "For Smarties" book? 17/01 02:02 Also, he looks like Anton LaVey. 17/01 02:03 yeah he does 17/01 02:03 lol 17/01 02:03 make plus := con con [(\ r r y -> y) (\ r -> con \ h r y -> suc (h y))] : Nat -> Nat -> Nat ; 17/01 13:07 does not make sense.. 17/01 13:07 (d : Desc)(v : Mu d)(P : Mu d -> Set)(p : (discharge : descOp (d, Mu d))(discharge : boxOp (d, Mu d, P, discharge)) -> P (con discharge^1)) -> P v 17/01 13:09 that's weird 17/01 13:09 discharge : boxOp (d, Mu d, P, discharge)? 17/01 13:09 I guess they're different names 17/01 13:09 cannot understand this free monad stuff 17/01 13:52 well I can't figure out what con con means 17/01 14:21 con - Constructor for inductive deﬁnitions 17/01 14:23 con con - ?? 17/01 14:23 > parse () 17/01 15:56 Parse failure: end of parser. 17/01 15:56 should that really be a parse error? 17/01 15:56 InTm ::= ... | () -- Unit | ... 17/01 15:56 > elab add two two 17/01 16:12 con ['suc (con ['suc (con ['suc (con ['suc []])])])] 17/01 16:12 nice 17/01 16:12 not taht make zero := [] : Nat ;  makes any sense 17/01 16:13 * ttt-- doesnt know how to prove a = 1 -> a >= 1 in agda 17/01 16:55 * ttt-- feels stupid :) 17/01 16:55 well ttt-- it depents on >= and = 17/01 16:56 what are the defintions of these? 17/01 16:56 the standard ones 17/01 16:56 ... 17/01 16:56 for nat 17/01 16:57 from Data.Nat 17/01 16:57 and PropositionalEquality 17/01 16:57 im probably doing it wrong 17/01 16:58 I think you can click on the things to get the definitions 17/01 16:58 foo : (a : ℕ) -> a ≡ 1 -> a ≥ 1 17/01 17:00 are there simpler ways that typing out the proof manually? 17/01 17:01 than* 17/01 17:01 Why cant it deduce that the only case of a can be 1 ? 17/01 17:09 in foo 17/01 17:09 you can prove 1 ≥ 1 first, and then use it to complete foo 17/01 17:10 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=16232#a16232 17/01 17:23 or not, as the case may be 17/01 17:24 you can skip matching on n I thin 17/01 17:24 think* 17/01 17:24 i dont really understand why the foob doesnt work 17/01 17:25 -the 17/01 17:25 it doesnt seem to use all the information available, unless you type it all out 17/01 17:26 that's how agda works 17/01 17:26 Arabic numerals in Pig seem to refer to some built-in natural type. 17/01 17:39 0 and 1 are not what the Epitome says they are. 17/01 17:39 yeah that's weird 17/01 17:39 that epitome thing is a bit confusing 17/01 17:40 I mean the BNF 17/01 17:40 How did you define a Nat type for adding? 17/01 17:40 well I didn't 17/01 17:40 I just took the one from /test 17/01 17:40 make Nat := (Mu con ['arg (Enum ['zero 'suc]) [ (con ['done]) (con ['ind1 con ['done]]) ] ] ) : Set ; 17/01 17:40 Ah. 17/01 17:40 we have 17/01 17:40 'zero : Enum ['zero 'suc] 17/01 17:40 'suc : Enum ['zero 'suc] 17/01 17:41 not sure if you can prove  Enum [] -> P 17/01 17:41 Oh, there's a Mu. 17/01 17:41 con ['arg ...] makes a Desc (I think), which you can Mu into an inductive 17/01 17:41 > infer con ['arg (Enum []) []] : Desc 17/01 17:42 Desc 17/01 17:42 Pig could use some readline, too. :) 17/01 17:48 yes ;( 17/01 18:08 haven't got around to that yet 17/01 18:08 hi, copumpkin: have you seen http://www.cse.chalmers.se/~ulfn/code/database/Main.html ? 17/01 19:02 ooh, nope I hadn't 17/01 19:02 thanks :) 17/01 19:03 :-) 17/01 19:03 soupdragon: Heh, did you enter the definition of addition by hand? 17/01 19:27 dolio I just pasted these things in from the file 17/01 19:28 there's some example/test programs already 17/01 19:28 soupdragon: hi, copumpkin: have you seen http://www.cse.chalmers.se/~ulfn/code/database/Main.html ? 17/01 19:28 (thought you might be interested too) 17/01 19:28 Yeah, I know. 17/01 19:28 copumpkin is that from power of pi ? 17/01 19:28 It produces some fairly incomprehensible goals on some of the entries. 17/01 19:28 soupdragon: not sure :) 17/01 19:28 the tactic stuff seems to work nice 17/01 19:28 Yeah. 17/01 19:29 I just don't know how I'd figure out what to enter for addition. 17/01 19:29 The incremental development is nice, though. 17/01 19:29 yeah in this thing: 17/01 19:29 make plus := con con [(\ r r y -> y) (\ r -> con \ h r y -> suc (h y))] : Nat -> Nat -> Nat ; 17/01 19:30 it's not exactly clear what con does 17/01 19:30 Yeah. 17/01 19:30 trying to work it out.. 17/01 19:30 In some of them they appear to define constructors 'zero and 'suc, but then they don't use them. 17/01 19:30 But they're still in the output. 17/01 19:30 like here? 17/01 19:30 make zero := con ['zero] : Nat ; 17/01 19:30 make suc := (\ x -> con ['suc x]) : Nat -> Nat ; 17/01 19:30 They use them there. 17/01 19:31 But sometimes it's just "make zero := [] : Nat". 17/01 19:31 oh yeah I don't understand that bit 17/01 19:31 And the NatD isn't any different in those. 17/01 19:31 I was thinking about trying to define integers as quotients of Nat * Nat, but I don't have any confidence in my ability to define subtraction. 17/01 19:33 wonder if you can prove con ['zero] = [] 17/01 19:33 I don't know. If you parse [], it gives Void, I think. 17/01 19:34 do you need subtracton?  (x,y) = (u,v) <=> y+u = v+x 17/01 19:35 Oh, I guess not. 17/01 19:35 Apparently "con ['zero]" is DC (Con (DC (Pair (DC (Tag "zero")) (DC Void)))) 17/01 19:36 So [] is for tuples, I guess? 17/01 19:37 yes 17/01 19:38 dolio another weird thing is this 17/01 19:40 Have you figured out what the type of 0, 1, 2, etc. are yet? 17/01 19:40 > make quux := Enum ['foo 'bar 'baz] : Set ; 17/01 19:40 Made. 17/01 19:40 > make quux2 := Enum ['foo 'baz] : Set ; 17/01 19:40 Made. 17/01 19:40 now we have  'foo : quux,  'foo : quux2,  'bar : quux but not 'bar : quux2 17/01 19:41 That doesn't surprise me, really. 17/01 19:44 well it just means that terms can have multiple types 17/01 19:44 I think one of the things they're going for is relatively structural typing. 17/01 19:44 So that datatypes really are fixed points of functors and stuff, and so you can define generic functions based on that and such. 17/01 19:45 ah 17/01 19:46 > elab 0 : quux 17/01 19:46 'foo 17/01 19:46 > elab 1 : quux 17/01 19:46 'bar 17/01 19:46 Ah hah. 17/01 19:46 > infer Switch 17/01 19:47 (e : EnumU)(x : Enum e)(p : Enum e -> Set)(b : Branches (e, 17/01 19:47 p)) -> p x 17/01 19:47 How did you find that? 17/01 19:48 it's in src/Features/Enum.hs 17/01 19:48 Ah. 17/01 19:48 > infer Switch ['foo 'bar] 0 17/01 19:49 (p : Enum ['foo 'bar] -> Set)(b : Sig (p 'foo ; p 'bar ;)) -> p 'foo 17/01 19:49 cool 17/01 19:49 hmm what the hell is b : 17/01 19:51 > make x := ? : Enum [] 17/01 19:52 Made. 17/01 19:52 > infer Switch [] x (\ x -> :- FF) 17/01 19:52 (b :) -> :- FF 17/01 19:52 > infer (\ x -> Switch [] x (\ o -> :- FF) []) : Enum [] -> :- FF 17/01 19:53 Enum [] -> :- FF 17/01 19:53 that works :D 17/01 19:54 I have no idea what that last [] is for thuogh 17/01 19:54 but I was wondering if you could prove that the empty label thing is empty 17/01 19:54 also I don't know what's going on with this free monad stuff 17/01 20:07 and I can't seem to find what 0 and 1 actually are  in src/DisplayLang/Lexer.hs 17/01 20:07 Free monads? 17/01 20:08 I was guessing like trees but I don't know yet 17/01 20:09 Free Kevin 17/01 20:09 I mean more: where do you see free monads? 17/01 20:10 In the code for pig? 17/01 20:10 Ooo, they have an example of unordered pairs. 17/01 20:11 Now I can't remember the example of why you'd want unordered pairs... 17/01 20:14 Oh, right, you can define commutative operations as functions on unordered pairs, which ensures their commutativity. 17/01 20:21 that's clever 17/01 20:35 thing is with unordered pairs ((x,y),z) isn't equal to (x,(y,z)) 17/01 20:49 ((x,y),z) isn't even a valid unordered pair. 17/01 20:55 oh why not 17/01 20:55 Because the types of the components are different. 17/01 20:56 doh!! 17/01 20:56 that was stupid of me 17/01 20:56 thanks 17/01 20:56 But ((x,y),(z,w)) may be different than ((x,z),(y,w)). 17/01 20:57 are you guys talking about epigram? 17/01 20:57 So, 'zero := con ['zero] : Nat ; elab zero' gives []. 17/01 20:59 Yes. 17/01 20:59 dolio O_O 17/01 20:59 f (x, y) seems to be the same as f x y, too. 17/01 21:02 Or, maybe not. 17/01 21:03 infer prints out stuff like "f (x, y)", but the parser complains when I try it. 17/01 21:04 what about f(x, y)? 17/01 21:06 no 17/01 21:06 Try "infer elimOp" 17/01 21:08 strange 17/01 21:10 soupdragon: free monads over a functor are what you get if you extend Mu with another constructor Return a, so in haskell it'd be data Free f a = Return a | Branch (f (Free f a)), so they are generally interpreted as terms with variables of type 'a' and signature F, and m >>= f applies the substitution f to the term m 17/01 22:39 the thing is 17/01 22:41 I don't see any fmap in the file 17/01 22:41 they use Monad like this,  make Expr := (\ X -> Monad ExprD X) : Set -> Set ;   and ExprD is the code of a type like  data Expr X = Var X | Num Nat | Add (Expr X) (Expr X) 17/01 22:42 maybe fmap is derived somehow 17/01 22:43 What's the definition of bind? 17/01 22:44 -!- opdolio is now known as dolio 17/01 22:44 there isn't one :P 17/01 22:44 Then they don't need fmap. 17/01 22:44 subst : (D : Desc)(X : Set)(Y : Set)(f : X -> Monad D Y)(t : Monad D X) -> Monad D Y 17/01 22:45 that's a built in 17/01 22:45 yeah, that's bind 17/01 22:47 nice :) 17/01 22:47 maybe there's also a built-in fmap? 17/01 22:49 well there's this box thing 17/01 22:50 infact there is map : (d : Desc)(a : Set)(b : Set)(f : a -> b)(x : descOp (d, a)) -> descOp (d, b) 17/01 22:50 so that's a generic map 17/01 22:51 I wonder how that can work. 17/01 23:03 Maybe Desc contains only strictly-positive functors... 17/01 23:06 what's not a functor these days 17/01 23:07 I don't know 17/01 23:07 it probably is SPFs only 17/01 23:07 there's IDesc for families 17/01 23:07 /\ A -> A -> A isn't a functor. 17/01 23:07 oh sure but I mean that's not described by Desc 17/01 23:08 Okay. 17/01 23:08 How can you tell? :) 17/01 23:08 wait is that not the identity functor 17/01 23:08 FA = A -> A 17/01 23:09 hm 17/01 23:09 you can define FA = A -> FA 17/01 23:09 The identity functor would be IA = A. 17/01 23:09 wait forget what I am saying I am confused 17/01 23:09 data F a = FCon (a -> a) 17/01 23:10 --- Day changed Mon Jan 18 2010 Aww, there's no cofree comonad built-in. 18/01 01:26 this is discrimination. 18/01 01:27 you should write in and complain 18/01 01:28 I'm not sure where to complain. There hasn't been traffic on the epigram list in ages. 18/01 01:29 I guess I could yell at edwinb. 18/01 01:29 * edwinb hides 18/01 01:34 * copumpkin reluctantly pulls out his pickaxe and torch 18/01 01:35 I could teach you how to add Features if you like ;) 18/01 01:35 Presumably I just write something like FreeMonad.lhs, and add it to Features.lhs. 18/01 01:36 yes 18/01 01:37 the theory is that this keeps all the relevant stuff for each feature in the same place 18/01 01:38 Yeah. It's growing on me. 18/01 01:38 it takes a bit of getting used to 18/01 01:38 Figuring that much out isn't the hard part. Writing the right stuff to make a cofree comonad is. 18/01 01:39 elimMonadOp doesn't mean much to me. :) 18/01 01:39 I don't really understand what's happening in the descriptions of the naturals in the tests folder, either, which are presumably even less complicated. :) 18/01 01:41 it'll probably all change several more times anyway, if past form is anything to by ;) 18/01 01:42 Or, for instance, I was surprised earlier that "con ['zero]" normalizes to []. 18/01 01:43 Is the core more like PiSigma now than the stuff in the OTT papers (0, 1, 2, pi, sigma, W)? 18/01 01:44 Still more like OTT 18/01 01:46 * edwinb decides he should have been asleep hours ago 18/01 01:46 Night, then. 18/01 01:47 night 18/01 01:47 Woo, I think I have a handle on the Descs now. 18/01 06:09 :O 18/01 06:10 are they restricted to form only functors? 18/01 06:11 There's three cases. 18/01 06:17 Done, which looks like "con ['done]", or [], for some reason. 18/01 06:17 con ['label] is identical to [], apparently, which is rather confusing. 18/01 06:18 Then there's "con ['ind1 desc]", which is equivalent to refering to the type you're defining. 18/01 06:19 Although the docs refer to it as Ind H d, for some H : Set, but I haven't seen any more general expansion of the 'ind1 version. 18/01 06:20 And then there's "con ['arg T (\ x -> desc)]", which is equivalent having a field of type T, with the lambda expression giving the rest of the description, dependent on x : T. 18/01 06:22 Although a lot of times, it doesn't look like that. 18/01 06:22 Because, say, "'arg (Enum ['one 'two]) [ (case_one) (case_two) ]" is equivalent to writing down the more explicit version with a case analysis eliminator for the enum. 18/01 06:24 this is how archeologists must feel, except backwards 18/01 06:25 So, I'm not exactly sure what all that gives you. 18/01 06:25 Enum is syntax? 18/01 06:26 Yeah, something like that. 18/01 06:27 Tags start with ' 18/01 06:27 Tuples containing just tags can be typed as EnumU, and Enum takes EnumUs to Set. 18/01 06:27 Except, Enum isn't really first-class. 18/01 06:28 so contructors in Descs don't have a tag 18/01 06:32 only Enums do 18/01 06:32 If you want to write a type with more than one constructor, you need to use an Enum, and then the tags for the enum will be the tags for the constructors, essentially. 18/01 06:35 ah, so in tests/Monad.pig in make ExprD the latter two "give"s fill in the ?s from the first one 18/01 06:37 Yes. 18/01 06:44 So, there is a more general Ind H d. 18/01 06:45 con ['ind H d], for some type H. 18/01 06:45 I think that lets you define W-types. 18/01 06:53 Yep. 18/01 06:55 make W := (\ T U -> Mu (con ['arg T \ x -> con ['ind (U x) []]])) : (T : Set) (U : T -> Set) -> Set 18/01 06:56 make w := (\ T U t f -> con [t f]) : (T : Set) (U : T -> Set) (t : T) (f : U t -> W T U) -> W T U 18/01 06:56 The required space after \ kills me. I'm not used to \x being wrong. 18/01 06:58 -!- Berengal_ is now known as Berengal 18/01 17:41 -!- solidsnack is now known as Guest57984 18/01 19:26 --- Day changed Tue Jan 19 2010 Wow, Idris is apparently pretty speedy. 19/01 00:11 what did you run? 19/01 00:15 It can be 19/01 00:18 Nothing. I was reading this: http://www.reddit.com/r/dependent_types/comments/ar2ai/scrapping_your_inefﬁcient_engine_using_partial/ 19/01 00:18 it needs more work to do more complex data structures well though 19/01 00:18 And in the benchmarks it was competitive or better than Java, which is generally better than I expect for a language with real dependent types. 19/01 00:19 there is no reason why a dependently typed language should be slow 19/01 00:19 quite the opposite really - you have more type information, so it'd be good to get optimisations out of that 19/01 00:19 No, but they usually come as interpreters written by one or two people. :) 19/01 00:20 that is true ;) 19/01 00:20 mh, an interpreter of Idris in Idris that specializes to id.. 19/01 02:33 So I'm going through the paper "Dependant Types At Work" and I can't seem to figure out how to write the eq-mult proof.  I'm sitting in front of an isar proof I whipped up for comparison 19/01 05:05 I also just don't particularly understand how to prove things using types in general so a paper for that (for us less intelligent folks) would be great too 19/01 05:06 -!- jeflak_ is now known as jeflak 19/01 11:05 -!- jeflak_ is now known as jeflak 19/01 23:53 --- Day changed Wed Jan 20 2010 MissPiggy: You tried anything with IDesc yet? 20/01 00:53 no 20/01 00:53 there's a Vector example 20/01 00:53 Oh, there is? 20/01 00:53 Ah, yes. 20/01 00:53 make VecD := (\ n -> IArg (Enum ['nil 'cons]) [ (IDone ((n : Nat) == (zero : Nat))) (IArg Nat (\ m -> IArg A (\ a -> IInd1 m (IDone ((n : Nat) == (suc m : Nat)))))) ]) : Nat -> IDesc Nat ; 20/01 00:54 Okay, that explains what I was missing. 20/01 00:54 I couldn't figure out where the out-index was supposed to come from. 20/01 00:54 So to speak. 20/01 00:55 I'm wondering if they might add an IRDesc sometime (for ind-rec) 20/01 00:55 if not we can always do it ourselves :) 20/01 00:56 I'm not really up on the formal underpinnings of induction recursion. 20/01 00:56 The current desc stuff has some limitations, anyhow, I think. 20/01 00:57 like what? 20/01 00:57 You can't have nested fixed points, for instance. 20/01 00:57 is that for mutual inductives? 20/01 00:57 (I think you can code mutuals using an single indexed inductive) 20/01 00:57 (that wouldn't cover munu though) 20/01 00:58 Well, NAD has an agda example: mu X. nu Y. Y + X. 20/01 00:58 Which doesn't work in Agda, anyway, but the opposite nesting does. 20/01 00:58 I don't 'understand' ind-rec but Peter Dybjer has some papers about giving a codification (similar to Desc) for it.. I'm sure implementing that would (make one go bald and) be illuminating 20/01 00:59 and Anton Setzer 20/01 00:59 Yeah, I have a bunch of papers by them that I've been meaning to read. 20/01 00:59 still don't have much clue what's going on in Cochon anyway, the asciiproximation they do is kind of painful to read/understand 20/01 01:02 Anyhow, maybe you can flatten mu X. mu Y stuff to a single (i)mu. I haven't thought about that much. 20/01 01:02 But I don't think you can do that for mu-nu, which is what I was thinking about trying out the other day, before I realized I couldn't think of a way of making it work. 20/01 01:03 I have a module of mu-nu stuff in Agda, but it needs Set : Set, because it uses encoding with forall/exists, which would require impredicativity to fit in Set. 20/01 01:05 is that on code.haskell or something? 20/01 01:06 I don't remember if I uploaded it. 20/01 01:06 Seems I did. 20/01 01:07 http://code.haskell.org/~dolio/agda-share/html/MuNu.html 20/01 01:07 bye 20/01 01:12 thanks 20/01 01:12 oaky, i checked the wiki a bit for this and can't find an answer: in "Dependent Types At Work" at the top of PDF page 12 it gives an example excercise to define the dependent sum type A + B with constructors inr and inl. how would one do this? would it be similar to the product type except when you inject somethin of type A then it'd be like < a, () > or what? it seems that the second position (for type B) would have to be indicated to be undefined someho 20/01 12:33 btw, nevermind the last question. i forgot that constructors won't normalize further. you'd simply patter match over inl a or inr b i suppose. silly me 20/01 12:51 guerrilla: yeah, it's just like Either in haskell 20/01 13:01 Saizan: yes, thanks for confirming that. i just figured that out :) 20/01 13:01 hehe 20/01 13:01 just a difference in notation i wasn't awake enough for 20/01 13:02 also, there's a bit of confusion between what's undestood by "dependent sum", while Either is commonly called a sum type or tagged union, "dependet sum" is commonly used for what looks like pairs, i.e. data \Sigma (A : Set) (B : A -> Set) where _,_ : (x : A) -> (B x) -> \Sigma A B 20/01 13:05 even if Agda's lib has the latter in Data.Product and the former in Data.Sum :) 20/01 13:05 and dependent products are dependent functions 20/01 13:06 so, it's quite a mess 20/01 13:06 -!- Saizan_ is now known as Saizan 20/01 13:56 sup 20/01 15:51 --- Day changed Thu Jan 21 2010 -!- mmm is now known as BMeph 21/01 03:46 since _, { and } are reserved symbols in Agda, it's not possible to use latex-style (e.g. non-UTF8) subscripting in literal Agda, is it? 21/01 10:10 I don't know of anyway to do it 21/01 10:17 ccasin: okay. i suppose that some postprocessing would solve the problem then 21/01 10:18 or maybe there's a mode in latex where you can use something other than { and } to indicate parameters/arguments to macros 21/01 10:19 i'll have to look into that 21/01 10:19 I mean, certainly you can use it in the literate parts 21/01 10:19 but I haven't found any way to add non-unicode subscripts to identifiers 21/01 10:19 if that was your question 21/01 10:19 yes it was 21/01 10:20 But, you could perhaps pick an arbitrary syntax for this in the agda and then use a %format pragma 21/01 10:22 yeah, going to try something like that right now 21/01 10:22 they can't be parameterized though (as far as I know) so you'd have to have one format clause for each subscript you want 21/01 10:22 or perhaps you could somehow be clever and make separate format clauses for the "_{" and the "}" parts 21/01 10:23 -!- opdolio is now known as dolio 21/01 21:52 -!- RichardO_ is now known as RichardO 21/01 21:52 -!- RichardO_ is now known as RichardO 21/01 23:53 --- Day changed Fri Jan 22 2010 -!- RichardO_ is now known as RichardO 22/01 05:50 -!- ertai is now known as npouillard 22/01 11:30 -!- npouillard is now known as ertai 22/01 11:43 -!- ertai is now known as npouillard[ertai 22/01 11:44 -!- npouillard[ertai is now known as npouillard 22/01 11:44 --- Log closed Fri Jan 22 13:02:28 2010 --- Log opened Fri Jan 22 13:02:32 2010 -!- Irssi: #agda: Total of 27 nicks [0 ops, 0 halfops, 0 voices, 27 normal] 22/01 13:02 -!- Irssi: Join to #agda was synced in 79 secs 22/01 13:03 -!- RichardO_ is now known as RichardO 22/01 14:44 -!- opdolio is now known as dolio 22/01 22:46 --- Day changed Sat Jan 23 2010 -!- Berengal_ is now known as Berengal 23/01 19:12 --- Day changed Sun Jan 24 2010 So, I've been thinking of writing a djinn-like proposition solving tactic thing in Agda. 24/01 09:12 Coming up with a good proposition+proof representation is tough, though. 24/01 09:12 are you indexing the proof terms with the proved proposition? 24/01 09:14 Yeah. 24/01 09:14 My difficulty is finding something such that I can easily lift something like "(P => Q) => ~ Q => ~ P" for some atomic proposition representation (probably Fin n for some n) into the Agda type "forall P Q -> (P -> Q) -> Not Q -> Not P", and turn associated proofs into values of that type. 24/01 09:17 i think the reflection module in the stdlib solves basically the same problem, wit the difference that the environment there is homogeneous 24/01 10:13 -!- EnglishGent is now known as EnglishGent^afk 24/01 10:26 Some of that is roughly what I've been trying to do. 24/01 10:26 I suppose I was trying to reify into types like "\all P Q R -> ..." instead of leaving P Q and R as parameters to a solve-like function. 24/01 10:28 yeah 24/01 10:35 http://64.131.71.66/fastcgi/hpaste.fcgi/view?id=16478#a16478 <- quite contorted 24/01 10:50 and in the terms you'd need an index for value-level variables too :) 24/01 10:50 Well, the solving's another whole enchilada. 24/01 10:53 I looked briefly at the code in djinn. There's a lot of it. 24/01 10:54 Way more than I expected. 24/01 10:54 yeah, i never got around to learning what it does 24/01 11:12 Well, I looked at the paper the algorithm is based on, although the paper itself doesn't describe any algorithm. 24/01 11:14 It just presents an alternate sequent calculus where all the rules result in structurally smaller sequents, and then you do backtracking search. 24/01 11:15 But djinn must have a lot more stuff going on, because that doesn't seem like it'd take that much code. 24/01 11:15 (Actually, djinn uses breadth-first search. 24/01 11:15 -!- EnglishGent^afk is now known as EnglishGent 24/01 11:22 hi all :) 24/01 11:28 hi 24/01 11:30 hello Saizan :) 24/01 11:36 -!- EnglishGent is now known as EnglishGent^bbl 24/01 11:38 -!- EnglishGent^bbl is now known as EnglishGent 24/01 16:08 -!- EnglishGent is now known as EnglishGent^afk 24/01 23:08 -!- copumpkin is now known as CoqLove 24/01 23:46 -!- CoqLove is now known as copumpkin 24/01 23:46 --- Day changed Mon Jan 25 2010 -!- lpsmith_ is now known as lpsmith 25/01 02:00 damn, we really need to introduce some form of "schematic" variables 25/01 12:32 just out of curiosity, are there many folks here from GU or Chalmers? 25/01 17:22 at least one! 25/01 17:41 looking at the user list, I know ski_ also studies there 25/01 17:42 you? 25/01 17:42 mikael: hah, yes, i didn't notice that :) 25/01 18:05 no, i'm in southern Sweden currently but going back to the US to study next semester 25/01 18:05 ah, okay - student exchange or just vacationing? 25/01 18:06 hmm, I guess nobody would vacation in southern sweden this time of year :-) 25/01 18:07 yeh, a bit cold :) 25/01 18:11 no, I've been working here for last 4 years 25/01 18:12 time to go finish my education now though 25/01 18:12 (I'm originally from the US, btw) 25/01 18:12 nice to get to combine travel and work!  I have vague plans to work in another country - feel like I should live in the US for at least a few years.  where are you from? 25/01 18:21 mikael: originally California 25/01 18:28 mikael: you? 25/01 18:28 i suppose /whois says .se :) 25/01 18:29 nice, I'd love to go there, work for Apple and spend my holidays reading beat poetry in the Yosemite park! 25/01 18:30 oh, yeah, I'm from Sweden, I come from further north (around Gävle) but live in Gothenburg and study at GU since 2006 25/01 18:31 ah yeah, i know Gavle 25/01 18:32 i think you're mixing California's 60's with it's 80's 25/01 18:32 :P 25/01 18:32 might want to try an internship or at least a vacation before up and go 25/01 18:33 * guerrilla loves .se :) 25/01 18:33 well, except this years winter :P 25/01 18:33 (usually barely snows in Blekinge) 25/01 18:34 hah, yeah, but I know a guy who graduated when I enrolled who got commit access to WebKit and ended up with a job in Cupertino :) 25/01 18:34 ah 25/01 18:34 well, i think i'll definitely be comming back here. unfortunately for the time being, there don't seem to be any undergraduate programs that work for me here 25/01 18:35 (in fact it seems there are none for math in english) 25/01 18:35 yeah, definitely gonna apply for some internships, or some exchange program.  anywhere'd be fine though :)  yeah, I dig winter as long as it's cold enough for permanent snow, not just wet sludge :( 25/01 18:35 yes, the sludge has been the worst this year imo 25/01 18:36 and sludge + random extreme swings in temp. = lots of ice on the roads 25/01 18:37 --- Day changed Tue Jan 26 2010 -!- Irssi: #agda: Total of 24 nicks [0 ops, 0 halfops, 0 voices, 24 normal] 26/01 11:40 -!- lpsmith_ is now known as lpsmith 26/01 22:55 --- Day changed Wed Jan 27 2010 -!- lpsmith_ is now known as lpsmith 27/01 06:05 -!- Saizan_ is now known as Saizan 27/01 11:03 -!- edwinb_ is now known as edwinb 27/01 11:43 http://progopedia.com/language/agda/ 27/01 21:49 well I guess that settles it 27/01 21:49 also 27/01 21:49 Elements of syntax: 27/01 21:49 Inline comments -- comment 27/01 21:49 Nestable comments {- ... -} 27/01 21:49 nice to know... that it has comments.. 27/01 21:50 -!- solidsna is now known as solidsnack 27/01 22:06 lol 27/01 22:37 --- Day changed Thu Jan 28 2010 -!- edwinb_ is now known as edwinb 28/01 08:39 if I have a function that proves a \== b, can I then simply get the proof that b \== a ? 28/01 09:47 even better, if there is some way I could use this in \==-Reasoning 28/01 09:47 I got the answer from stevan, sym is the function I was looking for 28/01 09:52 -!- opdolio is now known as dolio 28/01 12:48 -!- dolio is now known as opdolio 28/01 18:07 -!- opdolio is now known as dolio 28/01 18:07 -!- MissPiggy_ is now known as MissPiggy 28/01 19:28 --- Log closed Thu Jan 28 23:57:43 2010 --- Log opened Thu Jan 28 23:57:49 2010 -!- Irssi: #agda: Total of 28 nicks [0 ops, 0 halfops, 0 voices, 28 normal] 28/01 23:57 -!- Irssi: Join to #agda was synced in 81 secs 28/01 23:59 --- Day changed Fri Jan 29 2010 -!- lpsmith_ is now known as lpsmtih 29/01 01:20 -!- lpsmith_ is now known as lpsmith 29/01 05:58 -!- lpsmith_ is now known as lpsmith 29/01 15:29 -!- lpsmith_ is now known as lpsmith 29/01 16:20 -!- Berengal_ is now known as Berengal 29/01 17:28 --- Day changed Sat Jan 30 2010 --- Log closed Sat Jan 30 08:33:29 2010 --- Log opened Sat Jan 30 08:33:32 2010 -!- Irssi: #agda: Total of 8 nicks [1 ops, 0 halfops, 0 voices, 7 normal] 30/01 08:33 -!- Irssi: Join to #agda was synced in 79 secs 30/01 08:34 --- Day changed Sun Jan 31 2010 -!- lpsmith_ is now known as lpsmith 31/01 04:51 how to implement this function? ∣i-j∣≡∣j-i∣ : {i j : ℤ} → ∣ i - j ∣ ≡ ∣ j - i ∣ 31/01 10:21 -!- facsimile is now known as soupdragon 31/01 16:03

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