--- Log opened Fri Jan 01 00:00:34 2010
-!- copumpkin_ is now known as copumpkin01/01 00:20
copumpkinif I were to begin porting roconnor's computable reals to agda, should I call them computable reals (ugly, but correct) or just reals?01/01 22:04
copumpkinlike Data.Real? or Data.ComputableReal? Data.CReal (ugh)?01/01 22:04
dolioYou mean, in case someone implements non-computable reals in Agda?01/01 22:06
copumpkinwell, mostly just to pre-empt smartass comments about computability01/01 22:07
--- Day changed Sat Jan 02 2010
FunctorSalad:o prove what about omega? (omega monad?)02/01 00:25
copumpkinwell, prove that diagonal :: [[a]] -> [a] covers all elements in the input02/01 00:26
copumpkinI've been struggling with it on and off for a couple of weeks02/01 00:27
copumpkinprobably longer actually02/01 00:27
FunctorSaladhmm, using cantor's scheme?02/01 00:31
copumpkinsame as control-monad-omega02/01 00:31
FunctorSalad(seems to amount to showing that the pairing function N x N -> N is bijective)02/01 00:31
copumpkinI implemented the algorithm in agda and am trying to prove that if something is in one of the inner lists it will appear somewhere in the outer list02/01 00:31
FunctorSalad(then consider lists as functions N -> a)02/01 00:31
copumpkinI can't really do that02/01 00:32
FunctorSalad(but I don't know how easy all this is in agda)02/01 00:32
FunctorSaladerr I meant infinite lists02/01 00:32
copumpkinyeah, but I want to support finite lists too02/01 00:32
FunctorSaladoh right, you'd need omniscience to know beforehand which it is :)02/01 00:32
copumpkinyep02/01 00:33
FunctorSalad*looks at control-monad-omega*...02/01 00:36
luquisomeone going to write an omniscience module?02/01 00:39
copumpkinmaybe I should start again on the proof, it turned into this massive mess of lemmaNs for every bit I wasn't able to prove inline02/01 00:44
FunctorSaladluqui: I meant it in the sense "excluded middle" :)02/01 00:44
luquioh, well then it is reasonable to write such a module...02/01 00:45
FunctorSaladthere are some "principles of omniscience" which are weaker versions of LEM, IIRC02/01 00:45
copumpkinwell uorygl postulated not (not a) -> a02/01 00:45
FunctorSaladlike "every 0-1 sequence is constantly zero, or there is an index where it's one"02/01 00:46
FunctorSaladcopumpkin: that's full LEM, no?02/01 00:46
Saizani wonder if looking at the analogous proof for inductive lists (or vectors) would help02/01 00:49
FunctorSaladI thought copumpkin was working with inductive lists already02/01 00:51
copumpkinI am02/01 00:51
copumpkinoh wait02/01 00:51
copumpkincoinductive :)02/01 00:51
FunctorSaladoh right, different in agda02/01 00:51
copumpkinwell02/01 00:51
copumpkinthey have to be02/01 00:51
copumpkinI could probably relax the outer non-empty constraint actually now that I look at it02/01 00:53
copumpkincurrently I have diagonal : ∀ {a} → Colist⁺ (Colist⁺ a) → Colist⁺ a but it could probably just be diagonal : ∀ {a} → Colist (Colist⁺ a) → Colist a02/01 00:54
copumpkinbut I guess I can just take that on at the end02/01 00:54
copumpkin*tack02/01 00:55
-!- copumpkin is now known as pumpkin02/01 02:27
-!- pumpkin is now known as copumpkin02/01 02:28
-!- copumpkin_ is now known as copumpkin02/01 21:23
--- Day changed Sun Jan 03 2010
-!- copumpkin__ is now known as copumpkin03/01 00:26
soupdragonhi luqui nice blog post03/01 02:18
luquisoupdragon, thanks :-)03/01 02:28
-!- copumpkin_ is now known as copumpkin03/01 21:07
-!- copumpkin_ is now known as copumpkin03/01 22:02
--- Day changed Mon Jan 04 2010
-!- opdolio is now known as dolio04/01 01:34
-!- copumpkin_ is now known as copumpkin04/01 03:45
soupdragonhttp://www.e-pig.org/darcsweb?r=Pig09;a=headblob;f=test/Nat.pig04/01 12:48
copumpkin:o04/01 12:51
soupdragondolio?04/01 14:02
soupdragonhttp://www.cs.nott.ac.uk/~nad/listings/traces/Relation.Nullary.Negation.html04/01 15:17
soupdragonexcluded-middle : {P : Set} → ¬ ¬ Dec P04/01 15:17
soupdragonexcluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))04/01 15:17
soupdragonoh I get it04/01 15:18
copumpkin:)04/01 15:18
soupdragonI was baffled by this a second ago and was going to ask what the hell is going on here but I see it now04/01 15:18
Saizan"it's false!" "well, i have a proof.." "ah, ok, then it's true"04/01 15:25
copumpkinlol04/01 15:27
Saizan..but the world restarts from the point of the first answer when it gives you the second :)04/01 15:29
edwinb*thud*04/01 20:15
copumpkinoh yeah?04/01 20:15
edwinbSomehow all the pigweek participants have made it to the same place04/01 20:15
edwinbthis is a good start04/01 20:15
copumpkinnice!04/01 20:16
edwinbsome of them tried very hard not to manage it04/01 20:16
* copumpkin hopes to see lots of bacon04/01 20:16
edwinbme too04/01 20:16
edwinbwe have Dr Agda here too04/01 20:16
copumpkinis that Ulf?04/01 20:16
edwinbindeed04/01 20:16
copumpkinvery nice04/01 20:16
kosmikusedwinb: have fun :)04/01 20:31
--- Log closed Tue Jan 05 01:10:07 2010
--- Log opened Tue Jan 05 01:10:21 2010
-!- Irssi: #agda: Total of 2 nicks [0 ops, 0 halfops, 0 voices, 2 normal]05/01 01:10
-!- Irssi: Join to #agda was synced in 84 secs05/01 01:11
--- Log closed Tue Jan 05 01:15:42 2010
--- Log opened Tue Jan 05 01:15:47 2010
-!- Irssi: #agda: Total of 2 nicks [0 ops, 0 halfops, 0 voices, 2 normal]05/01 01:15
-!- Irssi: Join to #agda was synced in 96 secs05/01 01:17
-!- You're now known as Laney05/01 01:27
-!- Berengal_ is now known as Berengal05/01 01:27
luquicopumpkin, ping?05/01 08:34
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=15623#a1562305/01 08:59
dolioHold on, those don't need to be mutual. :)05/01 09:00
copumpkinluqui: pong05/01 09:35
luquicopumpkin, were you the one who observed the fallacy "X imples Y, Y is undesirable, therefor not X"05/01 09:37
copumpkindon't think so, but I remember seeing someone say that05/01 09:37
copumpkinor maybe it was05/01 09:37
* copumpkin just woke up05/01 09:37
luquiheh, i could have sworn it was you. i know it was on twitter, but i couldn't find it in your feed.05/01 09:38
luquioh well05/01 09:38
dolioThat's a pretty common argument.05/01 09:38
luquiduh, should have looked in my retweets.  it was kowey.05/01 09:39
dolioAlso, I'm going to beat copumpkin at proving diagonals. :)05/01 09:39
copumpkindamn!05/01 09:39
luquimy memory is as reliable as the contents of an array in a C program05/01 09:39
copumpkinwell, at least someone will do it :)05/01 09:39
luquidolio, cool.  let me know when you finish so i can reference it in control-monad-omega :-)05/01 09:40
luquialso because i'd like to see it05/01 09:40
dolioI'm still writing down what \in means for various things, so you've got some time. :)05/01 09:40
copumpkinhah, I've stopped trying for now, but I'll be interested to see how you do it05/01 09:40
dolioI pasted my diagonalization function earlier. It's probably different than yours.05/01 09:41
dolioAnd I hope easier to prove about.05/01 09:41
copumpkinit looks way better, without that nasty intermediate language shit05/01 09:41
dolioYeah.05/01 09:41
copumpkinbah, need to shower and go do stuff with parents, *sigh*05/01 09:44
soupdragonluqui I don't quite get it do you know an example?05/01 09:44
copumpkinbbl05/01 09:45
doliosoupdragon: Evolution implies eugenics, eugenics is undesirable, therefore evolution is false.05/01 09:45
soupdragonEvolution implies eugenics???05/01 09:46
dolioYeah, well, no one said you couldn't have fallacies *and* false premises.05/01 09:46
soupdragonobviously that's a double negative so the conclusion is true05/01 09:49
luqui1=2,  x=y implies x+1=y, therefore 2=205/01 09:51
luquiclearly double negation is correct logic.  it gives the right answer!05/01 09:52
luquis/double negation/double fallacy/05/01 09:52
copumpkinlol05/01 09:53
dolioWoo, 1/4 of the way there.05/01 10:49
copumpkinnice05/01 10:51
copumpkinI really should've picked a better diagonal function before trying to prove something about it05/01 10:51
copumpkinI still kind of hope you run into my unknown goal issue, so you can suggest a better way to display them on the mailing list :P05/01 10:52
dolio1/205/01 11:23
dolioActually, it may be 2/5.05/01 11:25
luqui8/17?05/01 11:31
dolioWell, I need about one proof for each xs \in xss.05/01 11:32
dolioIn the one there's just two lists-of-colists, but in the other there are those plus a colist of colists.05/01 11:32
dolioI've proved one function correct, though.05/01 11:33
luqui:-)05/01 11:33
dolioSo, a finite union of countable sets is countable. Ta-daa. :)05/01 11:41
dolioI guess that's not one of the exciting ones.05/01 11:41
luquievery theorem in agda is still exciting to me05/01 11:42
dolioGuess what: http://code.haskell.org/~dolio/agda-share/html/ZigZag.html05/01 12:34
luquiwow, those  ∈ lemmas are pretty nasty05/01 12:39
dolioThey look nastier than they actually are.05/01 12:40
luquiwow, nice05/01 12:43
dolioAt least, the last three were easy after the first two.05/01 12:43
luquii would need to study this for a while to grok it05/01 12:43
dolioSince they're all pretty much the same, and I just had to get the hang of them.05/01 12:43
-!- copumpkin_ is now known as copumpkin05/01 14:22
copumpkin:O05/01 17:19
Saizanmh, so dolio's zig-zag is the same as copumpkin's diagonal?05/01 18:05
-!- copumpkin_ is now known as copumpkin05/01 19:11
copumpkinSaizan: apparently05/01 19:42
Saizanwhich i guess passes the termination checker because it's written in a lower-level style05/01 19:45
copumpkinprobably05/01 19:45
copumpkinor just cause he's l33ter05/01 19:45
dolioThey're roughly the same.05/01 21:28
dolioThey probably don't produce results in the same order.05/01 21:29
doliotake 20 pairs ==> (0,0)::(0,1)::(1,0)::(1,1)::(0,2)::(2,0)::(2,1)::(0,3)::(1,2)::(3,0)::(3,1)::(1,3)::(0,4)::(2,2)::(4,0)::(4,1)::(2,3)::(0,5)::(1,4)::(3,2)::[]05/01 22:00
dolioStarting with, essentially [[(0,0),(0,1),(0,2)...], [(1,0),(1,1)...] ...].05/01 22:01
--- Day changed Wed Jan 06 2010
copumpkindolio: did you succeed in proving it too?06/01 00:13
dolioYes.06/01 00:13
copumpkincool :)06/01 00:13
doliohttp://code.haskell.org/~dolio/agda-share/html/ZigZag.html06/01 00:13
copumpkinholy crap :P06/01 00:14
copumpkinvery nice06/01 00:14
dolioIncidentally, I had goals like x \in y :: .ZigZag.#-106/01 00:15
copumpkindid you just reason about what they should be?06/01 00:16
dolioThat meant I needed to insert 'later ?'.06/01 00:16
copumpkinoh yeah, I needed stuff like that too06/01 00:16
copumpkinbut sometimes it didn't know enough for a later but still had nasty unnamed #s06/01 00:16
copumpkinI guess the answer is to figure out how to make it know enough for a later06/01 00:17
dolioWell, I never encountered those, luckily.06/01 00:17
copumpkinI guess the real answer is, if you want to prove something about something complicated, don't. Just make it simpler and try again :)06/01 00:17
copumpkinand/or call dolio06/01 00:17
dolioFinding the right algorithm to prove things about is worth days trying to prove the wrong algorithm.06/01 00:18
copumpkinyeah :)06/01 00:19
copumpkinI'll keep that in mind next time06/01 00:19
Saizanwhat is later?06/01 00:19
copumpkinthe item is in the list, but not at the head06/01 00:20
Saizanah, i didn't see it in the code06/01 00:20
dolioIt's those lovely walls of code.06/01 00:27
copumpkinI'm impressed though06/01 00:27
copumpkintime for some language work, I guess :)06/01 00:27
-!- copumpkin____ is now known as copumpkin06/01 04:12
-!- copumpkin__ is now known as copumpkin06/01 04:38
--- Day changed Thu Jan 07 2010
copumpkinzomg postulated excluded middle07/01 00:03
dolioMan, why is ACM always the #1 paper hit.07/01 01:57
copumpkindolio: I think I have a proxy running on my college computer that I set up for mmorrow a while back. I can let you on it if you want07/01 01:58
copumpkinbut it's not trying very hard to be transparent so I think some sites notice it07/01 01:59
dolioI just always get excited when I see the paper I'm looking for as the first google hit.07/01 02:00
dolioAnd I forget to notice that it's an ACM link before I click it and waste my time.07/01 02:00
copumpkinah07/01 02:00
dolioAlthough this paper may in fact not be available.07/01 02:01
dolioSo, I don't think J in that guy's mail can be written without LEM.07/01 02:01
dolioBut injectivity of type constructors does seem to be a non-classical axiom, I guess.07/01 02:02
dolioOr anti-classical, or whatever you want to call it.07/01 02:02
Saizanif i could write a function Set -> Set -> Set, that pattern matches on the I constructor and return the type function, then i could use my constructive diagonalization module07/01 02:24
dolioYes, but you can't do that.07/01 02:25
Saizanyeah, but i'm not so sure you can't come up with something using reflection07/01 02:28
-!- copumpkin_ is now known as copumpkin07/01 13:09
guerrillais it not possible to construct lists in Agda using the form [a , b , ... ] ?07/01 13:12
copumpkinno07/01 13:14
copumpkinwell, you could probably make some weird mixfix for it07/01 13:14
copumpkinbut what about the Enum typeclass?07/01 13:14
copumpkinyou could do it monomorphically07/01 13:14
dblhelixguerrilla: with some trickery, I suppose you could define write it like [ a , b , ... ]07/01 13:14
copumpkin[_,_..] :: Nat -> Nat -> Colist Nat07/01 13:14
guerrillayeah07/01 13:15
guerrillaok, no big deal, i was just surprised it wasn't part of the lib07/01 13:15
copumpkinI would like to see the ability to have basic list literals at least07/01 13:15
guerrilla(just trying to create some nice notation for a DSL to specify context-free grammars)07/01 13:15
dblhelixah, too bad.. I was hoping we were going to define [, _,_, and ] now :)07/01 13:15
soupdragonhow do you define context-free grammars07/01 13:15
guerrillahaha07/01 13:16
copumpkindblhelix: I did something like that once07/01 13:16
guerrillasoupdragon: you want the formal definition?07/01 13:16
soupdragonyeah07/01 13:16
copumpkinit worked but wasn't very pretty07/01 13:16
dblhelixcopumpkin: conor did something for semantic brackets ([[...]]) in Haskell, iirc07/01 13:16
copumpkinoh yeah, you sort of get those with -XArrows07/01 13:16
copumpkinidiom brackets07/01 13:17
guerrillasoupdragon: a 4-tuple, (N, T, R, S) where N is a set of nonterminal symbols, T is a set of terminal symbols, R is a set of production rules of the form N -> (N \cup T)* and S is a distinguished root symbol07/01 13:17
soupdragonheh just let ([) = id, (,) = cons and (]) = nil07/01 13:17
copumpkinhe put them into his preprocessor too07/01 13:17
guerrillasoupdragon: essentially a grammar with the restriction that the right-hand side (head) of each production rule is a single non-terminal07/01 13:17
soupdragonguerrilla but in Agda how does that look?07/01 13:17
guerrillasoupdragon: i don't know yet, i'm still trying to figure that out myself07/01 13:18
dblhelixsoupdragon: not enough... then you'll end up writing [ 1 , 2 , 3 , ]07/01 13:18
dblhelixsoupdragon: note the extra comma07/01 13:18
copumpkinguerrilla: ooh, you might have a use for dolio's zigzag :)07/01 13:18
guerrillai plan to define the terminals and nonterminals as data types (sets) and then i am right now working on constructors for production rules07/01 13:18
guerrilla(hence the ',' question)07/01 13:18
copumpkinguerrilla: I was working on something similar for regular languages07/01 13:18
copumpkinbut stopped to shave the diagonalization yak07/01 13:18
copumpkin(which I failed to do)07/01 13:18
guerrillawhat's "dolio's zigzag"?07/01 13:19
copumpkinhttp://code.haskell.org/~dolio/agda-share/html/ZigZag.html07/01 13:19
copumpkinfair merging of infinite lists of infinite lists07/01 13:19
copumpkinI was going to use it for enumerating my regular languages07/01 13:20
guerrillahmmm07/01 13:20
soupdragonguerrilla what will you do with context-free grammars in agda? :)07/01 13:20
copumpkintransform them to PDAs07/01 13:21
copumpkin!!07/01 13:21
guerrillasoupdragon: it's just a stepping stone to creating a fully typed system for creating LR-parser/generater pairs (pushdown transducers) automatically out of attribute grammars07/01 13:21
guerrillaindeed07/01 13:21
guerrillahehe07/01 13:21
guerrillare copumpkin07/01 13:21
soupdragoncool07/01 13:22
copumpkinbut you should enumerate them too cause it's cute, and gives you a simple way to define whether a string is in the language07/01 13:22
guerrillawe'll see07/01 13:22
guerrilla:)07/01 13:22
guerrillajust trying to get comfy with agda first.. see what i can get out of it07/01 13:22
copumpkin:)07/01 13:24
copumpkinbbl07/01 13:25
roconnorDoes agda have a cumaltive heirarchy07/01 16:31
roconnorie if x : Set then is x : Set1 and x : Set2 etc?07/01 16:32
soupdragonno07/01 16:34
soupdragonwell it didn't used to... I don't know if it does now07/01 16:35
soupdragon(but I don't think so)07/01 16:35
Saizan_no, even with universe polymorphism you need a wrapper to go from Set to Set107/01 16:45
Saizan_well, Set i to Set (i + n)07/01 16:46
roconnorok07/01 16:51
roconnoranyhow, I can't extend Chung-Kil's proof to a flat out contradiction because I don't have impredicativity.07/01 16:52
soupdragonaww :(07/01 16:52
roconnorbut it does make me appreciate how crazy Coq's impredicativity is07/01 17:06
-!- roconnor_ is now known as roconnor07/01 19:41
copumpkinomg Coquand on the agda mailing list :o07/01 21:45
--- Day changed Fri Jan 08 2010
-!- lpsmith_ is now known as lpsmith08/01 01:10
doliocopumpkin: I think he goes to the implementor meetings, too.08/01 01:49
copumpkinoh neat08/01 01:49
guerrillaso, my first try at creating a notation for context-free grammars in Agda: http://www.pastebin.ca/174277808/01 14:51
guerrillanot really satisfied on the appearance but should be functional anyway :)08/01 14:51
soupdragonwhen you define  contextFreeProductionRuleBody_08/01 14:52
soupdragonmaybe it's possible to just do  contextFreeProductionRuleBody  ?08/01 14:53
soupdragonI mean without the underscore08/01 14:53
guerrillathe _ is the parameter for the list that that constructor takes08/01 14:53
guerrillaor did i misunderstand something?08/01 14:53
soupdragonno I don't think you did08/01 14:54
guerrillaah, apparently it works without the _ as well. odd08/01 14:54
Saizan_foo_ defines foo as a prefix operator08/01 14:54
guerrillaright08/01 14:55
soupdragonwhy08/01 14:55
soupdragon#08/01 14:55
soupdragon        B := '0'08/01 14:55
soupdragon#08/01 14:55
soupdragon        B := '1'08/01 14:55
soupdragonrather than08/01 14:55
Saizan_while just foo defines it as a normal function08/01 14:55
soupdragonB := '0' | '1'08/01 14:55
soupdragon?08/01 14:55
Saizan_(syntax wise)08/01 14:55
guerrillaSaizan_: thanks08/01 14:55
soupdragonis it possible to install agda using cabal?08/01 14:56
guerrillasoupdragon: because the separation of the two is equivalent to the mathematical model A := B | C is just an unimportant syntactic abstraction08/01 14:56
soupdragonguerrilla, I wonder if this is useful to you08/01 14:57
soupdragondata Fin : Nat -> Set where08/01 14:57
soupdragon fz : forall {n} -> Fin (S n)08/01 14:57
soupdragon fs : forall {n} -> Fin n -> Fin (S n)08/01 14:57
soupdragonthe idea is that Fin 0 = {}, Fin 1 = {fz}, Fin 2 = {fz,fs fz} and so on08/01 14:57
Saizan_soupdragon: yes, "cabal install Agda" should work and "cabal install agda-executable" if you want the stand-alone compiler08/01 14:58
guerrillasoupdragon: how does this relate?08/01 14:59
soupdragonguerrilla well it just occured to me08/01 14:59
soupdragonit might not08/01 14:59
Saizan_guerrilla: instead of using a fixed enumeration for the terminal and non-terminal symbols08/01 14:59
Saizan_guerrilla: or you could be parametric in those types, but at that point you'd probably require some equality predicate for the members08/01 15:00
soupdragonis parsing CFG decidible??08/01 15:00
soupdragonwow08/01 15:01
guerrillasoupdragon: if by parsing you mean recognizing whether a word belongs to the language generated by grammar or not, then yeah08/01 15:01
copumpkinyou can also do more than that with CFGs08/01 15:01
copumpkinsome things about them are undecidable, but you can do a fair amount of interesting stuff with them08/01 15:01
guerrillaSaizan_: yeah, i was thinking that.. but i figured this is the closest thing to the tradtional meaning of set membership08/01 15:02
guerrillanot sure though08/01 15:02
soupdragonguerrilla it's kinda interesting to consider derivations of a parse08/01 15:02
guerrillacopumpkin: yeah, one thing that comes to mind is that deciding language equality for two cfgs is undecidable08/01 15:03
guerrillain general08/01 15:03
copumpkinyeah08/01 15:03
guerrillacopumpkin: do you know what an attribute grammar is?08/01 15:04
copumpkinthere are some sad undecidable problems :(08/01 15:04
copumpkinguerrilla: I glossed a paper (from UU I think) a while ago and know the basic idea, but haven't worked with them before08/01 15:05
guerrillaim wondering if you can prove that each L-attributed attribute grammar is equivalent to some context-free grammar (i can by intuition imagine that you "flatten out" an AG into a CFG by enumerating each value in each attribute)..08/01 15:05
soupdragonif you think about a simple concrete case first of all08/01 15:05
soupdragonmaybe08/01 15:05
guerrillanot important, just a curiosity08/01 15:05
copumpkinsoupdragon: maybe what?08/01 15:06
soupdragon<P> ::= epsilon | '(' <P> ')' <P>08/01 15:06
soupdragonis that the one for well parenthesized expressions?08/01 15:06
guerrilladepends on what you mean i suppose08/01 15:06
guerrillahehe08/01 15:06
guerrillaif you consider stuff like ()() valid, than yeah08/01 15:06
guerrillas/than/then08/01 15:06
copumpkinit's called Dyck iirc08/01 15:07
guerrillaah yes, for all "balanced" parenthesis08/01 15:07
guerrillacopumpkin: 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
copumpkinah08/01 15:14
copumpkinwhat are you going to prove?08/01 15:15
guerrillanothing actually, i'm only constructing a mathematically-founded counterexample for pattern-based computer virus detection08/01 15:18
guerrillabased on this paper: http://www.waset.org/journals/waset/v26/v26-1.pdf08/01 15:19
guerrillahaving such a system turns out to have a lot of other applications, but that was the initial inspiration anyway08/01 15:19
guerrilla(err, by system i mean a system where you can easily syntactically rewrite a string while preserving its semantic equivalence)08/01 15:21
guerrillabut i suppose if i can't find a proof that i can reference for my premise, i may attempt to tackle that08/01 15:22
soupdragon<P> ::= epsilon | '(' <P> ')' <P>08/01 15:22
guerrillayeah08/01 15:23
copumpkinguerrilla: interesting08/01 15:23
guerrilla09:07 < copumpkin> it's called Dyck iirc08/01 15:23
guerrilla09:07 < guerrilla> ah yes, for all "balanced" parenthesis08/01 15:23
guerrillahttp://en.wikipedia.org/wiki/Dyck_language08/01 15:23
soupdragonso a derivation for this is going to be08/01 15:23
soupdragonhm08/01 15:24
guerrillacopumpkin: 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 done08/01 15:24
soupdragonwell either08/01 15:24
copumpkin:)08/01 15:24
soupdragondata Dyck : String -> Set where08/01 15:24
soupdragon  empty : Dyck []08/01 15:24
soupdragon  wrappend : Dyck m -> Dyck n -> Dyck ("("++m++")"++n)08/01 15:24
soupdragonor the same thing without the String index08/01 15:25
guerrillacopumpkin: 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
soupdragondoesn't really matter08/01 15:25
copumpkinguerrilla: sounds great08/01 15:25
soupdragonor does it?08/01 15:25
soupdragonI don't think it does08/01 15:25
soupdragonanyway the point is:  Here's just one CFG -- what you are doing is programming in a generic way, over all CFGs08/01 15:26
soupdragonthat's all I wanted to say :)08/01 15:28
opdolioIncidentally, 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
soupdragonsimple expressions without binding (but with some finite set of variables) like "("++m++")"++n might be replaced by "("++#0++")"++#108/01 15:30
guerrillaopdolio: that's great to know, thanks08/01 15:30
soupdragon(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 dolio08/01 15:30
soupdragonI hope that I have said something meaningful08/01 15:33
soupdragonI know it made sense inside my head08/01 15:33
copumpkinI think I get it08/01 15:34
soupdragonthe set theoretic definitions of CFG are probably very awkward in the type theory08/01 15:36
soupdragonalthough, it's going to be really difficult no matter what08/01 15:36
soupdragonat least I don't really have the hang of this programming stuff yet08/01 15:36
guerrillanor I08/01 15:37
guerrillasoupdragon: yeah, i spent a few days looking into it from a pure set-theoretic view08/01 15:37
guerrillait's not that bad08/01 15:37
guerrillait's just not very convenient08/01 15:37
soupdragondata Dyck : Set where08/01 15:39
soupdragon empty : Dyck08/01 15:39
soupdragon wrappend : Dyck -> Dyck -> Dyck08/01 15:39
soupdragonthat's okay but for something like08/01 15:40
soupdragon<A> ::= epsilon | 'a' <B> 'a'08/01 15:40
soupdragon<B> ::= epsilon | 'b' <A> 'b'08/01 15:40
soupdragonmutual08/01 15:41
soupdragon data A : Set where emptyA : A ; wrapA : B -> A08/01 15:41
soupdragon data B : Set where emptyB : B ; wrapA : A -> B08/01 15:41
* guerrilla doesn't know what mutual means yet08/01 15:42
guerrilla?08/01 15:42
soupdragonit means they are both defined together08/01 15:42
soupdragonoops08/01 15:42
soupdragon data B : Set where emptyB : B ; wrapB* : A -> B08/01 15:42
soupdragoncorrection08/01 15:42
dolioWithout mutual, you can only refer to things that come prior in the source file.08/01 15:42
guerrillaright, that makes total sense08/01 15:42
guerrillagot it08/01 15:42
soupdragonbut it will be easier to use,08/01 15:43
soupdragondata AB : Fin 2 -> Set where08/01 15:43
soupdragon emptyA : AB #0 ; wrapA : AB #1 -> AB #008/01 15:43
soupdragon emptyB : AB #1 ; wrapB : AB #0 -> AB #108/01 15:43
soupdragonit says here Fin 2 meaning we have 2 different rules08/01 15:43
soupdragon(A and B)08/01 15:43
soupdragonyou can see in general.. for n rules it's just Fin n08/01 15:43
soupdragonso that's nicer08/01 15:44
guerrillaah08/01 15:44
dolioAB = Fin 2 * Nat08/01 15:44
soupdragonyou might also find the pattern in the constructors08/01 15:44
soupdragonit's just a list of lists of Fin 2's08/01 15:44
soupdragon[#0], [#1,#0], [#1], [#0,#1]08/01 15:45
soupdragonwe see there are 4 rules so Fin 4 can index a rule08/01 15:45
guerrillaok08/01 15:45
soupdragonmaybe some kind f generic tree type, which takes {2,4,[#0], [#1,#0], [#1], [#0,#1]} as signature08/01 15:45
soupdragoner08/01 15:45
soupdragon{2,4,{[#0], [#1,#0], [#1], [#0,#1]}} that's better08/01 15:45
soupdragonbut this loses the information about the strings08/01 15:46
guerrillathis seems like a rather awkward system to encode stuff in :\08/01 15:46
guerrillaor?08/01 15:47
soupdragonguerrilla that's hard to say08/01 15:55
soupdragonabout if it's awkward to encode stuff in08/01 15:55
guerrillarather subjective08/01 15:55
soupdragonif you know of some other generic notations then we could consider the complexity of conversions between them08/01 15:55
guerrillabut if i may digress a little bit, i can show you an example of the ideal input and state some facts about it08/01 15:56
soupdragonyes08/01 15:56
guerrillausing an ascii version of extended attribute grammar syntax:08/01 15:57
guerrilla                        p = <add \inh v:val32 \inh r:reg32> -> <addb \inh v:val8 \inh r:reg32>08/01 15:57
guerrillaadd and addb are nonterminals08/01 15:58
guerrillagenerated by a disassembler, lets supppose08/01 15:58
guerrillanow08/01 15:58
guerrillawait, actually08/01 15:58
guerrillathis is a terrible example08/01 15:59
guerrillahehe08/01 15:59
soupdragondon't rush :)08/01 15:59
guerrillaok, lemi just write this. 1sec08/01 15:59
guerrillahere, this is much better08/01 16:04
guerrillathunkers.net/~guerrilla/eag.pdf08/01 16:04
guerrillaerr, http://thunkers.net/~guerrilla/eag.pdf08/01 16:04
guerrilla<- meaning assignment and = meaning value equality08/01 16:04
guerrillaproper nonterminals in bold08/01 16:04
guerrillaaddl.v means the attribute names v of the symbol named addl08/01 16:04
soupdragonthis is confusing me08/01 16:04
guerrillaok?08/01 16:05
soupdragonwhat are the up arrows?08/01 16:05
guerrillaif you think in terms of a parse tree, its essentially propogating that semantic information (that attribute) "upwards"08/01 16:06
guerrilla\up e denots a synthesized attribute with an expression e08/01 16:06
soupdragonokay08/01 16:06
guerrillaso like <B \up b> --> <A \up a> is like saying B.b <- A.a08/01 16:07
guerrillathis should be familiar if you ever used Yacc, bison, antlr, or any of those parser generators08/01 16:07
guerrillait's a generalisation of that same method of passing up information when doing parsing08/01 16:08
guerrillaso, in essence it gives you context-sensitivity without needing to abandon context-free grammar's notation completely08/01 16:08
guerrillaanyway08/01 16:09
guerrillamy 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 PDA08/01 16:10
guerrillapoint 1, i suppose i didn't mention before - that the language should be able to operate on itself. sorry about that08/01 16:11
guerrillathat's i think why i got put off by the Fin version08/01 16:11
soupdragonwoah08/01 16:11
soupdragoncan you tell me more about that08/01 16:11
guerrillawhich part08/01 16:11
soupdragonit can operate on itself08/01 16:11
guerrillaah08/01 16:11
guerrillaone 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 rules08/01 16:12
soupdragonthat sounds really cool08/01 16:13
guerrillaits 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
guerrillas/counter//08/01 16:14
guerrillait moves the problem of detection from NP to undecidable08/01 16:15
guerrillaand in fact, is the only theory that means "metamorphic" like we mean in english08/01 16:15
guerrillaother so-called metamorphic viruses are just extremely coplex polymorphic viruses if you go by the dictionary definitions anyway08/01 16:16
soupdragonwow08/01 16:16
soupdragonso how does it operate on itsself are there examples?08/01 16:16
guerrillayeah, lemi see. i just saw an example in my notes08/01 16:17
guerrillathe 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
guerrillaso08/01 16:19
guerrillafor example08/01 16:19
guerrilla                We can change the rule08/01 16:19
guerrillasorry, it uses the stupid ascii version of EAG-syntax08/01 16:19
guerrilla                        p0 = <add \syn (v + 1):val32 \syn r:reg32> -> <addl \syn v:val32 \syn r:reg32> <incl \syn r:reg32>08/01 16:19
guerrilla                to be08/01 16:19
guerrilla                        p0 = <add \syn (v + 1):val32 \syn r:reg32> -> <subl \syn (-v):val32 \syn r:reg32> <incl \syn r:reg32>08/01 16:19
guerrillabut \syn = uparrow08/01 16:19
guerrillai added type annotations in this case for other purposes (:val32) but you can ignore that08/01 16:19
guerrillathe idea stands08/01 16:19
guerrillayou can replace the rule with a new rule that is sem. equiv08/01 16:19
guerrillajust in the same way you can replace seq.s of instructions08/01 16:20
soupdragonhow is that semantically equivalent?08/01 16:20
guerrillaadding a value to a register is the same as subtracting that value negated from a register08/01 16:20
soupdragonoh08/01 16:20
soupdragonI didn't notice it went from addl to subl, I see08/01 16:20
guerrillaright08/01 16:20
soupdragonbut there's an AG which expresses that transform?08/01 16:21
guerrillathat would be a rule in an AG08/01 16:21
guerrillaan attributed context-free prod. rule08/01 16:21
guerrilla(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
guerrillaoh wait, i missed what you asked08/01 16:23
guerrillayes08/01 16:23
guerrillathere would be other rules to do those type of transforms08/01 16:23
guerrillain a second grammar08/01 16:23
guerrilla(or if you wana go insane, part of the same grammar)08/01 16:24
soupdragon:D08/01 16:24
guerrillabut essentially you have G1 which can manipulate instrs, G2 which can manipulate grammars. so G2 can manipulate G1 and G208/01 16:24
guerrillasince both G1 and G2 are grammars08/01 16:24
guerrillameh08/01 16:24
* guerrilla done wasting channel bandwidth08/01 16:25
guerrillahehe08/01 16:25
soupdragonno this is good08/01 16:25
guerrillahehe ok08/01 16:25
soupdragonI am just trying to keep up08/01 16:25
soupdragonso the way it operates on other grammars imposes some particular structure/representation of these grammars?08/01 16:29
guerrillayes08/01 16:29
guerrillasorry i have to afk for a while (real work calls)08/01 16:31
-!- mak__ is now known as comak08/01 16:44
-!- lpsmith_ is now known as lpsmith08/01 16:48
solidsnacklarrytheliquid: Any luck getting categories stuff into Agda?08/01 18:11
copumpkinsolidsnack: there have been several attempts to do it as far as I know, but agda tends to gobble up all your memory to typecheck them08/01 18:12
solidsnackcopumpkin: What kind of stuff are you talking about?08/01 18:12
larrytheliquidsolidsnack: just working through exercises in the barr book08/01 18:13
copumpkinjust basic CT definitions and theorems, as far as I know08/01 18:13
solidsnackcopumpkin: Hmm.08/01 18:13
copumpkinI know that dolio tried it and ccasin did too08/01 18:13
soupdragonbarr book ??08/01 18:13
copumpkinI wrote something really basic a while back too08/01 18:13
larrytheliquidi 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
dolioMemory starts getting tight around products, for me.08/01 18:13
copumpkinsoupdragon: barr+wells notes?08/01 18:13
solidsnacksoupdragon: Category Theory for Computing Science08/01 18:13
copumpkinah08/01 18:13
solidsnackWe have a groud reading it in in San Francisco.08/01 18:14
larrytheliquidsolidsnack: ah who are you?08/01 18:14
solidsnacklarrytheliquid: I am Jason Dusek.08/01 18:14
larrytheliquidcool08/01 18:14
soupdragondude category theory is too hard08/01 18:14
copumpkinlol08/01 18:14
* copumpkin goes shopping08/01 18:15
solidsnacksoupdragon: I fear we have no choice.08/01 18:15
solidsnacksoupdragon: There is no alternative.08/01 18:15
larrytheliquidsolidsnack: have you seen the curry-howard <-> categories <-> quantum computing paper?08/01 18:15
soupdragonI'll just grow my own potatos and live in the mountains if ti comes to that08/01 18:15
solidsnacklarrytheliquid: No.08/01 18:15
solidsnackWhat is the name of the paper?08/01 18:15
soupdragoni want to see that lol08/01 18:15
copumpkinmaybe through curry-howard-lambek?08/01 18:16
larrytheliquidhttp://math.ucr.edu/home/baez/rosetta.pdf08/01 18:16
copumpkinsomeone made some sort of quantum CCC?08/01 18:16
copumpkinah08/01 18:16
larrytheliquidi didnt expect to get interested in physics again haha08/01 18:17
dolioDon't forget the <-> logic <-> topology.08/01 18:17
larrytheliquidyup08/01 18:17
solidsnackI'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.pdf08/01 18:17
larrytheliquidthe chart at the end of the paper is a nice one-slide summary08/01 18:17
copumpkin"‘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
soupdragonnice to have lots more activity in this channel even if I don't know what the hell anyone is talking about08/01 18:18
solidsnackcopumpkin: Why is Cartesian an antonym of quantum?08/01 18:18
copumpkinsolidsnack: just a quote from the paper, beats me :)08/01 18:19
larrytheliquidalso, 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=JDdCHfOyiN3ZBCx5hxzNNQ08/01 18:19
larrytheliquidgrr google links08/01 18:19
larrytheliquidmath.ucr.edu/~mike/rosettaslides.pdf08/01 18:19
larrytheliquidthere08/01 18:19
dolioI seem to recall seeing something about categories related to physical theories not being cartesian.08/01 18:19
dolioBraided monoidal closed or something.08/01 18:19
dolioI may be making things up, though.08/01 18:20
dolioMaybe it was that paper, even. I haven't looked at it in a while.08/01 18:20
solidsnacklarrytheliquid: That's pretty neat.08/01 18:21
copumpkinone day I shall understand all this crap08/01 18:21
* copumpkin changes his nick to CTLove08/01 18:21
solidsnackI am rather pleased by the recent streams combinator package and the new regions package on Hackage.08/01 18:21
solidsnackThey 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 CategoryLove08/01 18:22
dolioHeh.08/01 18:22
CategoryLoveI shall read all the books and tomorrow I'll know it all08/01 18:22
dolioHelp me complete project Euler with categories!08/01 18:22
solidsnackCategoryLove: You are Wolfram now.08/01 18:23
-!- CategoryLove is now known as copumpkin08/01 18:23
soupdragondolio I started doing project euler in http://esolangs.org/wiki/IRP08/01 18:24
soupdragonhttp://projecteuler.net/index.php?section=profile&profile=InternetRelayProgrammer08/01 18:24
soupdragonbasically you ask people on IRC to solve problems for you08/01 18:24
copumpkinoh wow, that sounds like HaskellLove (and me)08/01 18:24
soupdragonit's remarkably difficult compared to just writin programs to do it :P08/01 18:24
soupdragonannoying 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
solidsnackWho is HaskellLove?08/01 18:25
copumpkinsoupdragon: :)08/01 18:25
copumpkinsoupdragon: you pay attention to #haskell still?08/01 18:26
solidsnackWAT?08/01 18:26
larrytheliquidi thought it would be neat to try collaborative theorem proving via agda's goal system + making a googlewave bot that ran the compiler08/01 18:26
soupdragonno08/01 18:26
solidsnacklarrytheliquid: LOLz08/01 18:26
copumpkinsolidsnack: a kid (not terribly young) who wants to learn everything yesterday in #haskell08/01 18:26
soupdragon##algorithms #math #lisp #coq08/01 18:26
solidsnackIs doing categories stuff in other theorem provers easier/better?08/01 18:26
solidsnackI would like to know more about efforts to automate one's category theory homework, basically.08/01 18:27
soupdragonlarrytheliquid: I like the idea of an wiki style library of formal mathematics, but I wouldn't want to use agda for it08/01 18:27
solidsnackcopumpkin: Not young is like 25?08/01 18:27
copumpkinsolidsnack: he's 2108/01 18:27
copumpkinor claims o be08/01 18:27
solidsnackcopumpkin: Oh, okay.08/01 18:27
soupdragonit's always depressing when you find people that (1) you can't get along with (2) love the same things as you08/01 18:28
dolioInasmuch as they let you do bigger proofs without bringing your computer to its knees, probably.08/01 18:28
dolioOr more proofs, rather than bigger ones.08/01 18:28
solidsnackWhat is too much RAM, then?08/01 18:31
soupdragonlarrytheliquid: there's a couple projects like this cropping up but not sure if they're like, good, yet08/01 18:31
larrytheliquidnice, any links?08/01 18:31
dolioI have 2 GB.08/01 18:31
solidsnackLike, all the RAM on your laptop or all the RAM on a 16 core box at a math department?08/01 18:31
solidsnackOh, I see.08/01 18:32
soupdragonhttp://prover.cs.ru.nl/login.php08/01 18:47
soupdragonI can't remember the other one :/08/01 18:49
larrytheliquidcool thx08/01 18:50
soupdragonit's a great idea though08/01 18:50
copumpkinit'd be nice to have a builtin notation for fractional numbers08/01 21:50
copumpkinand a way to display values at compile time08/01 21:51
lpsmithunsafePerformIO from Template Haskell?08/01 21:52
copumpkinwell I mean if someone wrote a real module08/01 21:52
soupdragongreat idea lpsmith :P08/01 21:52
copumpkinthat is R08/01 21:52
copumpkinwe'd need a "show instance" for it08/01 21:52
soupdragonWhen 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 naturals08/01 23:11
copumpkinseems hard to convince agda that it terminates without doing that nasty type thing08/01 23:11
copumpkinand there's no unfold08/01 23:12
Saizanof all the naturals?08/01 23:12
copumpkinyep08/01 23:12
copumpkinall 1001 of them08/01 23:12
Saizani'm quite surprised that it's not straightforward08/01 23:12
copumpkinhttp://snapplr.com/3ryz08/01 23:13
copumpkinnot many utility functions in Colist08/01 23:13
Saizanwhat about natlist n = n :: \# natlist (n + 1); naturals = natlist 0 ?08/01 23:14
copumpkinthat works :)08/01 23:15
Saizani wonder if the termination checker is on par with the state of the art for coinductives08/01 23:18
* copumpkin is trying to figure out how to do left induction over colists08/01 23:37
copumpkinI wonder if I could do it as a foldl08/01 23:38
copumpkinprobably not, eh08/01 23:40
Saizanleft induction?08/01 23:42
copumpkinI have an infinite list of squares and I want to prove that they're all squares :)08/01 23:43
copumpkinjust to play with more coinduction08/01 23:43
Saizani think you've to define a coinductive version of All08/01 23:44
copumpkinyeah, there is one in Colist already08/01 23:44
copumpkinallSquares : All square squares08/01 23:44
copumpkinpretty nice eh08/01 23:44
Saizanheh, a bit lolcat-like :)08/01 23:45
copumpkinI think he left out foldr from Colist because it's pink08/01 23:45
Saizanwell, yeah, foldr it's definitely unsafe, you'd need to have a guarantee the folding function ignores its arguments at some point08/01 23:46
copumpkinyep08/01 23:46
Saizanbut unfoldr?08/01 23:47
copumpkinyou mean to unfold an All value?08/01 23:48
Saizanno on Colist, you said earlier there's no unfoldr08/01 23:50
copumpkinyeah, but what would I be unfolding?08/01 23:50
copumpkinI need an All square squares08/01 23:50
copumpkinI already have squares08/01 23:50
Saizanah, true, i was just disconnectly wondering why it's missing :)08/01 23:51
copumpkinah08/01 23:51
Saizanhow is squares defined?08/01 23:51
copumpkinscanl _+_ 0 odds08/01 23:51
copumpkinthat was my first encounter with induction a million years ago so I'm attached08/01 23:52
Saizanhah08/01 23:52
--- Day changed Sat Jan 09 2010
copumpkinah, it's probably smarter to use Stream for this09/01 00:02
copumpkinrather than colist09/01 00:03
copumpkinbut then it's missing an All type09/01 00:03
copumpkin*sigh*09/01 00:03
solidsnackcopumpkin: What do the `#' and `|' do in this code?09/01 00:13
copumpkinsolidsnack: the | is just my cursor09/01 00:14
copumpkin# lifts you into codata!09/01 00:14
solidsnackInteresting.09/01 00:14
copumpkinit's just a one-constructor data type09/01 00:14
copumpkinor codata type09/01 00:14
copumpkinthe type itself is \inf09/01 00:14
solidsnackIn Agda, `::' is `cons', right?09/01 00:14
copumpkinusually09/01 00:14
solidsnackWell, it doesn't mean `has type' in this case, right?09/01 00:15
copumpkinyeah, agda uses a single colon for type09/01 00:15
edwinb*zonk*09/01 00:25
copumpkinzonk!09/01 00:25
edwinbindeed09/01 00:28
edwinbI think we have just finished a productive PigWeek09/01 00:29
edwinbit is possible that when we get home we will figure out exactly where it is we've got to09/01 00:29
-!- solidsnack is now known as Guest4912209/01 01:55
-!- Saizan_ is now known as Saizan09/01 03:46
soupdragonI don't actually understand just what structure the self applicability critea imposes onto the representation09/01 07:53
dolioWas that in reference to something?09/01 07:58
soupdragonyeah09/01 07:58
soupdragonthe attribute grammar stuff09/01 07:58
dolioOh.09/01 07:58
dolioThey've got something to do with comonads.09/01 08:00
soupdragonoh god09/01 08:01
Saizanonly with memoization :)09/01 08:04
soupdragonI don't know I'm starting to think this programming stuff is just ridiculously difficult beyond all comprehension09/01 08:04
doliohttp://code.haskell.org/~dolio/agda-share/html/ZigZag.html now with stream proofs.09/01 10:21
dolioAll pairs of naturals are enumerable.09/01 10:21
Saizanmh, c.h.o is not responding09/01 10:46
opdolioIt's back up.09/01 11:10
-!- opdolio is now known as dolio09/01 11:10
copumpkindolio: very nice09/01 13:34
copumpkinnow you can show that crank that N x N is countable09/01 13:36
copumpkinis there any work on extracting code from agda to haskell or something?09/01 16:38
guerrillacopumpkin: doesn't one of the compilers do that?09/01 17:04
guerrillathe MAlonzo compiler, no?09/01 17:06
-!- copumpkin is now known as palomer09/01 21:27
-!- palomer is now known as copumpkin09/01 21:27
--- Day changed Sun Jan 10 2010
soupdragonhello Saizan10/01 09:47
Saizanhi10/01 09:47
soupdragonsomething like:  e1{x -> e2} => v  <-> (\x. e1) e2 => v10/01 09:47
soupdragon"Substitution Commutes"10/01 09:47
soupdragon[e]{x → [e']} = [e{x → e'}]10/01 09:48
Saizanoh, right10/01 09:49
Saizanwhich works well with an AST with named variables, so that \x. is trivial10/01 09:50
Saizanwould it still make sense if you use substitution to implement [_] or _=>_ ?10/01 09:54
soupdragonI think that you must :S10/01 09:55
* soupdragon gets angry at /haskell/10/01 09:59
soupdragon"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
soupdragoncrazy people10/01 10:04
dolioWhat do you think proofs are for?10/01 10:05
Saizanheh, he could look at the algorithm, and the proof of why the algorithm gives you a proof of the theorem10/01 10:05
Saizanfrom 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 it10/01 10:07
dolioI mean, there are several uses for proofs.10/01 10:07
dolioIf 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
dolioFor math proofs, you might use the proof to gain insight as to why the theorem is true.10/01 10:08
dolioAnd coq proof scripts appear to suck for the latter, on their own at least.10/01 10:09
soupdragonhttp://www.reddit.com/r/coding/comments/ajk0p/a_haskell_program_to_solve_a_sudoku_puzzle_pdf/10/01 10:09
dolioAt 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
Saizanand i guess the generated proof terms aren't much better10/01 10:12
dolioProbably not.10/01 10:12
soupdragonwell Ltac is TC so 10 lines of proof script can produce busybeaver(10) pages of lambda terms :D10/01 10:12
dolioThat'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
soupdragonyeah reflective proofs in general are great10/01 10:13
dolioInstead of "trans (trans (sym (cong (\x -> ...) foo)) (cong (\y -> ...) bar)) baz"10/01 10:14
soupdragonhttp://www.reddit.com/r/programming/comments/9sgw1/proof_driven_development_sudoku_pdf/10/01 10:15
soupdragonbleck!!! this is not "proof driven developmen"10/01 10:15
soupdragongrrrr!!10/01 10:21
Saizanwhy not?10/01 10:22
soupdragonbecause it's program derivation10/01 10:22
soupdragonapfelmus 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
Saizandolio: i wonder if the lisp/scheme people have tackled this problem for macros10/01 10:38
dolioWhat problem?10/01 10:38
Saizanof understanding generated code10/01 10:39
dolioYou don't need to be able to understand the proof term to understand the proof.10/01 10:40
dolioJust what it's doing at a reasonable level of abstraction.10/01 10:40
Saizansure, i guess i should have said "code that uses generated code", or "programs that use macros"10/01 10:41
dolioCoq 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
dolioOr why you'd use each strategy when it is used.10/01 10:41
Saizanstrategies are mostly searches, right?10/01 10:44
Saizani wasn't considering that10/01 10:44
soupdragonproof scripts in coq are usually just someone hacking away to make the blooding thing say "proof completed"10/01 10:46
soupdragonno matter HOW just get it done10/01 10:46
dolioThey can be, certainly.10/01 10:50
dolioThe ring solver module in agda was ported from coq.10/01 10:50
dolioAnd you can just tell it to prove arbitrary stuff involving operations on rings.10/01 10:50
Saizanyeah, and that's pretty deterministic, it just normalizes10/01 10:51
Saizanit 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 work10/01 10:54
Saizanwhcih might not be at a sufficiently high level of abstraction either..10/01 10:56
soupdragonmathematicians are warped :L10/01 11:05
soupdragonImplement an Agda-like language on top of ΠΣ.10/01 11:40
soupdragonΠΣ in ΠΣ.10/01 11:40
soupdragonOptimizing compiler.10/01 11:40
Saizan?10/01 11:40
soupdragon"what's next" regarding pi-sigma10/01 11:41
-!- jfredett_ is now known as jfredett10/01 17:02
--- Day changed Mon Jan 11 2010
copumpkinTacticalGrace: so you're going to teach an agda course? :)11/01 01:21
TacticalGracecopumpkin: I wouldn't call it an Agda course11/01 01:25
copumpkina course using agda, I meant :)11/01 01:25
TacticalGraceThe course is on formal methods and tools for software design, implementation, and testing11/01 01:26
copumpkinooh11/01 01:26
TacticalGraceSo, I plan to talk about formal specifications and proofs against such specifications11/01 01:26
copumpkincool11/01 01:27
TacticalGraceand this is what I want to use Agda for11/01 01:27
TacticalGracebut the course will also use Haskell and tools, such as QuickCheck and HPC11/01 01:27
copumpkinnice :) I wish we had courses like that11/01 01:27
TacticalGraceit's an existing course that was taught in an imho somewhat misguided way11/01 01:28
copumpkinwhat did it use before?11/01 01:28
TacticalGracebasically fancy tricks using C++ and working from somewhat mathematical, but not at all rigorous specs11/01 01:29
TacticalGraceI don't think it met the aim of the official course description at all11/01 01:29
copumpkinah11/01 01:30
TacticalGracethe classical thing to do would probably be Hoare calculus and/or WP and fuzz around with Java11/01 01:30
TacticalGracebut I think that's boring ;)11/01 01:30
copumpkin:)11/01 01:30
TacticalGraceso, I'm going to do the FP high-assurance thing11/01 01:30
TacticalGracebut most students will not know Haskell or FP11/01 01:31
TacticalGraceand as I don't think we'll get far with pen-and-paper proofs in such a class11/01 01:31
copumpkinoh I thought you taught that early on there?11/01 01:31
TacticalGraceI want something that is close to Haskell (which they'll learn anyway), but allows me to do rigorous specs and proofs11/01 01:32
TacticalGraceAgda seems to fit that pretty well11/01 01:32
TacticalGracewe used to11/01 01:32
copumpkinoh :(11/01 01:32
TacticalGracesince the CS intro was unified with the EE intro, not nymore11/01 01:33
TacticalGraceanymore*11/01 01:33
TacticalGrace(our CS school is part of the engineering faculty, and it was a faculty thing)11/01 01:33
copumpkinah11/01 01:33
copumpkincan't you just put a haskell course as a prereq?11/01 01:34
TacticalGracenah11/01 01:35
TacticalGracethis course now is a compulsory course for our CS and SE degrees11/01 01:35
copumpkinoh11/01 01:35
TacticalGraceso, this is where they are gonna learn Haskell now ;)11/01 01:35
TacticalGracewill be interesting11/01 01:36
edwinbthis sounds like it'll be interesting11/01 01:36
TacticalGraceI think it is not bad to tie it to the whole correctness thing11/01 01:36
TacticalGraceI mean, tie FP to it11/01 01:36
TacticalGracewill make it much easier to motivate11/01 01:36
copumpkinyeah :) reminds me of a course here where we were told to learn c in the first week and get on with the assignments11/01 01:36
copumpkinbut c is pretty easy to pick up :)11/01 01:36
TacticalGraceedwinb: yeah, I hope it'll also work! ;)11/01 01:36
edwinbindeed11/01 01:37
TacticalGraceI'm not worried about them picking up Haskell11/01 01:37
TacticalGraceI taught Concepts of Programming Languages the last two years in that way11/01 01:37
TacticalGraceI even refused to teach it in class (well, I had one quick intro)11/01 01:37
copumpkin:)11/01 01:37
TacticalGracebut I gave them exercises and Real World Haskell11/01 01:38
edwinbI got some students writing an interpreter in Haskell once after one quick intro11/01 01:38
TacticalGraceworked just fine11/01 01:38
edwinbthey didn't seem to find it that hard to pick up, with enough pointers in the right direction11/01 01:38
Saizan_ah, so that's where all those clueless newbies came from? j/k :)11/01 01:38
copumpkinlol11/01 01:38
TacticalGraceHaskell is actually pretty easy to pick up if you put aside any prejudice11/01 01:38
TacticalGraceSaizan_: hehehe11/01 01:38
edwinbI'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
TacticalGraceyeah, I forgot that I also tell them about #haskell11/01 01:39
TacticalGracethat sorts them out ;)11/01 01:39
edwinbheh11/01 01:39
TacticalGraceedwinb: 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 practice11/01 01:40
edwinbexactly11/01 01:40
TacticalGraceso, I think, tool support is crucial11/01 01:40
TacticalGraceand using code that you actual might consider to run is crucial11/01 01:40
Saizan_yup, same here wrt mu-calculus and concurrent systems11/01 01:40
TacticalGraceactually*11/01 01:40
TacticalGraceI think, dependent types might be a way to deliver that11/01 01:41
TacticalGraceI'm going to test that hypothesis! ;)11/01 01:41
TacticalGrace(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
TacticalGraceWhen 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
TacticalGraceSo, hopefully Agda can be a fast-path to more interesting verification problems.11/01 01:45
TacticalGrace(interesting assignments => better motivtation => happy students)11/01 01:45
edwinbyes, we have some good first year students who end up thinking CS is too easy because the first assignments are so trivial11/01 01:46
edwinbit's a pity we don't teach them any functional programming at all really...11/01 01:46
edwinbwell, not officially11/01 01:46
TacticalGraceedwinb: doesn't your group have courses where you could use it11/01 01:53
edwinbyes, we can sneak it in11/01 01:53
edwinbbut it'd be so much easier if we could assume more about what they know11/01 01:54
TacticalGraceyes, but it works fine for us in Concepts of Programming Languages11/01 01:54
TacticalGracesure, the students need to learn the language11/01 01:54
TacticalGracebut because it's a languages course that's easily motivated11/01 01:54
edwinbso in the compiling course and the logic course, say, they get functional programming, but you have to spend time teaching some basics11/01 01:54
TacticalGraceand the pay of comes in the assignments11/01 01:54
TacticalGraceand actually also the lectures11/01 01:54
-!- opdolio is now known as dolio11/01 04:39
-!- opdolio is now known as dolio11/01 19:50
--- Day changed Tue Jan 12 2010
-!- opdolio is now known as dolio12/01 04:38
-!- EnglishGent is now known as EnglishGent^afk12/01 13:51
soupdragongoorilla did you read about the x8612/01 22:11
soupdragonhttp://www.cl.cam.ac.uk/~mom22/jit/jit.pdf12/01 22:11
soupdragonself modification12/01 22:11
--- Day changed Wed Jan 13 2010
Saizanare there proper dependently typed languages where you can write a function on types by case analysis?13/01 00:22
Saizanyou could do something similar to extensible variants, i'd think13/01 00:23
copumpkinas in f : Set -> Nat; f Void = 0; f Unit = 1; f Bool = 2 ?13/01 00:27
copumpkinseems unnatural13/01 00:27
Saizan+ a catchall13/01 00:28
Saizanf _ = 313/01 00:28
Saizane.g. type families in GHC kind of do this13/01 00:29
Saizanexcept that they are open instead13/01 00:29
Saizanin Agda you've to use an "universe"13/01 00:29
Saizanto reify the types13/01 00:30
copumpkinyeah13/01 00:33
* copumpkin isn't sure how typecase breaks parametricity but our open typecase through typeclasses doesn't13/01 00:34
dolioType classes do it, too.13/01 00:55
copumpkinah okay13/01 00:56
dolioAnd it doesn't break parametricity because it shows up in the type.13/01 00:56
dolio'forall a. a -> a' doesn't use type case.13/01 00:56
copumpkinoh, that's the secret ingredient!13/01 00:56
Saizanwell, don't gadts break parametricity by themselves?13/01 00:56
dolioI wouldn't say so off the top of my head, but I'm not really sure.13/01 00:58
Saizani 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 F13/01 00:59
dolioYeah.13/01 00:59
dolioSo, 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
dolioSo whether you still have parametricity may be open.13/01 02:25
Saizani 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 = id13/01 02:27
dolioYes. In the FInt case you're forced to return an FOther.13/01 02:28
dolioBecause you don't know the return type.13/01 02:28
dolioWoo!13/01 19:35
soupdragonyou didn't??13/01 19:36
dolio"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
dolioHmm... Should I install GHC 6.12 before upgrading...13/01 19:39
dolioOoo, pattern matching on records, too.13/01 19:40
soupdragonaw i thouhght you hit false13/01 19:41
soupdragon(again)13/01 19:41
dolioNo, 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
dolioI guess I should get 6.12 since I have a patch sitting around to update bytestring-show for it.13/01 19:46
copumpkinnice!13/01 19:53
copumpkinmmm category theory13/01 19:54
-!- Saizan_ is now known as Saizan13/01 21:30
-!- lpsmith_ is now known as lpsmith13/01 22:48
--- Day changed Thu Jan 14 2010
uoryglTime to play with Agda again!14/01 03:08
uoryglWhat's the typecheck-and-all-that-jazz command?14/01 03:08
SaizanC-c C-l14/01 03:18
-!- opdolio is now known as dolio14/01 17:01
-!- dolio is now known as codolio14/01 17:07
-!- codolio is now known as dolio14/01 17:07
-!- dolio is now known as codolio14/01 17:08
-!- codolio is now known as dolio14/01 17:08
--- Day changed Fri Jan 15 2010
-!- opdolio is now known as dolio15/01 05:01
guerrillaDoes 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
edwinbProbably downloading it and taking it to a printing shop is the easiest...15/01 10:23
guerrillayeah, i suppose so15/01 10:30
jacobianIs agda likely to get a tactic based theorem prover at some point?15/01 10:38
-!- Berengal_ is now known as Berengal15/01 12:00
-!- ksf_ is now known as ksf15/01 22:41
-!- Berengal_ is now known as Berengal15/01 22:41
-!- solidsnack_ is now known as solidsnack15/01 23:24
-!- whoppix_ is now known as whoppix15/01 23:24
--- Day changed Sat Jan 16 2010
copumpkinwhat is this sized type stuff?16/01 01:24
copumpkinah, found a paper16/01 01:24
copumpkinor slides, at least16/01 01:24
copumpkincan't actually find much on them16/01 01:28
dolioIt'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
dolioAnd there's some kind of infinity when x = S x is inferred.16/01 01:31
copumpkinaha16/01 01:31
copumpkinin the slides it says it's equivalent to the ordinals though16/01 01:31
copumpkinnot naturals :o16/01 01:31
copumpkinwhich seems strange16/01 01:31
dolioOkay.16/01 01:31
copumpkinanyway, that doesn't change the basic point16/01 01:32
soupdragonwhich ordinals?16/01 01:32
copumpkinjust wondering how you'd write down inductive ordinals16/01 01:32
soupdragonthe set of ordinals --> BOOM16/01 01:32
copumpkindolio: 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 interesting16/01 01:32
dolioMy problem was proving transitivity for permutation proofs that didn't simply assume transitivity.16/01 01:34
copumpkinah16/01 01:35
dolioAnyhow, the usual inductive ordinal definition is: data O : Set where zero : O ; suc : O -> O ; lim : (Nat -> O) -> O16/01 01:42
copumpkinoh, hm16/01 01:43
dolioAlthough you can get fancier from there.16/01 01:43
soupdragonthis goes up to e^e^...^e?16/01 01:43
soupdragonerr16/01 01:44
copumpkinis that all of them?16/01 01:44
soupdragons/e/w/g16/01 01:44
dolioAll of them?16/01 01:44
soupdragoncopumkin (BOOM!)16/01 01:44
soupdragonI think O has the strength of epsilon_0 = w^w^...^w16/01 01:45
soupdragon(nice to be able to check somehow..)16/01 01:45
soupdragonGOT EPIGRAM WORKING!16/01 19:47
dolioWhich one?16/01 19:47
soupdragonPig0916/01 19:48
dolioSo you can write cryptic programs in some core language?16/01 20:02
soupdragonI haven't tried16/01 20:05
soupdragonI think I need to get TeX to build some documentation16/01 20:05
soupdragonthis is what .pig files look like16/01 20:06
soupdragonmake Nat := (Mu con ['arg (Enum ['zero 'suc]) [ (con ['done]) (con ['ind1 con ['done]]) ] ] ) : Set ;16/01 20:06
soupdragonmodule Vec ;16/01 20:06
soupdragonlambda A : Set ;16/01 20:06
soupdragonmake Vec : Nat -> Set ;16/01 20:06
soupdragonmake 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
soupdragonmake vnil := con [ 0 , [] ] : Vec zero ;16/01 20:06
soupdragonmake vcons := (\ n a as -> con [ 1 n a as , [] ]) : (n : Nat) -> A -> Vec n -> Vec (suc n) ;16/01 20:06
soupdragonand it's got quotients!16/01 20:07
dolioIt does?16/01 20:12
dolioI didn't realize that.16/01 20:12
soupdragonbetter than setoidsa16/01 20:12
soupdragon-a16/01 20:12
dolioYeah, you don't have to tell me that. :)16/01 20:13
soupdragonhave you looked at the epigram impl. it's all crazy16/01 20:13
soupdragonthey use aspect oriented program16/01 20:13
dolioI have a little. I have a lot of trouble figuring it out.16/01 20:13
dolioI 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
soupdragonoh really16/01 20:14
dolioWith all kinds of riffing on applicative stuff.16/01 20:14
dolioAnd I don't understand much of it.16/01 20:14
dolioPlus, 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
soupdragonah that's she doing that16/01 20:17
soupdragonlast time I looked it was higgelty piggelty or something16/01 20:18
soupdragonI think it's meant to be easier to read in this style though...16/01 20:18
dolioI'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
dolioOr red and green terms. I forget.16/01 20:21
dolioMaybe the red/green stuff is from older repositories. I don't see it anymore.16/01 20:24
dolioI've never been entirely clear on how you define functions on quotient types. I guess I should read up some.16/01 20:29
dolioThat is, how you define them without excessively burdensome proofs.16/01 20:29
soupdragondolio it looks like the eliminator you get requires the burdensome proof16/01 20:30
dolioAh. :)16/01 20:30
soupdragonbut you know that MOST functions you write are probaby just compositions of other programs16/01 20:30
dolioYeah, I guess providing the API for using the quotient type would be expected to fulfill the proof obligations.16/01 20:31
dolioI can't seem to pull from the repository.16/01 20:37
soupdragondolio that's weird16/01 20:39
soupdragonPulling from "http://www.e-pig.org/darcs/Pig09"...16/01 20:39
soupdragonI just pulled16/01 20:39
dolioAh, my repository was pointed at sneezy.cs.nott.ac.uk16/01 20:41
dolioHey, it's got coinductive types, too.16/01 20:56
soupdragon\o/16/01 20:57
soupdragonbut does it have equality on them16/01 20:57
soupdragonI think that's in the TODO16/01 20:57
dolioI thought their plan was to encode them using inductive types.16/01 20:57
dolioDo they still have Set : Set?16/01 20:59
dolioOh, the colors are back in the equality module.16/01 21:00
dolioOnly it's green and blue instead of green and red.16/01 21:00
soupdragonIll try and check Set : Set16/01 21:00
dolioOh, I think I know what the colors mean.16/01 21:00
soupdragonhehe Pig told me "I'm sorry, Dave. I'm afraid I can't do that."16/01 21:01
soupdragon> make Foo := Set : Set ;16/01 21:01
soupdragonMade.16/01 21:01
soupdragon> make Bar := Foo : Foo ;16/01 21:02
soupdragonMade.16/01 21:02
dolioHeh.16/01 21:02
dolioHow'd you build this? Just make in the src directory?16/01 21:03
soupdragonyes but I had to get GHC 6.12 and darcs She16/01 21:04
dolioI have 6.12.16/01 21:04
dolioGuess I made the right decision when re-installing Agda the other day.16/01 21:05
dolioHuh, I don't have lhs2TeX.16/01 21:08
soupdragonyou don't need it16/01 21:10
soupdragontry ./Pig16/01 21:11
soupdragonmake Pig16/01 21:11
dolioYou should install lhs2TeX. The output is pretty impressive.16/01 21:16
soupdragonokay16/01 21:16
Saizanhow do you run lhs2Tex on it?16/01 22:47
* edwinb spots people playing with the Pig16/01 22:58
edwinbmake Epitome will run lhs2Tex16/01 22:59
soupdragonhi edwin!!16/01 22:59
edwinbhello world16/01 22:59
Saizanthanks :)16/01 23:04
soupdragonso whats everyone wrote in epirgam16/01 23:53
edwinbwe have added two and two16/01 23:53
Laneydid you get five?16/01 23:53
edwinband taken the first few things from a stream16/01 23:53
edwinbI don't think we ever got five16/01 23:53
edwinbI'm fairly sure we got two at one point16/01 23:54
soupdragon> compile x foo16/01 23:58
soupdragon/bin/sh: epic: command not found16/01 23:58
soupdragonPig: user error (EPIC FAIL)16/01 23:58
* soupdragon snorts16/01 23:58
edwinbcabal install epic, no problem ;)16/01 23:58
soupdragonI knew it wouldn't be that easy16/01 23:59
soupdragonI'll need to install bohm and gmp I guess16/01 23:59
--- Day changed Sun Jan 17 2010
edwinbyou probably have gmp already17/01 00:00
edwinbbut you will need boehm, yes17/01 00:00
edwinbnot that any epigram programs actually need garbage collection yet17/01 00:00
edwinbboehm gc is a pretty painless install, fortunately17/01 00:00
edwinbunless you're on a weird system17/01 00:00
soupdragonyikes17/01 00:01
soupdragonedwinb have you seen this?17/01 00:02
soupdragon             *** This will be an error in GHC 6.14! Fix your code now!17/01 00:02
edwinbYes, it's from happy generated code though17/01 00:02
edwinbso it's just noise17/01 00:02
soupdragonghc is getting very snappy17/01 00:02
soupdragonerr17/01 00:02
soupdragonbossy17/01 00:02
edwinbI blame Simon M ;)17/01 00:02
dolioPig doesn't seem to like much of what I'm typing.17/01 01:42
soupdragonI'm gonna read the sources a bit more carefully before pulling on its tail17/01 01:43
soupdragontommorow :[17/01 01:43
dolioparse \ x -> x works, but asking it to infer gives me a parse error.17/01 01:45
soupdragonno wonder17/01 01:45
soupdragonhmm17/01 01:46
soupdragonmaybe not what I thought it was17/01 01:46
soupdragon> make f := (\ x -> x) : Set -> Set ;17/01 01:50
soupdragonMade.17/01 01:50
soupdragon> infer f17/01 01:50
soupdragonSet -> Set17/01 01:50
soupdragon\o/17/01 01:50
copumpkinforgetting about proofs, I wonder how nice a SQL library in agda would be nice :)17/01 01:53
copumpkin-nice17/01 01:53
copumpkinor maybe +nice17/01 01:53
dolioHow nice it would be nice nice?17/01 01:54
soupdragonSQL kicks ass17/01 01:54
soupdragonAnything to do with SQL is pure win17/01 01:54
copumpkinyou being sarcastic? :)17/01 01:54
dolioAnything to do with Joe Celko is pure win.17/01 01:54
soupdragonno I love SQL17/01 01:54
copumpkinit'd be nice to guarantee that types passed to compiled queries match what's expected17/01 01:55
soupdragonI submit SQL scripts to rosettacode sometimes17/01 01:55
soupdragonit's a seriously cool language17/01 01:55
copumpkin:)17/01 01:55
copumpkinI don't like what oracle did to it17/01 01:55
soupdragonalso I have a thing for expressive subturings17/01 01:55
soupdragonthey have a certain je ne calculer pas17/01 01:56
copumpkin:)17/01 01:56
soupdragonhttp://rosettacode.org/wiki/Look-and-say_sequence#SQL17/01 01:56
copumpkinwow17/01 01:56
copumpkinthat's pretty intense :)17/01 01:57
dolioJoe Celko is also intense.17/01 01:59
copumpkinyeah?17/01 02:00
dolioWho else has written a "For Smarties" book?17/01 02:02
dolioAlso, he looks like Anton LaVey.17/01 02:03
soupdragonyeah he does17/01 02:03
soupdragonlol17/01 02:03
soupdragonmake plus := con con [(\ r r y -> y) (\ r -> con \ h r y -> suc (h y))] : Nat -> Nat -> Nat ;17/01 13:07
soupdragondoes not make sense..17/01 13:07
soupdragon(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 v17/01 13:09
soupdragonthat's weird17/01 13:09
soupdragondischarge : boxOp (d, Mu d, P, discharge)?17/01 13:09
soupdragonI guess they're different names17/01 13:09
soupdragoncannot understand this free monad stuff17/01 13:52
soupdragonwell I can't figure out what con con means17/01 14:21
soupdragoncon - Constructor for inductive definitions17/01 14:23
soupdragoncon con - ??17/01 14:23
soupdragon> parse ()17/01 15:56
soupdragonParse failure: end of parser.17/01 15:56
soupdragonshould that really be a parse error?17/01 15:56
soupdragonInTm ::= ... | () -- Unit | ...17/01 15:56
soupdragon> elab add two two17/01 16:12
soupdragoncon ['suc (con ['suc (con ['suc (con ['suc []])])])]17/01 16:12
soupdragonnice17/01 16:12
soupdragonnot taht make zero := [] : Nat ;  makes any sense17/01 16:13
* ttt-- doesnt know how to prove a = 1 -> a >= 1 in agda17/01 16:55
* ttt-- feels stupid :)17/01 16:55
soupdragonwell ttt-- it depents on >= and =17/01 16:56
soupdragonwhat are the defintions of these?17/01 16:56
ttt--the standard ones17/01 16:56
soupdragon...17/01 16:56
ttt--for nat17/01 16:57
ttt--from Data.Nat17/01 16:57
ttt--and PropositionalEquality17/01 16:57
ttt--im probably doing it wrong17/01 16:58
soupdragonI think you can click on the things to get the definitions17/01 16:58
ttt-- foo : (a : ℕ) -> a ≡ 1 -> a ≥ 117/01 17:00
ttt--are there simpler ways that typing out the proof manually?17/01 17:01
ttt--than*17/01 17:01
ttt--Why cant it deduce that the only case of a can be 1 ?17/01 17:09
ttt--in foo17/01 17:09
soupdragonyou can prove 1 ≥ 1 first, and then use it to complete foo17/01 17:10
ttt--http://hpaste.org/fastcgi/hpaste.fcgi/view?id=16232#a1623217/01 17:23
soupdragonor not, as the case may be17/01 17:24
soupdragonyou can skip matching on n I thin17/01 17:24
soupdragonthink*17/01 17:24
ttt--i dont really understand why the foob doesnt work17/01 17:25
ttt---the17/01 17:25
ttt--it doesnt seem to use all the information available, unless you type it all out17/01 17:26
soupdragonthat's how agda works17/01 17:26
dolioArabic numerals in Pig seem to refer to some built-in natural type.17/01 17:39
dolio0 and 1 are not what the Epitome says they are.17/01 17:39
soupdragonyeah that's weird17/01 17:39
soupdragonthat epitome thing is a bit confusing17/01 17:40
soupdragonI mean the BNF17/01 17:40
dolioHow did you define a Nat type for adding?17/01 17:40
soupdragonwell I didn't17/01 17:40
soupdragonI just took the one from /test17/01 17:40
soupdragonmake Nat := (Mu con ['arg (Enum ['zero 'suc]) [ (con ['done]) (con ['ind1 con ['done]]) ] ] ) : Set ;17/01 17:40
dolioAh.17/01 17:40
soupdragonwe have17/01 17:40
soupdragon'zero : Enum ['zero 'suc]17/01 17:40
soupdragon'suc : Enum ['zero 'suc]17/01 17:41
soupdragonnot sure if you can prove  Enum [] -> P17/01 17:41
dolioOh, there's a Mu.17/01 17:41
soupdragoncon ['arg ...] makes a Desc (I think), which you can Mu into an inductive17/01 17:41
soupdragon> infer con ['arg (Enum []) []] : Desc17/01 17:42
soupdragonDesc17/01 17:42
dolioPig could use some readline, too. :)17/01 17:48
soupdragonyes ;(17/01 18:08
soupdragonhaven't got around to that yet17/01 18:08
stevanhi, copumpkin: have you seen http://www.cse.chalmers.se/~ulfn/code/database/Main.html ?17/01 19:02
copumpkinooh, nope I hadn't17/01 19:02
copumpkinthanks :)17/01 19:03
stevan:-)17/01 19:03
doliosoupdragon: Heh, did you enter the definition of addition by hand?17/01 19:27
soupdragondolio I just pasted these things in from the file17/01 19:28
soupdragonthere's some example/test programs already17/01 19:28
copumpkinsoupdragon: <stevan> hi, copumpkin: have you seen http://www.cse.chalmers.se/~ulfn/code/database/Main.html ?17/01 19:28
copumpkin(thought you might be interested too)17/01 19:28
dolioYeah, I know.17/01 19:28
soupdragoncopumpkin is that from power of pi ?17/01 19:28
dolioIt produces some fairly incomprehensible goals on some of the entries.17/01 19:28
copumpkinsoupdragon: not sure :)17/01 19:28
soupdragonthe tactic stuff seems to work nice17/01 19:28
dolioYeah.17/01 19:29
dolioI just don't know how I'd figure out what to enter for addition.17/01 19:29
dolioThe incremental development is nice, though.17/01 19:29
soupdragonyeah in this thing:17/01 19:29
soupdragonmake plus := con con [(\ r r y -> y) (\ r -> con \ h r y -> suc (h y))] : Nat -> Nat -> Nat ;17/01 19:30
soupdragonit's not exactly clear what con does17/01 19:30
dolioYeah.17/01 19:30
soupdragontrying to work it out..17/01 19:30
dolioIn some of them they appear to define constructors 'zero and 'suc, but then they don't use them.17/01 19:30
dolioBut they're still in the output.17/01 19:30
soupdragonlike here?17/01 19:30
soupdragonmake zero := con ['zero] : Nat ;17/01 19:30
soupdragonmake suc := (\ x -> con ['suc x]) : Nat -> Nat ;17/01 19:30
dolioThey use them there.17/01 19:31
dolioBut sometimes it's just "make zero := [] : Nat".17/01 19:31
soupdragonoh yeah I don't understand that bit17/01 19:31
dolioAnd the NatD isn't any different in those.17/01 19:31
dolioI 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
soupdragonwonder if you can prove con ['zero] = []17/01 19:33
dolioI don't know. If you parse [], it gives Void, I think.17/01 19:34
soupdragondo you need subtracton?  (x,y) = (u,v) <=> y+u = v+x17/01 19:35
dolioOh, I guess not.17/01 19:35
dolioApparently "con ['zero]" is DC (Con (DC (Pair (DC (Tag "zero")) (DC Void))))17/01 19:36
dolioSo [] is for tuples, I guess?17/01 19:37
soupdragonyes17/01 19:38
soupdragondolio another weird thing is this17/01 19:40
dolioHave you figured out what the type of 0, 1, 2, etc. are yet?17/01 19:40
soupdragon> make quux := Enum ['foo 'bar 'baz] : Set ;17/01 19:40
soupdragonMade.17/01 19:40
soupdragon> make quux2 := Enum ['foo 'baz] : Set ;17/01 19:40
soupdragonMade.17/01 19:40
soupdragonnow we have  'foo : quux,  'foo : quux2,  'bar : quux but not 'bar : quux217/01 19:41
dolioThat doesn't surprise me, really.17/01 19:44
soupdragonwell it just means that terms can have multiple types17/01 19:44
dolioI think one of the things they're going for is relatively structural typing.17/01 19:44
dolioSo 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
soupdragonah17/01 19:46
soupdragon> elab 0 : quux17/01 19:46
soupdragon'foo17/01 19:46
soupdragon> elab 1 : quux17/01 19:46
soupdragon'bar17/01 19:46
dolioAh hah.17/01 19:46
soupdragon> infer Switch17/01 19:47
soupdragon(e : EnumU)(x : Enum e)(p : Enum e -> Set)(b : Branches (e,17/01 19:47
soupdragon                                                         p)) -> p x17/01 19:47
dolioHow did you find that?17/01 19:48
soupdragonit's in src/Features/Enum.hs17/01 19:48
dolioAh.17/01 19:48
soupdragon> infer Switch ['foo 'bar] 017/01 19:49
soupdragon(p : Enum ['foo 'bar] -> Set)(b : Sig (p 'foo ; p 'bar ;)) -> p 'foo17/01 19:49
soupdragoncool17/01 19:49
soupdragonhmm what the hell is b :17/01 19:51
soupdragon> make x := ? : Enum []17/01 19:52
soupdragonMade.17/01 19:52
soupdragon> infer Switch [] x (\ x -> :- FF)17/01 19:52
soupdragon(b :) -> :- FF17/01 19:52
soupdragon> infer (\ x -> Switch [] x (\ o -> :- FF) []) : Enum [] -> :- FF17/01 19:53
soupdragonEnum [] -> :- FF17/01 19:53
soupdragonthat works :D17/01 19:54
soupdragonI have no idea what that last [] is for thuogh17/01 19:54
soupdragonbut I was wondering if you could prove that the empty label thing is empty17/01 19:54
soupdragonalso I don't know what's going on with this free monad stuff17/01 20:07
soupdragonand I can't seem to find what 0 and 1 actually are  in src/DisplayLang/Lexer.hs17/01 20:07
dolioFree monads?17/01 20:08
soupdragonI was guessing like trees but I don't know yet17/01 20:09
copumpkinFree Kevin17/01 20:09
dolioI mean more: where do you see free monads?17/01 20:10
dolioIn the code for pig?17/01 20:10
dolioOoo, they have an example of unordered pairs.17/01 20:11
dolioNow I can't remember the example of why you'd want unordered pairs...17/01 20:14
dolioOh, right, you can define commutative operations as functions on unordered pairs, which ensures their commutativity.17/01 20:21
soupdragonthat's clever17/01 20:35
soupdragonthing is with unordered pairs ((x,y),z) isn't equal to (x,(y,z))17/01 20:49
dolio((x,y),z) isn't even a valid unordered pair.17/01 20:55
soupdragonoh why not17/01 20:55
dolioBecause the types of the components are different.17/01 20:56
soupdragondoh!!17/01 20:56
soupdragonthat was stupid of me17/01 20:56
soupdragonthanks17/01 20:56
dolioBut ((x,y),(z,w)) may be different than ((x,z),(y,w)).17/01 20:57
copumpkinare you guys talking about epigram?17/01 20:57
dolioSo, 'zero := con ['zero] : Nat ; elab zero' gives [].17/01 20:59
dolioYes.17/01 20:59
soupdragondolio O_O17/01 20:59
doliof (x, y) seems to be the same as f x y, too.17/01 21:02
dolioOr, maybe not.17/01 21:03
dolioinfer prints out stuff like "f (x, y)", but the parser complains when I try it.17/01 21:04
soupdragonwhat about f(x, y)?17/01 21:06
soupdragonno17/01 21:06
dolioTry "infer elimOp"17/01 21:08
soupdragonstrange17/01 21:10
Saizansoupdragon: 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 m17/01 22:39
soupdragonthe thing is17/01 22:41
soupdragonI don't see any fmap in the file17/01 22:41
soupdragonthey 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
soupdragonmaybe fmap is derived somehow17/01 22:43
opdolioWhat's the definition of bind?17/01 22:44
-!- opdolio is now known as dolio17/01 22:44
soupdragonthere isn't one :P17/01 22:44
dolioThen they don't need fmap.17/01 22:44
soupdragonsubst : (D : Desc)(X : Set)(Y : Set)(f : X -> Monad D Y)(t : Monad D X) -> Monad D Y17/01 22:45
soupdragonthat's a built in17/01 22:45
Saizanyeah, that's bind17/01 22:47
Saizannice :)17/01 22:47
Saizanmaybe there's also a built-in fmap?17/01 22:49
soupdragonwell there's this box thing17/01 22:50
soupdragoninfact there is map : (d : Desc)(a : Set)(b : Set)(f : a -> b)(x : descOp (d, a)) -> descOp (d, b)17/01 22:50
soupdragonso that's a generic map17/01 22:51
dolioI wonder how that can work.17/01 23:03
dolioMaybe Desc contains only strictly-positive functors...17/01 23:06
soupdragonwhat's not a functor these days17/01 23:07
soupdragonI don't know17/01 23:07
soupdragonit probably is SPFs only17/01 23:07
soupdragonthere's IDesc for families17/01 23:07
dolio /\ A -> A -> A isn't a functor.17/01 23:07
soupdragonoh sure but I mean that's not described by Desc17/01 23:08
dolioOkay.17/01 23:08
dolioHow can you tell? :)17/01 23:08
soupdragonwait is that not the identity functor17/01 23:08
dolioFA = A -> A17/01 23:09
soupdragonhm17/01 23:09
soupdragonyou can define FA = A -> FA17/01 23:09
dolioThe identity functor would be IA = A.17/01 23:09
soupdragonwait forget what I am saying I am confused17/01 23:09
Saizandata F a = FCon (a -> a)17/01 23:10
--- Day changed Mon Jan 18 2010
dolioAww, there's no cofree comonad built-in.18/01 01:26
Saizanthis is discrimination.18/01 01:27
copumpkinyou should write in and complain18/01 01:28
dolioI'm not sure where to complain. There hasn't been traffic on the epigram list in ages.18/01 01:29
dolioI guess I could yell at edwinb.18/01 01:29
* edwinb hides18/01 01:34
* copumpkin reluctantly pulls out his pickaxe and torch18/01 01:35
edwinbI could teach you how to add Features if you like ;)18/01 01:35
dolioPresumably I just write something like FreeMonad.lhs, and add it to Features.lhs.18/01 01:36
edwinbyes18/01 01:37
edwinbthe theory is that this keeps all the relevant stuff for each feature in the same place18/01 01:38
dolioYeah. It's growing on me.18/01 01:38
edwinbit takes a bit of getting used to18/01 01:38
dolioFiguring that much out isn't the hard part. Writing the right stuff to make a cofree comonad is.18/01 01:39
dolioelimMonadOp doesn't mean much to me. :)18/01 01:39
dolioI 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
edwinbit'll probably all change several more times anyway, if past form is anything to by ;)18/01 01:42
dolioOr, for instance, I was surprised earlier that "con ['zero]" normalizes to [].18/01 01:43
dolioIs the core more like PiSigma now than the stuff in the OTT papers (0, 1, 2, pi, sigma, W)?18/01 01:44
edwinbStill more like OTT18/01 01:46
* edwinb decides he should have been asleep hours ago18/01 01:46
dolioNight, then.18/01 01:47
edwinbnight18/01 01:47
dolioWoo, I think I have a handle on the Descs now.18/01 06:09
Saizan:O18/01 06:10
Saizanare they restricted to form only functors?18/01 06:11
dolioThere's three cases.18/01 06:17
dolioDone, which looks like "con ['done]", or [], for some reason.18/01 06:17
doliocon ['label] is identical to [], apparently, which is rather confusing.18/01 06:18
dolioThen there's "con ['ind1 desc]", which is equivalent to refering to the type you're defining.18/01 06:19
dolioAlthough 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
dolioAnd 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
dolioAlthough a lot of times, it doesn't look like that.18/01 06:22
dolioBecause, 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
Saizanthis is how archeologists must feel, except backwards18/01 06:25
dolioSo, I'm not exactly sure what all that gives you.18/01 06:25
SaizanEnum is syntax?18/01 06:26
dolioYeah, something like that.18/01 06:27
dolioTags start with '18/01 06:27
dolioTuples containing just tags can be typed as EnumU, and Enum takes EnumUs to Set.18/01 06:27
dolioExcept, Enum isn't really first-class.18/01 06:28
Saizanso contructors in Descs don't have a tag18/01 06:32
Saizanonly Enums do18/01 06:32
dolioIf 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
Saizanah, so in tests/Monad.pig in make ExprD the latter two "give"s fill in the ?s from the first one18/01 06:37
dolioYes.18/01 06:44
dolioSo, there is a more general Ind H d.18/01 06:45
doliocon ['ind H d], for some type H.18/01 06:45
dolioI think that lets you define W-types.18/01 06:53
dolioYep.18/01 06:55
doliomake W := (\ T U -> Mu (con ['arg T \ x -> con ['ind (U x) []]])) : (T : Set) (U : T -> Set) -> Set18/01 06:56
doliomake w := (\ T U t f -> con [t f]) : (T : Set) (U : T -> Set) (t : T) (f : U t -> W T U) -> W T U18/01 06:56
dolioThe required space after \ kills me. I'm not used to \x being wrong.18/01 06:58
-!- Berengal_ is now known as Berengal18/01 17:41
-!- solidsnack is now known as Guest5798418/01 19:26
--- Day changed Tue Jan 19 2010
dolioWow, Idris is apparently pretty speedy.19/01 00:11
Saizanwhat did you run?19/01 00:15
edwinbIt can be19/01 00:18
dolioNothing. I was reading this: http://www.reddit.com/r/dependent_types/comments/ar2ai/scrapping_your_inefficient_engine_using_partial/19/01 00:18
edwinbit needs more work to do more complex data structures well though19/01 00:18
dolioAnd 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
edwinbthere is no reason why a dependently typed language should be slow19/01 00:19
edwinbquite the opposite really - you have more type information, so it'd be good to get optimisations out of that19/01 00:19
dolioNo, but they usually come as interpreters written by one or two people. :)19/01 00:20
edwinbthat is true ;)19/01 00:20
Saizanmh, an interpreter of Idris in Idris that specializes to id..19/01 02:33
lpjhjdhSo 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 comparison19/01 05:05
lpjhjdhI 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 too19/01 05:06
-!- jeflak_ is now known as jeflak19/01 11:05
-!- jeflak_ is now known as jeflak19/01 23:53
--- Day changed Wed Jan 20 2010
dolioMissPiggy: You tried anything with IDesc yet?20/01 00:53
MissPiggyno20/01 00:53
MissPiggythere's a Vector example20/01 00:53
dolioOh, there is?20/01 00:53
dolioAh, yes.20/01 00:53
MissPiggymake 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
dolioOkay, that explains what I was missing.20/01 00:54
dolioI couldn't figure out where the out-index was supposed to come from.20/01 00:54
dolioSo to speak.20/01 00:55
MissPiggyI'm wondering if they might add an IRDesc sometime (for ind-rec)20/01 00:55
MissPiggyif not we can always do it ourselves :)20/01 00:56
dolioI'm not really up on the formal underpinnings of induction recursion.20/01 00:56
dolioThe current desc stuff has some limitations, anyhow, I think.20/01 00:57
MissPiggylike what?20/01 00:57
dolioYou can't have nested fixed points, for instance.20/01 00:57
MissPiggyis that for mutual inductives?20/01 00:57
MissPiggy(I think you can code mutuals using an single indexed inductive)20/01 00:57
MissPiggy(that wouldn't cover munu though)20/01 00:58
dolioWell, NAD has an agda example: mu X. nu Y. Y + X.20/01 00:58
dolioWhich doesn't work in Agda, anyway, but the opposite nesting does.20/01 00:58
MissPiggyI 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 illuminating20/01 00:59
MissPiggyand Anton Setzer20/01 00:59
dolioYeah, I have a bunch of papers by them that I've been meaning to read.20/01 00:59
MissPiggystill don't have much clue what's going on in Cochon anyway, the asciiproximation they do is kind of painful to read/understand20/01 01:02
dolioAnyhow, 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
dolioBut 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
dolioI 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
MissPiggyis that on code.haskell or something?20/01 01:06
dolioI don't remember if I uploaded it.20/01 01:06
dolioSeems I did.20/01 01:07
doliohttp://code.haskell.org/~dolio/agda-share/html/MuNu.html20/01 01:07
MissPiggybye20/01 01:12
MissPiggythanks20/01 01:12
guerrill1oaky, 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 someho20/01 12:33
guerrillabtw, 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 me20/01 12:51
Saizanguerrilla: yeah, it's just like Either in haskell20/01 13:01
guerrillaSaizan: yes, thanks for confirming that. i just figured that out :)20/01 13:01
guerrillahehe20/01 13:01
guerrillajust a difference in notation i wasn't awake enough for20/01 13:02
Saizanalso, 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 B20/01 13:05
Saizaneven if Agda's lib has the latter in Data.Product and the former in Data.Sum :)20/01 13:05
Saizanand dependent products are dependent functions20/01 13:06
Saizanso, it's quite a mess20/01 13:06
-!- Saizan_ is now known as Saizan20/01 13:56
Laneysup20/01 15:51
--- Day changed Thu Jan 21 2010
-!- mmm is now known as BMeph21/01 03:46
guerrillasince _, { 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
ccasinI don't know of anyway to do it21/01 10:17
guerrillaccasin: okay. i suppose that some postprocessing would solve the problem then21/01 10:18
guerrillaor maybe there's a mode in latex where you can use something other than { and } to indicate parameters/arguments to macros21/01 10:19
guerrillai'll have to look into that21/01 10:19
ccasinI mean, certainly you can use it in the literate parts21/01 10:19
ccasinbut I haven't found any way to add non-unicode subscripts to identifiers21/01 10:19
ccasinif that was your question21/01 10:19
guerrillayes it was21/01 10:20
ccasinBut, you could perhaps pick an arbitrary syntax for this in the agda and then use a %format pragma21/01 10:22
guerrillayeah, going to try something like that right now21/01 10:22
ccasinthey can't be parameterized though (as far as I know) so you'd have to have one format clause for each subscript you want21/01 10:22
ccasinor perhaps you could somehow be clever and make separate format clauses for the "_{" and the "}" parts21/01 10:23
-!- opdolio is now known as dolio21/01 21:52
-!- RichardO_ is now known as RichardO21/01 21:52
-!- RichardO_ is now known as RichardO21/01 23:53
--- Day changed Fri Jan 22 2010
-!- RichardO_ is now known as RichardO22/01 05:50
-!- ertai is now known as npouillard22/01 11:30
-!- npouillard is now known as ertai22/01 11:43
-!- ertai is now known as npouillard[ertai22/01 11:44
-!- npouillard[ertai is now known as npouillard22/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 secs22/01 13:03
-!- RichardO_ is now known as RichardO22/01 14:44
-!- opdolio is now known as dolio22/01 22:46
--- Day changed Sat Jan 23 2010
-!- Berengal_ is now known as Berengal23/01 19:12
--- Day changed Sun Jan 24 2010
dolioSo, I've been thinking of writing a djinn-like proposition solving tactic thing in Agda.24/01 09:12
dolioComing up with a good proposition+proof representation is tough, though.24/01 09:12
Saizanare you indexing the proof terms with the proved proposition?24/01 09:14
dolioYeah.24/01 09:14
dolioMy 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
Saizani think the reflection module in the stdlib solves basically the same problem, wit the difference that the environment there is homogeneous24/01 10:13
-!- EnglishGent is now known as EnglishGent^afk24/01 10:26
dolioSome of that is roughly what I've been trying to do.24/01 10:26
dolioI 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
Saizanyeah24/01 10:35
Saizanhttp:// <- quite contorted24/01 10:50
Saizanand in the terms you'd need an index for value-level variables too :)24/01 10:50
dolioWell, the solving's another whole enchilada.24/01 10:53
dolioI looked briefly at the code in djinn. There's a lot of it.24/01 10:54
dolioWay more than I expected.24/01 10:54
Saizanyeah, i never got around to learning what it does24/01 11:12
dolioWell, I looked at the paper the algorithm is based on, although the paper itself doesn't describe any algorithm.24/01 11:14
dolioIt 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
dolioBut 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
dolio(Actually, djinn uses breadth-first search.24/01 11:15
-!- EnglishGent^afk is now known as EnglishGent24/01 11:22
EnglishGenthi all :)24/01 11:28
Saizanhi24/01 11:30
EnglishGenthello Saizan :)24/01 11:36
-!- EnglishGent is now known as EnglishGent^bbl24/01 11:38
-!- EnglishGent^bbl is now known as EnglishGent24/01 16:08
-!- EnglishGent is now known as EnglishGent^afk24/01 23:08
-!- copumpkin is now known as CoqLove24/01 23:46
-!- CoqLove is now known as copumpkin24/01 23:46
--- Day changed Mon Jan 25 2010
-!- lpsmith_ is now known as lpsmith25/01 02:00
Saizandamn, we really need to introduce some form of "schematic" variables25/01 12:32
guerrillajust out of curiosity, are there many folks here from GU or Chalmers?25/01 17:22
mikaelat least one!25/01 17:41
mikaellooking at the user list, I know ski_ also studies there25/01 17:42
mikaelyou?25/01 17:42
guerrillamikael: hah, yes, i didn't notice that :)25/01 18:05
guerrillano, i'm in southern Sweden currently but going back to the US to study next semester25/01 18:05
mikaelah, okay - student exchange or just vacationing?25/01 18:06
mikaelhmm, I guess nobody would vacation in southern sweden this time of year :-)25/01 18:07
guerrillayeh, a bit cold :)25/01 18:11
guerrillano, I've been working here for last 4 years25/01 18:12
guerrillatime to go finish my education now though25/01 18:12
guerrilla(I'm originally from the US, btw)25/01 18:12
mikaelnice 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
guerrillamikael: originally California25/01 18:28
guerrillamikael: you?25/01 18:28
guerrillai suppose /whois says .se :)25/01 18:29
mikaelnice, I'd love to go there, work for Apple and spend my holidays reading beat poetry in the Yosemite park!25/01 18:30
mikaeloh, yeah, I'm from Sweden, I come from further north (around Gävle) but live in Gothenburg and study at GU since 200625/01 18:31
guerrillaah yeah, i know Gavle25/01 18:32
guerrillai think you're mixing California's 60's with it's 80's25/01 18:32
guerrilla:P25/01 18:32
guerrillamight want to try an internship or at least a vacation before up and go25/01 18:33
* guerrilla loves .se :)25/01 18:33
guerrillawell, except this years winter :P25/01 18:33
guerrilla(usually barely snows in Blekinge)25/01 18:34
mikaelhah, 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
guerrillaah25/01 18:34
guerrillawell, 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 here25/01 18:35
guerrilla(in fact it seems there are none for math in english)25/01 18:35
mikaelyeah, 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
guerrillayes, the sludge has been the worst this year imo25/01 18:36
guerrillaand sludge + random extreme swings in temp. = lots of ice on the roads25/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 lpsmith26/01 22:55
--- Day changed Wed Jan 27 2010
-!- lpsmith_ is now known as lpsmith27/01 06:05
-!- Saizan_ is now known as Saizan27/01 11:03
-!- edwinb_ is now known as edwinb27/01 11:43
MissPiggyhttp://progopedia.com/language/agda/27/01 21:49
MissPiggywell I guess that settles it27/01 21:49
MissPiggyalso27/01 21:49
MissPiggyElements of syntax:27/01 21:49
MissPiggyInline comments -- comment27/01 21:49
MissPiggyNestable comments {- ... -}27/01 21:49
MissPiggynice to know... that it has comments..27/01 21:50
-!- solidsna` is now known as solidsnack27/01 22:06
copumpkinlol27/01 22:37
--- Day changed Thu Jan 28 2010
-!- edwinb_ is now known as edwinb28/01 08:39
danrif I have a function that proves a \== b, can I then simply get the proof that b \== a ?28/01 09:47
danreven better, if there is some way I could use this in \==-Reasoning28/01 09:47
danrI got the answer from stevan, sym is the function I was looking for28/01 09:52
-!- opdolio is now known as dolio28/01 12:48
-!- dolio is now known as opdolio28/01 18:07
-!- opdolio is now known as dolio28/01 18:07
-!- MissPiggy_ is now known as MissPiggy28/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 secs28/01 23:59
--- Day changed Fri Jan 29 2010
-!- lpsmith_ is now known as lpsmtih29/01 01:20
-!- lpsmith_ is now known as lpsmith29/01 05:58
-!- lpsmith_ is now known as lpsmith29/01 15:29
-!- lpsmith_ is now known as lpsmith29/01 16:20
-!- Berengal_ is now known as Berengal29/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 secs30/01 08:34
--- Day changed Sun Jan 31 2010
-!- lpsmith_ is now known as lpsmith31/01 04:51
rhzhow to implement this function? ∣i-j∣≡∣j-i∣ : {i j : ℤ} → ∣ i - j ∣ ≡ ∣ j - i ∣31/01 10:21
-!- facsimile is now known as soupdragon31/01 16:03

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