/home/laney/.irssi/irclogs/Freenode/2011/#agda/August.log

--- Log opened Mon Aug 01 00:00:43 2011
copumpkinyrlnry: you know what doesn't prevent you from dealing with wikileaks? ;)01/08 02:00
Saizanas the sole line in ~2 days that's fairly weird01/08 02:07
copumpkinlol01/08 02:07
copumpkinwell most of the agda regulars were in the same room together01/08 02:08
copumpkinso #agda became unnecessary01/08 02:08
Saizanyeah, figured so01/08 02:08
kmccopumpkin, Hacφ is secretly the Agda hackathon?01/08 02:11
djahandarieShould have realized it from the unicode in the name01/08 02:11
copumpkinwell, djahandarie, xplat, and I sat together and did agda all weekend01/08 02:12
djahandarieAnd got nothing done01/08 02:12
copumpkinbut we didn't get very far01/08 02:12
jmcarthuri watched them struggle from a distance :P01/08 03:40
augurSaizan: not the ONLY line in two days :P01/08 04:03
Saizanthe ~ saves me from any accuracy obligation :P01/08 04:19
* Saizan has streams of assumptions flowing everywhere01/08 04:21
augurSaizan: streams or lazy lists?01/08 04:34
auguri actually dont know what haskell streams are01/08 04:34
Saizanstreams, in that they are necessarily infinite01/08 04:34
augurhm!01/08 04:35
xplatso plex will compute, i think, if you compose it with, say, 'binary foo'01/08 12:06
augurwhats a plex01/08 12:07
xplatsince that will go through and enumerate the two components of the answer into a product category01/08 12:07
xplataugur: something from the CT library01/08 12:08
auguro01/08 12:08
xplatbut it won't compute if you right whisker it with B, since B is just on a power category and it will use the function straight instead of enumerating it01/08 12:09
copumpkinI proved the commutativity of reductions over a commutative semigroup last night on the train!01/08 15:35
copumpkinyay01/08 15:35
copumpkinit wasn't even horrifyingly ugly :)01/08 15:35
cayleecool!01/08 15:36
pumpkinhttps://github.com/copumpkin/containers01/08 15:39
pumpkinthat's the schtuff01/08 15:39
Saizananyone has an implementation of an environment for (typed) de-bruijn levels?01/08 16:07
yrlnrycopumpkin:  Bitcoins!!!!01/08 16:38
copumpkinso I hear :)01/08 16:38
augurcopumpkin!01/08 16:40
xplat¡¡¡¡suᴉoɔʇᴉq01/08 16:45
copumpkinoh wow, those coins are upside-down01/08 16:49
xplatit's kind of too bad ʇɐꞁdx isn't a valid nick01/08 16:50
copumpkinterrible!01/08 16:51
xplatactually it's a terrible nick, nobody could tab-complete it except maybe augur01/08 16:52
copumpkinlol01/08 16:52
copumpkinkmc probably could too01/08 16:52
augurxplat: :)01/08 16:53
augurim not actually sure how i would type the turned t01/08 16:53
auguris it in the phonetics code table?01/08 16:53
augurit is indee01/08 16:53
augurd01/08 16:53
xplatyeah, ipa extensions, supposed to represent a dental click01/08 16:54
augurno i dont think its for a dental click01/08 16:55
auguroh its an old symbol for the dental click01/08 16:55
augurthat explains it01/08 16:55
yrlnryturned t would be a very logical glyph for a dental click.01/08 16:55
yrlnrysince it's like a t, but implosive instead of plosive.01/08 16:56
augurits not a bad symbol, ill give you that01/08 16:56
xplatthe new version looks like a pipe01/08 16:56
augurindeed01/08 16:57
augur|!01/08 16:58
auguraha!01/08 16:58
auguri found it!01/08 16:58
augurʇ01/08 16:58
xplatapparently there are antecedents for it in african orthography, but seriously, did ipa (or latinate orthography generally) really need another symbol that is a single vertical line?01/08 16:58
augur|t with the ipa input01/08 16:58
augurnow whats turned a01/08 16:58
xplater, latinoid scripts ...01/08 16:58
augurxplat: ipa isnt the most readable script ever01/08 16:58
auguraha!01/08 17:08
augurɐ01/08 17:08
augurʇɐ01/08 17:08
augurnow what is this low l01/08 17:08
augurnope, i dont think its IPA01/08 17:09
xplatin any sane channel you'd have enough to tab-complete :)01/08 17:10
augur;)01/08 17:10
augurʇ is enough, yeah01/08 17:10
augurʇɐ should be MORe than enough01/08 17:10
yrlnrycopumpkin:  My associate here asked me what is the purported market value of 17k bitcoins.01/08 18:12
yrlnryI really had no idea.  Was it supposed to be $500k or something?01/08 18:13
copumpkinaround 240k iirc01/08 18:13
copumpkin23001/08 18:13
yrlnryThanks.01/08 18:14
yrlnryI said I thought I remembered that $10 < 1btc < $100 but I couldn't be more sure.01/08 18:15
copumpkinyeah, it's fluctuated a lot :)01/08 18:15
copumpkinup to about $33 after a media bubble01/08 18:15
copumpkinto 0.01 after a major hack :P01/08 18:15
copumpkinbeen hovering around 13-14 pretty stably recently01/08 18:15
yrlnryThanks very much.01/08 18:16
* ccasin wishes he sold at $3301/08 18:58
thoughtpolicebitcoinsbitcoinsbitcoins01/08 19:03
copumpkinccasin: yeah :/01/08 19:07
yrlnryMy big regret is not letting go of my Magic the Gathering cards when they were hot.01/08 19:09
thoughtpolicei also should have kept some of my pokemon cards. 1st editions man, 1st editions. holographic even01/08 19:16
xplatsell high, make more ;)01/08 19:43
--- Day changed Tue Aug 02 2011
djahandarieWhat exactly is trustMe anyways?02/08 17:48
doliotrustMe is a magic builtin that tests whether two things are definitionally equal, and either computes to refl if they are, or doesn't compute if they aren't.02/08 17:50
* xplat tries to build the infamous (and incomplete) braided triangle02/08 17:56
copumpkinaaaah02/08 17:57
djahandarie:o It's online?02/08 17:57
xplataka the adventures of SteveBob02/08 17:57
copumpkindjahandarie: yeah, it went online on Sunday02/08 17:57
djahandarieAh I see it02/08 17:58
bxcwhat is the infamous and incomplete braided triangle?02/08 17:58
djahandarieI would try and help but I'm convinced that I'm too stupid to do it by myself now :P02/08 17:59
djahandariebxc, so in a braided monoidal category, there are three laws, which are two hexagons and one triangle. But apparently the hexagons imply the triangle so we were trying to prove that in Agda02/08 18:00
djahandarie(Three laws in addition to the usual monoidal category ones)02/08 18:00
djahandarieSo far we're just trying to get the types of the triangle and the hexagon to match up :p02/08 18:01
djahandarieAnd that is what we were doing for 3 days, lol...02/08 18:01
djahandarieBut hopefully once that is done it becomes easier02/08 18:01
xplatone states that an object must not intersect an object or by inaction cause an object to be intersected02/08 18:02
xplat(i kid; they actually say things like 'braiding past two things gives the same result whether you do them one at a time or together'02/08 18:03
xplatstill building.  but there were some things that needed fixed, so it's not just still loading ...02/08 19:03
rochaelcan adga define a type for floats in a certain range?02/08 21:54
copumpkinit could, if we had floats02/08 21:55
copumpkinbut you don't want floats02/08 21:55
copumpkinwell, you might, but they're not pleasant02/08 21:55
rochaelso can we define an integer of certain range?02/08 21:58
copumpkinsure02/08 21:58
copumpkinyou can put arbitrary constraints onto things02/08 21:58
copumpkinbut you need to prove that your values fit into the type when it isn't obvious :)02/08 21:58
rochaelarbitrarily large integer? not only natural numbers02/08 21:58
copumpkinsure02/08 21:59
rochaelis there any example? i only saw NAT...02/08 21:59
copumpkinhttp://www.cse.chalmers.se/~nad/listings/lib/Data.Integer.html#102/08 22:00
copumpkinit contains a <= predicate02/08 22:00
copumpkinwhich is enough to construct the type you want02/08 22:00
rochaelit is still using NAT..02/08 22:03
rochaelso some type checking will take forever?02/08 22:03
rochaeland does not have multiply or divide02/08 22:04
copumpkinyou can define anything you want02/08 22:31
copumpkinbut most people don't work with things like that so don't write much code for them02/08 22:32
copumpkinso you'll need to build the basics first02/08 22:32
copumpkinthere are probably more libraries in coq (I see you asked there too)02/08 22:32
rochaeli'm not comparing libraries. just want to know more about dependent types:)02/08 22:32
copumpkinbut in general, most invariants you care about can be written in dependent types02/08 22:33
rochaeli'm wondering if it will take forever to prove some interger programs.02/08 22:34
copumpkinbut the more precise your types are, the more difficult they might be to work with02/08 22:34
copumpkinit won't take forever, unless you actually talk about huge integers in your proofs02/08 22:34
copumpkinif you just say "for all integers, P holds"02/08 22:34
copumpkinthat'll be small02/08 22:34
copumpkinif you say "for integers 500000000000000 and up, P holds"02/08 22:34
copumpkinthat'll be painful02/08 22:34
rochaeli see.02/08 22:35
xplat    .verify : SBHexagon2SideA ≡ⁿ BobSteveTop02/08 22:35
copumpkinxplat: you proved that!?02/08 22:36
xplat    verify = Equiv.refl02/08 22:36
copumpkinholy shit :P02/08 22:36
rochaelby the way can we define something like heterogeneous list in agda easily?02/08 22:36
xplatslightly different definition of B-over02/08 22:36
copumpkinrochael: yeah02/08 22:36
copumpkinxplat: beautiful02/08 22:36
copumpkined is giving me crap now saying "so it took you three days to write refl"02/08 22:38
copumpkinoh, speak of the devil02/08 22:38
edwardk3 days, 3 developers, to figure out 'refl' =)02/08 22:38
lambdabotedwardk: You have 1 new message. '/msg lambdabot @messages' to read it.02/08 22:38
xplatlol02/08 22:38
rochaelsomething like T :: Set => [(Set, T)] ? (in haskell syntax)02/08 22:38
copumpkinrochael: you'd probably write something like02/08 22:38
edwardkgratz on the proof though =)02/08 22:39
copumpkindata HeteroList : List Set -> Set where02/08 22:39
copumpkin[] : HeteroList []02/08 22:39
xplatit doesn't take 9 developer-days to figure out that it's refl, it takes 9 developer-days to figure out *why* it's refl :)02/08 22:39
copumpkin_::_ : forall {A As} -> (x : A) -> HeteroList As -> HeteroList (A :: As)02/08 22:39
copumpkindata HeteroList : HomoList Set -> Set where02/08 22:40
copumpkinlest we be too homonormative in here02/08 22:40
edwardk=P02/08 22:40
rochaelinteresting.02/08 22:41
pigworkerisn't there a size problem with that?02/08 22:41
copumpkinpigworker: yeah02/08 22:42
copumpkinso the thing needs to live in Set102/08 22:42
pigworkeryou can define it in Set by recursion02/08 22:43
copumpkinHeteroList : List Set → Set02/08 22:44
copumpkinHeteroList [] = ⊤02/08 22:44
copumpkinHeteroList (A ∷ As) = A × HeteroList As02/08 22:44
copumpkinthat?02/08 22:44
copumpkinso ugly :(02/08 22:44
pigworkeraye; in any case, it's a bogus size restriction forced upon you by a limitation of inductive families02/08 22:44
copumpkinwhat's a good answer?02/08 22:44
pigworkerif you could do case analysis on the indices *before* deciding what constructor to offer, you'd be laughing02/08 22:45
pigworkeryou can sort of do that in Agda like this...02/08 22:45
pigworkerHelp : (List Set -> Set) -> List Set -> Set; Help F [] = One; Help F (A :: As) = A * F As    ...02/08 22:46
pigworkerand then   data Het (As : List Set) : Set where <_> : Help Het As -> Het As02/08 22:47
pigworkerand nobody used equality!02/08 22:47
copumpkinwhat's the advantage of that over just using Help?02/08 22:48
copumpkinyou could even make Het a record, I guess02/08 22:49
xplatyou get your own constructor02/08 22:49
xplat?02/08 22:49
pigworkerit's academic here, but this definition doesn't rely on recursion over lists02/08 22:49
pigworkerits inductive structure comes from data Het02/08 22:50
xplataha02/08 22:50
pigworkerI've just replaced equational constraint by case analysis02/08 22:50
pigworkerand done edwinb optimiziation, to boot02/08 22:51
copumpkinwhat optimization is that?02/08 22:51
edwardkspeaking of edwinb, is epic supposed to build these days?02/08 22:51
pigworkernot as part of Epigram just now, but the library should be fine on its own02/08 22:52
pigworkercopumpkin: not needing to duplicate info in constructors that's extractable from type02/08 22:52
edwardkit complains very loudly when i try to compile it on my mac02/08 22:52
copumpkinpigworker: by the way, do you have some sort of story to share as much as possible in epigram to avoid the memory explosions we get regularly (in the CT libraries) in agda?02/08 22:53
dolioIf you're allowed impredicative quantification, it can be in Set.02/08 22:53
copumpkinpigworker: cause if not, I know someone who has a present for you02/08 22:53
dolioI should get around to showing that you can do Hurkens' paradox even if impredicative quantification is required to be parametric.02/08 22:54
dolioThen we could be sure that that isn't a good solution.02/08 22:54
dolioIt'd be nice if I had a language with real dependent irrelevance to use, though.02/08 22:55
copumpkinpigworker: and another random question, going back to hetero lists: you mentioned the other day that you could ornament a natural far enough to make heterogeneous lists. Would the result of that live in Set1 or Set?02/08 22:55
dolioInstead of pen and paper.02/08 22:55
dolioOr latex.02/08 22:55
pigworkerI don't know what's causing the memory explosions. We're quite naive at the moment, but we could take the trouble to craftier about eta-expansion.02/08 22:56
pigworkeras for het-lists, that depends entirely on whether we allow large indices02/08 22:58
cayleeand by large do you mean Set as an index?02/08 22:59
pigworkeryeah, can a Set be indexed over Set ?02/08 23:00
pigworkerif you look for an initial algebra semantics, you'll find that "yes" is a much scarier answer than "no"02/08 23:01
cayleeright02/08 23:01
cayleejust trying to make sure I was on the right page02/08 23:01
cayleeif not the proper paragraph yet02/08 23:01
dolioEven if you decide that the answer is "yes," asking if Sets can be indexed by Set1s is probably yet scarier.02/08 23:04
pigworkerSo strictly positive Help : (List Set -> Set1) -> (List Set -> Set1) has fixpoints, no problem...02/08 23:04
pigworker...but drop the Set1 down to Set and eek!02/08 23:05
cayleedolio: well, not so much scary as confusing - it seems not entirely well-formed to ask that02/08 23:05
pigworkerdolio: yes, that's too scary, as it would allow ways to introduce new Sets reliant on things in a larger universe02/08 23:06
dolioWell, I heard muttering over on the HTT mailing list not long ago about the identity type for U being in U.02/08 23:06
pigworkerlarge parameters are ok02/08 23:07
dolioBecause the type of weak equivalences on types is in U.02/08 23:07
dolioSo why not the identity type?02/08 23:07
dolioAnd the identity type is sort of the primordial inductive family.02/08 23:07
dolioHowever I'm quite sure that the weak equivalences of types in U', which is a universe that contains U, does not easily live in U.02/08 23:08
pigworkerthe inductively defined identity type is a mistake02/08 23:08
pigworkerI'd be inclined to separate Set- and value- equality.02/08 23:10
pigworker_<->_ : forall {l} -> Set l -> Set l -> Set l02/08 23:10
pigworker_==_ : forall {l}(X : Set l) -> X -> X -> Set l     (or one of its heterogeneous friends)02/08 23:11
dolioYeah.02/08 23:11
pigworkersorry, {X : Set l}02/08 23:12
cayleeknew what you meant, don't worry02/08 23:12
dolioAnd you can talk about == on Set l in Set (l+1) just because Set l inhabits that universe.02/08 23:12
pigworkerand then _==_ {suc l}{Set l} S T  is a large copy of  _<->_ {l} S T02/08 23:12
dolioYeah.02/08 23:12
pigworkerI think that's the way Epigram will go, once we stratify.02/08 23:14
cayleeah, Epigram is still Set : Set?02/08 23:14
pigworkeryeah, there's so much else to get working02/08 23:14
cayleemakes sense02/08 23:14
pigworkerbut I haz planz02/08 23:14
dolioHow does that not get you Set-indexed types, though?02/08 23:14
dolioBy using a large parameter, and X <-> Ix.02/08 23:15
pigworkerit totally does give Set-indexed Sets, but we just have to be good, for now02/08 23:15
dolioOkay.02/08 23:16
pigworkernote that in Epigram "parameter" means what Dybjer means, not what's done in Agda (with the parameters that can change, huh?)02/08 23:17
dolioRight, that's not what I mean.02/08 23:17
dolioAlthough nested types can be nice.02/08 23:18
dolioAnd there are initial algebra semantics for them, if I'm not mistaken.02/08 23:18
pigworkerbut they're terrifying02/08 23:18
pigworkersee works of Ralph Matthes02/08 23:19
dolioTerrifying as in complicated, or as in the categories required are bad?02/08 23:19
pigworkerthe former, primarily02/08 23:20
pigworkerquite a lot of impredicative Set, IIRC02/08 23:20
pigworkerso not going to shift easily upward through the hierarchy02/08 23:20
pigworkerbut maybe that was just an artefact of the formalization02/08 23:21
dolioIt's been a while since I read Initial Algebra Semantics is Enough. Did that require some impredicativity?02/08 23:22
cayleewell, that paper was sorta steeped in CPO like categories, wasn't it?02/08 23:23
dolioPossibly.02/08 23:23
pigworkerwell, it was targeted at System F + GADTs02/08 23:23
dolioAnyhow, I could probably live without nested datatypes, ultimately.02/08 23:24
pigworkerthey don't make interesting use of their largeness02/08 23:24
dolioVery often you see their use in, "hey, you thought this was only possible with indexed types, but guess what, nested types."02/08 23:25
pigworkerthat's like "you thought this was only possible with a pencil, but guess what, a punch in the face"02/08 23:26
cayleehah02/08 23:26
dolioHahaha. Exactly.02/08 23:26
cayleePeople have gotten me that way *so* many times...02/08 23:26
pigworkeryou can replace your (Set -> Set) -> (Set -> Set) with some (U -> Set) -> (U -> Set), where U is a suitably constructed small universe02/08 23:28
pigworkerI think Ghani and Hancock wrote a paper about it (but I don't know what happened to it).02/08 23:29
pigworkerIt's like replacing yer de Bruijn terms   Tm x = .. | Lam (Tm (Maybe x))  with something indexed over Nat02/08 23:30
dolioYes, but the former let me fit into the arbitrary feature set defined by the Haskell committee in 1998!02/08 23:36
cayleeheh02/08 23:41
pigworkerreminds me of the bad old days02/08 23:43
pigworkerlast century, dependently typed programming could get quite lonely02/08 23:44
cayleeyeah, I can believe that - being the only type theorist at this university is frustrating enough as it is02/08 23:49
pigworkerit's fun to be a bit of an outsider and take potshots at orthodoxy, but it's good to run with a gang02/08 23:51
cayleeindeed - especially when you're getting *started* in a field. ;-)02/08 23:54
pigworkeryeah, playing-chess-by-post is one thing; learning-chess-by-post is another02/08 23:59
xplatspeaking of memory blowups that happen regularly in agda, my agda process is 1541m while i'm loading the monoidal helpers02/08 23:59
xplater, braided helpers02/08 23:59
--- Day changed Wed Aug 03 2011
pigworkerwhat's it doing with all that memory? where is it losing the sharing?03/08 00:00
xplatpigworker: it seems to lose sharing mostly in implicit inference, where it builds and rebuilds trees top-down03/08 00:04
pigworkereta-expanding unknowns before inspecting the constraints?03/08 00:05
xplatyes indeed it does03/08 00:06
cayleexplat: how did you find out where it was losing sharing?03/08 00:06
Saizancopumpkin: got a runST at last03/08 00:07
SaizanThis patch contains the following changes:03/08 00:07
Saizan./ST-Example.agda -> ./ST.agda03/08 00:07
SaizanM ./ST.agda -1 +103/08 00:07
Saizan~03/08 00:07
Saizan~03/08 00:07
xplatcaylee: by skimming through gigabytes (literally) of debug traces with the aid of a perl script to help visualize them03/08 00:07
Saizan~03/08 00:07
cayleegah, okay03/08 00:08
Saizansorry for the flood..03/08 00:08
pigworkerit's one of those situations where the optimization (not eta-expanding unless provoked by a constraint) is easy to get wrong, and thus not done; clearly now worth thinking about getting right03/08 00:09
xplatcopumpkin: djahandarie: i pushed a new version of braided-triangle to my repo, where verify is just Equiv.refl03/08 00:09
copumpkinSaizan: excellent03/08 00:10
copumpkinxplat: very nice!03/08 00:10
xplati'm using a weird operator in my code though, i had to make my own user binding of it to \fork03/08 00:10
Saizandid i manage to link http://code.haskell.org/~Saizan/ST/ST.agda P03/08 00:10
Saizan?03/08 00:10
dolioI think they've done a lot of work on not eta expanding things when they don't have to.03/08 00:10
dolioBut, not enough, I guess.03/08 00:11
pigworkerbetter safe than sorry03/08 00:11
xplatwell, the worst is when you don't even have a nice equality constraint you can get right off03/08 00:14
xplatbut as you recurse on the term, you get a 'same head constructor' constraint for every subterm03/08 00:15
xplatthen not only do you have to recurse all the way down to produce an answer, but you have to drag around a fresh copy of the term when you're done03/08 00:16
xplatand worse, when you have duplicate indices anywhere, it's a fresh copy of the term with the duplicates disunified03/08 01:07
xplat(or it can be, anyway, depending on constraint ordering)03/08 01:07
xplatoh, the talk of eta expansion actually jogged something in my brain, and so i have this question:03/08 01:13
xplatis it safe to turn an implicit meta that is irrelevant into an instance meta?03/08 01:14
xplator is the proper safe level of hygiene for an irrelevant meta somewhere in the middle?03/08 01:15
djahandariexplat, nice!!!03/08 01:33
Saizanwhat's an instance meta?03/08 01:33
xplatwhatever is used as a means to fill in an instance argument03/08 01:49
xplat(formerly known as non-canonical implicit arguments)03/08 01:50
Saizansounds sensible then03/08 01:53
jmcarthurtoday was the first time i used agda at work03/08 03:02
copumpkin:O03/08 03:02
copumpkinwhat for?03/08 03:02
jmcarthurwas working through a problem with some coworkers (one of those "can we express thisin ocaml's type system?" kind of things) and laid out the spec in agda03/08 03:02
jmcarthur*this in03/08 03:03
jmcarthurneedless to say the agda version was a lot nicer03/08 03:03
jmcarthurwell, maybe that's not needless to say... but in any case, it holds true this time03/08 03:04
stepcutWould it be possible to create xml combinators using mfix like, <div>_</div>, <p>_</p>, and then do, <div><p>foo bar</p></div>. Or is it not quite that powerful03/08 03:05
jmcarthurhmm... i don't see why not03/08 03:05
jmcarthuryou'd need spaces, of course03/08 03:06
stepcutthat would be acceptable03/08 03:06
jmcarthur<div> <p> foo bar </p> </div>03/08 03:06
stepcuti think the trick part is that 'foo bar' is supposed to be cdata03/08 03:07
jmcarthuryou mean interpreted as a string or something?03/08 03:07
stepcutyeah03/08 03:07
stepcutinstead of foo and bar being functions03/08 03:07
jmcarthuryeah i think you'd need to use a string literal for that03/08 03:07
stepcutyeah03/08 03:08
stepcutare there any plans for a system for adding syntax extensions? Obviously that is not really the focus of agda at the moment..03/08 03:09
stepcutit would be neat to allow 'literal' html in agda source that as also staticly validated at compile time03/08 03:12
Saizanur/web envy?03/08 03:19
Saizanin theory you could just use string literals passing them to a richly typed parser03/08 03:21
xplatxhtml syntax with a fixed utf-8 charset might just be doable03/08 03:47
stepcutSaizan: no.. just too many competitors in the haskell web space, gotta port happstack to agda :)03/08 03:59
cayleestepcut: y'know, there's probably a number of things about happstack that would have been easier with dependent types :-p03/08 04:23
cayleethere was certainly enough machinery that felt like faking it with ghc-extensions...03/08 04:24
stepcutcaylee: I think you mean *will be*03/08 04:44
stepcutthe agda irc bot I wrote was just the prototype ;)03/08 04:45
cayleeHah, I didn't know if you were being serious about it or not. Amusingly, I wouldn't be surprised if you hit less issues with memory usage than attempting to do category theory. :-p03/08 04:52
arcatanre irc bots, someone should write an Agda version of lambdabot's @faq :)03/08 06:57
guerrillawhat does the order of unification refer to? like "high-order", "second-order", etc?03/08 10:18
pigworkerguerilla: typically the order of the types of the unknowns and the constraints03/08 10:43
pigworkerfirst-order problems concern concrete data, with constraints over the language of constructors and data variables03/08 10:44
guerrillapigworker: ok thanks03/08 11:00
guerrillai'm wondering how elaboration of implicit arguments could introduce non-first-order constraints though. do you have an example?03/08 11:03
guerrillapigworker: ok this second thesis (finished the first) Construction and Deduction in Type Theories explains it03/08 11:32
augurhmm!03/08 18:18
augurcomposition and adjoints (of relations) are related in an interesting way03/08 18:19
auguri feel i should learn more about universal properties and techniques for constructive objects that have these universal properties03/08 18:29
copumpkinaugur is going down the rabbit hole03/08 18:33
augurwhat :|03/08 18:33
copumpkincrazy math03/08 18:34
copumpkinyou'll never escape03/08 18:34
augur:p03/08 18:34
augurwhat should i investigate?03/08 18:35
copumpkinmaff!03/08 18:37
augur:P03/08 18:37
auguri mean, i feel like universal properties are related to specifications in a very important way03/08 18:37
auguri suppose most (all?) universal properties have the object of predication on both sides of the biconditional tho03/08 18:38
augurwhereas specifications dont require this, i dont think03/08 18:38
auguri'd be interested in seeing how the universal property for folds relates to the definition of folds for a given data type, for instance03/08 18:40
augurthe definition seems so unrelated, to me03/08 18:40
augurhmm03/08 18:47
auguractually, nevermind03/08 18:48
auguri see now how it relates :)03/08 18:48
augurif you eliminate the points-freeness, you get the generic definition   h (in x) = f (F h x)03/08 18:55
augurand clearly if you want to bind f instead of vary it, you just replace h with h' f03/08 18:55
augurh' f (in x) = f (F (h' f) x)   -->   fold f (in x) = f (F (fold f) x)03/08 18:56
augurthe biconditional isn't so much a definition as an observational that binding f is possible03/08 18:57
augurobservation*03/08 18:57
augurwhich i suppose doesnt help me03/08 18:59
augurcopumpkin: do you know anything about relational adjoints?03/08 19:05
copumpkinnope03/08 19:05
augur:(03/08 19:05
copumpkinI have a pretty shabby math background :)03/08 19:07
augurwell tell me if you have any insights:   if ~, ~' are relations, x (~ . ~') y = \Sigma[ z : _ ] x ~ z & z ~' y   ;   x (~ \ ~') y = \forall z -> z ~ x -> z ~' y03/08 19:11
augurand apparently,   f . g <= h   <->   g <= f \ h03/08 19:12
augurwhere <= is sub-relation03/08 19:12
augurso like, f <= g = \forall x y -> x f y -> x g y03/08 19:13
augurnow the thing is, i have a special version of . that operates on trees instead of just sets, where instead of an existential closure to introduce z, you have join03/08 19:14
augurie,   x (~ .. ~') y = x ~ (x V y) & (x V y) ~' y03/08 19:15
augurand im curious how this would carry over to the division case03/08 19:15
augurwhat is \\ such that   f .. g <= h   <->   g <= f \\ h03/08 19:16
augurbecause i feel like if i could express this in terms of adjoints, i might be able to leverage some CT concepts that otherwise wouldn't be explicitly available03/08 19:16
augurpumpkin! :D03/08 19:30
augurthank god you're here, this schmuck copumpkin really blows03/08 19:30
pumpkin:P03/08 19:30
djahandariexplat, looked at the braided triangle stuff, nice refactoring03/08 21:36
djahandarierebase seems to have made things a lot nicer...03/08 21:37
augurcopumpkin: whats with your internet being so flakey03/08 22:11
copumpkinblame apple03/08 22:11
copumpkinwhose wireless I steal03/08 22:11
auguro03/08 22:11
--- Day changed Thu Aug 04 2011
copumpkinanyone have any secrets for proving things nicely with foldl?04/08 03:20
copumpkinI feel like my proof should have the same structure as the foldl, but I can't quite turn my mind inside-out enough to make that work04/08 03:20
copumpkintail-recursive proofs :o04/08 03:21
Saizani guess you could make an eliminator like : {A B : Set}{f : B -> A -> B}{z : B}(P : List A -> B -> Set) -> P [] z -> (forall {x xs acc} -> P xs acc -> P (f acc x) (xs ++ [ x ])) -> forall xs -> P xs (foldl f z xs)04/08 03:32
Saizan"P (xs ++ [ x ]) (f acc x)" i meant04/08 03:33
copumpkin++ [ x ] would be nicer as ::^r wouldn't it?04/08 03:34
Saizanyeah04/08 03:34
Saizanlet me know if it helps if you try it :)04/08 03:36
copumpkinthat thing is kind of mind-bending too :P04/08 04:12
copumpkinSaizan: you sure that's the right signature for that? :P04/08 04:29
xplatit looks like just an induction on the way foldl builds up terms ... which means you prove that tail-recursively once and then you don't have to think about tail-recursive proofs anymore04/08 04:37
copumpkinyeah04/08 04:39
copumpkinI really want to prove this cause I can see how it'll be easy to prove the things I want with it04/08 04:39
copumpkinbut it feels slightly wrong and I'm not sure how04/08 04:39
xplatmaybe you just want to prove that universal-over-foldl is also universal-over-foldr with the witnesses being reversed04/08 04:41
xplator the converse, depending how you interpreted that 'is'04/08 04:42
copumpkinyeah04/08 04:43
copumpkinbut this feels like it shouldn't be this hard04/08 04:43
copumpkinI must just be doing something dumb04/08 04:43
xplati think you have to do double recursion for this, or at least it's easier if you do04/08 04:44
copumpkinsee, I thought I might04/08 04:45
copumpkinbut that seemed like it shouldn't be necessary04/08 04:45
copumpkinactually, the way I want to do it doesn't even terminate04/08 04:45
xplatlemma : foldl f z (xs ::^r x) == f (foldl f z xs) x04/08 04:46
copumpkinokay, proved that04/08 04:53
copumpkinI was trying to write the foldl eliminator with the same structure as foldl itself04/08 04:54
copumpkinbut it's tricky04/08 04:54
augurcopumpkin: do you know of any techniques for eliminating backtracking by enriching a data structure?04/08 08:39
xplataugur: for doing what?04/08 14:38
augureliminating the necessity of backtracking by somehow enriching the data structures involved04/08 14:38
xplataugur: you mean for eliminating the necessity of needing to backtrack by using some technique to somehow enrich the data structures involved in the problem?04/08 14:40
auguri mean devising some methodological approach to programming the elimination of the necessity of needing to ..04/08 14:42
auguryes.04/08 14:43
xplataugur: oh.  why didn't you just say so?04/08 14:43
xplataugur: would you count glr/gll's use of graph-structured stacks to be an example of this?04/08 14:44
xplator changing your algorithm from backtracking to greedy/dynamic-programming?04/08 14:46
augurill accept anything that avoids backtracking but doesn't change input-output relations04/08 14:47
auguranything that can turn backtracking into some sort of pruning of a search space, or some sort of type-enforced pre-pruned space, or whatever04/08 14:49
xplatthat parsing algorithm that's three initials beginning with C is dynamic programming, and packrat parsers, and i think earley, are lazy dynamic programming04/08 14:49
augurCYK?04/08 14:49
augur /CKY04/08 14:49
xplatright.  i can never remember it because it's too close to CJK04/08 14:49
auguri consider laziness to be effectively backtracking built into the system04/08 14:50
augursince you have to go through the failures to compute that they're failures04/08 14:50
xplatwhat?  that's the opposite of backtracking04/08 14:50
augurat least if you use lazi lists04/08 14:50
augurlazy even04/08 14:50
xplati mean, you can use it to implement backtracking, but mostly only in the 'you can implement anything with anything' sense04/08 14:51
augurlazy lists just avoid the explicit references to backtracking points by pre-compiling the alternative, and just not executing it immediately04/08 14:51
augurwhereas backtracking dynamically steps backwards until it finds the location of the alternative.04/08 14:51
augureither way you're walking through the search space in basically the same way04/08 14:52
xplatlazy dynamic programming is completely different from backtracking-via-laziness04/08 14:52
augurok04/08 14:52
xplatit's basically like regular dynamic programming, except you do even less work because if you can decide top-down that some subproblems aren't important you don't compute them even once04/08 14:53
auguri suppose i need to learn some more about dynamic programming04/08 14:53
yrlnryWhy is "Agda" called "Agda"?04/08 18:19
cayleebecause Coq was taken?04/08 18:23
* copumpkin repeats the puerile joke about Calculus of Constructions with K04/08 18:48
Saizanlol04/08 18:53
copumpkincaylee: yeah, I heard voevodsky likes coq, *giggle* *sigh*04/08 18:53
copumpkinmaybe I need a Kalculus of Inductive Constructions with K for making such bad jokes04/08 18:54
xplatin Calculus of Coinductive Constructions with Profunctors, puerile joke makes YOU04/08 18:58
copumpkinlol04/08 18:59
cayleeheh04/08 19:06
caylee:-p04/08 19:06
cayleecopumpkin: but seriously, it was kinda bad at the summer school a couple of years ago - guys giggling as they asked each other "did you like your first taste of Coq?". Seriously annoying...04/08 19:08
copumpkinyeah, I can imagine04/08 19:09
copumpkinwe need epigram to take over the world04/08 19:11
copumpkinso people can make pig jokes instead of cock jokes04/08 19:11
cayleehah, maybe that's the way out04/08 19:14
xplatno, now people will make the 'pig, ram, and cock' evil dependent-type conspiracy jokes and people will look at them like this: ?_?04/08 19:30
joe8hello, what is the agda equivalent for  the haskell eroor monad?04/08 19:42
yrlnrySo seriously, why is "Agda" called "Agda"?04/08 19:47
djahandariecaylee, interestingly enough there was absolutely none of that at the most recent one04/08 19:57
glguyWith the advent of instance arguments, I hope that there are plans to move "map" into a record in the various modules04/08 19:57
copumpkinthat'd be nice04/08 19:58
copumpkininstance arguments break parsing in a few instances :(04/08 19:58
glguyIs that a fundamental flaw in the approach or in the current implementation?04/08 19:59
glguyNow that we have irrelevant fields in records is it still necessary for the various Raw* records to exist without the associated laws?04/08 20:01
copumpkinprobably not, but the std lib doesn't use irrelevance at all04/08 20:01
glguy(is that related to why they are not presently included?)04/08 20:01
copumpkinand irrelevance seems to be getting progressively less useful04/08 20:01
copumpkinin that in the CT lib we actually need to postulate something to be able to use it at all04/08 20:01
djahandarie:(04/08 20:03
djahandarieDid you ever send something to the mailing list asking about it?04/08 20:03
glguyOne of the ways to define a recursive function is to provide a Nat as "fuel" along with a proof that fuel never runs out. In this case you never actually branch on the Nat parameter, but you do pattern match on it to demonstrate to the termination checker that termination occurs. Is there a way to show that this parameter is unnecessary (so that it doesn't get extracted when compiled)?04/08 20:04
copumpkinnope, but there's a bug report about it04/08 20:04
glguyMight Epic notice that there is only a single pattern and drop it?04/08 20:04
copumpkinglguy: I think sized types are aiming for that?04/08 20:04
copumpkinnot really sure otherwise04/08 20:04
joe8any examples of haskell monad transformers in agda? or, is there a need for monad transformers for agda?04/08 20:05
glguyjoe8: I would expect them to look very similar04/08 20:05
joe8glguy, do I need them in agda? is there a need to stack multple monads as we do in haskell?04/08 20:07
glguyjoe8: You need the if you want to write the same programs in Agda that you do in Haskell04/08 20:08
glguyThe need for monads stems from the language's purity and wanting to tightly isolate effects04/08 20:08
glguyI suspect that you don't see them in Agda as much because people don't write as many actual programs in Agda04/08 20:09
joe8I read somewhere that agda uses ml style. I am trying to find some docs that can explain the transition to agda04/08 20:09
glguybut use it more to formalize various things04/08 20:09
joe8Do I need monad stacks in agda for tranlating a haskell program to agda? or, does agda use something different?04/08 20:11
joe8s/tranlating/translating/04/08 20:12
glguyIf you want your code to look similar you'd have to use monads just the same04/08 20:13
Saizanand you can't play the ml card of effects either04/08 20:14
glguyAgda uses ML style if the styles you know about are C and ML04/08 20:14
glguybut it is closer to Haskell than ML04/08 20:14
thoughtpolicesyntactically agda is way closer to haskell than ML, and that's a good thing IMO. coq is a bit more ml-ish i suppose in some syntactical elements04/08 20:15
copumpkinomg a mokus04/08 20:16
mokusomg, the dual of a pumpkin!04/08 20:16
mokusthought i'd lurk in here a while and see what i can glean04/08 20:17
mokusi don't supposed there's any central go-to place to find out what agda code others have written, so I don't reinvent too many wheels?04/08 20:18
Saizanagda has ml-style modules04/08 20:19
copumpkinmokus: sadly not agda hackage04/08 20:19
copumpkin*no04/08 20:19
copumpkinI have a few small projects up on github04/08 20:19
glguyCan ML modules do all the things that Agda modules can?04/08 20:19
copumpkinbut nothing too exciting04/08 20:19
Saizansome incarnations of them have a more clear phase distinction04/08 20:21
Saizanalso, they have signatures, agda gets by with record types there though, but it lacks the subtyping04/08 20:22
joe8"See Agda for a language that can encode more monads than Haskell." - I read this. Any place where I can find this explained?04/08 20:28
djahandarieI'm not sure that is entirely true04/08 20:29
djahandarieWell, Agda can actually encode a monad at all, but aside from that detail I don't know if that is true04/08 20:29
copumpkinyou can have monads in any category in agda04/08 20:30
copumpkinyou wouldn't define the class like you did in haskell though04/08 20:30
djahandarieCouldn't you do the same in Haskell?04/08 20:30
copumpkinthe agda-ification of the haskell class would just be a monad in the agda category of types and functions (at a specific universe level, probably)04/08 20:30
copumpkinnot really04/08 20:30
copumpkinhow would you write a monad on the order category of naturals and <=?04/08 20:31
copumpkinyou'd need to talk about type-level naturals, and <=, which can be done in the haskell category class04/08 20:31
copumpkinbut then going from there to monad would require talking about type-level functions on type-level naturals04/08 20:32
djahandarieOrder category?04/08 20:32
copumpkinyou know, the naturals are objects, morphisms are <=04/08 20:33
djahandarieOkay.04/08 20:33
copumpkin0 is initial04/08 20:33
mokusit certainly would be tricky, if it could be done at all - the naive version with type level naturals and MPTCs+fundeps wouldn't work because you'd have no way to quantify over the morphisms04/08 20:34
mokusmight be doable with TFs though04/08 20:35
copumpkinthe monad bit you mean?04/08 20:35
copumpkinI've written the category instance before04/08 20:35
mokusyea04/08 20:35
copumpkinyeah, the issue is that you can write type families for functions on naturals04/08 20:35
copumpkinhowever, you can't partially apply them04/08 20:35
copumpkinyou might get some ugly newtype thing around it04/08 20:35
copumpkinthat makes it work04/08 20:35
mokusI guess that makes sense, otherwise you'd have a way to do something with type families that can't be done with MPTCs and fundeps, which are supposed to be equivalent04/08 20:35
mokusspecifically, quantifying over type classes / instances04/08 20:36
musteloin agda-mode when displaying types there are often things like "_123". what do these mean?04/08 21:17
copumpkinevil metavariables04/08 21:17
copumpkinthey lurk behind the scenes and cramp yo style04/08 21:18
musteloany way to get my style uncramped?04/08 21:18
copumpkinif any of those are lurkin in ur program, u get yello04/08 21:18
copumpkinyou need to tell it more to help it figure out what's missing04/08 21:19
mustelofor example, if _::_ is defined for both List and Vec, then it's type is shown as a meta variable. is there any way to get it to show a list of all possibilities?04/08 21:19
copumpkinoh04/08 21:19
copumpkinno04/08 21:19
glguyIs there any way to see progress when recursively loading a lot of things in emacs mode?04/08 22:33
glguyother than to trust that it is doing something productive while the UI becomes unresponsive?04/08 22:33
copumpkinnot that I know of :/04/08 22:34
copumpkinin dolio's case, the UI becomes unresponsive and it isn't doing anything at all04/08 22:34
dolioOh, is someone else affected now?04/08 22:34
Saizanthe *ghci* buffer would show progress if you could see it04/08 22:35
* glguy thinks that the new behavior where meta variables are frozen immediately after definition / mutual block is having an effect on a few of his files04/08 22:39
glguyFound an implicit application where an explicit application was04/08 22:39
glguyexpected04/08 22:40
glguywhen checking that {P} are valid arguments to a function of type04/08 22:40
glguy(xs : List A) → _304/08 22:40
glguyBut I don't really understand how that error message is related04/08 22:40
copumpkinoh is that new behavior documented somewhere?04/08 22:42
copumpkincause I'm having an issue that sounds a bit like that in my derpa project04/08 22:42
copumpkinmy reaction was "fuck this"04/08 22:43
glguyThe darcs version has this now. (which I thought I'd install to play with instance arguments)04/08 22:43
copumpkinyeah, I did too04/08 22:43
glguyThey talk about it in the release notes04/08 22:43
copumpkinah, I should check that out04/08 22:43
glguyIt isn't clear to me that the behavior is working as expected at this point04/08 22:44
glguyBecause if it is, this change sucks...04/08 22:44
copumpkinyeah :/04/08 22:45
copumpkinjust wait until you see the change in irrelevance!04/08 22:45
copumpkinif you use that04/08 22:45
glguyAh, I figured out what was happening in my case04/08 22:45
copumpkinthere were several WTFs chanted at hac phi04/08 22:45
glguyway up in the top of my file I had it inferring (A -> Set) on a predicate04/08 22:45
glguybut now it would no longer use future information to figure out that I wanted Set0 and not some other set04/08 22:46
copumpkinwhere are these release notes of which you speak?04/08 22:46
glguyin the doc/ directory?04/08 22:46
glguy/doc/release-notes/2-2-12.txt04/08 22:46
copumpkinoh man, who woulda thunk it04/08 22:46
copumpkinawesome04/08 22:47
copumpkinI had no idea that was updated04/08 22:47
glguyHurray, everything is back to awesome :)04/08 22:47
glguyIt feels like files load a lot more slowly than they used to under 2.2.1004/08 22:52
augurregarding coq jokes04/08 23:08
augurits so much easier if you just counter the jokes with the most unambiguously gay-sex related comment.04/08 23:09
copumpkinthat reminds me of http://www.youtube.com/watch?v=wcBOX1JBcjQ04/08 23:10
copumpkin[moderately NSFW, audio-wise]04/08 23:10
augurahh mitchell and webb04/08 23:11
--- Day changed Fri Aug 05 2011
pigworkerRegarding Coq jokes. The whole joke is that you're not allowed to make Coq jokes if you're a native English speaker. You have to pretend that you don't know what it means, while being as disgusting as possible. It's brilliant French revenge for the anglocentricity of our community.05/08 00:21
musteloI'm trying to prove the following lemma and I'm stuck: http://hpaste.org/4987005/08 00:26
copumpkinmustelo: I think your problem is that Bool doesn't tell you much :)05/08 00:28
mustelocopumpkin, so what should I be pattern matching on?05/08 00:28
copumpkinnah, that should be fine05/08 00:29
musteloso first I tried pattern matching on "satisfies p x" but I "can't pattern match on non-datatype Set"05/08 00:31
copumpkinthe issue is that it forgot that p x is true05/08 00:31
mustelowell that's unfortunate05/08 00:32
augurso yeah05/08 00:34
augurcopumpkin: avoiding backtracking by enriching data? :D05/08 00:34
copumpkinmustelo: you can get it to remember, but it's kind of subtle05/08 00:35
copumpkinaugur: :O05/08 00:35
augurdo you know if its possible?05/08 00:35
copumpkinnot a clue :P05/08 00:35
mustelocopumpkin, so one thing that's confusing me is that agda is telling me the type of that whole should be "isTrue (p x)" but I have no idea how to get my hands on such a thing05/08 00:37
mustelos/whole/hole/05/08 00:37
copumpkinwell the thing is that isTrue (p x) will be True (and thus have a trivial constructor) if p x is true05/08 00:37
augurcopumpkin: :(05/08 00:38
augurbut yo're the pumpkin god!05/08 00:38
augurwhat kind of god doesnt know?!05/08 00:38
augur>|05/08 00:38
copumpkinlol05/08 00:39
mokusif only your question were about pumpkins... ;)05/08 00:39
copumpkinmustelo: it's remarkably dumb when it comes to this situation :P05/08 00:44
copumpkinone of the reasons we should never use bool!05/08 00:44
mustelocopumpkin, so if I change the with clause to "isTrue (p x)"...?05/08 00:44
copumpkinyou can't pattern match on that, and it isn't quite what you want anyway05/08 00:44
mustelo*sigh*05/08 00:44
copumpkinhere05/08 00:44
augurcopumpkin: how can pumpkins avoid backtracking by enriching data?05/08 00:44
mustelocopumpkin, what did you mean by "we should never use bool"?05/08 00:46
copumpkinthere's this horrible thing: http://hpaste.org/4987005/08 00:48
copumpkinBool carries no information about what is true and what is false with it05/08 00:48
copumpkinDec is a much nicer type, that looks mostly like Bool05/08 00:49
copumpkinexcept the true side of it carries a proof of truthiness05/08 00:49
copumpkinand the false side carries a proof of falsiness05/08 00:49
mustelointeresting, I see05/08 00:50
copumpkinwhat I wrote is horrible though05/08 00:50
copumpkinin the annotation05/08 00:50
mustelothis was given as an exercise in a tutorial, I can't imagine they expected that?05/08 00:51
copumpkinyeah, probably not05/08 00:51
Saizanit'd be interesting to ask the author of the tutorial for the intended solution05/08 00:53
musteloit's on page 23 of http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf05/08 00:54
mustelo(the exercise, not the solution)05/08 00:54
copumpkinhmm05/08 00:57
mustelodid I misinterpret "Sat p" on that page? I thought it was just a typo for "satisfies p" but maybe not?05/08 00:59
Saizanah, it's not really an exercise of the tutorial it's just "left as an exercise" i.e. "this is atrocious i won't deal with it" ;)05/08 01:02
Saizantbh, it explains Inspect in the next page though05/08 01:02
copumpkinthe rewrite thing wasn't even around at the time05/08 01:03
copumpkinit'd be nice if it could see inspect is injective somehow05/08 01:03
copumpkinand not force me to add a with clause for (p x) just to pattern match on the refl05/08 01:03
copumpkinI'm really kind of confused why I needed to use the subst there05/08 01:04
copumpkinsince it could see p x = true enough to reduce filter, but not enough to reduce isTrue (p x)05/08 01:04
Saizando you really need the rewrite?05/08 01:05
copumpkinwithout it, it won't let me put the _:all:_ in05/08 01:05
copumpkinbecause it can't see that p x = true to reduce the filter05/08 01:05
copumpkino.O :)05/08 01:05
Saizanah, right, the content of inspect is not linked to p x otherwise05/08 01:05
copumpkinyeah, that's what I was saying, I'd really like it to be able to spot those connections05/08 01:06
copumpkinsince inspect is a lot more annoying to use than it should be, in an ideal world05/08 01:06
copumpkinbut ideally it'd be nice if agda magically put an inspect-like equality into scope for all with blocks05/08 01:06
copumpkinthat doesn't seem too unreasonable does it?05/08 01:07
copumpkin:P05/08 01:07
copumpkinpigworker: how unreasonable is that?05/08 01:07
mustelohmm, well I'd be interested to hear if anyone comes up with some nice solution to that one. I guess I'll just move on05/08 01:07
Saizanwell, the not completely reasonable bit is how smart you expect the typechecker to be in making use of those equalities automatically05/08 01:08
Saizanunless you want to use them manually :)05/08 01:08
copumpkinI wouldn't mind using them manually, but I'm not sure how to do that syntactically05/08 01:08
copumpkinhow would I talk about them and/or pattern match on them?05/08 01:08
pigworkersorry, not paying attention, arguing about the death penalty...05/08 01:09
copumpkinoh :(05/08 01:09
Saizanone way would be to name them by their type05/08 01:10
pigworkerhang on, are you asking the Altenkirch question... can we just extend the definitional equality with random shit?05/08 01:11
Saizan(also, maybe <= in epigram already leaves some equalities in scope when it can't discharge them throgh unification?)05/08 01:11
pigworkerI mean, just taking n = t, where n is some goddamn neutral term05/08 01:11
copumpkinpigworker: you know the "inspect idiom" or how values from blocks forget where they came from?05/08 01:11
copumpkinfrom with blocks, that is05/08 01:11
copumpkinI can write f x y with g x; ... | q = ? and in the ? it won't know that g x == q05/08 01:12
pigworkerwhat does make sense is to allow "with" to abstract the equation x = t at the same time as abstracting t by x, so no info is lost05/08 01:13
copumpkinyeah05/08 01:13
pigworkerwhat's more, Nicolas Oury has shown that in a sufficiently extensional theory (like Epigram 2), this is always possible05/08 01:13
copumpkinooh05/08 01:13
Saizanthe next question was what syntax to use to refer to the x = t equation05/08 01:14
Saizan*the proof of05/08 01:14
pigworkeryou can always replace let x = s : S in t by \ (x : S) (q : x = s) -> t' where t' is t with explicit subst q inserted here and there05/08 01:14
pigworkerI always fancied   .... with q : x = s    creating columns for x and q05/08 01:16
pigworkerbut in Epigram 2, naming proofs is considered rude, so we'll just leave the with notation as it is, and chuck the equation into the context05/08 01:16
copumpkinrude :o05/08 01:18
pigworkerone proof is as good as another, so one should speak rather of propositions, and hope that a proof is somehow available05/08 01:18
Saizan"Equational Reasoning" will look weird that way :)05/08 01:20
pigworkerIt might look uncannily like stating which things are equal to which other things. How odd!05/08 01:21
copumpkinhow perverse05/08 01:22
Saizanit'll miss all the reasons!05/08 01:23
Saizanbut i'd be glad if we can avoid all the cong stuff05/08 01:23
copumpkinxplat: I like your unpossible lemma05/08 01:23
pigworkerNo it exactly won't miss the reasons. It will state the reasons, not the names of the proofs of the reasons.05/08 01:23
copumpkinI agree05/08 01:23
copumpkinoh, because the names are rude?05/08 01:24
pigworkeryes05/08 01:24
pigworkerit is permitted to name propositions, of course05/08 01:24
copumpkincan you give an example of how you envision it?05/08 01:24
copumpkinSaizan: by the way, is this the correct type:05/08 01:27
copumpkinfoldl-elim : ∀ {a b c} {A : Set a} {B : Set b} (P : ∀ {n} → Vec A n → B → Set c) {f : B → A → B} {z : B}05/08 01:27
copumpkin           → P [] z05/08 01:27
copumpkin           → (∀ {n x′ z′} {xs′ : Vec A n} → P xs′ z′ → P (xs′ ∷ʳ x′) (f z′ x′))05/08 01:27
copumpkin           → ∀ {n} (xs : Vec A n) → P xs (foldl _ f z xs)05/08 01:27
pigworkerI've thought more about deduction than equational reasoning, but...05/08 01:27
Saizancopumpkin: yep05/08 01:28
pigworkerone typically asserts t[a] = t[b] because a = b05/08 01:29
pigworkerin a typical step, one can identify the a and the b by difference matching05/08 01:30
pigworkerthe question is thus how one justifies the step by showing that a = b05/08 01:30
copumpkinSaizan: aha, proved it :)05/08 01:32
pigworkerthat is, an equational step, explicitly stated as such, demands a deduction05/08 01:32
pigworkercopumpkin: this is McCarthy's "recursion induction"05/08 01:33
Saizancopumpkin: complicated?05/08 01:33
copumpkinnah, clean05/08 01:33
pigworkerevery time you write a total function, you are entitled to induction on its graph05/08 01:33
copumpkinI was overcomplicating it :)05/08 01:33
pigworkerthis should be gratis!05/08 01:33
Saizanthey have it by Ltac in Coq, i've seen05/08 01:34
pigworkerI said gratis05/08 01:34
pigworkerone should not reconstruct "the proof method that follows the structure of the function"; that proof method is clearly justified by the existence of the function05/08 01:36
copumpkinI see05/08 01:36
copumpkinI'd quite like that :)05/08 01:36
pigworkerYves Bertot and Antonia Balaa did it for Coq about ten years ago. Functional induction.05/08 01:37
pigworkerBut in a world where datatype descriptions are first class, why should we not construct the graph of a function even as we construct the function?05/08 01:38
pigworkerMcKinna has been planning this for years.05/08 01:39
Saizanhow do first class datatype descriptions help here?05/08 01:41
pigworkerAs part of the package of elaborating a function of type Pi S T, say, one can construct the corresponding graph description in (Sg S T) -> Desc (Sg S T). Indeed, with a bit of jiggering about, one can make them part of the same goal.05/08 01:43
pigworkerof course, one also needs that if f : Pi S T, then (s : S) -> Graph(f) s (f s) as part of the construction05/08 01:44
Saizanright, but the elaborator is still an outside of language process, so even without first class descriptions it could just produce a new datatype05/08 01:46
Saizans/just produce/still produce/05/08 01:47
pigworkeryes, that's true05/08 01:47
pigworkerbut first-class datatypes make it much cheaper to implement05/08 01:48
pigworkeryou don't need to wait until the function's finished before figuring out which datatype you want and then proving that it covers the function05/08 01:48
pigworkeryou (or rather a machine) can build the datatype description and the covering proof incrementally, along with the construction of the function05/08 01:49
pigworkerincrementality is fundamental to elaboration05/08 01:50
pigworkerAgda goes to great lengths to conceal the fact that it uses your source file as the script for a private incremental construction.05/08 01:51
Saizan(and yet it reloads the whole file each time?)05/08 01:51
Saizan(i feel cheated)05/08 01:52
pigworkeroh yes05/08 01:52
pigworkerbut it's really figuring out to what incremental case-splitting process a given unicode turd corresponds05/08 01:52
Saizanwhy is incrementality so fundamental though? so that my defition of f could possibly use Graph(f) ?05/08 01:53
pigworkerI mean that incrementality is fundamental to the construction of f, so you might as well construct Graph(f) incrementally too, if only you can.05/08 01:54
pigworkerpronouns05/08 01:55
pigworkerI mean Agda might as well construct Graph(f)05/08 01:55
pigworkerBut Agda does not have much of a notion of unfinished datatype.05/08 01:56
Saizanat this point i would ask why incrementality is fundamental to the construction of f, but i feel like i'm supposed to know that :)05/08 01:58
* xplat hms at incremental elaboration05/08 01:59
xplati like the idea of a function being built by a script that reflects the reasoning involved in building it rather than 'specified' like it fell out of the sky05/08 02:05
xplatit feels like things would refactor better that way05/08 02:05
xplatcoq kind of goes to the opposite extreme, though05/08 02:05
Saizanyeah, the equations alone can be misleading wrt which tree of cases gets built05/08 02:14
copumpkin∀ {n} {a} {A : Set a} (ys : Vec A n) x → reverse ys ∷ʳ x ≡ reverse (x ∷ ys)05/08 02:44
copumpkinthat's true, right?05/08 02:44
augurcopumpkin: is ::^r snoc?05/08 02:53
copumpkinyeah05/08 02:55
augurcause if so, then surely its true, since you could reverse a list just as   reverse (cons x xs) = snoc (reverse xs) x05/08 02:55
copumpkinyeah05/08 02:55
copumpkinokay05/08 02:55
auguratleast thats how you'd define it05/08 02:55
augurso surely05/08 02:55
copumpkinnow I just need to prove it :)05/08 02:55
augurshouldnt be too hard05/08 02:55
copumpkingive it a go!05/08 02:55
augurif you define reverse appropriately05/08 02:55
augurok!05/08 02:55
copumpkinI mean the std lib reverse :)05/08 02:55
auguro05/08 02:56
copumpkinit's just defined using foldl05/08 02:56
augurnm!05/08 02:56
copumpkin:P05/08 02:56
augurin that case, then its probably false05/08 02:56
augurbecause [] ::^r x /= x :: []05/08 02:56
copumpkinwhy?05/08 02:57
augurif reverse : Vec X n -> Vec X n05/08 02:57
copumpkin[] ::\^r x == x :: []05/08 02:57
copumpkindefinitionally05/08 02:57
auguroh, so its not snoc05/08 02:57
copumpkinhow is it not?05/08 02:57
augurwell, for one05/08 02:58
augursnoc lists are a different type05/08 02:58
copumpkinnot in the std lib05/08 02:58
augurreally now!05/08 02:58
copumpkinyou just get a snoc operator on regular vectors :P05/08 02:58
augurwhere in the library?05/08 02:58
copumpkinI don't think it has a snoc list type05/08 02:58
augurData.Vector?05/08 02:58
copumpkinhttp://www.cse.chalmers.se/~nad/listings/lib/Data.Vec.html#456305/08 02:58
copumpkinVec05/08 02:58
augurahaaa i see05/08 02:59
* glguy gambles this isn't supposed to happen05/08 03:21
glguyPanic: Pattern match failure in do expression at05/08 03:21
glguysrc/full/Agda/TypeChecking/Rules/Term.hs:517:15-2605/08 03:21
Saizanwould be weird if it did05/08 03:26
glguyHappened when I turned universe polymorphism on. Agda didn't know what sort something had and then tried to use it later05/08 03:27
copumpkinanyone able to prove that thing?05/08 03:45
glguyhuh?05/08 03:45
copumpkin  reverse-∷ʳ : ∀ {n} {a} {A : Set a} (ys : Vec A n) x → reverse ys ∷ʳ x ≡ reverse (x ∷ ys)05/08 03:45
copumpkinthat one05/08 03:45
glguyhttp://www.galois.com/~emertens/revrev/revlistapp.html05/08 03:49
glguyI did a bunch of stuff about reversing Lists at one point05/08 03:49
copumpkinhmm05/08 03:50
glguydist-reverse05/08 03:50
glguy  : ∀ xs ys → reverse-app (xs ++ ys) ≡ reverse-app ys ++ reverse-app xs05/08 03:50
copumpkinthat definition would make my property almost trivially true05/08 03:50
glguyif you picked [ y ] for ys05/08 03:50
copumpkinreverse-app (x ∷ xs) = reverse-app xs ++ [ x ]05/08 03:50
copumpkinthat's basically ::\^r05/08 03:50
glguyI think it might be exactly ::\^r05/08 03:50
copumpkinonly difference is type05/08 03:51
copumpkin++ [ x ] gives you n + 105/08 03:51
copumpkin::\^r gives you 1 + n05/08 03:51
copumpkinyours works fine for List05/08 03:51
glguybut does that technique not have an obvious translation to vectors?05/08 03:53
pumpkinit sort of does, but I'm working with the std lib definition of reverse05/08 03:53
pumpkinthat is based on foldl (flip cons)05/08 03:53
pumpkinbasically the statement I wrote above is that your definition is equivalent to the one in the standard library05/08 03:54
glguythat's what the file I linked does05/08 03:54
glguyit shows that the app version of reverse is the same as the left fold one05/08 03:54
glguyand then uses the faction that the append version is easier to prove things about05/08 03:54
glguyfact that*05/08 03:54
pumpkinah, I see, cool05/08 03:55
pumpkinlooks like we're trying to prove more or less the same thing here :P05/08 03:55
pumpkinin the end, I'm trying to prove that reverse is a permutation05/08 03:55
pumpkinbut I state that it's a permutation in a very different way05/08 03:56
copumpkinanyway thanks :) I didn't see the bits at the bottom involving the left fold05/08 03:56
copumpkinI was hoping to use that fancy foldl eliminator05/08 03:57
glguywhich one is that?05/08 03:58
copumpkinfoldl-elim : ∀ {a b c} {A : Set a} {B : Set b} (P : ∀ {n} → Vec A n → B → Set c) {f : B → A → B} {z : B}05/08 03:58
copumpkin           → P [] z05/08 03:58
copumpkin           → (∀ {n x′ z′} {xs′ : Vec A n} → P xs′ z′ → P (xs′ ∷ʳ x′) (f z′ x′))05/08 03:58
copumpkin           → ∀ {n} (xs : Vec A n) → P xs (foldl _ f z xs)05/08 03:58
copumpkinthat terrifying beast05/08 03:58
copumpkinhmm, not sure I can use it though05/08 04:02
copumpkinit's not dependent enough!05/08 04:02
copumpkinthe horror05/08 04:02
glguyhttp://www.galois.com/~emertens/rlistrec/Induction.List.html05/08 04:03
glguyApparently I did some stuff for induction on lists from the end05/08 04:03
glguyLess obviously relevant05/08 04:03
glguybut sounds like its in the same ballpark :)05/08 04:04
Saizancopumpkin: how did you prove it, btw?05/08 04:08
copumpkinoh, the massive beast?05/08 04:08
Saizanyep05/08 04:08
copumpkinfoldl-elim P Pz Ps [] = Pz05/08 04:08
copumpkinfoldl-elim {A} {B} P {f} {z} Pz Ps (x ∷ xs) = foldl-elim (λ {m} xs′ z′ → P (x ∷ xs′) z′) {f} {f z x} (Ps Pz) Ps xs05/08 04:08
Saizanah, right, changing the predicate05/08 04:08
copumpkinyeah, it's very similar to foldl itself, in some ways05/08 04:08
copumpkinI wonder if I can make it more dependent05/08 04:09
copumpkinto be as powerful as the actual foldl05/08 04:09
copumpkinyeah, doesn't seem too painful05/08 04:10
SaizanP could also take an equation thating that the second argument is the the first folded05/08 04:10
copumpkinokay, the more dependent version is a trivial change05/08 04:12
Saizanhow does it look?05/08 04:14
Saizani.e. what do you mean by more dependent, exactly?05/08 04:14
copumpkinfoldl-elim : ∀ {a b c} {A : Set a} {B : ℕ → Set b} (P : ∀ {n} → Vec A n → B n → Set c) {f : ∀ {n} → B n → A → B (1 + n)} {z : B 0}05/08 04:15
copumpkin           → P [] z05/08 04:15
copumpkin           → (∀ {n x′ z′} {xs′ : Vec A n} → P xs′ z′ → P (xs′ ∷ʳ x′) (f z′ x′))05/08 04:15
copumpkin           → ∀ {n} (xs : Vec A n) → P xs (foldl B f z xs)05/08 04:15
copumpkinsame definition05/08 04:15
augurhttp://www.youtube.com/watch?v=E8NHcQesYl805/08 04:21
augurapparently dna can only be copied in one direction05/08 04:21
auguralso, we're robots.05/08 04:21
copumpkinreplicat05/08 04:22
copumpkinmeow05/08 04:22
augurmeee-heee-heee-owww ;o05/08 04:22
copumpkin:)05/08 04:22
augurseriously tho05/08 04:23
augurthe second half of that video05/08 04:23
augurcrazy05/08 04:23
augurits so robotic05/08 04:23
copumpkindude, this is proof that there was an intelligent designer05/08 04:24
copumpkinduh05/08 04:24
copumpkinthis is irreducibly* complex!05/08 04:24
copumpkin* (I can't think of how to do it)05/08 04:24
auguri think His name is Data05/08 04:24
copumpkinit is pretty cool though :)05/08 04:25
auguri mean, it really looks like something in a factory05/08 04:25
augurlike those factories that manufacture paper05/08 04:25
augurwith the massive sheets being cut into smaller sheets that can be put on spools or whatever05/08 04:26
augurit just looks so unlike what im used to seeing in biology05/08 04:26
Saizanfoldl-elim is too specific05/08 04:51
ProofWizardyeah05/08 04:52
Saizanhttp://hpaste.org/49875 <- though here's a proof05/08 04:53
copumpkinoh, fancy05/08 04:53
copumpkinthanks!05/08 05:00
copumpkinthat's quite nice05/08 05:00
Saizannp05/08 05:02
copumpkinokay, so with that05/08 05:18
copumpkinthese proofs are complete!05/08 05:18
copumpkinI can now prove that on a commutative semigroup, foldl1 of a reversed list is the same as doing a tree fold of the original list05/08 05:21
copumpkindammit, maybe not the tree fold05/08 05:40
copumpkintermination checker, y u no see this terminate05/08 05:41
Saizanhttp://hpaste.org/49875 <- much simpler this way, though for vectors there'd be some juggling of sizes in the definition of foldl-elim05/08 05:51
copumpkinoh, that is nice05/08 05:52
musteloah, fuck me. there's a solution to the filter lemma I was asking about earlier given later in the tutorial. pg 36 if anyone's interested.05/08 06:47
Saizanah, nice05/08 07:44
dsouzaaccount off05/08 11:18
augurxplat: so im curious how you were thinking of using lazy dynamic programming to eliminate backtracking05/08 15:50
copumpkinhttps://github.com/copumpkin/containers05/08 17:48
cayleecontainers as in container functors?05/08 17:52
copumpkinnah, it's a bad name :)05/08 17:52
copumpkinreally just proving things about folds for now05/08 17:52
copumpkinif you have an associative operator or a commutative one05/08 17:52
cayleeah, okay05/08 17:52
cayleeI have container functors on the brain right now05/08 17:53
cayleeshould probably see a doctor about it05/08 17:53
copumpkinyeah, sounds painful05/08 17:53
cayleeeh, you get use to it pretty quickly05/08 17:53
dolioClearly you need a better name.05/08 18:22
dolioI suggest derpers.05/08 18:22
cayleediapers?05/08 18:23
djahandariecopumpkin, what's an example of a monad on the order category of (<=)?05/08 20:28
copumpkina "closure operator"05/08 20:29
copumpkinhttp://en.wikipedia.org/wiki/Closure_operator05/08 20:29
copumpkinif you squint at the laws there05/08 20:30
djahandarie Ah, good one, thanks05/08 20:30
copumpkinthey're exactly the monad laws05/08 20:30
djahandarieIt seems harder than it should be to find one of these too :p05/08 20:35
copumpkinceiling/floor work05/08 20:44
djahandarieI'm doing naturals05/08 20:45
copumpkindepending on the direction your order goes05/08 20:45
copumpkinthen pick "clamp to even" or something like that05/08 20:45
djahandarieBut I think I can just do "first even number >= this one"05/08 20:45
djahandarieYeah05/08 20:45
djahandarieHm this is getting annoying to write :P05/08 20:53
pumpkin?05/08 20:54
augurcopumpkin: wark05/08 21:55
augurim finishing awodey, so i can undertand fibered categories05/08 21:56
copumpkinindeed05/08 21:56
copumpkincool :)05/08 21:56
augurso i can understand categorical logic05/08 21:56
augur:P05/08 21:56
auguralso, copumpkin, i think ive asked you this before but i dont remember05/08 21:57
augurer, lemme ask this in #ct05/08 21:57
--- Day changed Sat Aug 06 2011
xplataugur: the problem with any way of eliminating backtracking is it either only works for some problems, only eliminates some of the backtracking, can take more than polynomial space for NP problems, or proves P = NP06/08 01:46
xplatso in practice, you can't eliminate backtracking unless you know what the problem space is06/08 01:47
* glguy wonders what the correct way to fix the connection between the Set level of the element and the set level of the relation with the well-founded induction module06/08 03:32
glguywould be… it seems like I'm going to have to update the whole Induction module framework06/08 03:33
copumpkinglguy: by the way, Saizan came up with a very elegant proof of that reverse statement I was trying to prove yesterday06/08 03:33
glguySaizan: http://hpaste.org/49875 <- though here's a proof ?06/08 03:33
copumpkinyeah, the annotated one06/08 03:34
copumpkinif you just care about lists06/08 03:34
glguyOh, I love lists :)06/08 03:34
copumpkinI kind of need Vecs :(06/08 03:34
glguyhaven't done it yet?06/08 03:36
copumpkinoh, the first proof works fine for Vecs06/08 03:37
copumpkinI put all the stuff I was working on into github06/08 03:37
Saizanadd a presburger solver to agda's typechecker, then foldl-elim will be easy for Vec's too :)06/08 04:04
Boxoso um, silly general question about type systems06/08 16:09
BoxoI've only ever seen type systems where if (a : b) and (b : c), a and b may be complicated terms, but c is always some simple constant. Why couldn't you have many levels of more and more general information about a, where with (a : b), (b : c), (c : d), (d : e),... c,d,e and so on would also be complicated terms?06/08 16:10
dolioThere's no reason you couldn't invent a system like that in principle.06/08 16:15
dolioBut people don't.06/08 16:15
Saizanc is really information about b, not a06/08 16:18
dolioI don't think they've been studied very extensively, but there are lambda-only calculi.06/08 16:25
dolioWhere the type of a lambda term is also a lambda term.06/08 16:25
dolioSo conceivably, you could have lambdas all the way up.06/08 16:25
BoxoSo do you know what they're called?06/08 16:29
BoxoAlso why don06/08 16:30
Boxo't people invent systems like that if they could? Is there some preface of a book where the guy outlines the reasons for only having one level, or is it something that supposed to be obvious?06/08 16:31
dolioThere isn't only one level.06/08 16:33
BoxoSorry I didn't mean it literally. I meant that given (a : b : c : ...) there's only one level of complicated terms above a.06/08 16:35
dolioUsually you have values, classified by types. And then the types that have values are classified by a particular kind (or several).06/08 16:37
dolioBut Things like k1 -> k2 designate functions between types.06/08 16:37
dolioWhich don't themselves have values.06/08 16:37
xplatyou could always make a system where you could define your own kinds/universes that can be on the right of : and have values06/08 20:29
xplatbut i'm pretty sure it's basically equivalent to a system with induction-recursion where you interpret the custom kinds into 'normal' kinds by writing an interpretation function06/08 20:30
xplatso it might be a nice thing to have, but it hasn't gotten to the top of anyone's priority list06/08 20:31
xplatboxo: essentially you define a universe of 'codes' that can't have their own values, and along with them a function to turn codes into normal types in normal kinds06/08 20:32
xplatand then you pass the codes around instead of, or in addition to, the types themselves.  and the codes can be anything you want, and you can repeat this multiple times to get the kind of situation you were interested in06/08 20:34
--- Day changed Sun Aug 07 2011
derivingShowDoes Agda support lazy evaluation?07/08 14:21
Saizanif you want infinite structures there is Coinduction07/08 14:50
--- Day changed Mon Aug 08 2011
glguyDoes someone with more emacs experience know how to add fonts to your agda mode? "Apple Symbol" has support for \{{ and \}}, so I thought it might be nice to add it somehow08/08 02:06
Eduard_MunteanuDoesn't it use any system fonts, through, say, xft?08/08 02:08
Eduard_MunteanuOr are you asking how to change the default font?08/08 02:09
glguyI'm using OS X and Monaco is my default font, but as far as I know you can use a whole list of fonts and it will cascade through them to look up symbols08/08 02:12
glguyugh, I guess now that zero is no longer a constructor and is postulated it collides with Data.Nat's zero08/08 04:13
copumpkinyeah08/08 04:15
copumpkinthat bit us a few times08/08 04:15
glguyIs that change to stop people from pattern matching on the level constructors?08/08 04:16
Saizanseems most likely08/08 04:17
Saizani mean, why else?08/08 04:18
Saizanof course now we should carry around Nat's and inject them into levels so that we can still pattern match of the levels indirectly08/08 04:18
Saizans/of the/on the/08/08 04:19
glguyThat'll show ’em !08/08 04:21
copumpkinlol08/08 04:25
augurSaizan: you cant pattern match on levels? surely you can08/08 04:29
Saizanaugur: not in the new order of things08/08 04:33
augurwhat08/08 04:33
Saizanin the new stdlib they are postulates rather than datatypes08/08 04:35
glguyIt makes sense that they should be opaque. I’m just annoyed that I have name clashes now :)08/08 04:38
glguyDoes this make sense as the most faithful translation of the GMapKey associated data types examples from Haskell to Agda with Instance Arguments?08/08 04:41
glguyhttp://www.galois.com/~emertens/AssocDataTypesAgda/InstanceExperiments2.html08/08 04:41
glguyhttp://www.haskell.org/haskellwiki/GHC/Type_families08/08 04:41
glguyMy thought was that the associated data type needed to be one of the parameters of the record since its constructor is enough to identify the desired instance08/08 04:42
glguyand not simply a parameter08/08 04:42
Saizani think this way if i say "lookup Nat.zero empty" it won't infer that it has to use the NatInstance because GMap will still be free08/08 04:46
Saizanthough maybe it's more aggressive than i think08/08 04:47
Saizani.e. i think having GMap as a parameter of the record rather than as a field fails to represent the fundep08/08 04:48
glguyas far as I know it will infer the other parameter if there is only one match for the first08/08 04:49
glguytest : Maybe ℕ08/08 04:51
glguytest = lookup {!!} (gmapUnit {!!})08/08 04:51
glguyin this case the first parameter is inferred to be a Unit08/08 04:51
glguyusing implicit arguments08/08 04:52
Saizanand lookup tt ? will infer the ? to be GMapUnit, i guess?08/08 04:53
glguycorrect08/08 04:53
Saizannice, i withdraw my objection then :)08/08 04:55
glguyI think this is a neat language feature08/08 04:56
glguyI’ve been toying with it just a little this week08/08 04:56
Saizanisn't it annoying that you need a perfect match?08/08 05:00
Saizanin the sense that generalInstance : forall {k} -> GMapKey k (Map k) won't ever work because of the implicit in front, for example08/08 05:01
glguythat would potentially overlap with a lot of things08/08 05:02
Saizanyeah, bad example08/08 05:02
glguyI haven’t done anything complicated enough to really get bit by the lack of a recursive search algorithm08/08 05:03
Saizana good one would be a universe polymorphic monad instance for some specific monad08/08 05:03
Saizannot even talking about recursivity here08/08 05:04
glguybut it would only require one line of code to put the particular instantiation into scope08/08 05:04
glguyand you could go about the rest of the file using it08/08 05:04
augurwark08/08 05:06
Saizantrue, but it's ugly to me08/08 05:06
glguycan you give a particular example that we could look at?08/08 05:07
glguysomething really simple08/08 05:08
glguythat you had in mind?08/08 05:08
glguybecause it might not be as bad as you are thinking08/08 05:08
Saizani'm thinking it's "a one line to instantiate that universe level" bad08/08 05:09
glguyyeah, but that might not actually be the case08/08 05:09
glguyI think you can structure the module definition so that the implicit level parameter is resolved at the call site08/08 05:12
Saizanwell, the monad one seems simple and specific enough to me, you can use functor if you want08/08 05:12
Saizanrecord Functor (F : Set -> Set) : Set where fmap : forall {a b} -> (a -> b) -> F a -> F b08/08 05:13
glguybut generalized beyond Set -> Set?08/08 05:13
Saizanheh, yeah08/08 05:14
Saizanrecord Functor {l : Level} (F : Set l -> Set l) : Set (suc l) where ... -- i guess08/08 05:14
Saizanthen instanceMaybe : {l : Level} -> Functor (Maybe {l})08/08 05:15
glguyIn this case the level is an argument to the record08/08 05:17
Saizanit's not like it can be a field :)08/08 05:18
glguybut the thing I was thinking of for not having to manually instantiate it isn’t right :)08/08 05:18
Saizanheh08/08 05:19
glguywell, how about this:08/08 05:19
glguyjust let me test it first :)08/08 05:20
glguyhttp://hpaste.org/49965   this doesn’t work as is, but I’m not sure that it can’t work08/08 05:22
glguyMy idea was that you could have a module which exported everything at exactly one level, which would be inferred by where you used it08/08 05:23
glguyso you’d import it once per level08/08 05:23
glguy(and if you were only using it at one level that wouldn’t be terrible)08/08 05:23
glguybut now I have to go afk08/08 05:24
Saizanmaybe you wanted "open Functor {l} {{...}} public" but i don't think that'd work either08/08 05:25
glguyI get this behavior when I’ve used Algebra.FunctionProperties08/08 06:27
copumpkinxplat: the reflection bug is fixed08/08 17:51
Saizanhttp://www.cse.chalmers.se/~bernardy/Memos/Parametricity-Iteration-Structure.html <- nice stuff08/08 23:31
Saizanwhen i saw that A! A! appear in my personal attempt at iterating free theorems i thought i miscalculated.08/08 23:32
--- Day changed Tue Aug 09 2011
augurSaizan: wat09/08 00:42
auguroh09/08 00:42
auguri dont get what iterated parametricity is09/08 00:42
Saizansuppose you've some magical function that given an argument (x : A) returns the proof that x respects the free theorem for A09/08 00:59
Saizanthen you just call that twice09/08 00:59
augurwhat09/08 00:59
Saizando you know what parametricity is?09/08 01:00
auguri think so09/08 01:01
auguruniversal quantification over types09/08 01:01
Saizanno09/08 01:02
augurok then maybe not!09/08 01:02
Saizanfree theorems?09/08 01:02
augurstuff relating to universal quantification over types. xp09/08 01:02
augurfree theorems are those fun little equations you get from certain polymorphically parametric types09/08 01:03
Saizanok09/08 01:03
augurala wadler's paper09/08 01:03
Saizanyep09/08 01:03
auguror is it parametrically polymorphic09/08 01:03
augurits that one09/08 01:03
Saizanso, the point is that you can calculate a free theorem like that for any type, except that those theorems are pretty dull for monomorphic types09/08 01:04
Saizaniterated parametricity is simply "what is the free theorem of this free theorem?"09/08 01:05
Saizanand of course you can repeat that09/08 01:06
augurthe free theorem of a free theorem?09/08 01:06
augurbut the free theorem isnt a type its an equation of functions and such09/08 01:06
Saizanit's a type09/08 01:06
auguri suppos if you view the equation as a type sure09/08 01:06
augurbut09/08 01:06
Saizanyeah, curry-howard ftw :)09/08 01:07
auguri see09/08 01:07
augurso the map theorem09/08 01:07
augurwhat was it, flatten . map (map f) = map f . flatten09/08 01:07
Saizani think that's a specialization of the free theorem09/08 01:08
Saizan@free map09/08 01:08
lambdabotg . h = k . f => $map g . map h = map k . $map f09/08 01:08
augurwe're talking about the type   \forall X Y (xs : List X) (f : X -> Y) -> flatten (map (map f) xs) \== map f (flatten xs)09/08 01:08
auguror that09/08 01:08
augurbut crucially its that type09/08 01:09
augurhm.09/08 01:09
augurinteresting09/08 01:09
djahandarieI don't see why it's interesting yet09/08 01:09
Saizanyeah, though in their paper they have a different encoding of this stuff that's more uniform and doesn't use \== explicitly09/08 01:10
auguri'll have to read the P&DT paper09/08 01:10
augur(again?)09/08 01:10
Saizani'm not sure why iterated parametricty is interesting either, but i'm hopeful it can help with breaking some circularity that arises when i try to do the proof that runST is safe without a closed universe09/08 01:11
djahandarieAh, I see how it'd be helpful there09/08 01:11
* copumpkin just universe-polymorphized Data.Graph.Acyclic09/08 04:08
guerrilla:)09/08 04:09
Saizanyay!09/08 04:16
Saizannow do TrustMe09/08 04:16
guerrilla:)09/08 04:17
* glguy makes Induction.* “actually” universe polymorphic09/08 04:53
glguyWhat was that envvar you give darcs so that unicode is displayed?09/08 04:54
glguyFor the record: DARCS_DONT_ESCAPE_8BIT=109/08 04:57
copumpkinglguy: oh, I was just doing that09/08 04:59
glguywell, let me show you what I did and you tell me if its the same :)09/08 05:01
glguyhttp://www.galois.com/~emertens/induction-universe.patch09/08 05:02
copumpkinoh, I didn't get that far :)09/08 05:03
copumpkinwas in the process of doing something close to that09/08 05:03
glguyYou need this patch to do well-founded induction on universe polymorphic stuff09/08 05:03
glguyhttp://www.galois.com/~emertens/mergesort/MergeSort.html09/08 05:05
glguyOtherwise you can’t do this because the universe of the elements [c] is different than the universe of the relation _<_ [zero]09/08 05:06
copumpkinyeah, that's still not general enough for Tree09/08 05:08
copumpkin:/09/08 05:09
glguycan you show me?09/08 05:09
glguyI’d love additional examples09/08 05:09
copumpkinhttp://www.cse.chalmers.se/~nad/listings/lib/Data.Graph.Acyclic.html#817509/08 05:09
copumpkinthat thing09/08 05:09
copumpkinif I make everything more universe-polymorphic, it doesn't work09/08 05:09
glguyOh, you mean your changes, not my Induction changes?09/08 05:10
glguyor the <-Rec?09/08 05:10
copumpkinI mean my changes along with your changes :)09/08 05:10
copumpkinthe <-Rec09/08 05:10
copumpkinmake sense?09/08 05:16
copumpkinif you make the Tree polymorphic09/08 05:16
copumpkinthen the <-Rec doesn't fit anymore09/08 05:16
glguyuniverse polymorphic stuff is soooo verbose…09/08 05:18
copumpkinI agree :/09/08 05:23
copumpkinnow prove that your merge-sort produces a sorted list :)09/08 05:26
glguyI’ve done that before, but I can’t find it :)09/08 05:26
copumpkin:o09/08 05:26
glguyI had to reproduce that example09/08 05:26
copumpkinlost and gone forever :(09/08 05:26
glguyI just made that module universe polymorphic09/08 05:29
glguyand <-Rec was fine09/08 05:29
copumpkinhmm09/08 05:29
copumpkincan I see your source for it?09/08 05:29
glguyyes09/08 05:29
glguyask, wife calls09/08 05:30
copumpkin:)09/08 05:30
copumpkinI don't see how it can work09/08 05:32
copumpkin<-Rec : (ℕ → Set) → ℕ → Set09/08 05:33
glguyuplodaing09/08 05:34
glguyheh, yeah, I didn’t do <-Rec correctly :)09/08 05:36
copumpkinah okay09/08 05:36
augurcopumpkin: wobble09/08 06:45
copumpkinwark09/08 07:55
* copumpkin about to go to sleep09/08 07:55
arcatanhark! a pumpkin09/08 07:58
xplathuh, why were lzero and lsuc re-renamed to zero and suc when they now conflict with all other uses of those names?09/08 12:51
xplatalso, i wonder what this change was:09/08 13:31
xplat[Added an encoding of record types with manifest fields and "with".09/08 13:31
SaizanRecord.agda09/08 16:21
glguycopumpkin: you about?09/08 17:50
copumpkinyep09/08 17:52
copumpkinglguy: pong09/08 17:54
glguyI universe polymorphized .Acyclic without having to fuss with Induction.*09/08 17:55
copumpkinhow?09/08 17:55
glguyI'll show you!09/08 17:55
copumpkinthe main bit works fine, until you touch the Tree stuff09/08 17:55
copumpkin:o09/08 17:55
glguyhttp://www.galois.com/~emertens/universe-acyclic/Data.Graph.Acyclic.html09/08 17:56
copumpkinoh, Lift :)09/08 17:56
glguyhttp://www.galois.com/~emertens/universe-acyclic/AccLift.html#28709/08 17:57
glguyIs what you need to do WfRec at various levels09/08 17:57
glguyand I think that that is actually one of the submodules of Induction.WellFounded09/08 17:57
copumpkinoh, interesting09/08 17:58
glguyI think it is inverse-image09/08 17:58
glguyOH, no. It is a merger of Inverse-image and Subrelation09/08 17:59
copumpkinI see :)09/08 17:59
glguybut you can't do them separately because you have to change the levels both at the same time09/08 17:59
glguycopumpkin: if you were interested in using that implementation, I've cleaned up the code I linked to earlier09/08 18:17
glguyIt doesn't look like I immediately went to get your attention as soon as the file loaded now :)09/08 18:17
copumpkinglguy: cool, I'll check it out later when I get home from work09/08 18:59
copumpkin@ask xplat how have your agda general graphs been going?09/08 21:47
lambdabotConsider it noted.09/08 21:47
--- Day changed Wed Aug 10 2011
xplatannoying that stdlib doesn't seem to contain the symmetric closure of a poset10/08 01:53
lambdabotxplat: You have 2 new messages. '/msg lambdabot @messages' to read them.10/08 01:53
xplatcopumpkin: my generic graph stuff mostly went to the 'i don't actually need anything worthy of the name in that project' pile10/08 01:54
glguy_Ooh, anonymous pattern matching10/08 03:30
copumpkinglguy: in a new agda?10/08 04:46
dolioYes. darcs pull10/08 04:49
augureugh10/08 04:50
augurthis parametricity paper :(10/08 04:50
augurwhat is anonymous pattern matching?10/08 04:50
djahandarieI imagine just what it sounds like. Pattern matching in a lambda10/08 05:06
--- Day changed Thu Aug 11 2011
copumpkinanyone know where I can read about Data.Star? "reflexive-transitive closures of mcbride, norell, and jansson" but that doesn't help me much11/08 01:45
augurcopumpkin: search through their bib to see what they've coauthored11/08 01:55
augurprobably not many things!11/08 01:55
copumpkinI did11/08 01:55
copumpkinthen I asked in here when I failed :)11/08 01:55
augurwell11/08 01:57
augurpigworker!11/08 01:57
xplatso i started another proof :-711/08 03:32
copumpkinof what? :o11/08 03:33
copumpkinP != NP?11/08 03:33
xplatno, not ready to start that one yet :)11/08 03:34
xplatSetoids (and later ISetoids) is cocomplete11/08 03:34
copumpkin:o11/08 03:34
xplator more specifically, Setoids l is cocomplete up to diagrams of level l11/08 03:36
xplati had to build colimits, cocompleteness, and the symmetric closure of preorders11/08 03:37
copumpkinsounds like a lot of work :P11/08 03:37
xplatand now i have everything but parts of the ! for the limit cocone and the proof that ! is unique11/08 03:38
xplati don't think Sets is cocomplete in Agda, so i won't be proving that one.   also, i'm going to have to break the proofs for Setoids and ISetoids into their own modules probably, because while they don't look very epic the typechecker likes to think of them that way11/08 03:39
xplatit's probably all the sigmas11/08 03:42
xplati can't really fuse them together into custom records though because they cut into dependent sigmas right on the natural boundaries11/08 03:43
xplatvery annoying, really11/08 03:44
xplatseems like it would give a lot of nice chances to use anonymous pattern matching though!11/08 03:45
dolioSets is definitely not cocomplete.11/08 03:52
pigworkeraugur: a draft paper was started but didn't get far; there were some talks of which http://sneezy.cs.nott.ac.uk/fun/nov-07/R-star.pdf is probably the most comprehensive11/08 09:26
augurcopumpkin: theres your answer!11/08 09:31
augurpigworker: it was only for our gourdian friend there. he seemed to have the most roundabout way of finding out what your stars were11/08 09:32
pigworkerTo be fair, I think they're Kleene's stars.11/08 09:34
pigworkerBut Ulf, Patrik and I had a lot of fun with them, one AIM.11/08 09:34
augurwell, sure, but he meant your Data.Star implementation or whatever11/08 09:34
augurunless Kleene's been coding in agda from beyond the grave!11/08 09:35
pigworkerI live in hope of programming beyond the grave. I have often felt that other people wrote the programs which I am merely typing in.11/08 09:36
auguryour implementation of * looks an awwwwful lot like the definition of the monad for Cat11/08 09:37
auguroh no sorry11/08 09:37
augurrather11/08 09:37
augurthe free category over a graph11/08 09:38
augurthats what im thinking of11/08 09:38
pigworkersee the last slide11/08 09:38
augur:X11/08 09:38
augurX:11/08 09:38
augurim learning more and more about category theory and its quiet pleasing11/08 09:39
pigworkerI find I can only learn CT on a need-to-know basis, when it connects with the tangible stuff I'm programming with.11/08 09:41
pigworkerAs a result, I'm learning quite a lot of CT.11/08 09:41
auguri would agree. unfortunately, i have to learn it in the context of the tangible stuff, which means theres not much in the way of resources :\11/08 09:43
auguri mean, you try finding a good explanation of adjunctions that isn't done purely from the perspective of abstract algebra. i hear often enough that its connected to all sorts of interesting CS/PLT issues, and logic issues, but ill be damned if i can find an explanation of the idea via those perspectives11/08 09:44
augurand since i have no background in abstract algebra, im often at a loss for whats going on. homotopies? vector spaces? groups? clueless, i am.11/08 09:45
pigworkersomeone needs to write a new Rydeheard-and-Burstall, but for Agda; theirs was a CT-concepts-as-they-show-up-in-ML textbook11/08 09:47
augurim working my way through that currently. so far it seems moooostly like a typical CT intro, but with code, but my hope is that they'll also have some good examples of pre-existing ideas that get a useful CT analysis11/08 09:49
augurhonestly, OAAO was as insightful to me for CT reasons as it was for the PLT reasons, i have to thank you for that11/08 09:49
pigworkere.g., syntax-with-free-variables (renaming is the functor structure, substitution the monad structure); I learned a lot that way11/08 09:50
augurthe whole catamorphisms-abstractly thing never really made any sort of sense until i read it11/08 09:50
pigworkerthanks11/08 09:51
auguraaand i have to get to sleep, so11/08 09:51
augurnight :)11/08 09:51
pigworkerg'night11/08 09:52
xplatokay, suddenly i'm not so sure Setoids is cocomplete11/08 16:39
xplathere's the problem: in order to construct a proof that the quotient-of-indexed-coproduct actually is a cocone i needed to use data from the functor that describes the diagram11/08 16:40
xplatnamely, the proofs that it respects composition and identities11/08 16:41
xplatbut those proofs are irrelevant, so i've had to wrap part of the relation that i'm quotienting over in an irrelevant-record-field wrapper11/08 16:42
xplatbecause otherwise i couldn't take them into account11/08 16:42
xplatbut now because of that i'm not sure i'll be able to prove that ! is a proper setoid function, because now it wants me to convert a proof of equality in the quotient-of-coproducts into a proof of equality in some arbitrary setoid11/08 16:44
xplatand because of the hidden irrelevance i'm not sure there's enough information to construct the relevant proof that it wants11/08 16:45
xplati suppose if it comes down to it i could use primTrustMe11/08 16:45
xplatwait, that won't work either11/08 16:49
xplatshoot :(11/08 16:49
xplatwell, ISetoids is definitely cocomplete.  almost definitely.  i think it's cocomplete?11/08 16:50
xplati wonder if this is a manifestation of the fact that Set (or whatever your ordinary categories are enriched over) is determined by being a complete and cocomplete well-pointed topos (i think the rest of the conditions should hold for all three of Sets, Setoids, and ISetoids)11/08 16:53
xplati would have thought Setoids and ISetoids are 'equivalent enough' to share in the generalized-uniqueness, but maybe not11/08 16:53
copumpkinxplat: maybe it's cocococomplete?11/08 19:35
mokusor maybe just "mplete" :)11/08 19:40
djahandarieHe's coo coo for cocococomplete!11/08 19:43
xplatgah, up to 2147mb and still loading11/08 23:21
xplatand, i've realized i have no idea what to do on this last goal anyway11/08 23:21
xplatthe only thing left is !-unique11/08 23:22
copumpkinso it may be cocomplete after all?11/08 23:22
xplatnah, i moved over to ISetoids, since that's where i really care anyway11/08 23:23
copumpkinso I was thinking11/08 23:36
copumpkinwould it make sense to actually have a Category record take a Setoid of its objects as a parameter, instead of as a field?11/08 23:36
copumpkinif we make an object setoid11/08 23:36
copumpkinthat way you can say in the type that you're using the propositional equality setoid and make some things easier11/08 23:37
copumpkin(and have a type alias for a Category that uses that setoid)11/08 23:37
--- Day changed Fri Aug 12 2011
xplatmaybe12/08 00:18
xplathaving extra indexes can be painful at times too though12/08 00:19
xplatoh, the file didn't load12/08 00:19
xplatbecause _|_-unique is not an irrelevant field12/08 00:20
xplat(...☠☢☣☄⚛)12/08 00:23
guerrillaare non-canonical implicits (a la dominique deviese or similar) implemented in any version of agda i can check out and use?12/08 03:08
copumpkinyeah, it's been in the darcs version for a few weeks now12/08 03:09
djahandarieI'm consideribly sure they are in darcs12/08 03:09
guerrillaok12/08 03:10
guerrillaawesome12/08 03:10
guerrilla'cos i have a little mini-project i want to do and haskell is killing me12/08 03:10
djahandariecopumpkin, we should switch everything in the CT library to use them12/08 03:10
djahandarieIt'd be a good stress test at least...12/08 03:10
copumpkinthat wouldn't really work very nicely12/08 03:11
copumpkinit would once we start making a category-extras-ish thing12/08 03:11
copumpkinwith agda categories and structures12/08 03:11
xplatcopumpkin: oh, btw i got cocompleteness loading much faster and it's almost done.  1 more hole and this time i know what to put in it12/08 03:44
xplatugly as hell though12/08 03:44
copumpkinsweet :)12/08 03:45
xplatthe whole thing is part 1 of my plan to make profunctors compose12/08 03:45
copumpkinoh!12/08 03:46
copumpkin'tis a noble goal12/08 03:46
copumpkinwhy do you need all that to make them compose?12/08 03:46
xplatwell, apparently coends can be reduced to colimits12/08 03:47
xplatperhaps by the intermediary of pointwise kan extensions12/08 03:48
xplatbut i don't think the colimit diagrams that come up will all necessarily be 'nice', or even finite12/08 03:49
xplatthus, cocompleteness12/08 03:50
xplatif it turns out i don't need that much power, well, at least i learned something12/08 03:51
copumpkinsounds cool12/08 03:52
* guerrilla wishes he knew what you guys are talking about :P12/08 03:59
xplatit looks like actually for coends i only need (small) indexed coproducts and binary coequalizers12/08 16:32
--- Day changed Sat Aug 13 2011
xplatargh13/08 01:21
xplati have a type that's dependent on an irrelevant item13/08 01:21
xplatbasically : i have a function that will give me an irrelevant propositional equality13/08 01:22
xplati have a function that produces a type dependent on that equality13/08 01:22
xplatbut then i have to make that function irrelevant13/08 01:22
xplatand then i can't seem to use it in the type of another function, even an irrelevant function13/08 01:23
xplatis there some way around this, or am i just fucked?13/08 01:23
augurxplat: i dont think its possible to be dependent on irrelevant arguments in agda13/08 01:26
augurdunno why13/08 01:26
auguryoud think that as long as its definitionally irrelevant, type relevancy should be ok13/08 01:27
dolioThere are technical quirks about Agda that prevent dependent irrelevancy from being as simple as it is in the literature.13/08 01:28
xplatyeah, i mean if you computed something that you typed based on this you could end up doing something unsound like mistaking an ext postulate for a refl, BUT.  anything that's irrelevant won't be computed anyway?13/08 01:28
dolioThe lack of it is kind of disappointing to me, though.13/08 01:29
auguri want irrelevant arguments to be usable in dependent contexts to be able to state things about kinds of induction principles13/08 01:30
xplatif i can't do this then i guess it's back to writing Yet Another Annoying Heterogeneous Equality Wrapper13/08 01:31
augurnamely the kinds that are almost-but-not-quite catamorphisms except at the type level13/08 01:31
dolioIt's questions like: Agda's definitional equality is type-directed. You need to eta expand some things. But, you may not know whether you need to eta expand once you've erased things from the type.13/08 01:31
augurdependency introduces extra arguments that can be matched on by the algebra, and i dont like that13/08 01:32
xplatdolio: hm, that could be a problem13/08 01:33
xplatof course in this case the only thing i'm erasing is a neutral-headed type constructor13/08 01:33
xplatwell, i guess at point-of-use it could be more13/08 01:34
xplati guess i mean 'neutral-headed application' anyway13/08 01:34
xplatthis all happened because i was trying to avoid introducing a different type of 'indexed setoids' when i already had 'functions from setoids to things'13/08 01:36
xplatbut instead i'm going to end up introducing a type of 'heterogeneous equalities'13/08 01:37
xplatwhich is different from the one that i already have13/08 01:37
xplathm, and agda is doing a lousy job of remembering the indexes on my records too13/08 01:48
xplati have From ⟶[ ct , ℓt ] = From ⟶ set→setoid (Setoid ct ℓt)13/08 01:49
xplatset→setoid is exactly what you would think13/08 01:49
xplatwhen i use something of this type, agda cannot figure out what From was13/08 01:50
xplatFrom directly becomes a type parameter for a record type13/08 01:50
xplati would have thought that would be a pretty easy thing13/08 01:51
xplati can't even see where eta-expanding would cause confusion here, unless it's eta-expanding *all the way back when the record type is being defined* maybe13/08 01:53
xplatand even then it's more 'hey that sounds complicated so i might have missed something' rather than 'OH, it's because of THAT'13/08 01:53
xplatokay, my type inference problem was that agda failed to see through a single-clause, type-constructor-headed function13/08 15:06
xplatif i inlined it in the type of my other function, everything worked13/08 15:07
xplatexcept for, of course, the irrelevant dependence i wanted that function for in the first place :(13/08 15:07
xplatat least it means my approach would have worked for regular setoid pis13/08 15:08
xplatoh, hm, that wasn't the problem, it was the OTHER helper function i was using that i inlined without realizing it13/08 15:11
xplatokay, so i have ‘.test : ∀ {cf ℓf ct ℓt} {From : Setoid cf ℓf} (To : From ⟶[ ct , ℓt ]) (x : Carrier From) → (_[$]_ {ct = ct}{ℓt = ℓt}{record { _≈_ = _; isEquivalence = Setoid.isEquivalence From }} To x) → Set ℓt’13/08 15:24
xplatall those implicits/record fields that are shown are the ones that are yellow with a normal application; the ones that are filled are the minimum necessary to remove all yellow13/08 15:25
xplat_[$]_ : ∀ {cf ℓf ct ℓt} {From : Setoid cf ℓf} → (From ⟶[ ct , ℓt ]) → Carrier From → Set ct13/08 15:30
xplatf [$] x = Carrier (f ⟨$⟩₀ x)13/08 15:30
xplatif i inline [$] there are no problems13/08 15:30
xplat_≈_ fills in if i provide EITHER isEquivalence OR ℓt, weirdly13/08 15:31
xplatwhy isn't the known type of To enough to provide this information?13/08 15:32
xplati guess _≈_ fills in for ℓt because it is the only type in scope in Set ℓt, but if agda can make such an esoteric deduction why does it fail the obvious?13/08 15:33
xplatwait, no, my last line doesn't even make sense, that _≈_ isn't even in Set ℓt, it's in Set ℓf, and ℓf already fills in just fine ...13/08 15:35
xplati just thought of a great idea13/08 16:14
xplatmeta names should print out not with an absolute sequence number of the meta, but with an identifier and a sequence number of metas with that identifier13/08 16:16
xplatlike, if it's a meta for a sort, then the identifier is 'sort'.  if it's a meta for an implicit or record field (after eta expansion), the identifier is the name of that.13/08 16:17
xplatthat way it would be easy to see what's missing when you look at the unsolved metas in emacs, and compiler traces would also diff better13/08 16:17
xplat(guess what i'm doing now?  :)13/08 16:18
xplatso if i provide just the levels it can solve the rest (because then it doesn't eta-expand the Setoid record)13/08 16:50
xplatit can't figure out the levels and that blocks the comparison of the type of the actual and formal f arguments of _[$]_13/08 16:51
xplatinstead it turns it into a constraint, creates metas, eta-expands them to figure out the carrier, and blooey13/08 16:52
xplatand it never does figure out the levels, even when it has the carrier which i would have thought would be enough to figure out at least the carrier level13/08 16:53
xplatbasically comes down to the fact that it won't (can't?) proceed down the telescope of _⟶[_,_] to the later arguments until it is convinced the earlier ones are unifiable?13/08 16:59
xplator technically of _⟶_ since it converts first13/08 17:01
xplatpigworker: do you understand why this is done this way?  i can't figure it out ... seems levels usually have to come first and they are among the hardest things to solve first because of lub, so this is going to miss a lot of chances ...13/08 17:03
xplati guess the obvious reason is that you can't be sure you're comparing two terms of the same type, in general, if you skip something and keep walking down the line13/08 17:12
pigworkersolving heterogeneous constraints is a paranoid business, but not pointless; even so, it's good to keep as many constraints homogeneous as possible by solving the early ones13/08 17:12
pigworkerbasically, you can decompose rigid-rigid constraints at any time, but you can only solve for variables homogeneously13/08 17:13
xplathm, but the early ones are often going to be levels ... and levels are as i mentioned hard to solve because a lot of level constraints that pop up include lub13/08 17:14
pigworkeryes; lub is bad news13/08 17:14
xplatbut often there is something that comes up 'later' that pins the levels down exactly13/08 17:15
pigworkersure; you can't get away with just working left-to-right13/08 17:15
xplatand also often because of the lubs you can get more information about whether a constraint is homogeneous than merely checking off solved variables would indicate13/08 17:16
pigworkeryou sometimes need to pay to check if a constraint is actually homogeneous, even though it's not leftmost13/08 17:16
xplatah, but is agda actually paying the tolls it needs to?  looks like it's not happening here ...13/08 17:18
xplatwell, actually it looks like a lot of work is happening, but nothing gets done13/08 17:19
pigworkerI don't know how Agda's constraint-solving strategy works. I do know I never enjoy writing them myself.13/08 17:20
xplatah13/08 17:20
xplatBlockedConst (Lam Hidden (Abs "cf" Lam Hidden (Abs "\8467f" Lam Hidden (Abs "ct" Lam Hidden (Abs "\8467t" Lam Hidden (Abs "From" Lam NotHidden (Abs "To" Lam NotHidden (Abs "x" Var 1 []))))))))13/08 17:21
xplatit seems like that's what keeps it from proceeding, in the end13/08 17:21
pigworkerI don't know how to read that.13/08 17:22
xplati'm a little fuzzy myself, but looks like BlockedConst '(\ {cf lf ct lt From} To x -> To)13/08 17:23
xplatnow if only i knew what that referred to13/08 17:24
pigworkerIt's the BlockedConst bit that confuses me.13/08 17:26
xplatme too ...13/08 17:27
xplatit doesn't appear anywhere else in the compiler trace anyway13/08 17:35
xplatoh, that's what agda thinks _64 is, but it won't commit to it unless it first knows 5 other things13/08 17:46
pigworkeraha, so what are the constraints which block that solution?13/08 17:49
xplatthree level constraints of the form _n lub <stuff> == a lub <stuff>, one constraint that From equals a partially instantiated record, and one constraint that 'my-fun {a lub c} (MyType c a)' == 'my-fun {_n lub c} (MyType c _n)'13/08 17:56
pigworkerso, a big clue that n=a, but nothing conclusive13/08 17:57
xplatseems conclusive to me, but not apparently to agda13/08 17:57
pigworkerdepends on what my-fun does13/08 17:58
xplatah, true.  the result of my-fun is a record one of whose relevant fields is the explicit argument of my-fun13/08 17:59
pigworkertoo many variables, too few constraints13/08 17:59
xplatspecifically, my-fun x = record { Carrier = x ; ... }13/08 18:00
xplatbut the type of the record has a parameter that is instantiated with the implicit argument13/08 18:01
xplatit seems that after it generates these guards on assigning _64, it always checks them in order when solving constraints13/08 18:09
xplatso whenever it adds more information, agda asks 'can i solve _n lub <stuff> == a lub <stuff>?  no, time to move on'13/08 18:10
xplatand never pays attention to the constraints lower down the list that could actually solve something13/08 18:10
Saizanis it safe to deduce x = y from record { Carrier = x ; ..} = record { Carrier = y; ..} without knowing if the two sides have the same type?13/08 18:11
xplatand the only reason _64 is generated in the first place (it's an explicit argument, not something that should need a meta) is because agda isn't sure the call was type-correct without knowing those levels13/08 18:12
xplatSaizan: good question.  it probably depends what else you know about their types, i would think13/08 18:12
xplatit's probably safer in newer agdas where you're not allowed to pattern match on levels13/08 18:16
xplat(the only things not known to be equal in those two types are level parameters)13/08 18:17
Saizanhere one is pretty sure there's no pattern matching going on13/08 18:18
xplattrue13/08 18:19
xplatthe type of the Carrier field is Set (unknown parameter)13/08 18:20
xplati wonder to what extent one truly can ignore size constraints when solving other type constraints13/08 18:24
xplatit would seem to simplify things a lot if they could all be put off as long as necessary to solve other constraints ...13/08 18:25
xplatbut i'm not sure that's true even if you can't pattern-match on them13/08 18:25
Saizanwe should formalize agda's definitional equality and check :)13/08 18:26
xplathere's where it would really help to have a good metathloses13/08 18:26
xplati can kind of see why in the stdlib they invent a weird concept like 'IndexedSetoid' and use it instead of setoid functions to a universe of setoids13/08 22:28
xplatyou really can't make your own function arrow13/08 22:28
xplatit has a completely different way of handling universe polymorphism13/08 22:28
xplatcompared to other type formers13/08 22:28
xplatand without that, i end up writing two levels on every application of everything13/08 22:30
xplatand that's not even counting the injuries i get from badhandling of irrelevant record fields13/08 22:30
xplat*bad handling13/08 22:30
xplat(i'm sure it also helps that sets have just one level instead of two so there are fewer lubs and more constraints can be solved)13/08 22:37
copumpkinif I have free variables in a solver I'm writing, should I treat them existentially or universally?13/08 22:53
copumpkinwhen I see x + y == y + x, that suggests universal to me13/08 22:54
copumpkinbut sat solvers seem to be existential, so I'm not sure13/08 22:54
dolioIt depends what they mean by that.13/08 22:56
dolioPresumably you don't want to solve for particular x and y such that that holds.13/08 22:57
dolioWhich would be finding a proof of exists x y. x + y == y + x13/08 22:57
xplatargh, if agda's not having irrelevant opens, it really needs to have something like scala's _ to suppress instantiation of implicit variables13/08 22:58
dolioHowever, you can find a proof for forall x y. x + y == y + x by finding a proof of x + y == y + x with x and y held abstract.13/08 22:58
dolioWhich some people might call existential.13/08 22:58
dolioFrom the perspective of the solver, anyway.13/08 22:59
xplatinstead of just ‘.refl : _ ; refl = E.refl e’ i need ‘.refl : _ ; refl = \ {i : I} {x : Carrier i} -> E.refl e’13/08 22:59
xplatannoyingly it can't even infer the ‘: I’ if i take that out13/08 23:00
dolioI don't think that's a very precise use of 'existential', though.13/08 23:01
xplatcopumpkin: you should probably either treat them universally or complain and make the user bind them13/08 23:01
dolioIt's a variable on the left of a turnstile.13/08 23:01
dolioThere are no free variables. There's only variables bound by a quantifier, and variables bound in the context. :)13/08 23:02
xplatcopumpkin: what kind of solver are you writing?13/08 23:58
--- Day changed Sun Aug 14 2011
copumpkinplaying with presburger :)14/08 00:38
copumpkinpresburgler14/08 00:39
xplatah14/08 01:10
xplatyeah, you should force all variables to be quantified14/08 01:10
xplatman, i'm having the hardest time converting a --> into Setoid c l into an IndexedSetoid14/08 03:28
xplatmy first attempt at the heterogeneous equality type couldn't prove symmetry or transitivity14/08 03:29
xplatbecause you could only recover the identity of the carrier types, not of the relations14/08 03:29
xplatso you could happen to have the same carrier type and a different relation and have an inhabited type corresponding to that situation, where the symmetric type would have different inhabitants because of the different relation14/08 03:31
xplatand the type i tried to make to fix that won't typecheck14/08 03:31
xplatbut it's necessary to do this somehow if i want indexed products in Setoids14/08 03:34
xplater, ISetoids either14/08 03:34
bxc-paella|  main = putStrLn (fromString (show 2001))14/08 15:18
bxc-paellathat should not segfault?14/08 15:18
bxc-paellahttp://pastebin.com/7ZrSky5E14/08 15:20
* bxc-paella had some broken code that was not showing 2001 correctly (instead showing 2100) and then realised that there was a stdlib implememntation of integer show, but that does this for me14/08 15:20
xplati really need to get a better handle on with rewriting somehow, the error messages are so opaque14/08 15:58
xplati have this heterogeneous equality type for setoids that kind of works, but it contains a propositional equality on two setoids14/08 17:01
xplatand i have never been able to match on that as refl no matter what twisty things i try to do with the with clauses14/08 17:02
xplatno luck so far using auxiliary functions either :(14/08 17:04
xplatactually, i am finding it almost impossible to match on an equality of type To <$> i == To <$> j14/08 17:58
xplatbecause if i match To <$> j in a with as well, it complains that the equality has the wrong type14/08 17:59
xplatbut if i don't, it complains everything else has the wrong type14/08 17:59
copumpkintough : ∀ {a} {A : Set a} → ¬ (∀ (x : A) → const ⊥ x)14/08 20:24
copumpkincan that be proven?14/08 20:24
Saizanonly for NonEmpty A14/08 20:25
copumpkinah, I see14/08 20:26
SaizanNonEmpty being Id, i guess :)14/08 20:26
copumpkintough : ∀ {a} {A : Set a} → (¬ (¬ A)) → ¬ (∀ (x : A) → const ⊥ x)14/08 20:26
copumpkinthat's easy, but meh14/08 20:26
xplatanyone know anything about proving equality of records from equalities of their fields?14/08 22:13
xplati have a record with two fields, one dependent on the other, and one extra field that's irrelevant14/08 22:16
xplatoh, and it has no constructor14/08 22:16
copumpkinconstructors are just syntactic sugar anyway14/08 22:16
xplatno they're not14/08 22:16
copumpkinno?14/08 22:16
copumpkinhmm14/08 22:16
xplatrecord { x = a ; y = b } is not a valid pattern14/08 22:16
copumpkinyeah, you can't pattern match on records14/08 22:17
copumpkinit desugars a pattern match on them to projections14/08 22:17
copumpkinI thought14/08 22:17
xplatthat's the key thing that's hanging me up14/08 22:17
copumpkindo you have a simple example of what doesn't work?14/08 22:18
Saizancurrying your theorem should probably help14/08 22:18
Saizanbut that'd need HetEq14/08 22:19
xplatwell, what doesn't work is matching on an equality between two projections, because the indices on == don't match14/08 22:19
xplatmatching on an equality between projections along with a projection from one record (as a with) kind of works, but it doesn't refine the dependent field14/08 22:20
Saizanxplat: http://hpaste.org/5031014/08 22:29
copumpkinwhy do you need heterogeneous equality on the fst?14/08 22:30
Saizani just didn't want to import another equality14/08 22:31
copumpkinah :)14/08 22:31
Saizani find it weird that it needs the {A = A} {B = B} only on one side14/08 22:34
xplatwhoa, the first part looks like what i came up with while i was waiting for an answer, the second part is WHOA14/08 22:39
xplatSaizan: it needs it on one side so it can infer implicit argument A of ==14/08 22:40
xplatthat is, the type14/08 22:40
xplatyou could put it on either side or straight on ==14/08 22:40
Saizanbut it's Het14/08 22:41
Saizanthey could be of different types14/08 22:41
xplathm, good point14/08 22:46
xplatargh, i copied that but i had to make the second one irrelevant because i had to project out the irrelevant fields and i have no irrelevant pi on 2.2.10 to stuff them back in with14/08 22:47
xplatit's not a huge problem since i only need it in an irrelevant context, but ...14/08 22:48
Saizantricky14/08 22:53
copumpkinis anyone getting a lot of "Found an implicit application where an explicit application was14/08 22:58
copumpkinexpected"14/08 22:58
copumpkinerrors where they don't belong?14/08 22:58
copumpkinaround with blocks and rewrites14/08 22:58
xplathm, hard to notice, since i kind of expect mysterious weirdness around with blocks :)14/08 23:02
xplatuh-oh.  it seems like the things i want to be equal might not be equal14/08 23:03
xplatdata family, different indexes14/08 23:03
xplater, different parameters14/08 23:06
xplati didn't even want a data family in the first place ...14/08 23:11
PeakerCan dependent type checkers mechanically know if there's just one value to a type -- making the particular code irrelevant?14/08 23:12
xplatthe second doesn't always follow from the first14/08 23:12
Saizanit depends on what you mean by irrelevant14/08 23:13
PeakerWell, it frees up the optimizer to choose any other code that generates that value14/08 23:13
Saizanheh, if you're talking about runtime you might not want to generate that value at all14/08 23:13
Saizananyhow the answer is probably "in some cases yes"14/08 23:14
Peakerwell, that value could be the result of a (linear) search in a sorted array -- and it would be nice if the type was enough evidence that it is OK to interchange that with a binary search on the array14/08 23:14
xplatit can be enough evidence, but you still have to write the binary search14/08 23:16
Peakerwell, ideally the IDE can djinn up alternate ways to create that value from the stdlib -- and try to offer different options (e.g: binary search in this case)14/08 23:17
Saizanthat's still nowhere in sight, i'd say14/08 23:21
Saizanthough you already get some simpler things14/08 23:22
PeakerSaizan: but for it to be valid to suggest djinn replacements at all -- it would need to prove that there's just 1 value of that type.. is it mechanically testable in the general case? In interesting special cases?14/08 23:28
Saizanto suggest replacement i think it'd be sufficient to show that it's equal to the code you have14/08 23:30
Saizan*observationally equal, i mean14/08 23:30
Peakeryeah -- well showing the type has just 1 value is a way to show that14/08 23:30
Saizananyhow, i don't know of any specific result on deciding if a type is a singleton14/08 23:30
Saizani'd guess that as for emptyness you can't get a complete decision procedure, and the easy cases will be those where the normalized type doesn't contain functions but only constructors14/08 23:32
xplatwell, fuck14/08 23:36
xplatwithout the should-be-irrelevant index that blocks equality, agda drops the ball on inferring the irrelevant field as usual14/08 23:37
xplat(the first 'irrelevant' in that sentence is not the technical term)14/08 23:37
xplatthere are days i really hate me some eta14/08 23:38
--- Day changed Mon Aug 15 2011
xplathttp://hpaste.org/5031515/08 00:06
xplati get a type error when loading this :(15/08 00:06
xplatsomething about /home/james/proj/copumpkin/categories/Categories/Support/SetoidPi.agda:130,71-8715/08 00:07
xplatsuc (ℓt ⊔ ct) != suc ℓt ⊔ ct of type Level15/08 00:07
xplatwhen checking that the expression resp-helper₂ i∼j has type15/08 00:07
xplat_[_≈_] (To$ i) ≅ _[_≈_] (To$ j)15/08 00:07
xplati don't see anywhere the latter level could be coming from15/08 00:08
xplatnever mind, i found it15/08 00:21
xplatDone!15/08 00:59
xplater.15/08 01:00
xplatactually, i still have an unsolved level constraint from who-knows-where :(15/08 01:01
xplatand it's a good thing it's not solved, since it's not true15/08 01:02
xplat(Set (suc (ℓt ⊔ ct))) =< (Set (ct ⊔ ℓt))15/08 01:02
xplatgarrrh, just when i thought i was done15/08 01:05
xplatokay, *now* i'm done15/08 01:08
xplati just hope with these types i still have small products15/08 01:08
xplathm, seems like to make this really tractable i still need an intermediate abstraction of families of products and arrows15/08 02:21
xplat*families of objects and arrows15/08 02:23
xplatthere are going to be a lot of bald yaks running around the hills by the time i get profunctor composition done :(15/08 02:33
copumpkinsounds like it :P15/08 03:16
xplatcopumpkin: so i noticed some annoying things while i've been doing this15/08 16:58
copumpkinoh?15/08 16:59
xplatinstead of being equivalent to internal categories in ISetoids, our raw categories are equivalent to internal ISetoid-enriched categories in Set15/08 17:00
copumpkin:o15/08 17:01
xplatamong other things, this means that ISetoids doesn't embed in Cat as discrete categories, and (probably) weighted limits are different from conical limits15/08 17:01
copumpkinhow would you change that?15/08 17:02
xplatSetoids embeds in Set but not as discrete categories, and i think ISetoids will embed in Setoids, but i don't think the adjoints that are usually there are there15/08 17:02
xplati'm not sure i would change it.  i'm not sure an irrelevant setoid of objects is doable, and a relevant setoid of arrows is almost certainly not :(15/08 17:03
xplatalthough i might try writing an experimental library to do Setoids-logic with relevant, single-leveled setoids15/08 17:05
xplatyou inherently lose a lot of essential convenience features from Set-logic, though, like automatic promotion into implicit functionspaces15/08 17:06
xplatso i'm not sure if even with a single index the setoids would compose nicely15/08 17:07
xplati'm starting to think, though, that something like Agda won't be usable for a lot of Real Math without some quotient types15/08 17:10
xplator else a lot of inference improvements15/08 17:10
copumpkinyeah15/08 17:12
xplatin particular it appears hard to deal with anything that has more than one level parameter and lubs them, or any universe codes or other implicits containing irrelevant fields15/08 17:16
xplatbecause you'll be going along fine, and suddenly something random will cause eta-expansion to come before unification and *boom*, you lose your codes15/08 17:17
Saizando you think there's room for eta-expansion to be less blunt?15/08 17:31
xplatprobably, or for inference of irrelevants to be more aggressive15/08 18:53
xplatmaybe a little of bots15/08 18:53
xplat*both15/08 18:53
djahandariecopumpkin, damn you. :) Been hacking on-and-off on making this <= monad possible in Haskell. I'm getting closer but it's damn slow :p15/08 20:40
copumpkinlol15/08 20:40
copumpkinyou have the category instance already?15/08 20:40
djahandarieOh sure15/08 20:41
djahandarieOn the Functor right now15/08 20:41
copumpkinyou might as well make an initial object too15/08 20:41
djahandarieMaking S a functor on it was easy15/08 20:41
copumpkin:)15/08 20:41
djahandarieBut the really annoying thing is making ClampEven a functor15/08 20:41
copumpkinlol15/08 20:41
djahandarieBecause it's a type family15/08 20:41
copumpkinwell, you need a different functor class, right?15/08 20:41
djahandarieYes15/08 20:41
djahandarieMight as well show you what I have so far15/08 20:41
copumpkinyou probably don't want it to be a type family15/08 20:41
copumpkinsince you can't partially apply type families15/08 20:42
djahandariehttp://hpaste.org/5034215/08 20:42
djahandarieYeah15/08 20:42
djahandarieWas going to get past that blockade once I got there15/08 20:42
djahandarieI actually don't need any of those closed things, just got sidetracked to see if I could actually do that15/08 20:42
djahandarieTrying to write clampEvenTimesTwo right now, attempting to find a good way to do it. Probably need to change how I'm doing clampEven15/08 20:43
copumpkinlol, you've done a lot :P15/08 20:43
copumpkinvery nice15/08 20:43
djahandarieIf I have clampEvenTimesTwo, that's enough to convince the compiler that c is valid15/08 20:44
copumpkinzomg15/08 20:44
copumpkinunsafeCoerce15/08 20:44
copumpkindjahandarie--15/08 20:44
djahandarieHeh15/08 20:45
djahandarieNone of that is actually required15/08 20:45
djahandarieUsed it to write divTwo15/08 20:45
copumpkinyeah15/08 20:45
djahandarieAnd it's safe as far as I can tell, as long as you actually keep the type family closed15/08 20:45
djahandarieI was originally using ~ for a lot of this, but then had to move to :=: because the constraints were unifying too early for me15/08 20:47
copumpkinah15/08 20:47
copumpkinif you want an initial object, the other LTE representation might be easier to work with15/08 20:48
copumpkinnot that there's really much point to making one :P15/08 20:49
djahandarieI wonder if it'd be possible to try and port EqReasoning type stuff to Haskell15/08 20:50
djahandarieI imagine it'd be a royal pita if it is possible15/08 20:50
xplatan example of where that eta stuff gets painful15/08 20:52
xplat (≜-trans {π▹ uncurry gs} {gs} {fs} (commute∗ gs) (≜-sym {fs} {gs} eq))15/08 20:52
xplatif the setoids were all relevant ones, it would be:15/08 20:52
xplat (≜-trans commute∗ (≜-sym eq))15/08 20:53
xplat(and there would be an fs left out of the previous line too)15/08 20:54
xplatdjahandarie: did you ever finish that triangle law?15/08 20:56
djahandarieI didn't... maybe I'll hack on that tonight15/08 20:56
xplatcopumpkin: i finished IndexedProduct, now i do IndexedProducts ... then turn around to coproducts15/08 20:58
copumpkin:O15/08 20:58
xplatactually there might be some laws i want for IndexedProduct, but i probably won't know what they are until i miss them :)15/08 20:59
xplatwhen i did binary coproducts instead of reproducing those looooong proofs of commutativity-and-associativity-up-to-iso, i just reflected them from the opposite category15/08 21:01
xplatthe machinery to reflect them was less than those two proofs alone15/08 21:01
xplatah, dammit15/08 21:12
xplatthe natural order of specifying the category and the shape doesn't seem to let me say 'small products'15/08 21:12
xplatwhen i did Cocomplete i cheated and said the indexing category must have the exact same sizes as the target category15/08 21:14
xplatit's annoying to have to put lifts in15/08 21:15
xplatbut i don't see any other way :(15/08 21:15
copumpkincould you maybe stick a function of some sort into the universe level?15/08 21:16
copumpkinthat's how N-ary works15/08 21:16
copumpkinkind of voodooish15/08 21:16
copumpkinbut if you're not pattern matching on anything that probably won't help15/08 21:16
xplati can't build a function like that out of lub and suc15/08 21:17
xplatyou can only bound universe levels below, not above, and still have any ability to specify them15/08 21:18
xplati.e. you either have an exact level or 'at least foo'15/08 21:18
copumpkinyeah15/08 21:19
xplatso you can't say 'for a given Thingy of size y, feel free to hand me a bar of size <= y', you can only say, 'given a bar of size z, feel free to give me any foo of size >=y'15/08 21:24
xplatnot really the right quantifier order15/08 21:24
copumpkinyeah15/08 21:24
--- Day changed Tue Aug 16 2011
xplatgah, this irrelevant field lossage is killing me16/08 00:04
xplat _⋉π {As} {Bs} fs = _⋉_ {Ys = As} {Bs} fs (π {As})16/08 01:28
xplatyou know what that would be with relevant setoids?  nothing, because i'd be using ⋉ π inline instead!16/08 01:28
xplatand even after doing all that, i still can't use it as an operator because i still need to supply As and Bs at the call sites16/08 01:29
xplatgnnnnnrrrrgghhh16/08 01:30
xplatwell, there will be a very nice library waiting when agda is fixed :(16/08 02:15
pumpkinaww16/08 03:08
pumpkinwhat do you need changed? did you file bugs?16/08 03:08
xplatwell, i'm not sure exactly what circumstances16/08 03:35
xplati made a test before that showed inferring a record from a return type context won't work if it has irrelevant fields16/08 03:35
xplatbut apparently there are other circumstances when it fails too16/08 03:36
xplati'd kind of like to get a better characterization of when it happens, or at least multiple tests16/08 03:37
xplatuncurry-cong∗ {Cs} {_} {_⋉_ {Ys = As} {Cs} (_◽_ {As} {Bs} {Cs} fs gs) (π {As})} {_⋉_ {Ys = Bs} {Cs} fs (_⋉_ {Ys = As} {Bs} gs (π {As}))} (assoc-◽⋉ {Ys = As} {Bs} {Cs} {fs} {gs} {π {As}})16/08 16:47
xplatshould be: uncurry-cong∗ assoc-◽⋉16/08 16:47
xplatbut when i try to make a simple demo test, everything works16/08 17:14
leohi16/08 19:49
leoi have a problem with Emacs (or Agda?), my question marks are not replaced with holes :-S16/08 19:51
leoC-c C-l doesn't work16/08 19:51
leo(i'm sorry for my english)16/08 19:51
leohelp16/08 19:52
Saizando you have a *ghci* buffer?16/08 19:59
--- Day changed Wed Aug 17 2011
ppavelhi17/08 14:39
bxc-paellahi17/08 14:54
xplata test instance, unfortunately pretty involved: http://hpaste.org/5040017/08 16:47
xplatit shows, though, that eta expansions that 'work' in the normal case can fail in the presence of irrelevance17/08 16:50
copumpkinwow :)17/08 16:59
xplatthere was a much smaller one i had pasted involving return types17/08 17:07
xplatcopumpkin: does that one work the same on darcs agda?17/08 17:07
xplathttp://hpaste.org/48930 was the other one17/08 17:09
xplatthat one is more clearly wrong without comparing it with the relevant case17/08 17:12
xplatbut i don't think the new test and the simple test fail because of the same trigger of eta expansion17/08 17:13
xplatcopumpkin: so i reworked some of the proofs in Product based on the odd, but possibly true, principle that it is easier to prove that you can construct a product structure than to prove two complex morphisms are inverse17/08 22:16
copumpkinoh?17/08 22:16
xplatcopumpkin: and then constructing all the isos from pairs of product structures in a uniform way17/08 22:17
xplati think there are considerably fewer lines in the new versions of the proofs even if you count the stuff i added to Categories.Square17/08 22:18
copumpkinyay17/08 22:18
xplati think the stuff in there will be generally useful too (‘a . b = c & c . d = e -> a . (b . d) = e’ and its mirror image plus three 'cancellers' for pairs that compose to id)17/08 22:20
xplatoh, and now i further refactored that to have 'pull left' and 'pull right'17/08 22:51
xplatwhich is basically 'associate in that direction then apply the equation on that side of the .'17/08 22:51
copumpkinneat17/08 22:51
copumpkinwe need lots of higher-order proof combinators!17/08 22:52
copumpkinmmm17/08 22:52
xplatit turns out one does that a LOT in equational reasoning17/08 22:52
copumpkinyeah17/08 22:52
xplateven most of the simple combinators in Squares itself benefit17/08 22:53
xplatactually Squares only had *one* use of assoc that wasn't a pull17/08 22:54
copumpkincool :)17/08 22:54
copumpkinthere's no way to use reflection to ask for the structure of a type, right now, is there?17/08 22:55
xplatno17/08 22:55
copumpkindamn17/08 22:55
xplatyou could feed in all the constructors by hand though17/08 22:56
xplatto make a type descriptor for further use in reflection17/08 22:56
copumpkinyeah, but that's ugly :/17/08 22:57
xplatthere's also no way to make a map keyed by Names with sublinear lookup17/08 22:57
copumpkinI was hoping to write a decidable equality automatically for finite types17/08 22:57
copumpkinxplat: why not?17/08 22:58
xplatbecause the only operation on Names is equality17/08 22:58
copumpkinoh17/08 22:58
copumpkinlame17/08 22:58
xplatyou could go all levitate-y and make a universe of types where all the finite ones have decidable equality17/08 22:59
copumpkinyeah17/08 22:59
copumpkinbut I just wanted to save myself some typing really17/08 22:59
copumpkinwhen writing finite types17/08 22:59
copumpkinthere's a project on the github agda that does that with some scripts17/08 23:00
copumpkinbut it'd be nice to do it internally17/08 23:00
xplatah, yeah, none of the ways that works saves you much typing, except maybe the 'mapping to Fin' way17/08 23:00
copumpkinyeah17/08 23:02
* copumpkin tries to remember why he wrote Grothendieck : ∀ {o ℓ e o′} {C : Category o ℓ e} → Functor C (Sets o′) → Category _ _ _17/08 23:02
copumpkininto Sets rather than Setoids17/08 23:02
dolioWhat does that express? I forget.17/08 23:08
copumpkinit's a bad name, but it's this thing17/08 23:08
copumpkinhttp://en.wikipedia.org/wiki/Grothendieck_construction17/08 23:09
copumpkinthe databases as categories construction uses it17/08 23:09
copumpkinto talk about actual rows17/08 23:09
xplatah, that would make sense17/08 23:09
xplatthe fiber-based view is great for talking about relations without mentioning the rows17/08 23:10
xplatin fact some of the constructions make sense even without rows existing17/08 23:10
* copumpkin wonders if this setoid grothendieck thing is even possible17/08 23:25
copumpkinah, I'm just being dumb17/08 23:41
copumpkinyay17/08 23:58
copumpkinhmm actually, I got the type wrong for my grothendieck of hom thing17/08 23:59
copumpkinI wonder what this constructs17/08 23:59
--- Day changed Thu Aug 18 2011
copumpkinhmm, it isn't very interesting, whatever it is18/08 00:06
glguyeww, I think that a bug in the development version of agda makes is such that I don't learn about a type unless I name the implicit argument18/08 00:57
glguy  AddA : ∀ {a} → IsNumber a → BinOpA a a a18/08 00:57
glguyI have this constructor18/08 00:57
glguy  auxBin (AddA {a} p) x y = {!AddA!}18/08 00:57
glguywithout naming {a} agda doesn't know that x and y have the same type18/08 00:58
glguyperhaps I need to pull18/08 00:58
ppavelV6hi everybody.18/08 16:05
ppavelV6i just defined18/08 16:06
ppavelV6promote : {A : Set} → .A → A18/08 16:06
ppavelV6without using postulate. is it ok? :)18/08 16:06
copumpkinhum18/08 16:07
copumpkinso promote x = x18/08 16:07
copumpkin?18/08 16:07
copumpkinthat seems unfortunate18/08 16:07
ppavelV6promote x = x gets (correctly?) rejected :)18/08 16:08
ppavelV6mine is a bit trickier18/08 16:08
ppavelV6record Promoted (A : Set) : Set where18/08 16:08
ppavelV6   constructor irrelevant18/08 16:08
ppavelV6   field18/08 16:08
ppavelV6     .val : A18/08 16:08
ppavelV6promote : {A : Set} → .A → A18/08 16:08
ppavelV6promote c = promote' (irrelevant c) where18/08 16:08
ppavelV6 promote' : {A : Set} → Promoted A → A18/08 16:08
ppavelV6 promote' (irrelevant y) = y18/08 16:08
copumpkinyeah, that definitely seems bad18/08 16:08
copumpkinit should not be letting you project the val out of your Promoted record18/08 16:09
copumpkin(I think?)18/08 16:09
ppavelV6can we invent how to prove ⊥ using the above or at least blow the Universe up?18/08 16:09
ppavelV6compumkin: I think so too18/08 16:09
ppavelV6no18/08 16:10
ppavelV6it should not let me return irrelevant value from promote'18/08 16:10
ppavelV6promote'' x = x gets rejected but not promote' (irrelevant x) = x18/08 16:11
ppavelV6or, probably, i misunderstand what irrelevance is for.18/08 16:12
dolioYou shouldn't be able to prove bottom, but you can probably cause a loop.18/08 16:14
dolioWell, perhaps not, actually.18/08 16:14
dolioAnyhow, I don't understand why it accepts promote'.18/08 16:14
copumpkinppavelV6: which version is this on?18/08 16:15
ppavelV6yep, there's no way for me to pas bottom even as irrelevant18/08 16:15
ppavelV62.2.1018/08 16:15
copumpkinah18/08 16:15
ppavelV6?18/08 16:15
copumpkinso much has changed since then18/08 16:15
copumpkinit doesn't work on my recent checkout18/08 16:15
copumpkin(neither do legitimate uses of irrelevance though :( )18/08 16:16
ppavelV6wow. that's good.18/08 16:16
ppavelV6that's bad :)18/08 16:16
copumpkinppavelV6: the only way I can think you might be able to prove bottom with that18/08 16:16
copumpkinis if you can somehow provide an irrelevant proof that irrelevant x == irrelevant y -> x == y18/08 16:16
copumpkinbut I guess that's bad even without promote18/08 16:16
dolioYes.18/08 16:17
ppavelV6injectivity of irrelevant? :)18/08 16:17
dolioCertain things, if you erase them too eagerly, can cause loops when normalizing under a false hypothesis, though.18/08 16:18
copumpkinhey, it's a constructor! :P18/08 16:18
ppavelV6if something is like a duck... :)18/08 16:18
dolioHowever, it depends a lot on what all gets erased.18/08 16:18
dolioStuff using that promote might get stuck instead.18/08 16:19
ppavelV6evaluating promote 5 prints out _18/08 16:19
ppavelV6ok, so what's wrong? Agda-2.2.10 or my understanding of irrelevance stating that Agda should not accept promote?18/08 16:19
dolio2.2.1018/08 16:20
ppavelV6warm safe feeling...18/08 16:20
ppavelV6not so safe, actually (18/08 16:20
ppavelV6bugs in proof assistant are discouraging :)18/08 16:21
dolioWell, Agda's design doesn't exactly shoot for the extreme confidence angle.18/08 16:22
dolioIt's more like a playground.18/08 16:22
ppavelV6yep.18/08 16:22
ppavelV6and Coq's ?18/08 16:23
dolioThat's designed more for confidence.18/08 16:23
ppavelV6heh... my personal problem - i don't like Coq :) and i like Agda and confidence :)18/08 16:24
dolioYeah, I'm in a similar boat.18/08 16:25
dolioAlthough, I just play myself, so the confidence concerns don't bug me that much.18/08 16:26
ppavelV6I too :) but I'd like to promote (hehe) my game to something much more serious :)18/08 16:27
dolioThe irrelevance stuff, in particular, isn't following any established script.18/08 16:27
ppavelV6not in a way i just demonstrated :)18/08 16:27
dolioIt's based on existing work, but it's different in non-trivial ways.18/08 16:28
ppavelV6probably having a core language for Agda would be a good thing :) something like ΠΣ18/08 16:29
dolioPart of which is due to Agda simply being different from the starting point of most of the irrelevance stuff.18/08 16:29
ppavelV6i personally no little about the theory and even the motivation for irrelevant18/08 16:29
dolioAgda has eta equality, for instance, and I don't think any of the theory on irrelevance considers that.18/08 16:30
copumpkinppavelV6: the motivation seems fairly reasonable :)18/08 16:32
copumpkinI definitely want irrelevance18/08 16:32
copumpkinI just want it to work in all the ways I want, and in none of the ways that I don't18/08 16:32
copumpkin:P18/08 16:32
ppavelV6copumpkin: i mean i just don't know what i can do with irrelevance that can't be done without it. no theoretical background and my common sense does not help me here either18/08 16:35
ppavelV6:)18/08 16:35
dolioIf you go far enough with it, irrelevance gives you a kind of abstraction that you wouldn't otherwise have.18/08 16:37
ppavelV6it let me specify that i'm not interesting in internals of something, just in it existance.18/08 16:37
ppavelV6?18/08 16:38
dolioA function of type (.A -> ...) can't look at the A argument.18/08 16:38
dolioSo it is parametric in that argument.18/08 16:38
dolioOr, if you use modules as records...18/08 16:38
dolio{ .T : Set ; ... }18/08 16:39
dolioEr, records as modules.18/08 16:39
dolioWhen you make a value of that type, what T actually is is hidden.18/08 16:39
ppavelV6so irrelevance let's me specify more precise types telling me more about terms (like function can't look at the argument)18/08 16:39
copumpkinideally18/08 16:40
dolioSo records gain the ability to represent modules providing an abstract type.18/08 16:40
dolioHowever, Agda's irrelevance doesn't let you do this kind of thing (yet), because you can't actually depend on an irrelevant thing.18/08 16:41
ppavelV6i see18/08 16:42
dolioSo if you try to do { .T : Set ; z : T ; s : T -> T } as an abstract specification of natural numbers, for instance, it won't work.18/08 16:42
ppavelV6but record Nat (T : Set) : Set where z : T ; s : T -> T   does not achieve the same thing?18/08 16:44
dolioNo.18/08 16:44
ppavelV6ok. so what to do with promote? report it as a bug or is it irrelevant considering that latest build does not accept it?18/08 16:47
dolioYou should download the development version and use that.18/08 16:47
ppavelV6nice idea anyway18/08 16:48
copumpkin2.2.10 has several issues18/08 16:48
dolioThere are probably some proofs of false that have been fixed already.18/08 16:48
copumpkinI can't remember them all18/08 16:48
* ppavelV6 thinks about his relations with agda in general :)18/08 16:48
ppavelV6dolio: by development version do you mean latest darcs snapshot?18/08 16:50
dolioYes.18/08 16:50
dolioI don't think I've ever run a release of Agda.18/08 16:50
dolioOf course, right now I don't run it at all, because my copy of emacs hangs on agda-mode.18/08 16:51
ppavelV6:)))18/08 16:57
ppavelV6ok, i'll try the latest greatest version18/08 16:57
ppavelV6hmmm.... would it be great a pack of trusted features in Agda probably the "trusted mode"? what it will take? some formal verification down to compact kernel?18/08 17:06
copumpkinhah!18/08 17:08
ppavelV6copumpkin: let's relax and just dream a bit :)18/08 17:09
dolioIf you wanted trusted mode agda....18/08 17:09
dolioYou'd probably want to rewrite the system to not implement dependent pattern matching directly like it does now.18/08 17:09
dolioAnd instead compile matching down to a more traditional type theory.18/08 17:10
dolioWhich would be a huge change.18/08 17:10
ppavelV6i probably have to review Ulf's "Toward a practical..."... I've got an impression that dependent pattern matching is ok somehow.18/08 17:11
dolioIt's okay.18/08 17:12
dolioBut I can't really think of many type theories with normalization proofs and whatnot that incorporate dependent pattern matching directly.18/08 17:13
dolioWhere by many, I mean any.18/08 17:13
ppavelV6dolio: so the most interesting feature that closes the gap between a proof assistant and a programming language  (for me) lacks a good foundation :)18/08 17:16
copumpkinppavelV6: it can still exist, but should maybe not be a primitive?18/08 17:17
* copumpkin shrugs18/08 17:17
ppavelV6copumpkin: and by "it" you mean "a type theory that ..." ?18/08 17:18
* ppavelV6 installed Agda-2.2.1118/08 17:19
copumpkinppavelV6: I mean pattern matching is fine18/08 17:19
copumpkinbut if you build it in as a primitive, it's hard to be sure you've done it right18/08 17:19
copumpkinsince it's a massive and terrfying piece of code, I think18/08 17:19
ppavelV6copumpkin: that's true18/08 17:19
copumpkinif you translated it down to something simpler first, then checked that18/08 17:20
copumpkinI think people would feel more comfortable about it18/08 17:20
dolioppavelV6: McBride gave a translation of dependent matching into a type theory with eliminators and K a while back.18/08 17:20
ppavelV6i looked into Agda's sources and while I tend to say it's a very good piece of code I have to admit it's a large piece of code :)18/08 17:20
dolioIt just hasn't been used directly as a foundation.18/08 17:20
dolioOr, proved correct as such.18/08 17:20
ppavelV6dolio: i understand that getting something like agda in usability and with the high degree of trust in it is a frightening task :)18/08 17:22
dolioI think it's easier to trust a plain type theory and not need to trust the translation to it, than it is to trust a direct implementation of dependent matching.18/08 17:22
dolioAnd you don't have to trust the translation because it can't introduce inconsistency to the underlying theory.18/08 17:23
dolioThe translation might generate the wrong underlying stuff, but the underlying stuff still can't contain a proof of false.18/08 17:23
ppavelV6dolio: absolutely. That's why small trusted kernel18/08 17:23
dolioThat is, I mean the translator might have a bug. Not that the translation it's trying to implement is wrong.18/08 17:24
ppavelV6yes18/08 17:24
slomdolio: but dont you still have to translate the "results" back?18/08 17:26
dolioDepends what you're doing.18/08 17:27
ppavelV6ok, 2.2.11 does not accept promote anymore :) that's nice18/08 17:34
ppavelV6so the next question :))) What I really tried to achieve was proving that18/08 17:44
ppavelV6promote : {A : Set} → {pred : A → Set} → (a : A) → .(pred a) → ((a : A) → Dec (pred a)) → pred a18/08 17:44
copumpkinah18/08 17:45
ppavelV6having irrelevant "certificate" and the decision procedure recover [some] certificate :)18/08 17:45
ppavelV6it seem that absurdity does not play very well here or i fail to see how to use it18/08 17:45
copumpkinnot sure you can do that18/08 17:45
glguyYou'd just need a new Dec with an irrelevant field?18/08 17:45
ppavelV6glguy: not sure about Dec...18/08 17:46
dolioCan you match on irrelevant absurds? I forget.18/08 17:47
glguyyes18/08 17:47
dolioThen that should be how you do it.18/08 17:47
ppavelV6copumpkin: do i get my reasoning incorrect or is this some limitation of agda?18/08 17:47
ppavelV6promote a cert decision with decision a18/08 17:48
ppavelV6promote a cert decision | yes p = {!!}18/08 17:48
ppavelV6promote a () decision | no ¬p18/08 17:48
copumpkinwell, you can't do that, but you can feed cert to \negp18/08 17:48
glguyYou can't construct the "yes" with an irrelevant proof18/08 17:48
copumpkinI'm just not sure whether it'll let you do that18/08 17:48
glguyyou'd need to make a new type that had an irrelevant field18/08 17:48
copumpkinonly for the no, right?18/08 17:49
ppavelV6hm18/08 17:49
glguyOh, my client linewrapped18/08 17:49
glguyso I didn't see the final → pred a18/08 17:49
glguyso i thought you were trying to construct a Dec18/08 17:50
ppavelV6glguy: oh :)18/08 17:50
ppavelV6copumpkin: took this seriosly and suggested "no" being irrelevant on a parameter i suppose18/08 17:50
ppavelV6no : (.p) -> \bot ?18/08 17:50
dolioIn the no case, you have an irrelevant pred a, and a relevant pred a -> \bot.18/08 17:51
ppavelV6but i fail to see a reason for feeding cert to ¬p18/08 17:51
dolioYou can use that to get an irrelevant \bot.18/08 17:51
dolioWhich you can then do an absurd match on.18/08 17:52
dolioYou might need some helper functions, I'm not sure.18/08 17:52
copumpkinppavelV6: \negp takes cert and gives you \bot18/08 17:52
ppavelV6ok, thanks everybody have to go now , i will give a try to the suggestions. Thanks!18/08 17:52
glguyconvert : {A : Set} → (A → ⊥) → (.A → ⊥)18/08 17:53
glguythis is what we are trying to prove now, right?18/08 17:53
dolioEffectively.18/08 17:53
glguybecause I can't see how one would go about implementing convert18/08 17:55
copumpkinI wrote it18/08 17:55
* ppavelV6 still here :)18/08 17:55
copumpkinglguy: start with18/08 17:55
glguydo you get to use some double negation business since your final result is bottom?18/08 17:55
copumpkin  zomg : .⊥ → ⊥18/08 17:55
copumpkin:P18/08 17:55
copumpkinguess how you define that18/08 17:55
ppavelV6zomg () ? :)18/08 17:56
glguyha18/08 17:56
glguyconvert : (A : Set) → (A → ⊥) → (.A → ⊥)18/08 17:56
glguyconvert A f x = zomg (f x)18/08 17:56
copumpkinyeah18/08 17:56
copumpkinhttp://hpaste.org/5043518/08 17:56
copumpkinthat's kind of neat18/08 17:56
copumpkinI didn't think it'd be possible18/08 17:56
ppavelV6copumpkin: Thanks!18/08 17:57
ppavelV6If it didn't it would be my second large hit got from Agda for today :)18/08 17:57
ppavelV6promote let us have data structures with irrelevant invariants and, having the decision procedure that decides that the invariant is satisfied recover the proove18/08 17:58
ppavelV6proof18/08 17:59
copumpkinyeah, seems neat :)18/08 17:59
ppavelV6i just need proof that an index in a list is valid  back to do a lookup %)18/08 17:59
ppavelV6ok, have to go! thanks for your support18/08 18:00
copumpkinnp :)18/08 18:14
dolioMatching on irrelevant bottoms is kind of questionable.18/08 18:14
copumpkinI was just going to ask :)18/08 18:14
copumpkinbut you aren't really getting any "information" out of it18/08 18:15
copumpkinhmm18/08 18:15
dolioIt's not really wrong. It has some undesirable effects on the theory, though.18/08 18:16
dolioLike, weird normal forms.18/08 18:16
copumpkinah18/08 18:16
ppavelV6dolio:  can u elaborate about undesirable effects?18/08 19:41
dolioppavelV6: If you really want the details, you should read Nathan Mishra-Linger's thesis. But I'll attempt to explain.18/08 19:57
dolioI think the deal is that when you erase the irrelevant stuff, normally anything with a type like '.A -> B' would erase to a canonical B term.18/08 19:57
dolioSo, even .False -> Nat would erase to some natural number, or a term that normalizes to one.18/08 19:58
dolioHowever, if your elimination for False takes an irrelevant False, then it could also normalize to 'elim-False'.18/08 19:59
ppavelV6dolio: i have to think much more about it, but my current understanding is that irrelevance is a step in a wrong direction: "implementation detail" so to speak18/08 19:59
dolioI don't know what that means.18/08 20:01
ppavelV6dolio: it's my fault :) i'll try to explain when i'll make (or fail to) my intuition about it more explicit18/08 20:12
ppavelV6talking about irrelevance... and promote : {A : Set} → {pred : A → Set} → {a : A} → .(pred a) → ((a : A) → Dec (pred a)) → pred a18/08 22:15
Saizanbtw you just need Dec (pred a) as an argument there, i think?18/08 22:15
ppavelV6no matter how obvious the fact is i'd like to mention that18/08 22:16
ppavelV6irr : ∀{P Q R : Set} → (P → Q) → (.Q → R) → (.P → R)18/08 22:16
ppavelV6irr f cont p = cont (f p)18/08 22:16
ppavelV6i think that it's a useful fact to have around :) good night18/08 22:16
ppavelV6though it may be a bug in irrelevance implementation in agda, but it seem "true" :)18/08 22:18
glguyLooks legit18/08 22:18
ppavelV6i fail to see how agda allows f p providing that p is irrelevant and nothing about f says that it is willing to accept irrelevant argument18/08 22:19
glguywhen you give f a '.P' you will get a '.Q' back18/08 22:19
Saizanbecause it's going to ignore the whole (f p) anyway18/08 22:20
ppavelV6looks legit, citing glguy :)18/08 22:20
glguyAgda automatically lifts functions to return irrelevant results when you apply unexpected irrelevant arguments18/08 22:20
ppavelV6glguy: oh.18/08 22:21
ppavelV6glguy: reasonable18/08 22:21
dolioThat's not really how it works.18/08 22:21
dolioBut you can think about it that way.18/08 22:21
ppavelV6having irr at hand we can relax many cases to irrelevant arguments18/08 22:21
Saizani guess it's more that in an irrelevant context you're allowed to use irrelevant arguments everywhere18/08 22:23
dolioYes.18/08 22:23
dolioIn an irrelevant position, the environment is reset so that irrelevant things become relevant.18/08 22:23
ppavelV6i'm too sleepy now but i'm sure that18/08 22:24
ppavelV6lookup : {A : Set} (l : List A) (n : ℕ)  →  .( n < length l)  → A18/08 22:24
ppavelV6for example18/08 22:24
ppavelV6maybe related to runtime erasure18/08 22:24
ppavelV6interesting question is if irrelevance can be inferred18/08 22:24
dolioSome can.18/08 22:24
ppavelV6dolio: any cases when it can't?18/08 22:25
dolioYes.18/08 22:25
ppavelV6:) not constructive Yes :)18/08 22:25
glguyI can think of cases where one of two arguments could be irrelevant and it would be up to the user to decide which that was18/08 22:25
ppavelV6glguy: even if the code is present?18/08 22:26
glguysure18/08 22:26
ppavelV6hm18/08 22:26
dolioWell, if you do: f k = k 5.18/08 22:26
dolioThen you don't know whether the author wants k to be able to look at its argument or not.18/08 22:26
* glguy guesses that the author … did18/08 22:27
ppavelV6dolio: ok, get the point :) really time to go to bed for me :))18/08 22:27
ppavelV6good night18/08 22:27
dolioOr, f k = k 5 [a,b,c,d,e], where 5 is the length of the sized vector.18/08 22:28
Saizanrelevance polymorphism?18/08 22:28
glguyI'd like if Agda could see that pattern matching on an argument was irrelevant when there is only one constructor that can match18/08 22:28
dolioYou don't necessarily want to be polymorphic in it.18/08 22:29
glguycomes up when you are bolting on extra arguments to prove termination which don't actually affect the execution or evaluation18/08 22:29
dolioThink about: f : ((s : U) -> El s -> El s) -> ...18/08 22:29
dolioVersus f : (.(s : U) -> El s -> El s) -> ...18/08 22:30
dolioIn the second one, you're specifying that the argument is a parametric function over the universe.18/08 22:30
dolioThat is, you probably know that it's the identity.18/08 22:30
dolioIn the first one you don't know that.18/08 22:31
dolioSo the choice lets you say interesting things.18/08 22:31
glguyis there a theory reason why what I said isn't possible or is it just a matter of implementation?18/08 22:31
glguyif someone gives you an irrelevant refl, why can't you match on it?18/08 22:32
glguyThere is obviously only one constructor18/08 22:32
dolioI and others think you could probably write a similar system for that.18/08 22:32
glguyno secret18/08 22:32
Saizantrue, but if we have "principal irrelelvant types" then you can add annotations only where you want to restrict18/08 22:32
dolioHowever, it's not exactly the same modality as the parametric irrelevance.18/08 22:33
Saizanmatching on an irrelevant refl with current agda irrelevance probably breaks strong normalization18/08 22:33
dolioFor instance, you can erase the parametric parameters during checking. But you can't erase equality proofs without potentially causing looping during type checking.18/08 22:33
dolioSaizan: I think the principal type is probably the relevant one.18/08 22:35
dolioSince if you have a function that is explicitly irrelevant in the argument, it's okay to pass it to the one that expects a relevant function.18/08 22:36
Saizanah, true18/08 22:36
dolioYou will just have information that doesn't get used.18/08 22:37
ppavelV6lazyness18/08 22:37
ppavelV6%)18/08 22:37
Saizanbut f k x = k x; could be f : (.A -> B) -> .A -> B; or f : (A -> B) -> A -> B; are those types comparable?18/08 22:38
dolioNot sure about that one.18/08 22:39
dolioIt's probably a problem.18/08 22:39
ppavelV6is it safe to say that if argument is used only to match on absurdity or passed to irrelevant position it is irrelevant?18/08 22:41
ppavelV6lokup : {A : Set} (l : List A) (n : ℕ)  →  .( n < length l)  → A18/08 22:42
ppavelV6lookup [] _ ()18/08 22:42
ppavelV6lookup (x ∷ xs) zero _ = x18/08 22:42
ppavelV6lookup (x ∷ xs) (suc n) cer = lookup xs n (conv cer) where18/08 22:42
ppavelV6  conv : (suc n < length (x ∷ xs)) → n < length xs18/08 22:42
ppavelV6  conv (s≤s m≤n) = m≤n18/08 22:42
dolioI'd say only the latter.18/08 22:42
dolioBut Agda has extra cases.18/08 22:42
dolioYou can match on absurdity, or on the unit type.18/08 22:42
ppavelV6dolio: true18/08 22:43
ppavelV6dolio: about unit18/08 22:43
glguyThe unit type or any record (producing irrelevant fields)?18/08 22:44
ppavelV6glguy: nice :)18/08 22:44
glguyI'm asking18/08 22:45
glguyI'm clearly not the expert ;-)18/08 22:45
ppavelV6glguy: nice idea, seem very plausible. at least without dependent fields18/08 22:45
copumpkinwe should elect dolio to be the agda czar18/08 22:45
* ppavelV6 : is a screwdriver guy18/08 22:45
Saizanbtw, we could push that trustMe trick directly in the semantics of pattern matching on single-constructor irrelevant args, to be more experimental :)18/08 22:46
dolioYeah, that sounds great.18/08 22:46
Saizanit's so convenient!18/08 22:47
* ppavelV6 likes to see a flag to Agda --i-m-the-one-who-wants-experiments-let's-go-wild18/08 22:47
glguyWell, my quick experimentation seems to confirm my take on recors18/08 22:47
glguyrecords and irrelevance18/08 22:47
Saizanmy runST would get stuck on the free-theorem postulate without of it18/08 22:48
Saizans/of/18/08 22:48
--- Day changed Fri Aug 19 2011
augurwhich conference did conor present on agda at?19/08 19:57
augurwhere he talked about a compiler for a stack machine19/08 19:58
auguraha i think i found it19/08 20:04
--- Day changed Sat Aug 20 2011
xplatcategories like Cones F really should have a setoid of objects, since their objects contain arrows20/08 00:29
copumpkinyeah, lots of things kind of need setoids of objects20/08 00:30
copumpkingrr20/08 00:30
xplati ran into that when i was trying to prove limits are unique up to isomorphism and whatnot20/08 00:30
xplatyou can end up with a cone morphism whose natural domain is only 'weakly' equal to its actual domain20/08 00:31
xplatand that messes up the equivalent of the 'commute₁' and 'commute₂' properties for limits20/08 00:32
xplatpossibly the equivalent of 'universal' too20/08 00:33
xplattype-theoretic programming language with proper quotients, where are you?20/08 00:34
augurxplat: whats the point of quotients in a programming language20/08 01:26
cayleeaugur: quotients show up all the time in mathematics20/08 01:28
auguryes but20/08 01:29
cayleeaugur: well xplat is doing constructive math :-p20/08 01:31
xplatit seems like even without a fancy module-calculus-alike there should be a way to make function signatures more manageable20/08 23:48
xplatwhen you apply modules any unspecified parameters of the modules are automatically lifted to the individual exported functions20/08 23:49
xplatone could do the same type of thing when a partially applied type constructor was used on the right side of a : in a telescope20/08 23:50
xplatonly allow it for named arguments, and shove them all to the left of the explicit argument, and give them composite names (there would have to be some form of hierarchical argument names, even if it's something simple like concatenating them with a - separator)20/08 23:52
xplatand make all of them implicit20/08 23:52
xplatif out-of-order applications were allowed for the head term to the right of : too, then you'd get a lot of the power of sharing annotations in ml20/08 23:55
xplatbut i'm not sure how well this would mix with implicits in type constructors20/08 23:56
xplatbecause there would still be cases, most likely, when you'd rather they be inferred than deferred20/08 23:57
xplatyou could try to infer them, and defer them on failure, but that might be too unpredictable20/08 23:58
--- Day changed Sun Aug 21 2011
xplatalso, the whole thing would be much more useful in combination with an ornamentation-esque mechanism for lightweight shuffling of ... thingies ... between field and parameter positions of records21/08 00:01
xplatthe strong distinction between the two in agda turns out to be unfortunate a lot of the time21/08 00:03
xplatthe only difference between IsEquivalence and Setoid is in what's a field and what's a parameter21/08 00:04
xplatand the concept in between, where Carrier is a parameter but _\~~_ is still a field is missing21/08 00:05
xplata Level of course can never be a field, only a parameter, but for every other thing you can via any map to the poset ‘parameter < field’ monotonic in dependency21/08 00:09
xplat*can choose via21/08 00:10
xplatand you often end up regretting the choice you made for one kind of use elsewhere, and if you try to make it flexible you end up with code duplication and/or awkward nested records21/08 00:11
xplatbtw i understand what _ is about logically a lot better now that i realized it actually means 'i know i said ∀ but i really meant ∃!; could you just skolemize that for me?  kthxbye'21/08 04:21
xplatit's probably terribly obvious but i never actually heard somebody spell it out that way21/08 04:21
dolio_ where?21/08 04:21
xplatas an argument21/08 04:22
dolioIs that also what choosing an actual name for the argument, but never using it means?21/08 04:24
xplatno, i mean as an argument, not a pattern21/08 04:24
xplat_ as a pattern, or not using an argument, is just the term-level reflection of weakening, isn't it?21/08 04:26
dolioNot necessarily.21/08 04:26
xplat?21/08 04:27
dolioThe argument you don't care about may appear in a type that agda allows you to elide, for instance.21/08 04:27
dolioid _ x = x21/08 04:28
xplater, yes.  of course in a sense that's not unused even though it's _ since it's the type of x21/08 04:29
xplatif you had a calculus with all explicit types you would have to write id (A : Set) (x : A) = (x : A)21/08 04:30
augurwe should make a web interface for agda21/08 04:30
augurjust enough to post something to r/programming21/08 04:30
augurtitled21/08 04:30
xplatand so you couldn't use _21/08 04:30
dolioAnyhow, I don't see how _ as a term is some forall vs. exists! thing, really.21/08 04:30
augurMost fun way I've seen of learning Agda21/08 04:30
dolioYou get to use _ when the argument is uniquely determined, but that doesn't mean you screwed up with a forall vs. an exists!.21/08 04:31
xplataugur: "of learning what?"  "what is this?  it's like qwop only hard"21/08 04:31
dolioIt may mean the subsequent arguments determine which instantiation of the forall you're using.21/08 04:31
augurxplat: whats qwop XD21/08 04:31
auguri imagine we could have some sort of little interactive website like that actually21/08 04:32
augurthat teaches interesting principles of functional programming, theory of computation, logic, etc21/08 04:32
xplatdolio: hm, true, it can go out of order to an extent in ways that regular exists! can't21/08 04:32
augurmaybe with a dependently typed language with more haskell syntax, so there'd be no mixfixes or anything21/08 04:33
dolioid is properly forall A -> A -> A, not exists! A -> A -> A.21/08 04:33
augurmaybe just {pre/suf/in}fixes21/08 04:33
dolioBut knowing the second argument determines the first.21/08 04:33
xplatbut there's still a big similarity21/08 04:34
xplatanyway you can't determine the first argument if you need to actually know the second21/08 04:35
xplat_ can look ahead in the telescope, or all over the source, for types, but only backward in the telescope and outward in the environment for values21/08 04:36
xplatbecause it produces a single skolem-ish function that only gets those things as arguments21/08 04:37
dolioI don't even think of _ as part of the language.21/08 04:37
dolioIt's just the compiler generating code for me.21/08 04:37
xplatwell, even the operation i originally suggested was a meta-logic one21/08 04:38
liyangGuess it's too late to get invited to AIM XIV? >_<;;21/08 09:36
russrusshey, so I'm an absolute beginner and I'm trying to work through the agda tutorial.  I don't have a lot of experience with dependent types and all of my limited experience is with tactics-based systems, so I'm having some trouble understanding how to actually prove things in agda.  My current stumbling block is with proving equality.  I'm confused about the definition of equality given in the tutorial.  say I wanted to say something like21/08 21:34
russruss"function application preserves equality".  With the definition of equality given in the tutorial (==2 in https://gist.github.com/1161120), I don't know how to say this.  If I remove the equality type's index on the value, I can use pattern matching to say this.21/08 21:34
russrussone part of the tutorial challenges you to prove that lookup and tabulate are inverses.  I have no idea how to do this with the definition of equality given in the tutorial.  Adding an argument to the refl constructor made it easy if verbose.  https://gist.github.com/1161148  .  I'm sure there's a better way to prove this, but I don't understand enough about agda to do it.21/08 21:57
Saizanwhat's the problem with refl : {x : A} -> x == x ?21/08 22:02
Saizanit seems like you'd just have to remove the arguments from you uses of refl and it'll still typecheck21/08 22:03
russrussyeah, that'd be fine too I think21/08 22:03
russrussbut in the tutorial it's refl : x == x because _==_ itself is indexed on x21/08 22:04
Saizanit boils down to the same21/08 22:04
russrusshrm21/08 22:04
russrusswell, in https://gist.github.com/1161120 is there any way to fill in the question mark?  I couldn't figure out how21/08 22:05
russruss==2 is the definition of == they recommend in the tutorial21/08 22:05
Saizanwith their version refl still has type forall {A : Set} {x : A} -> x == x21/08 22:05
Saizan"app-eq2 f a .a refl = refl" will work21/08 22:06
russrussokay cool, that totally works21/08 22:07
russrussI thanks21/08 22:09
Saizanbtw, you could make x and y implicit, since they will get inferred from the type of the x == y argument21/08 22:09
russrusswhere?21/08 22:10
russrussoh in the app-eq's?  yeah.21/08 22:11
Saizanyep21/08 22:11
russrussso in my other example, https://gist.github.com/1161148, I have a feeling that my proof of lem-tab-! is way too verbose.  The idea is I'm trying to show that tabulate and lookup are inverses.21/08 22:12
russrussI understand now that I can get rid of the arguments to refl without a problem :-)21/08 22:13
russrussbut it's still pretty gross21/08 22:13
russrussis there a way to nest with statements?  that might help clean it up at least a little21/08 22:14
Saizanthere's a simpler definition21/08 22:19
Saizanlem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs21/08 22:20
Saizanlem-tab-! {A} {zero} [] = refl21/08 22:20
Saizanlem-tab-! {A} {suc n} (x :: xs) with tabulate (_!_ xs) | lem-tab-! xs21/08 22:20
Saizan... | .xs | refl = refl21/08 22:20
russrusshrm, that doesn't seem to be working for me....  tabulate ((λ {.x} → _!_ (x :: xs)) ∘ fsuc) != xs of type Vec .A n21/08 22:30
russrusswhen checking that the expression refl has type21/08 22:30
russrussx :: tabulate ((λ {.x} → _!_ (x :: xs)) ∘ fsuc) == x :: xs21/08 22:30
russrusswhich is why I added the tab-!-lem2 term21/08 22:31
Saizanah, i know, eta contract _\o_21/08 22:33
Saizanwell, not eta-contract..21/08 22:33
Saizanbut define it like this: (f ∘ g) = \ x -> f (g x)21/08 22:33
Saizanthen "(λ {.x} → _!_ (x :: xs)) ∘ fsuc" will be definitionally equal to (_!_ xs)21/08 22:34
russrussaha21/08 22:35
russrussI see that it works but I'm not exactly sure why that doesn't happen automatically21/08 22:36
Saizanyeah, there's a ticket open on this21/08 22:36
russrusswell, awesome.  That's a much more sensible proof then21/08 22:37
--- Day changed Mon Aug 22 2011
xplatrussruss: did you still need help or did someone answer?22/08 02:11
russrussyeah, I think I'm pretty much set... I still don't quite understand what was going on but fixing my definition of compose to be point-free seemed to help22/08 02:12
russrussI'm sort of stumbling around in the dark as far as the rules for unification during type checking goes :-)22/08 02:13
xplatah, that's the fun of higher-order preunification22/08 02:14
xplatnever gets boring like plain old first-order unification :)22/08 02:14
xplatit does get a little *more* boring, though22/08 02:15
NihilistDandySorry. Lightning storm. Did that question go through?22/08 02:17
xplatNihilistDandy: lightning storm, so i'm not sure i could tell22/08 02:20
NihilistDandyRight.22/08 02:20
NihilistDandyI was just wondering if the dev version of Agda built under 7.2.122/08 02:20
xplatoh, bad timing then.  i'm probably the only one in here who still uses 2.2.10 release ...22/08 02:21
djahandarieNah I use it too22/08 02:22
NihilistDandyI was using it, but I just started playing with 7.2.122/08 02:22
NihilistDandySo I thought I'd ask before I did anything drastic :D22/08 02:23
xplatlightning came back :(22/08 02:26
NihilistDandyThe answer so far is yes!22/08 02:27
augurhmm. now i understand why \Sigma is used for existential closer22/08 12:11
augur.. closure :|22/08 12:11
augur\Sigma[ x : X ] P x   ~   P x0 + P x1 + ...22/08 12:11
augurand you're just using each X to form the disjointness, rather than {0,1}22/08 12:12
augurfascinating22/08 12:13
xplatwhat does the runtime do when you compile agda code and it ends up trying to reduce a term headed by a postulate that's not linked to the FFI?22/08 13:01
copumpkinxplat: "such is the nature of irrelevance, wontfix and FU" was the stern reply22/08 13:32
xplatO_o22/08 13:33
copumpkinwell, the FU was me reading between the lines :)22/08 13:34
Saizandoes it work if you use a record type instead?22/08 13:35
copumpkinlike the squash type?22/08 13:41
copumpkinI don't think so22/08 13:41
copumpkinWe can still postulate the old behavior22/08 13:41
copumpkinbut it's just a pain22/08 13:41
copumpkinand makes irrelevance significantly less relevant to us :P22/08 13:41
xplatholy crap, did you see 431?22/08 13:48
copumpkinoh yeah22/08 13:50
xplatthat's an amazing bug that makes my head hurt even thinking about how it could be fixed22/08 13:56
xplateven the last proposed solution probably doesn't work, i think having seen this i could probably come up with an example that never repeats a problem that's still open22/08 13:58
copumpkinI wonder how coq catches it22/08 13:59
xplatdoes coq catch it?  does it even come up in coq?22/08 13:59
xplati think the 'constructor-headed functions' stuff is an agda-specific enhancement of the higher-order preunification algorithm22/08 14:01
xplatat least it seemed that way from the description in the slides i saw22/08 14:03
copumpkinah22/08 14:05
xplati guess if worst came to worst they could just never consider recursive functions as constructor-headed, or use the arbitrary depth cutoff22/08 14:14
xplatsince the basic problem is that constructor-headedness only guarantees tractable search if either the functions aren't recursive or one term is ground22/08 14:15
xplathm, i think i can actually see the shape of a more principled solution now22/08 14:17
Saizanit seems like you could catch this with a particularly smart occurs check?22/08 14:17
xplatit would probably still break some existing code though22/08 14:17
xplatwell, you'd have to check that you never recurse on both sides of a problem22/08 14:18
xplatrecursing on only one side is fine22/08 14:18
xplatbut if both sides undergo a recursive expansion you have to give up22/08 14:18
xplatyou could even generalize it as 'if both sides recurse beyond the given depth bound'22/08 14:19
xplatfor when people are willing to trade off predictability for power a la the termination check22/08 14:20
xplatthe only thing is, you have to check for recursion strictly by function name, because if you start considering arguments you hit undecidability22/08 14:22
augurso guys, remember how i complained and moaned about how there surely must be some study of how to impose constraints on types inductively?22/08 14:22
augurwell the whole ornamentation literature is basically that, but i never properly realized this22/08 14:22
--- Day changed Tue Aug 23 2011
auguri wonder what would happen if you had a type system that let you do things like define a constructor as an interactional with other constructors23/08 11:20
Saizaninteractional?23/08 11:20
augurwell, im thinking of grammars, right23/08 11:20
Saizanah, so it's a term from linguistics?23/08 11:21
augurno no23/08 11:21
augurthere shouldnt be an -al there23/08 11:21
augurbut23/08 11:21
augursometimes you want to do something like data Exp : Set where foo : Exp * Exp -> Exp23/08 11:21
auguror whatever23/08 11:21
augurand other times you want to do stuff like23/08 11:21
augurdata If : Set where if : Bool * Exp * Exp -> If23/08 11:22
auguror whatever.23/08 11:22
Saizan..and?23/08 11:22
augurwell, i mean23/08 11:22
augurobviously you can do   data Exp : Set where if : Exp * Exp * Exp -> Exp, and so forth23/08 11:23
augurbut then the If-expression-ness of it gets lost23/08 11:23
augurbut if you have an If data type, the Exp-ness gets lost23/08 11:23
augurso you end up wrapping and unwrapping things23/08 11:23
augurso i was thinking23/08 11:23
augurwhy not something like23/08 11:23
augurdata Exp : Set where   if : Exp^3 -> Exp ;   foo . if : Exp^4 -> Exp23/08 11:24
auguror whatever23/08 11:24
augurI suppose you could also index the type by the extra information23/08 11:25
augurdata Exp (T : Subtype) : Set where   if : ... -> Exp if ; foo : Exp if -> Exp -> Exp23/08 11:26
auguror whatever23/08 11:26
augurbut the idea of defining constructors by composition with other constructors intrigues me23/08 11:27
xplatthe data Exp (T : Subtype) : Set is the usual way of doing these things23/08 13:25
xplatit's basically GADTs23/08 13:26
xplater, sorry, you'd want data Exp : (T : Subtype) -> Set23/08 13:26
auguryeah, that too :)23/08 13:33
--- Day changed Wed Aug 24 2011
RotsorHello everyone! I wonder if there is an online-judge problem solving competition site where users would be required to submit solutions with proofs.24/08 15:21
RotsorThat is formal machine-checked proofs, like Agda programs.24/08 15:22
RotsorAnd if there is no such site, if that is a sane idea at all. :D24/08 15:22
mokusthat could be fun.  maybe even make the goal just to prove certain properties, and score the proofs on length and/or some measure of "complexity"24/08 16:00
Rotsormokus: so, are there no known efforts in this direction? It's not exactly fun learning a programming language without being able to compete in it. :)24/08 16:05
mokusRotsor: none known to me, but that doesn't mean there isn't24/08 16:15
byorgeyRotsor: there is http://as305.dyndns.org/aps/24/08 16:21
lambdabotbyorgey: You have 2 new messages. '/msg lambdabot @messages' to read them.24/08 16:21
danrNew agda-patch today in darcs that makes record projections a lot quicker!24/08 16:35
danr(just a notification, not by me, by Ulf Norell)24/08 16:35
Eduard_MunteanuNeat, is this about typechecking or running code?24/08 16:36
danrTypechecking.24/08 16:37
danrBut that's what it's all about, isn't it? :)24/08 16:37
Eduard_MunteanuHeh, I guess so :)24/08 16:37
Eduard_Munteanu"Prove 'Fermat's last theorem' in Falso -- Right Axiomatic System. "24/08 16:41
Eduard_Munteanu:)24/08 16:41
danrYeah, I tried Falso. Really easy to get used to. Not as steep learning curve as Agda.24/08 16:42
Eduard_MunteanuIt gave me the jitters before seeing the stuff about Falso.24/08 16:42
Eduard_MunteanuYeah, definitely easier and more elegant.24/08 16:42
danr:)24/08 16:43
danrI love how they write "Resistant to Gödel attacks" on the webpage :)24/08 16:47
Rotsorbyorgey, thank you! The same should be implemented with Agda!24/08 17:20
jacobianWow24/08 21:55
jacobianSo many people here!24/08 21:55
copumpkin#agda is where all the cool kids hang, yo24/08 21:56
glguyand Agda is what makes my computer hang24/08 21:56
* glguy needs more gigs24/08 21:56
djahandarieHeh.24/08 23:20
--- Day changed Thu Aug 25 2011
ppavelhi :)25/08 07:54
* ppavel wonders what does it mean to not having impredicative Prop (like Coq's) for him25/08 10:41
jacobianDo you use impredicativity much ppavel?25/08 11:25
ppaveljacobian: no, so that's the question :) what i really loose here :) in case it's something very useful :)25/08 11:27
jacobianI think it's pretty useful personally25/08 11:31
jacobianYou can do some pretty crazy stuff with impredicativity25/08 11:31
jacobianLike, the sorts of inductive style types which are representable is greater than those allowable with some positivity restriction on the form of types.25/08 11:32
jacobianHowever, it's also rather difficult to work with in other ways.25/08 11:32
jacobianI'd say if you don't know what you're missing, you're probably fine25/08 11:32
jacobianI have an example of the constructors of the lambda-mu calculus described impredicatively.  They can not be directly represented in a language that has a positivity restriction on inductively defined types.25/08 11:33
ppaveljacobian: I see. Agda had Prop at some point I believe. Was it impredicative? Why was it removed?25/08 11:37
jacobianDunno25/08 11:38
jacobianI'm new to agda25/08 11:38
ppavelsame25/08 11:39
* ppavel considers himself new to many things25/08 11:39
jacobianI'd be interested if it's possible to take some of those results from representing recursive types impredicatively by demonstrating a church encoding and lift them to inductive types.25/08 12:21
jacobianI played with the idea a bit, and I can't exactly wrap my head around what a proof system which allowed it would look like.25/08 12:21
copumpkinxplat: AGDA PERFORMANCE IMPROVEMENTS25/08 14:46
copumpkinnested sigmas are usable now, apparently25/08 14:46
Saizan30% improvement on the stdlib25/08 15:00
mokuscopumpkin: your categories library sure is a lot of fun to hack on25/08 15:43
copumpkinooh, what are you doing with it? :)25/08 15:43
mokusworking on exponential objects25/08 15:43
copumpkinooh, nice25/08 15:43
copumpkinthanks!25/08 15:44
mokusit's all in my github, you're welcome to take a look and pull anything that isn't too cluttered ;)25/08 15:44
copumpkinthanks25/08 15:44
copumpkindid you also see xplat's branch?25/08 15:44
mokusyea25/08 15:44
copumpkinhe's got quite a bit of stuff too25/08 15:44
mokusmy ultimate goal is to implement at least the basics of Taylor's abstract Stone duality25/08 15:45
mokusso I'm focusing right now on defining the double-exponential monad25/08 15:45
copumpkin:O25/08 15:46
copumpkinI haven't come across that25/08 15:46
copumpkinyou should join ##categorytheory too25/08 15:46
copumpkinit's actually reasonably active25/08 15:46
mokusthis is my first "serious" foray into agda25/08 15:47
mokusfound it a lot harder than expected to prove that X^- is a functor25/08 15:48
copumpkina lot of things are a lot harder than expected, sadly :)25/08 15:48
copumpkinlots of things that need to be made explicit25/08 15:48
mokusyea, took me a long time to wrap my head around the heterogeneous equality25/08 15:48
copumpkinI had trouble even stating the interchange law for natural transformations25/08 15:48
mokusyea, took a while to come up with the right laws for exponentials too, especially since i was tryng to preserve the spirit of the 'skeleton' implementation that was there25/08 15:49
mokusspecifically the fact that it doesn't assume existence of products25/08 15:49
copumpkinah25/08 15:49
copumpkinin future, no need to do that :P25/08 15:49
copumpkinI was probably clueless about CT when I wrote it25/08 15:49
mokusheh25/08 15:49
mokuswell, it's an interesting bit of generality25/08 15:50
mokuswhat i came up with is that lambda-abstraction is unique _when_ the product exists25/08 15:50
mokuswhich i think is an interesting twist25/08 15:50
mokusthe main challenge was just coming up with notation to be able to state that without taking a whole paragraph for each type signature ;)25/08 15:51
copumpkinawesome :)25/08 15:51
mokusalso, i don't know if anyone here is as emacs-averse as me, but i've got a growing TextMate bundle for agda :)25/08 15:52
copumpkinby the way, if you value your memory, don't try to typecheck the monoidal stuff25/08 15:52
copumpkinor braided etc.25/08 15:52
mokusheh25/08 15:52
copumpkinalthough with today's new changes, it might actually be tractable25/08 15:52
mokusi'll have to check them out, i haven't been tracking the darcs releases though - still on 2.2.1025/08 15:53
mokushad to restructure what I was working on a couple times because of running out of memory25/08 15:53
copumpkinah yes25/08 15:53
mokusi've "only" got 4GB on my laptop ;)25/08 15:53
copumpkinulf updated agda today to not suck memory-wise25/08 15:53
mokuscool25/08 15:54
copumpkinhe says typechecking can be an unbounded number of times faster now25/08 15:54
copumpkinwhich sounds pretty good to me25/08 15:54
mokusme too, even with my current structure it takes over a minute to check my Exponentiating module25/08 15:54
augurdjahandarie: oh?25/08 17:53
djahandarieAgda performance improvements!!!25/08 17:53
djahandariecopumpkin, tried compiling CT lib yet?25/08 17:53
djahandarieaugur, https://lists.chalmers.se/pipermail/agda/2011/003266.html25/08 17:54
dolioUsing records got arbitrarily faster.25/08 17:54
dolioWhich is huge.25/08 17:54
copumpkinpity dolio can't enjoy it25/08 17:54
dolioBecause lots of good library structuring revolves around records of records of....25/08 17:54
* copumpkin laughs evilly25/08 17:55
augurweird25/08 17:55
djahandariedolio can't use it because he isn't smart enough? Too bad, too bad...25/08 17:55
dolioAgda mode hangs emacs on my computer.25/08 17:56
djahandarieHey, technically I can't use Agda either since my laptop is a piece of crap25/08 17:58
djahandarieAlthough maybe this is the saving grace...25/08 17:58
dolioMaybe you can now.25/08 17:58
dolio"New Agda, for piece-of-crap laptops."25/08 17:58
glguyOoh, 30% is one of my favorite numbers for performance improvements25/08 18:00
* Saizan tries Everything.agda from categories25/08 18:02
glguyIs that fix in the public darcs repository?25/08 18:03
Saizanyep25/08 18:03
glguyWhen designing things which are "correct by construction" are irrelevant parameters the only way to ensure that the complexity of associated proposition construction doesn't change the complexity of the algorithm?25/08 18:08
dolioSaizan's nested sigmas got even better than 30% speedup.25/08 18:11
glguyI have the same question for implementing algorithms with have a non-trivial termination proof. (Suppose you need well-founded induction on naturals with <)25/08 18:17
glguyOr will Agda programs only be able to approximate these algorithms?25/08 18:17
--- Day changed Fri Aug 26 2011
Saizanglguy: accessibility proofs can't be made compile-time irrelevant (which is the kind of irrelevance agda has) without losing strong normalization, i think, but there are known optimizations to get rid of them at runtime26/08 03:20
Saizan..i hope? you could ask edwinb26/08 03:20
Saizani guess it'd be nice to ensure that at the source level by having a runtime irrelevance, though that would also introduce a new Pi type, which has its problems26/08 03:25
glguy_I guess there aren't enough Agda programs being executed for it to matter at this point :)26/08 03:26
Saizanyep, it's surely more important to optimize typechecking :)26/08 03:27
glguy_Do you know if the Haskell or Epic backends will optimize away functions which can only have a single possible return value?26/08 03:31
glguy_Since we know all of our functions terminate is it safe to shortcut evaluation?26/08 03:31
glguy_suppose a function returns a refl, equivalence proof26/08 03:31
glguy_unlike Haskell where the unit type is inhabited by all manner of Exception class instances and loops26/08 03:34
Saizanyep, it's safe to do so, and i believe epic is supposed to but i'm not sure if it's implemented26/08 03:43
glguy_It would be interesting to see that optimization optimize away accessibility proofs as they have a single constructor containing a function which returns the same26/08 04:09
dolioWhich optimization?26/08 04:09
glguy_but it isn't completely obvious that that is something which only has a single inhabitant26/08 04:09
glguy_at run-time not evaluating functions whose return type has a single inhabitant26/08 04:10
copumpkinmaybe make a proofy-optimizer26/08 04:10
copumpkinif you can prove that for your type A, (x : A) -> x == theOneConstructor, then you stick that in a pragma26/08 04:11
copumpkinand it'll check your proof and if satisfied, it'll hide all that stuff26/08 04:11
copumpkinor maybe x == theOneConstructor or x -> \bot26/08 04:12
copumpkin:P26/08 04:12
dolioProving that accessibility predicates only have one inhabitant is kind of non-trivial.26/08 04:13
copumpkin(x y : A) -> x == y26/08 04:13
copumpkinthat26/08 04:13
copumpkinwould that work?26/08 04:13
dolioI certainly doubt that you can do it in Agda.26/08 04:13
dolioBecause it would need extensionality.26/08 04:13
Saizanyeah, though it's quite easy with extensionality26/08 04:15
Saizani guess it depends on the relation though26/08 04:16
dolioYeah, I was also thinking the relation could be a problem.26/08 04:16
dolioIf it's not itself a proposition.26/08 04:16
Saizanor maybe you just have to pass it along.. i'll try after this run of categories/Everything.agda overflows :)26/08 04:18
dolioIt might not actually be a problem. Just a potential source.26/08 04:19
dolioActually, if you want to prove it once for all relations, it is a problem.26/08 04:19
dolioUnless you impose parametricity on the argument or something.26/08 04:20
Saizandolio: http://hpaste.org/50674 ?26/08 04:30
glguy_http://www.galois.com/~emertens/oneacc/OneAcc.html26/08 04:31
glguy_Hey, no fair :)26/08 04:31
Saizan:D26/08 04:32
dolioOh right, of course.26/08 04:32
dolioBecause 1^n = 1.26/08 04:32
glguy_Would it be possible to use reflection to prove this for all types having one constructor  and fields that all satisfy the single-inhabitant property themselves (mod extensionality)?26/08 05:16
copumpkinreflection doesn't let you inspect the structure of types26/08 05:31
glguy_Hmm… we need SYB, then :)26/08 05:34
* Saizan wonders if anyone is using Agda to teach a course on computability26/08 07:05
ppavelcopumpkin: at least in Agda-2.2.11 you can inspect the structure of data types26/08 09:08
ppavelglguy_: http://hpaste.org/50681 to get an idea26/08 09:11
* npouillard code.haskell.org is unreachable26/08 10:53
npouillardcan someone confirm that I have the latest Agda patch "Thu Aug 25 15:05:20 CEST 2011  ulfn@chalmers.se: benchmark run" ?26/08 10:54
Saizanonly someone with26/08 10:58
Saizandirect access to c.h.o could, no? anyhow that's the last one i have from my yesterday pull26/08 10:59
npouillardSaizan: thanks26/08 12:12
npouillardwe have a way too centralized architecture...26/08 12:13
xplatppavel: wait, what?!  how can that work?  isn't A just 'A' in printGoal?26/08 12:35
ppavelreducing n gives me str "def data "26/08 12:39
xplatif you can do that types aren't erasable at runtime26/08 12:40
ppavelxplat: too strong statement26/08 12:41
xplatwell, i guess it depends on what 'that' is26/08 12:42
ppavelxplat: n is a constant in runtime in this case26/08 12:42
xplatand depending what 'that' is it could be hard to predict what will happen when you reflect26/08 12:43
xplatif quoteGoal could be inlined at some times and not others ...26/08 12:44
xplater, inlined into callers, i mean26/08 12:45
ppavelxplat: I fail to see how this all is related to runtime, frankly26/08 12:45
ppavelThe reduction takes place in type checking26/08 12:46
xplatwell imagine you're passing something like printGoal to higher-order functions26/08 12:46
ppavelok26/08 12:47
ppaveland? :)26/08 12:47
xplatwhich are compiled in other modules26/08 12:47
ppavelxplat: and? :)26/08 12:47
ppavelbtw, what do you mean by a runtime ? :) the result of MALonzo?26/08 12:48
xplathow does it get the 'real' goal if it can be called at arbitrary nested recursion steps?26/08 12:48
xplati mean that, yes, and whatever else people normally mean when they say 'agda can erase types at runtime'26/08 12:49
ppavelto go to runtime you program should type check, so types will be known at any "call site" of printGoal26/08 12:50
xplatbut what if you're calling it with an indexed type and there are an infinite number of possible indexes at runtime?26/08 12:51
ppavelxplat: I believe Agda has nothing to do with type erasure. It's up to the compiler, btw26/08 12:51
ppavelxplat: and what are all that indexes? :)26/08 12:52
xplatthe indexes could be types too26/08 12:53
ppavelxplat: can you come out with a quick example. I'm interested in the subject, but I'm a bit busy right now to switch to it :))26/08 12:54
xplati'll have a hard time since i never wrote IO code in Agda yet :-/26/08 12:55
ppavel:) you just can't get infinite collection of types in agda i believe :)26/08 13:01
ppavelif you're reading numbers from a file converting them to type, calling something like printGoal and printing the output you'll get a reduction to something of type ℕ → String :) right?26/08 13:03
ppavelIO code works using postulated things the MALonzo knows how to translate to haskell. Those things are in terms of Haskell types, at least the {-# COMPILED a whatever #-} can't use dependent types in any meaningful way.26/08 13:05
ppavelprobably somebody will explain all the matter much clearer :)26/08 13:05
Saizanxplat: it is quite puzzling26/08 16:51
skrapshelp get SSL options for everyone for free on pastebin like this page on face book http://pastebin.com/f4e0diQP26/08 16:52
Saizanppavel, xplat: i think the data it finds isn't \bn but StringRepr itself, actually, so it's not anything problematic26/08 16:56
ppavelSaizan: i still fail to see anything problematic :)26/08 16:57
glguycopumpkin: I asked that same question about Num a => a in #haskell when this conversation came up (sometime in the last couple of days)26/08 17:01
Saizanppavel: quoteGoal is sort of a macro, right? so it shouldn't have access to dynamic data, but if you were able to abstract it transparently behind a normal function it'd be hard to enforce this sort of phase distinction, or at least it wouldn't be clear at all to the reader which actual goal quoteGoal would see26/08 17:05
ppavelwith 'dynamic data' the reduction of type (the goal) will not be made and the Term you get inside quoteGoal will not be  a data constructor. It will be some other Term26/08 17:07
Saizanah, a simpler objection: if it worked that way it'd break parametricity26/08 17:10
Saizani fact, by parametricity it follows that forall (s t : Set) -> printGoal {s} == printGoal {t}26/08 17:12
Saizanso you can't have printGoal {Bool -> Bool} /= printGoal {Bool}26/08 17:12
ppavelSaizan: i don't think quoteGoal is a function after all26/08 17:16
Saizanright, it isn't26/08 17:16
ppavelsorry have to go now. The nice thing about quoteGoal is that it works :)26/08 17:22
glguyDo either of you have a nice example showing where quoteGoal was useful?26/08 17:25
Saizanthat would require an implementation of an useful solver first :)26/08 17:27
glguyThe goal of quoteGoal is to allow you to write "tactics" in Agda, right?26/08 17:29
Saizanto use them without having to type down a representation of your goal by hand26/08 17:30
Saizanbecause it hands one to you26/08 17:30
glguyWhen you use tactics in other languages one of the acceptable behaviors is for the tactic to fail to solve the goal, or only solve part of it26/08 17:31
glguyHow does this translate into this model?26/08 17:31
glguyIt seems like it would be impossible to write a function from an arbitrary goal to anything interesting26/08 17:32
Saizanright, i think the idea is that each tactic would cover a well defined class of goals26/08 17:32
Saizanand fail if called with something else26/08 17:33
Saizanto fail you just have to require an argument (maybe implicit) of the empty type or the goal itself26/08 17:33
Saizanto transform you can do the same too26/08 17:33
glguyHow would you define the class of supported goals? Require the user to construct some predicate as a parameter to the tactic?26/08 17:34
Saizanin fact the ring solver in the stdlib does something like this, even if it's lacks the code to accept the term representation of quoteGoal26/08 17:34
glguyWrapping the ring solver to accept quoted goals seems like the most obvious and immediately realizable useful case for quoteGoal26/08 17:35
glguy(now that you say it)26/08 17:35
Saizanglguy: the idea is that the tactic itself would attempt to construct the proof of that sort of predicate26/08 17:36
Saizanor even just a "parser" from the representation of quoteGoal to some other more convenient for implementic the rest of the tactic26/08 17:36
glguyCould you construct some trivial case that showed how "attempt" was good enough?26/08 17:36
glguyI'm trying to wrap my head around what failure looks like26/08 17:37
glguy(I'd love for code like this to not need to explicitly implement the goal http://www.galois.com/~emertens/integer-properties/Data.Integer.Properties.html#4853 )26/08 17:38
Saizana simple way would be: tactic : (t : Term) -> {T (isSupported t)} -> Eval t (no idea if Term and Eval are called Term and Eval though :)26/08 17:41
glguyWhat about a simple "tactic" that solved quoted goals of a single natural number26/08 17:41
Saizanwhere T true = \top; T false = \bot26/08 17:41
glguyOK, I can kind of see this now26/08 17:41
glguyhttp://hpaste.org/5068926/08 17:49
glguySo first I'll need a predicate that matches these things26/08 17:49
Saizani don't see anything working as Eval in Reflection though, maybe it's not implemented yet..26/08 17:50
Saizanbut yes :)26/08 17:50
glguyHow might I compare the first argument of def (whose type is Name) to the name of Relation.Binary.PropositionalEquality._\==_?26/08 17:55
* glguy scans through the Reflection module...26/08 17:55
Saizanglguy: btw, in this case you'd just want to write a conversion function from Term to the representation the ring solver uses26/08 17:56
glguyI'll also need to identify the number of variables in the goal and instantiate "solver" with that number26/08 18:05
glguyWell… without a way to quote arbitrary expressions, I don't see how to write this predicate26/08 18:07
glguyto enforce that the term I see is made up of the types I can support26/08 18:07
glguyah, perhaps I need to make my predicate as an indexed family to support matching in that way26/08 18:10
glguyI found a paper which states that "It is now very simple to code a function that will automatically transform a quoted term into an input term for the solver." regarding using quoteGoal for Ring Solver26/08 18:21
glguyhttp://perso.ens-lyon.fr/guillaume.allais/pdf/gallais_m1-1.pdf26/08 18:21
glguyI like the sound of that26/08 18:21
glguyah ha, there is a primitive "quote"26/08 18:24
glguySaizan: http://hpaste.org/5069426/08 22:53
glguySuper early prototype26/08 22:53
glguydoesn't support all of the possible goals and doesn't automatically build the set of variables yet26/08 22:54
copumpkinwhat's that?26/08 23:01
copumpkinxplat already bound the semiring solver to reflection26/08 23:01
glguyoh, perfect26/08 23:02
augurwhats a semiring solver26/08 23:02
* copumpkin pokes xplat26/08 23:02
copumpkinaugur: it can determine that x^3 - 3x + 5 == 5 + x*(-3 + x^2)26/08 23:02
copumpkinand prove that for you26/08 23:02
copumpkinand that's valid over any semiring26/08 23:02
augurer26/08 23:03
glguyand I implemented the proof that integers for a semiring, so you can use it for those, too, now.26/08 23:03
augurbut what is it in agda?26/08 23:03
copumpkinyay26/08 23:03
auguris it agda code that you execute?26/08 23:03
auguror is it a "tactic"?26/08 23:03
copumpkinaugur: yeah26/08 23:03
copumpkinit's a pseudotactic26/08 23:03
augurshow?26/08 23:03
glguyIt is written in pure agda26/08 23:03
glguyand runs as part of your program26/08 23:03
copumpkinhttp://www.cse.chalmers.se/~nad/listings/lib/Algebra.RingSolver.html#126/08 23:03
xplatglguy: i already wrapped the ring solver to solve natural number goals, but it didn't work in 2.2.10 because of a bug in quoting of the natural number suc constructor specifically26/08 23:05
augurhmm26/08 23:05
augurhow do pseudotactics work in agda?26/08 23:06
glguyI just implemented "suc" and "zero" :)26/08 23:06
xplatglguy: rather, it works as long as you have terms whose reduced representation does not include any sucs26/08 23:06
glguybuild1 xs (con name []) = con 026/08 23:06
glguybuild1 xs (con name (arg visible relevant n ∷ [])) = con 1 :+ build1 xs n26/08 23:06
glguythis is my test case26/08 23:07
glguydemo : ∀ a b c → a * (b + c) + 2 ≡ 2 + a * b + a * (c + 0)26/08 23:07
xplatit should be able to do that if you modify it for 2.2.1126/08 23:09
xplati think there's a version up on hpaste, let me see if it's the right version26/08 23:10
glguyAh, you're using the hpaste revision control software?26/08 23:11
xplatheh, yeah26/08 23:11
xplatupstream took so long to even roll a fix for the suc bug into 2.2.11 that i kind of lost interest before turning it into a real library26/08 23:12
glguycopumpkin: I resubmitted the Semiring patch yesterday after remembering about it and doing some substantial clean-ups26/08 23:16
glguyhttp://www.galois.com/~emertens/integer-properties/Data.Integer.Properties.html26/08 23:16
glguyWe'll see if the patch is accepted this time26/08 23:17
xplathttp://hpaste.org/4948926/08 23:23
xplatnot in any of my logs, i must have been ircing from my laptop (not through screen) when i pasted it26/08 23:25
glguyThanks for the link26/08 23:26
glguyI'll have to read through this tonight26/08 23:26
xplatto run it you either need to use 2.2.10 with it as-is, in which case you need to be careful about your terms, or you have to modify it to accept the new Arg structure in 2.2.11, in which case it's best to use a very recent version since then it should solve everything implied by the semiring laws26/08 23:28
copumpkinzomg26/08 23:30
copumpkinxplat: where you been recently!26/08 23:30
glguyIt looks like I save a ton of code because I don't try to solve for the whole proof but just the semi ring solver's reflected view26/08 23:30
glguyYour code should be a great learning experience26/08 23:30
xplatif you give it a term outside of its competence it will turn yellow; if you give it a false goal the refl for the second argument won't typecheck26/08 23:31
glguye.g. http://hpaste.org/edit/5069426/08 23:31
xplatcopumpkin: i had a some more than usual $work and other stuff, not so many chances to talk on irc.  i've been keeping track of here and ##ct though.26/08 23:36
copumpkinah :)26/08 23:37
copumpkinwe missed you!26/08 23:37
xplatglguy: yeah, the code to keep the tactic self-contained is ... not insignificant26/08 23:37
xplatthe hardest parts were that, getting abstractions past the termination checker, and of course the ****** suc thing which had me scratching my head for a while26/08 23:39
xplatthat's why i rewrote the whole thing applicatively with error messages, though, so bonus, i guess26/08 23:40
glguyxplat: is this code specific to Data.Nat or does it work over an arbitrary SemiringSolver?26/08 23:45
glguyI'm guessing specific26/08 23:53
glguywould a generic solution be possible?26/08 23:53
--- Day changed Sat Aug 27 2011
xplatmine is specific27/08 00:02
xplati was working on something more general, but i got distracted27/08 00:02
xplatyou would need to parameterize it on names, or more generally, signatures, for the fundamental operations, but you would also have to fold raw constructors to constants and so on27/08 00:03
xplatand you can often end up with artifacts of normalization where the semiring operations mutate into something type-specific, like suc of a variable27/08 00:04
xplatso it gets to be a pretty involved problem27/08 00:05
glguygiven that you have to understand how the constructors interact with the operators I'd be a little surprised if it could work at all27/08 00:11
xplatwell, it's basically just having an extra normalization stage in front of the one for semirings27/08 00:14
xplatfor naturals just replacing all zero by const 0 and suc by const 1 + would work, but not be the most efficient27/08 00:16
glguyyeah, it does work, but I'm thinking about other types27/08 00:17
xplatother types are probably similar27/08 00:17
xplataside from maybe something pretty exotic like creals27/08 00:19
glguybut if you wanted to implement this without knowing anything more than that you had a SemiringSolver for the type27/08 00:20
glguyit would be hard to make assumptions about the constructors, I'd think27/08 00:20
xplatyeah, you would have to have someplace to indicate your assumptions27/08 00:21
xplatif you get a type that's too horrible you'd just have to use the semiring solver as-is, i guess27/08 00:21
xplatwhat i really wanted to implement was a smarter form of equational reasoning27/08 00:23
copumpkin:o27/08 00:25
glguysome kind of automatic congruence application would be nice27/08 00:26
xplatwhere it could do automatic congs based on tree diffs, and steps justified by 'so yeah it's a ring'27/08 00:26
glguyso you could skip those when doing the ==< ? > stuff27/08 00:26
glguyI guess "smarter equaltional reasoning" means the same thing to each of us27/08 00:27
copumpkinthat'd be awesome27/08 00:27
xplatso if you had a bunch of nice laws already in scope and you wanted to rearrange some terms to apply an equation, you just write the before and after and between you write something like 'duh'27/08 00:29
copumpkinthe quotegoal syntax is kind of cumbersome though27/08 00:30
glguyIf instance arguments *did* do recursive search you could use that to solve a bunch of equational reasoning stuff :)27/08 00:30
glguyI need a proof that: a + b == b + a ...27/08 00:31
xplati figured on applying it once at the top level, a la 'open ==-reasoning; begin'27/08 00:31
glguyand so on, go instance search!27/08 00:31
copumpkinah27/08 00:32
xplatglguy: yeah, but after that nice looping bug in the implicit search the instance dudes are laughing into their sleeves because THEY didn't introduce a stealth computational model that could loop27/08 00:32
glguyheh, don't worry, I understand why it doesn't search27/08 00:32
copumpkinxplat: you noticed any difference in the latest agda on CT?27/08 00:35
xplatcopumpkin: haven't built it yet, didn't Saizan say something about that though?27/08 00:36
copumpkinyeah, it's <unbounded number of times faster> at typechecking now27/08 00:36
copumpkinwhich sounds pretty good27/08 00:36
copumpkinI haven't tried yet though27/08 00:36
mokusi compiled the whole categories library in 4GB of ram with the new agda27/08 00:37
mokusonly took 30 min27/08 00:37
mokusi believe peak VM usage was around 6.5G27/08 00:38
copumpkinI think I could do that in 30 minutes before :/27/08 00:38
mokusmaybe... seemed longer27/08 00:38
xplatcopumpkin: i meant ‘13:13  * Saizan tries Everything.agda from categories’27/08 00:39
copumpkinoh :o27/08 00:39
xplat(yesterday)27/08 00:39
xplatit sounds like from mokus' experience it didn't make the revolutionary difference i was hoping for27/08 00:40
mokuswell, you only have to compile the whole thing once... my individual modules were noticeably faster, though i wouldn't call it revolutionary either27/08 00:41
xplatwhat i was really hoping is it would speed things up so much that the setoids could be relevant27/08 00:41
xplatthe optimization specifically speeds up projections, but it doesn't speed up all the other cases of inferred arguments that are duplicated-but-not-shared.27/08 01:01
xplatafaict27/08 01:01
copumpkinmaybe you could reply to him and suggest that?27/08 01:02
xplatprobably the principle that lets the projection's hidden arguments be erased doesn't hold in the general case, so i think it would take a whole different approach, but it might be worth mentioning anyway27/08 01:03
xplati'll probably send something tomorrow if i can use the internet27/08 01:04
xplatstupid hurricanes.  it's the 21st century, where are my damned weather control satellites?27/08 01:10
copumpkinlol27/08 01:10
copumpkinI was just about to launch one27/08 01:11
copumpkinbut the hurricane is stopping me27/08 01:11
mokusthat's tragic27/08 01:11
xplatsrsly, a lot of work has been done on control theory for chaotic systems, someone should put it to use27/08 01:11
augurin the novel Permutation City, Greg Egan hypothesized a real weather control system27/08 01:11
augurthat basically works like so:27/08 01:11
augurdue to the chaotic nature of weather, initial conditions matter alot27/08 01:12
augurso spend a lot of computing power modelling the weather to determine when a storm will brew27/08 01:12
augurand then spend a lot of computing power modelling what minor changes to initial conditions will prevent the storm27/08 01:13
augurthen, use pumps to alter cold water flow to modify the initial conditions so that storms never happen27/08 01:13
xplatyeah, i remember.  it was one of the major antagonists in the novel :)27/08 01:14
augurwell27/08 01:15
augurnot really27/08 01:15
augurit stole cloud time for about 10 hours and that was the end of it27/08 01:15
augurproject butterfly27/08 01:15
mokusi'm kinda looking forward to the hurricane hitting, never been hit so dead-on by one before27/08 01:16
augur:|27/08 01:16
augurmokus, where are you?27/08 01:16
mokusnew york, lower hudson valley27/08 01:16
augurah, well27/08 01:16
xplatyeah, well, it ended up actually helping wossface with his goal because the threat it prevented caused the *spoiler*s to want to *spoiler*27/08 01:16
augurit wont be bad when it gets up there27/08 01:16
mokusyea, it could be worse27/08 01:16
augurxplat: not... really27/08 01:16
mokusstill calling for up to 70 mph winds here though27/08 01:16
xplataugur: not the threat it presented by itself, of course, but what it demonstrated27/08 01:18
augurwhat27/08 01:18
xplataugur: that the world didn't care about them getting their timeslices27/08 01:18
auguroh you mean how it was one of the potential future threats to uploads?27/08 01:18
xplatyeah27/08 01:19
augurmokus: http://news.blogs.cnn.com/2011/08/26/hurricane-models-prepare-new-yorkers-for-worst-case-storm-scenarios/?hpt=hp_t127/08 01:41
mokusyea, so much of NYC relies on below-ground infrastructure27/08 01:46
glguyI just read the paper linked from http://www.reddit.com/r/programming/comments/jvu2w/total_functional_programming_and_the_unimportance/27/08 05:47
glguyI feel like he underestimates the difficulties that you start to experience when you require totality (or he's just way better at it than I am)27/08 05:49
copumpkinyeah27/08 05:52
djahandarieI need to go make something really complicated in Agda27/08 05:53
glguyEvery time I think I'm going to write something in Agda I get side tracked implementing some supporting module :)27/08 06:00
Saizansection 5 acknowledges some of that, it seems27/08 06:08
djahandarieglguy, that might be true for any in-development language though27/08 06:09
glguyOh, that was just my response to your wanting to write something really complicated27/08 06:10
glguyI'm not saying that Agda is necessarily unsuitable27/08 06:10
glguyjust relating my experience :)27/08 06:10
djahandarieWell, I just want to make something complicated to see what sorts of walls I hit, since I don't really feel like I hit walls very often. Mainly because I don't use Agda very often.27/08 06:11
Saizanthe termination checker not seeing through HOFs is the most annoying wall for me27/08 06:16
Svrogwhat exactly does the . do in patterns in agda? unification?27/08 10:12
Saizanit means that the argument in question is forced to have that shape from the other patterns27/08 10:27
Saizanthe typechecker is indeed going to check that with unification27/08 10:28
Svrogdoes it force the shape with unification?27/08 10:32
Svrogalso does agda use first order unification or higher order?27/08 10:32
Svrogfor type checking27/08 10:32
Svrogwhat i mean is with the '.' the variables seem to behave a bit like logic variables in prolog - it seems like the different terms get unified but just wanted to check whether that is the case27/08 10:35
Svrogsorry - those are 2 different questions - first order vs higher order unification for type checking was a different question27/08 10:37
Saizanthe . patterns aren't really patterns, they don't induce any computation27/08 10:39
Saizanthey are just a source level representation of what you have learned by pattern matching on some other argument27/08 10:40
Saizanthe minimal example would be sym : {A : Set}(a b : A) -> a == b -> b == a; sym a .a refl = refl27/08 10:41
Saizanthere it's not trying to check if the first two arguments are equal, it assumes that they are because of the matching on refl27/08 10:42
Saizanand the .a is showing this fact27/08 10:42
Svrogyup i think i can get27/08 10:43
Saizansym a b refl = .. wouldn't typecheck though, because it interprets that source as insisting on keeping the first two arguments distinct27/08 10:43
Svrogyup cool27/08 10:49
Svrogthanks27/08 10:49
Svrogto prove that a language is strongly normalizable, would it be sufficient to write an evaluation function in agda?27/08 11:04
Saizanit depends on the type of that evaluation function, but yeah27/08 11:07
Svrogoh27/08 11:08
Saizane.g. if you use the non-termination monad to define that evaluation function it's not going to be enough :)27/08 11:09
Svrognon-termination monad?27/08 11:10
Saizanyep, you can define one with coinduction27/08 11:10
Svrogoh right27/08 11:10
Svrogis there an example of that somewhere?27/08 11:10
SaizanCategory.Monad.Partiality in the stdlib27/08 11:11
Saizandata _⊥ {a} (A : Set a) : Set a where now   : (x : A) → A ⊥ later : (x : ∞ (A ⊥)) → A ⊥27/08 11:11
Svrogoh27/08 11:11
Svroginteresting27/08 11:11
Saizanyeah, neat way to model turing-complete stuff27/08 11:13
Svrogi'm having a hard time deciding whether to first play with agda or coq - agda seems more interesting but the documentation is really frustrating, or lack of documentation27/08 11:14
Svrogalso running the interpreter from the command line is a pain27/08 11:14
Svrogmostly due to lack of readline support27/08 11:15
Svrogso i can't just up-arrow, down-arrow to reenter something i typed previously27/08 11:15
Saizanyou can use rlwrap for that27/08 11:15
Svrogi tried27/08 11:15
Svrogdoesn't seem to work27/08 11:16
Saizanah27/08 11:16
Saizani'd recommend the emacs mode anyhow27/08 11:16
Svrogyeah i might have to try that27/08 11:16
Svrog<- vim user27/08 11:16
Svroghaha27/08 11:16
Svrogare there any other provers that are as expressive as coq and agda?27/08 11:25
Svrogand that are somewhat mature27/08 11:25
Svrogwell i guess epigram too27/08 11:25
Svrogbut are there any others?27/08 11:25
Saizani've seen NuPrl and Isabelle being mentioned, but i don't know much about them27/08 11:27
Svrogisabelle lacks dependent types27/08 11:27
Svrogi think nuprl is also missing something, not sure what27/08 11:28
wiresMight it be possible to use agda's emacs input mode outside of agda mode, say in haskell mode or latex mode27/08 11:30
wires?27/08 11:30
wires(I mean the unicode input)27/08 11:30
* wires is emacs n00b27/08 11:31
Saizanit should be, but i don't know the details27/08 11:31
wiresAny idea where i can look further?27/08 11:32
SaizanM-x set-input-method27/08 11:33
Saizanthe input method is called Agda :)27/08 11:34
wiresawesome, let me test it27/08 11:35
Svrogin Data.Nat, in the type definition of ≤′, what are ≤′-refl and ≤′-step ? they are not referenced anywhere else in the file27/08 11:45
Svroginstead ≤′ is used27/08 11:46
Svrogwhich only appears to be defined as a type, no constructor or a function with that name27/08 11:47
Saizan≤′-refl and ≤′-step are the constructors of ≤′27/08 11:51
Svrogis that some special syntax?27/08 11:51
Svrogthe -refl and -step parts27/08 11:51
Saizanno27/08 11:52
Svrogoh27/08 11:52
Saizan- can appear in identifiers27/08 11:52
Svrogyeah i was just confused as they're not used anywhere27/08 11:52
Svrogwhile ≤′ is27/08 11:52
Saizanyeah, there isn't anything defined that needs to mention them in that module27/08 11:53
Svrogoh they're used Induction.Nat27/08 11:53
Svrogso then z≤n is a constructor too? for ≤27/08 11:55
Saizanyep27/08 11:55
Svrogah cool27/08 11:55
Svrogi was initially reading that as a constructor ≤ which takes z and n as arguments27/08 11:56
Saizanheh, nope27/08 11:56
Svrogyeah - doesn't make any sense when read that way - i wasn't paying much attention to the definition until just now, comparing it to the other one27/08 11:57
Svrogis compare what i'd normally use to compare 2 natural numbers? there's nothing in the standard library like the usual <, <=, ==, ... functions?27/08 12:26
Saizanthere's ≤? just above27/08 12:28
Svrogbut that's a type27/08 12:28
Svrogin the interpreter it lets me type 3 < 227/08 12:28
Saizan_≤?_ is not a type27/08 12:28
Svrogooh oops27/08 12:28
Saizanit's a comparisong function27/08 12:28
Svrogmissed the question mark27/08 12:28
Saizanthere's _≟_ too27/08 12:29
Svrogthanks, that's just what i was after27/08 12:29
Svrogyeah i know of that 2nd one27/08 12:30
Svrogdoes agda have something like @ in haskell?27/08 12:56
Saizanno27/08 12:57
Svrogah27/08 12:58
Svrogannoying27/08 12:58
Svrogwhat are the scoping rules for where? is it possible to define some things that are usable across a few clauses of a definition?27/08 13:01
Saizansimilar to haskell, so no, except for "with"27/08 13:04
Svrogi am using with and it's not working :(27/08 13:04
Svrogonly appears to be defined in one clause27/08 13:04
Svrogoh well27/08 13:05
Saizanyou've to put the where clause after the with but before the patterns27/08 13:06
Svrogaaah27/08 13:06
Svrogcool, very useful27/08 13:07
Svroghmm, nope i still get out of scope variables27/08 13:12
Saizancode?27/08 13:19
Svroghttp://hpaste.org/5070827/08 13:21
Svrogthat's not the whole thing, but yeah - i just tried to put in t' and it's complaining that it's not in scope27/08 13:21
Svrogwhen i inline it, then it's fine27/08 13:22
Svrogwell... except for the termination-check error haha27/08 13:22
Svrogadded a simpler example of what's failing27/08 13:31
Saizani see, i guess z's scope is only the expression feeded to with27/08 13:32
Svrogso there's no way to extend that to the 2 clauses below?27/08 13:33
Saizannot that i know of, at least27/08 13:35
Svrogjust noticed i messed up the type - missing an extra ℕ27/08 13:35
Svrogagda didn't complain though - at least not while z was out of scope27/08 13:36
Svrogsomehow i'd have expected the type error to be reported before variables out of scope, not that it matters much i suppose27/08 13:37
Saizannah, resolving scoping is always done first27/08 13:38
Svrogah27/08 13:39
Svrogi'm off for a bit - thanks for helping me out Saizan27/08 14:19
Saizannp27/08 14:34
glguy_Is there a name for this property:   (a + b) * (c + d) = (a * c) + (b * d)      (+ and * are just used as generic operators here)27/08 19:29
copumpkininterchange27/08 19:30
copumpkinsort of27/08 19:30
copumpkinhttp://en.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_argument is also related27/08 19:30
augurcopumpkin: its the middle 4 interchange law!27/08 19:35
copumpkin?27/08 19:35
augurwhat glguy_ is asking about27/08 19:36
auguratleast, it its middle 4 if we're in a bicategory27/08 19:36
glguy_I threw this up to that total programming thread on reedit ( http://www.reddit.com/r/programming/comments/jvu2w/x/c2fm58g ). Do you think I did anything to make Agda look more confusing than it should?27/08 19:43
glguy_(I'm aware this is about as trivial as things get)27/08 19:44
glguy_I just suspect that if anyone bothers looking at it it could be their first impression of Agda27/08 19:44
nappingI think the lemma can be improved27/08 20:03
copumpkinis that the opposite of proved?27/08 20:04
glguy_meh, gtg now27/08 20:04
glguy_o/27/08 20:04
copumpkinfare thee well27/08 20:04
AMER}ALHOBHi27/08 23:49
AMER}ALHOBCan see me27/08 23:49
glguyCan see you27/08 23:50
AMER}ALHOBOh27/08 23:50
AMER}ALHOBWhat the channle27/08 23:50
AMER}ALHOBSpeak arabic27/08 23:51
glguyI don't think there is an Arabic-speaking Agda channel.27/08 23:51
AMER}ALHOBhawo cuntry you?27/08 23:53
AMER}ALHOBHow27/08 23:54
AMER}ALHOBGood bay27/08 23:56
AMER}ALHOBحدا يحكي عربي27/08 23:56
AMER}ALHOBيا شباب27/08 23:57
glguyEnglish, please.27/08 23:57
AMER}ALHOBOK27/08 23:57
AMER}ALHOBI need name channle speak arabic27/08 23:58
AMER}ALHOByou know?27/08 23:58
--- Day changed Sun Aug 28 2011
glguySorry, no.28/08 00:00
AMER}ALHOBThank you28/08 00:02
xplatagda my dear, whatever do you mean "record types are not allowed in mutual blocks"?28/08 00:37
xplatsurely you can't mean that record types are not allowed in mutual blocks28/08 00:37
glguyMaybe it means that record types are allowed in mutual blocks?28/08 00:37
xplatsuch a pronouncement could only be discovered in the ravings of a lunatic28/08 00:38
xplatmore seriously, how do i define my context type mutually-recursively with my type-family type if i don't have records in mutual blocks?28/08 00:40
xplati could make it a data, but then it won't ... eta.28/08 00:42
Saizani thought they lifted that restriction28/08 02:20
xplatis it lifted in darcs?28/08 02:54
glguyI was just playing with that trivial fib / fib' from the Reddit discussion of the total functional programming paper and came up with this: http://hpaste.org/50725  … I know enough Coq to get this far (and #coq is dead), Everything there loads, but what am I doing wrong that is making this so difficult?28/08 02:55
glguyAnyone know if you can leave holes when defining functions in Coq like you can in Agda?28/08 17:34
npouillardglguy: the refine tactic has some ressemblance but not much28/08 18:12
npouillard"Program" might be tricked to do that maybe28/08 18:13
glguyUsing Program resulted in definitions that refused to unfold nicely28/08 18:13
glguyI would get something like: fib (S (S p)) and I couldn't figure out how to get it to take one step from that point. I'm sure it makes sense when you know what's going on :)28/08 18:14
npouillardhum sad...28/08 18:14
npouillardfib 2 does reduce though. right?28/08 18:15
glguyYeah, fib of a constant would simplify to a single value28/08 18:16
npouillardif you Show fib. is that readable?28/08 18:16
glguyusing program my fib ended up being an unreadable mess wrapped around an accessibility proof because I tried to do a single pattern match and had S (S p) => fib (S p) + fib p28/08 18:17
npouillardyep28/08 18:18
glguyThe alternative is to do two separate matches and structural induction, but I just wanted to see what happens if you define it the textbook way rather than fitting into structural recursion constraints28/08 18:18
glguyThe incorporation of termination proofs into function definitions is really unfortunate28/08 18:26
--- Day changed Mon Aug 29 2011
dolioSo, emacs on my laptop is in fact a newer version than on my desktop here.29/08 02:56
glguyWhat's the best way to define a "less-than" relation on a type with 5 constructors?29/08 05:11
glguyI have a particular ordering in mind29/08 05:11
glguyproject them to naturals and use the existing < ?29/08 05:12
glguyenumerate the 10 valid pairings?29/08 05:12
copumpkinugh :P29/08 05:12
glguyscrew it, I'm not going to let this hold me up! 10 pairings it is :)29/08 05:16
glguyhttp://hpaste.org/5075129/08 06:41
glguyany idea what part of this is exhausting Agda?29/08 06:41
glguyIs it just too long? Are instance arguments slow?29/08 06:41
glguy(darcs Agda)29/08 06:41
copumpkinlol29/08 06:44
copumpkinnot a clue :)29/08 06:45
djahandarieIt's not possible to get lt-irreflexive for free?29/08 06:45
copumpkinno29/08 06:47
copumpkinalthough agsy will write it for you29/08 06:47
copumpkinand many of those annoying functions29/08 06:47
copumpkinif you tell it to pattern match29/08 06:47
glguyAny other suggestions on how to structure this? I'm just kind of playing around but I thought it would be fun to work through one of these29/08 06:49
augurman29/08 13:18
augurconor29/08 13:18
augur:|29/08 13:18
augurhe linked me to his partial refinement solution. so simple.29/08 13:25
Saizani.e. adding a Maybe somewhere?29/08 13:33
augurSaizan: yeah29/08 15:15
augurSaizan: but pretending like you didnt :)29/08 15:15
augurbasically his solution is to index things by their "type" (not in-agda type, but the name of the type that you're simulating)29/08 15:16
augurbut to use a partial algebra F A -> Maybe A29/08 15:16
augurand then just include a constructor argument of type IsJust t (for your new Maybe "type" index t)29/08 15:17
augurso that prevents any failure indices, so you can fromJust your indices and get out only the "type"29/08 15:18
augurso you never index by Maybe "type"s, just by pure "type"s29/08 15:18
augurthis might be how its done in WiaTRaIT, but i dont fully understand the paper so i cant tell29/08 15:19
Saizan@decode  WiaTRaIT29/08 15:22
lambdabotUnknown command, try @list29/08 15:22
auguri should add it!29/08 15:22
augurhow?29/08 15:22
augur@help29/08 15:22
lambdabothelp <command>. Ask for help for <command>. Try 'list' for all commands29/08 15:22
augur@help list29/08 15:23
lambdabotlist [module|command]29/08 15:23
lambdabotshow all commands or command for [module]. http://code.haskell.org/lambdabot/COMMANDS29/08 15:23
augur@help @list29/08 15:23
lambdabothelp <command>. Ask for help for <command>. Try 'list' for all commands29/08 15:23
auguroh woops haha29/08 15:23
augur@help @decode29/08 15:23
lambdabothelp <command>. Ask for help for <command>. Try 'list' for all commands29/08 15:23
augur@help decode29/08 15:23
lambdabothelp <command>. Ask for help for <command>. Try 'list' for all commands29/08 15:23
augur:|29/08 15:23
Saizanno, there's no decode command29/08 15:23
auguroh right29/08 15:24
Saizani was actually asking you29/08 15:24
augurhaha <329/08 15:24
augurtell me how to add a @where and ill tell you and teach lambdabot at the same time :D29/08 15:24
Saizan @where+29/08 15:24
augur @where+ <name> <url>?29/08 15:24
Saizanyep29/08 15:25
augur@where+ wiatrait http://personal.cis.strath.ac.uk/~raa/inductive-refinement.pdf29/08 15:25
lambdabotIt is stored.29/08 15:25
augur@where oaao29/08 15:25
lambdabotI know nothing about oaao.29/08 15:25
augur@where+ oaao http://personal.cis.strath.ac.uk/~conor/pub/OAAO/Ornament.pdf29/08 15:25
lambdabotI will remember.29/08 15:26
Saizan(ah, right, papers i linked to you at the start of this quest :)29/08 15:27
augurprobably!29/08 15:27
Saizanno, for sure29/08 15:27
auguri didnt understand enough to understand why they were the correct answer29/08 15:27
Saizananyhow, the CT is a bit too thick for me there..29/08 15:27
auguroaao was certainly an important first step tho29/08 15:27
Saizanand it feels not much more than the theory behind oaao29/08 15:28
augurindeed29/08 15:28
auguri mean, once you slog through the CT, it looks like oaao is an almost direct translation29/08 15:28
augurmodulo the need to use codes29/08 15:29
auguror so it seems29/08 15:30
augurthe wiatrait treatment of dependent types is interesting tho. basically, for something like Vec X : Nat -> Set, the type is (Nat, Vec X)29/08 15:32
augurwhere whats being refined is actually Nat29/08 15:33
Saizan one is the Pow(erset) representation the other is the Fam(ily) one, conor explained the relationship here not so long ago29/08 15:35
augur?29/08 15:35
Saizanno, maybe i'm wrong29/08 15:36
augurmaybe, maybe not. im not sure what "one" and "the other" refer to so its hard to know!29/08 15:37
Saizanhttp://hpaste.org/50758 <- i was thinking of this29/08 15:37
SaizanVec A : Pow Nat; (List A , length) : Fam Nat29/08 15:39
Saizanand (Sigma Nat (Vec A) , proj1) : Fam Nat as well29/08 15:40
Saizanthough this doesn't seems to have much to do with (Nat , Vec X)29/08 15:40
Saizanexcept that (Nat , Vec X) : Sigma Set Pow29/08 15:41
wires_Saizan, I wrote a short blog on using agda input method for coq29/08 15:42
augurhm. well, im guessing that the families model is easier to work with29/08 15:42
wires_Saizan, http://agda.posterous.com/use-agda-input-mode-in-code29/08 15:42
wires_thanks for your suggestion yesterday29/08 15:42
Saizancheers :)29/08 15:43
wires_augur, Saizan on DTP 2011 two days ago there was a nice talk explaining ornaments29/08 15:44
auguroh?29/08 15:44
Saizanyeah, i wanted to go :\29/08 15:45
augurwhats DTP29/08 15:45
wires_http://www.cs.ru.nl/dtp11/program.html29/08 15:45
wires_see the talk by Josh Ko29/08 15:45
Saizanwere the talks filmed?29/08 15:45
auguroh that explains why conor was tweeting about nijmegen29/08 15:46
wires_sadly, not filmed29/08 15:46
wires_i brought a camera but forgot to use it29/08 15:46
wires_did record a little bit of conors talk, which was very entertaining as usual29/08 15:47
kosmikus:)29/08 15:47
wires_hehe29/08 15:47
wires_Josh explained it really nicely, so it's a bummer that it wasn't recorded29/08 15:47
wires_But his slides are very nice too29/08 15:48
kosmikusJosh's talk was great29/08 15:48
wires_agreed, many talks were great29/08 15:48
kosmikusyes, but this was one I didn't know what to expect of (hadn't looked at the paper before, didn't know the speaker)29/08 15:48
kosmikusso it was unexpectedly great29/08 15:48
wires_hehe29/08 15:49
wires_what about Caprettas talk? I thought that was very clear and enjoyable29/08 15:49
kosmikusit was29/08 15:49
kosmikusquite nice one, too29/08 15:49
* wires_ nods29/08 15:50
kosmikusit was a good day, all in all29/08 15:50
wires_I took pictures of all speakers, will put them online maybe tonight29/08 15:50
kosmikusI felt very exhausted after the summer school. I wasn't sure if I'd regret staying in .nl for another day.29/08 15:50
kosmikusI didn't regret it at all in the end.29/08 15:50
augurconors slides look like his talk wouldve been hilarious29/08 15:50
augurid ID id : ID29/08 15:50
augurx.x29/08 15:50
wires_kosmikus, I had appointment on saterday and was first thinking not to go, I already went to the coq workshop29/08 15:51
wires_but it was very much worth it29/08 15:51
wires_anyway, back to work29/08 15:52
auguranyone know of a good introduction to using the equational reasoning part of the standard library?29/08 18:10
ppavelV6augur: http://www.iis.sinica.edu.tw/~scm/pub/mpc08.pdf Algebra of programming has some tips29/08 19:05
glguyheh, I finished that puzzle last night http://www.galois.com/~emertens/puzzle2/Puzzle2.html29/08 21:57
glguypoor Agda takes between 15 seconds and 60 seconds to load29/08 21:58
copumpkindid it find the solution for you, at least?29/08 21:58
glguyI had to find the solution, it verified that it was the one29/08 21:58
copumpkinboo29/08 21:58
copumpkinagsy should have found it :)29/08 21:58
glguyWhat is "agsy"?29/08 21:59
glguyYou mentioned that last night, too.29/08 21:59
copumpkinC-c C-a29/08 22:00
copumpkinthe proof finder29/08 22:00
copumpkinI use it to write annoying but obvious proofs of things29/08 22:00
copumpkinif you give it the -c option, it'll do case-splitting29/08 22:00
copumpkin(that is, put -c in the hole and then do C-c C-a)29/08 22:00
glguyoh, interesting29/08 22:00
copumpkinI've used it to write annoying decision procedures for equality of large types and such29/08 22:01
glguyFunction.Inverse._↔_ ended up being a nice way to deal with explaining the relationship between the different types29/08 22:01
glguyAnd I'd still like a nicer way to write: The 5 people were the owner of the purple house, the one who loves turnips, the person whose flight departs at 2:00pm, Julia, and the owner of the red house.29/08 22:03
glguy(rule 10)29/08 22:03
mokuscopumpkin: are there any already-existing convenience functions for creating objects/morphisms in Categories.Power.Exp (Fin n)?29/08 22:33
mokusif so I seem to be missing them29/08 22:33
copumpkinhmm29/08 22:33
copumpkinthat stuff is mostly xplat29/08 22:33
mokusah, k29/08 22:34
copumpkinI'd expect them to be though29/08 22:34
copumpkindoesn't that have an alias?29/08 22:34
mokusnot that I see, but there are a lot of functor type aliases that use it29/08 22:34
copumpkinPower : (n : ℕ) → Category o ℓ e29/08 22:34
copumpkinPower n = Exp (Fin n)29/08 22:34
mokusmaybe in his branch, i'll check that out29/08 22:34
mokusoh, duh... I'm a little blind today I guess29/08 22:35
mokuswas too focused on the Powerendo specifically, and since it didn't use that alias I must have made the leap to thinking there wasn't one29/08 22:35
mokusin any case, I guess all i'm really after is something like an existing 'flip Data.Vec.index'29/08 22:36
mokusto avoid recreating the wheel29/08 22:36
copumpkinbut iirc there are several helpers for Power29/08 22:38
mokusyea, i'm looking through them29/08 22:39
copumpkinmostly on functors from Power though29/08 22:39
mokusit's not that big a deal, just figured i'd ask before reimplementing something so trivial ;)29/08 22:39
copumpkin:)29/08 22:40
copumpkinI kind of enjoy them29/08 22:40
copumpkinthey're much nicer than picking an arbitrary association of pairs29/08 22:40
copumpkinit'd be nice if we had clean syntax for constructing them easily though29/08 22:40
mokusyea, it's a nice abstraction, but it's making it more complicated that it seems it should be to express monadic strength29/08 22:41
copumpkinah29/08 22:41
copumpkinyeah, xplat's been busy recently so hasn't been on much29/08 22:41
copumpkinbut if you ask him a question I'm sure you'll get an answer in < a couple of days :P29/08 22:41
mokusof course if i grokked enriched categories better i'd probably be able to do it more easily, as all the good descriptions seem to involve categories enriched over themselves29/08 22:42
mokusseems like if i knew what that actually meant i'd be able to tell it to Agda in fewer words29/08 22:42
copumpkinhttp://hpaste.org/5076429/08 23:10
mokusnice29/08 23:10
mokusthat's a fun proof on paper29/08 23:11
mokusmakes nice pictures ;)29/08 23:11
copumpkinmade it cleaner in an annotation :)29/08 23:14
copumpkinand again29/08 23:16
mokuswhy is math so fun?  ;)29/08 23:24
mokusand more importantly, why doesn't everyone think so?29/08 23:24
copumpkinbeats me29/08 23:25
copumpkinpoor everyone29/08 23:25
copumpkinthey're missing out29/08 23:25
mokusyea, they sure are29/08 23:25
mokusthey never believe me when i tell them that though29/08 23:25
copumpkinyeah :/29/08 23:26
npouillardglguy: did you see my follow up on your yesterday paste about Puzzle2 + instance arguments ?29/08 23:38
glguyI did not29/08 23:39
glguyI will check the logs29/08 23:39
npouillardthis one http://hpaste.org/5075129/08 23:39
glguyOH29/08 23:40
glguyso using29/08 23:40
glguyopen module Inverse2 {From To : Set} {{x : From ↔ To}} = Inverse x29/08 23:40
glguyI eliminated a bunch of instance argument usage29/08 23:41
glguyI'm down to these two:29/08 23:41
glguytoProp : {A : Set} {{iso : Person ↔ A}} → Person → A29/08 23:41
glguytoProp {{iso}} p = to iso ⟨$⟩ p29/08 23:41
glguyfromProp : {A : Set} {{iso : Person  ↔ A}} → A → Person29/08 23:41
glguyfromProp {{iso}} p = from iso ⟨$⟩ p29/08 23:41
glguydo you think those suffer from the same problem?29/08 23:42
npouillardnop29/08 23:42
npouillardthe issue is somewhere between:29/08 23:43
glguySo the important difference is that open Inverse {{…}} in general in level29/08 23:43
glguywhile your faster version only searches for the two sets?29/08 23:43
glguyat zero29/08 23:43
npouillardnot only levels, but setoids as well29/08 23:43
glguyah, right29/08 23:44
glguycurrent iteration: http://www.galois.com/~emertens/puzzle2/Puzzle2.html29/08 23:44
glguyThis still takes somewhere between 15 and 60 seconds on my computer29/08 23:44
glguyI don't know what causes the variation between runs29/08 23:44
glguy(I've been changing little bits here and there)29/08 23:45
glguyoh, good. The current version compiles to html in 15 seconds :)29/08 23:46
npouillardand I guess that the less you have in context the faster it goes (using vs hiding)29/08 23:46
glguyoh, then I'll have to switch to usings29/08 23:47
npouillardI don't know what kind of difference this can make29/08 23:48
glguyopen import M using (n), can't you still access M.z29/08 23:50
glguydoes the using actually affect what is in scope?29/08 23:50
npouillardhum not sure29/08 23:51
glguyanyway, I think that it is better style to be explicit29/08 23:51
npouillardbut for sure the instance argument engine never pick an M.x thing29/08 23:52
glguyat this point I think it is just slow because Agda is slow, and not because I have instance arguments29/08 23:52
npouillardok, but open Inverse {{...}} was deadly slow29/08 23:53
* npouillard is tried, better go to sleep29/08 23:56
glguynpouillard: thanks for looking into that speed issue for me29/08 23:59
--- Day changed Tue Aug 30 2011
xplathm, irreflexivity proofs might be a fun one for someone to do as a tactic now that reflection can inspect types30/08 01:56
copumpkinoh, it can?30/08 02:00
copumpkindecision procedures would also be fun30/08 02:00
xplatusing doesn't actually affect what's visible, only what name(s) it's visible under30/08 02:12
xplatif anything using vs hiding makes less things visible by creating scope conflicts, but that won't speed things up either :)30/08 02:13
copumpkinusing?30/08 02:13
xplatbut yeah, i guess it might affect what's available to instance args, i wasn't thinking about that30/08 02:14
xplatcopumpkin: i guess 'opening vs hiding' would be a better term30/08 02:14
xplatmokus: i'd like to help you out, but Data.Vec doesn't even have 'index'.  assuming you mean 'lookup', the best i can come up with as a guess is 'select'30/08 02:19
mokusxplat: yea, i realized shortly after i said it that i had said the wrong one, meant lookup30/08 02:20
augurcopumpkin!30/08 02:20
augurhave you read wiatrait or oaao?30/08 02:20
auguror both!30/08 02:21
copumpkinno30/08 02:21
auguryou should. they're wonderful30/08 02:21
xplati've read parts of them, they are nice30/08 02:21
copumpkinlinks?30/08 02:22
xplat@where oaao30/08 02:22
lambdabothttp://personal.cis.strath.ac.uk/~conor/pub/OAAO/Ornament.pdf30/08 02:22
augur@where wiatrait30/08 02:22
lambdabothttp://personal.cis.strath.ac.uk/~raa/inductive-refinement.pdf30/08 02:22
copumpkinoh, that30/08 02:22
copumpkinoh, that30/08 02:22
copumpkinyeah, then both :P30/08 02:22
augurthen both what30/08 02:22
augur:|30/08 02:22
copumpkinthen I've read both of them30/08 02:23
xplati'm going to be going through them more deeply soon for something i'm working on30/08 02:23
auguroh!30/08 02:23
augurgood :D30/08 02:23
xplatalong with levitation30/08 02:23
augurconor shared his partial refinement implementation with me30/08 02:23
augurwhat a beautiful but of code it is30/08 02:23
xplatwhat you described sounds like a straight reading of how it was done in wiatrait30/08 02:24
xplator wherever it was i saw it done categorically30/08 02:25
augurit probably is30/08 02:25
augurwiatrait is hard to understand tho30/08 02:25
augurlots of categorical concepts that im not familiar with30/08 02:25
augursome of which go unexplained30/08 02:25
xplatthe original dream of the world wide web was something like 'all of the world's knowledge, with every potentially unfamiliar term as an underlined blue link'30/08 02:27
xplatso if you were a caveman thawed out of a glacier, and someone had taught you Simple English and how to click on links and sat you there with an internet connection, you could sit there 20 years and bootstrap yourself to aerospace engineer30/08 02:28
augursounds like wikipedia30/08 02:29
augura little bit, anyway30/08 02:29
mokusI just realized that when I was talking a few days ago about compile times under the new agda I was also including the compilation of the part of the std lib depended on by categories30/08 15:54
mokusso it probably _was_ doing significantly better than 2.2.1030/08 15:55
copumpkinyay30/08 15:57
copumpkinI actually pulled your changes and xplat's30/08 15:57
copumpkinand tried to rebuild before pushing again, but ran out of memory30/08 15:57
mokuscool, i'll resync with yours too30/08 15:57
copumpkinbut that may be caused by the fact that I'm on a 64-bit ghc30/08 15:57
copumpkinnah, I haven't pushed yet30/08 15:58
mokusah30/08 15:58
copumpkincause I haven't made sure everything fits together nicely :P30/08 15:58
copumpkinI found one issue but am not sure where it's from30/08 15:58
mokusi was able to build Everything.agda using 64-bit30/08 15:58
mokusit took a peak of about 6.5 GB for the agda process30/08 15:58
copumpkinthere was a pattern match on Fin 2 with only two cases that needed three30/08 15:58
copumpkinhah30/08 15:58
copumpkinyeah, mine started swapping and I decided to give up30/08 15:58
mokusyea, mine did too - i only have 4GB on that machine30/08 15:59
mokusi just took a coffee break and came back in about half an hour and it was done30/08 16:00
mokustiming categories/Everything.agda on my desktop machine now, which won't run out of mem30/08 16:00
copumpkin:)30/08 16:01
mokusif that Fin pattern matching issue is in my code, it'll be in the monad strength part which is still very ugly30/08 16:02
mokusthough i think i eliminated all the direct use of Fin, and have it just using Vec30/08 16:02
copumpkinhmm, not sure where it came from :) I'll run git blame later30/08 16:03
copumpkinTHEN WE WILL KNOW30/08 16:03
* mokus cowers30/08 16:03
mokus;(30/08 16:03
mokuswas there a recent change in matching that would change whether you have to match on the impossible case?30/08 16:04
copumpkinI don't think so30/08 16:04
copumpkinnot sure though30/08 16:04
copumpkinyou generally have to match on anything that's well-typed30/08 16:05
mokusyea, that's what i thought30/08 16:05
mokusin the few places i've used Fin I remember having to include the impossible case30/08 16:05
mokushow weird, Everything.agda built on whatever darcs build of Agda I have on my laptop, but doesn't now on my desktop30/08 16:10
mokusguess i'll go back a few patches30/08 16:12
mokuscopumpkin: got distracted, but in case you were wondering it took 11 min to compile30/08 18:01
copumpkinmokus: ah, nice30/08 18:02
mokusunfortunately i don't know how long 2.2.10 would take for the same, maybe i'll start that going in the background and see30/08 18:03
--- Day changed Wed Aug 31 2011
xplatso i just had a thought today: if delimited continuations break the symmetry between positive and negative like the polarity folks say, then there should be a dual that breaks it the other way31/08 03:22
xplatand from that follows that there should be a notion of a delimited value, that includes another value31/08 03:23
xplatbut that's a value with a hole, which is a derivative of a value31/08 03:24
xplatso are delimited continuations derivatives of continuations?31/08 03:24
xplator maybe antiderivatives?31/08 03:25
xplati guess i need to read more than the abstract of that paper after all31/08 03:25
xplatbut not immediately31/08 03:25
xplathm, come to think of it delimited values might be the LF functionspace31/08 03:38
xplatthe one that's so good for junk-free HOAS31/08 03:39
dschoepeIs it normal that "open import Data.String" needs about 800M of RAM and takes incredibly long to finish? (using Agda-2.2.10 and stdlib-0.5)31/08 15:16
Saizanif that's the first time you load the relative stuff from the stdlib then it's not so surprising31/08 15:19
dschoepeSaizan: Yes, it's the first time. thanks31/08 15:21
augurxplat: did you find the answer to your question?31/08 15:58
skihm, is there some common work-around when you want a data type which is not strictly positive ?31/08 16:41
skii want a type `A' which should be isomorphic to `(X -> A -> O) -> O' (or a type `B' which is isomorphic to `X -> (B -> O) -> O' -- `A' and `B' could also be mutually recursively defined)31/08 16:45
* ski wonders whether `codata' would help, and what the syntax for that would be, then31/08 16:48
copumpkinit doesn't exist anymore31/08 16:50
* ski has Agda2 - 2.1.3 - 2008-08-27 here31/08 16:55
Saizancodata still required strict positivity, i think31/08 16:55
Eduard_Munteanuski: you can turn off the positivity checker IIRC31/08 19:22
Eduard_MunteanuYou should really get the darcs version, lots of fun stuff in there.31/08 19:23
dolioThe only way is to turn off the positivity checker.31/08 19:36
dolioThose datatypes aren't justified by the set theoretic semantics people usually use for type theory, so they aren't allowed.31/08 19:37
skiwell, do you mean the positive but not *strictly* positive ones or do you mean the negative ones (such as `Santa') ?31/08 19:39
ski(btw, wouldn't one need some hoops to interpret `Stream a' set-theoretically (assuming here it's not defined as `Nat -> a', but as consisting of an `a' and an `Stream a') ?)31/08 19:40
dolioI mean the positive but not strictly positive ones.31/08 19:41
dolioHaving a set S that is isomorphic to 2^2^S is problematic.31/08 19:42
dolioOr hyperfunctions.31/08 19:44
dolioFoo a b ~ (Foo a b -> b) -> a31/08 19:44
dolioI don't think they let you prove false like the negative types do, but there's no story for them set theoretically.31/08 19:45
dolioIf you read the Fibrational Induction Rules or what have you paper, they mention some of this.31/08 19:47
dolioAnd how their framework is nice, because you can apply it to systems that don't work with the usual set theoretic semantics of things.31/08 19:48
dolioSo, they derive an induction principle for hyperfunctions, which other proposals couldn't, because they don't work with the right categories or something.31/08 19:49
dolioFibrational Induction Rules for Initial Algebras.31/08 19:50
dolioAnyhow, codata isn't a problem in Set. They're just terminal coalgebras.31/08 19:52
dolioYou can take greatest fixed points in set theory.31/08 19:52
dolioUnion instead of intersection.31/08 19:52
skiyeah, but you can't have `Stream a = a * Stream a' (foundation strikes again)31/08 20:09
skiat least not with the usual definition of product .. istr seeing Girard(?) talking about an alternative definition using powersets and unions31/08 20:09
ski(maybe that's what you alluded to)31/08 20:09
dolioThe set of naturals is isomorphic to the product of itself with itself.31/08 20:33
dolioSo it satisfies a similar equation.31/08 20:33
dolioSo you should be able to take the union of all sets S such that S ~ A * S, and that would be the terminal coalgebra.31/08 20:35
dolioUnless I'm forgetting something.31/08 20:37
dolioFoundation is about sets containing themselves as elements.31/08 20:37
Eduard_MunteanuSanta? Is that like Warrior?31/08 23:03
* Eduard_Munteanu saw somebody posting that some time ago31/08 23:03

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