/home/laney/.irssi/irclogs/Freenode/2010/#agda/October.log

--- Log opened Fri Oct 01 00:00:45 2010
copumpkinhmm01/10 00:14
copumpkinhttp://snapplr.com/bsdd01/10 00:14
copumpkinis that normal?01/10 00:14
copumpkinI'd expect if all of assoc is declared to be irrelevant01/10 00:21
copumpkinthat I'm safe to use any irrelevant terms anywhere, including a rewrite?01/10 00:22
stevani think so too. try using the projection rather than pattern matching?01/10 00:31
copumpkinyeah, that works :/01/10 00:34
stevanbug?01/10 00:34
copumpkinI guess they might have forgotten a case in the patch for irrelevant fields?01/10 00:34
stevanyea01/10 00:35
copumpkinI thought pattern matching on the constructor to a record desugared to projections anyway?01/10 00:35
stevanirrelevant stuff is perhaps treated differently? i dunno01/10 00:36
copumpkinhmm01/10 00:41
copumpkinI'm not sure what universe to put this slice category in01/10 00:41
stevanso this should work: http://hpaste.org/40253/bug    yes?01/10 00:55
copumpkinunless I'm misunderstanding it, I'd say yes01/10 00:56
Saizanproj′ doesn't typecheck?01/10 00:56
stevannope01/10 00:56
stevani wonder why --irrelevant-projections is an option while irrelevance in general isn't01/10 00:57
stevanis there something unsafe about irr proj?01/10 00:57
dolioproj′ should not type check.01/10 00:59
stevanwhy's that?01/10 00:59
dolioBecause \(c x) -> x is not elligible to have type [ A ] -> A, even at compile time.01/10 01:00
dolioYou'd have to take it as an axiom.01/10 01:00
dolioirrelevant : forall {i} {A : Set i} -> .A -> A01/10 01:01
dolioThen use that.01/10 01:01
dolioEr, that should be .irrelevant.01/10 01:01
dolioThat is how the irrelevant projections will eventually work.01/10 01:02
copumpkinhmm01/10 01:03
dolioRight now they do something weird.01/10 01:03
dolioIf you get it to normalize an irrelevant projection, you'll just get a blank lower bar.01/10 01:03
dolioBecause it's been erased to the empty expression.01/10 01:03
copumpkinyeah, I've seen that01/10 01:04
dolioBut that doesn't really make sense.01/10 01:04
dolioReally, unless you go via an axiom like that, to make sense of projections being irrelevant themselves, you'd lose the ability to erase at compile time.01/10 01:06
copumpkinah01/10 01:06
copumpkinnot sure I really understand why proj is okay though01/10 01:07
copumpkinseems like it would suffer the same issue01/10 01:07
dolioIt's okay by fiat currently.01/10 01:07
copumpkinah :)01/10 01:08
doliohttp://hpaste.org/paste/40253/an_example#p4025401/10 01:08
dolioAgda complains about inflate being used in foo's type, but it shouldn't.01/10 01:09
dolioBecause type annotations are an irrelevant context.01/10 01:09
copumpkinoh, hmm01/10 01:09
dolioSo, what should that evaluate to?01/10 01:09
dolioRight now, it'd be 'foo : <empty expression>'.01/10 01:10
dolioBecause the inflate field of the record has already been erased.01/10 01:10
copumpkinso foo has no accessible type, but has a value?01/10 01:10
copumpkinor would01/10 01:10
copumpkinso is there a "good" way to make this all behave nicely?01/10 01:10
dolioIf you decide it should evaluate to ℕ, then you can't do erasure on open terms (which EPTSes normally allow).01/10 01:10
copumpkinwell, not being able to use nice things like rewrite makes this a lot more painful :)01/10 01:13
doliohttp://hpaste.org/paste/40253/alternate_implementation#p4025501/10 01:13
dolioThat's how it will eventually work, I think.01/10 01:13
dolioUsing a datatype instead of a record.01/10 01:13
copumpkinseems similar to the codata spiel01/10 01:14
dolioAt least, that's the current plan.01/10 01:14
dolioThat of course doesn't type check, either, because it erroneously complains about inflate's irrelevance.01/10 01:15
copumpkinyeah01/10 01:17
copumpkinGoal: (Category._∘_ C (Category._∘_ C c⇒d b⇒c) a⇒b ,′ _) ≡01/10 01:20
copumpkin      (Category._∘_ C c⇒d (Category._∘_ C b⇒c a⇒b) ,′ _)01/10 01:20
* copumpkin isn't even sure how to prove the _ part of that01/10 01:31
Saizanthat should be automatic01/10 01:31
copumpkinif only :)01/10 01:31
copumpkinit gets refined to something a bit more useful, but not much01/10 01:32
Saizani mean only the _ part01/10 01:32
copumpkinhmm01/10 01:33
copumpkinwell, at first glance I wanted to use cong\_2 _,\'_01/10 01:33
copumpkinbut it says it makes a variable depend on one it can't depend on01/10 01:33
copumpkin(grr)01/10 01:33
copumpkinso I'm using a plain old cong01/10 01:33
Saizani guess that's because of the dependece01/10 01:34
copumpkinyeah01/10 01:34
copumpkinoh okay01/10 01:34
copumpkina rewrite solved it :)01/10 01:34
copumpkinnow the scary part01/10 01:35
copumpkintrying to figure out what universe level this whole thing should live in01/10 01:35
* copumpkin cries01/10 01:39
copumpkinI think this might need Lift :(01/10 01:39
copumpkinand I really dislike Lift :(01/10 01:41
copumpkinhttp://hpaste.org/40256/slice_category01/10 01:53
copumpkinanyone have any ideas?01/10 01:54
Saizanwhat for, precisely?01/10 01:55
copumpkinwhat universe level the slice category should live in01/10 01:57
copumpkinI can't put identity\^l into the left hole for identity01/10 01:59
copumpkinbecause it complains the universe level is wrong01/10 01:59
copumpkinand thinking about it, I'm not too sure what universe level it should live in, given that the arrows are promoted to objects01/10 01:59
copumpkinmaybe that isn't the problem, hmm01/10 02:09
copumpkinbut in that case, I'm not sure what is01/10 02:09
copumpkinsomething is at the wrong universe level01/10 02:09
Saizanit works if you eta expand01/10 02:17
copumpkinwow, what's up with that?01/10 02:19
Saizani bet it's the implicits01/10 02:21
copumpkinoh01/10 02:21
copumpkinyeah01/10 02:21
copumpkingood point01/10 02:22
copumpkindamned implicits01/10 02:22
Saizanbtw, you only need to abstract them, i.e. "λ {_} {_} {_} {_} → assoc" works too01/10 02:23
Saizannot that it's that much better :)01/10 02:23
copumpkinlol01/10 02:23
copumpkinmeh, I'll just not do any of those implicit lambdas01/10 02:24
copumpkinnow the question is how to fill in the last two holes01/10 02:24
copumpkinwhich happen to be in types :P01/10 02:24
copumpkinoh okay01/10 02:29
Saizan"comp id\' f" instead of inlining it?01/10 02:32
copumpkin?01/10 02:35
copumpkinI'm done01/10 02:36
copumpkinnot very pretty though01/10 02:36
copumpkinhttp://hpaste.org/paste/40256/filled_in_all_the_holes#p4025801/10 02:37
copumpkinworth pushing in its current state?01/10 02:38
Saizanhttp://hpaste.org/paste/40256/a#p40257 <- see my type for identity\^l01/10 02:38
* edwinb is bored waiting in JFK so entertains himself by looking at the Agda code01/10 02:39
copumpkinoh :)01/10 02:39
copumpkinSaizan: that's a lot cleaner, thanks :)01/10 02:39
Saizan"filled in all the holes" is a NSFW title, btw01/10 02:40
copumpkinlol01/10 02:40
copumpkinokay01/10 02:43
copumpkinWAY cleaner now01/10 02:43
copumpkin<_<01/10 02:44
copumpkinhttp://hpaste.org/paste/40256/holes_filled_cleanup_time#p4025901/10 02:44
* copumpkin apologizes01/10 02:44
edwinbyou did that deliberately ;)01/10 02:44
copumpkinI admit it!01/10 02:45
copumpkinnot the comfy chair!01/10 02:45
* edwinb has a stack on Monty Python DVDs in his hand luggage01/10 02:45
edwinbof*01/10 02:45
copumpkin:)01/10 02:45
Saizan:D01/10 02:47
Saizanlooks nice01/10 02:47
Saizanexcept for comp..01/10 02:48
pumpkinit'd be a beautiful rewrite01/10 02:55
pumpkinbut I can't01/10 02:55
pumpkinoh maybe I know01/10 02:55
copumpkinyeah, I can use rewrites in an irrelevant where helper01/10 03:12
copumpkinhttp://snapplr.com/q10b01/10 03:14
copumpkinbetter?01/10 03:14
copumpkinmaybe with a consistent where indentation01/10 03:14
copumpkinokay, pushed :)01/10 03:16
copumpkinnow commas01/10 03:17
* copumpkin coughs01/10 03:38
copumpkin  Hom′ (α , β , f) (α′ , β′ , f′) = Σ′ (A [ α , α′ ]) (λ g → Σ′ (B [ β , β′ ]) (λ h → f′ ∘ T₁ g ≡ S₁ h ∘ f))01/10 03:38
copumpkinwhoops, one \' too many in there01/10 03:50
copumpkinwow this comma category is gobbling up my memory01/10 05:18
dolioYou did slice before comma?01/10 05:27
copumpkinyep :) it was a bit simpler01/10 05:28
dolioThat is true.01/10 05:28
copumpkinI'll probably make a function to convert afterwards01/10 05:28
copumpkin:o01/10 05:57
copumpkintypechecking this thing takes several minutes each time01/10 07:22
copumpkinI'm glad I started with the slice01/10 07:22
copumpkinokay, done with comma01/10 07:53
copumpkinnow the question is whether it's worth making an arrow category separately or just to write it in terms of the comma01/10 07:57
copumpkinI'm all for code reuse but it's nice to show that the different definitions work together too01/10 07:58
copumpkinI wonder what happened the project to fill in Data.Rational01/10 14:53
jonrafkind'first const ∘ f t', how should this be read? o has infixr precendence of 9001/10 17:41
jonrafkindis it ((first const) o f) t ?01/10 17:41
copumpkinI'd guess (first const) o (f t)01/10 17:42
jonrafkindyea, i tried working through the types but it doesnt work out01/10 17:42
jonrafkindfirst (const o f) t, looksl ike it might work01/10 17:42
copumpkinthat seems quite unlikel01/10 17:42
jonrafkindhm01/10 17:42
jonrafkindso what precedence level is function application?01/10 17:43
jonrafkindok (first const) o (f t) worked01/10 18:06
copumpkinsorry, I think function application is higher than any other precedence, always01/10 18:07
copumpkinit's the case in haskell at least01/10 18:07
copumpkinand I assume agda keeps that01/10 18:07
copumpkinif you want to change it for specific functions, you can rename f to f_01/10 18:07
jonrafkindah ok01/10 18:08
jonrafkindcurrying and composition mess with my head :p01/10 18:08
copumpkinbyorgey: species in agda? :) :)01/10 18:09
copumpkinor epigram!01/10 18:09
copumpkindamn, stevan left01/10 18:10
byorgeycopumpkin: yeah, coding up some species stuff in a dependently typed language is something I'd like to try01/10 20:00
copumpkincool paper though :) really enjoyed it01/10 20:00
byorgeycopumpkin: I've gone through lots of odd contortions to get my haskell library to work, basically because Haskell does not have dependent types =)01/10 20:00
byorgeythanks =)01/10 20:00
* copumpkin tries to decide what to add next to the ctfp repo01/10 20:11
copumpkinor maybe I should work on something more concrete01/10 20:11
djahandarieDependent types sure are neat01/10 20:45
copumpkinyep01/10 20:45
djahandarieFor some reason I understood Idris really easily01/10 20:46
copumpkinit's a pretty accessible language01/10 20:46
djahandarieHopefully Agda will be easier now because of that01/10 20:46
copumpkinidris' author is in here, too01/10 20:46
copumpkinthat can't hurt :)01/10 20:46
* edwinb hides01/10 20:47
djahandarieHehe01/10 20:47
* djahandarie bows to edwinb 01/10 20:47
djahandarieedwinb, this is a really minor note, but for some reason the 'Next' link on the 1st page of the Idris tutorial skips to the 3rd page rather than going to the 2nd.01/10 20:48
edwinboops01/10 20:48
edwinbthanks01/10 20:48
* edwinb looks01/10 20:49
danbrownhow would i find out the precedence of to -> operator?01/10 20:50
djahandarieEither way, it's much better than the non-existent Agda tutorial haha01/10 20:50
edwinbthere is an agda one isn't there?01/10 20:50
copumpkinhey, there's a fairly decent agda tutorial, but it's a bit out of date01/10 20:50
edwinbbut I think it's quite old01/10 20:50
djahandarieYeah, the PDF01/10 20:50
djahandarieI also think it is assuming a totally different background than 'Haskell programmer', which your tutorial seems to be aiming at01/10 20:51
edwinbthat's possibly true01/10 20:51
danbrownon http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation01/10 20:52
danbrownunder "Introductions to Agda"01/10 20:52
danbrownthe first paper is described as "aimed at functional programmers"01/10 20:53
danbrown;)01/10 20:53
djahandarieYeah, that is the one I'm refering to. I would agree that it is aimed at functional programmers01/10 20:53
danbrownmoreover, that's the one that sucked me in01/10 20:53
djahandarieI'd just like one that is "Hey, you've doing Haskell for awhile now and are pretty good. Ever had [blah] happen? Yeah, we fix that... [boom]"01/10 20:54
danbrownah01/10 20:54
djahandarieObviously that first example would be something trivial like Vec01/10 20:55
djahandarieLooking at Agda again it doesn't seem as foreign anymore01/10 20:57
danbrownhmm. -> appears to have precedence < 001/10 20:57
danbrownso it's magic01/10 20:58
copumpkinyeah01/10 20:58
copumpkinwhat's nicer? expressing a CCC as a record containing a category and simple properties about that category, or a record parametrized by a category containing the properties?01/10 22:45
copumpkinmaybe one of each, a bit like in the Algebra modules with Monoid and IsMonoid etc.01/10 22:56
--- Day changed Sat Oct 02 2010
copumpkinugh, agda's very stateful :(02/10 02:08
dolioYour mom is stateful.02/10 02:21
copumpkinindeed02/10 02:22
copumpkinI'm trying to make a fairly easy syntax highlighter for agda, using the API02/10 02:23
copumpkinexcept when I try to typecheck, I get *** Exception: An internal error has occurred. Please report this as a bug.02/10 02:24
copumpkinah, I might know what's wrong02/10 02:25
copumpkinfixed it, now I get a type error and don't think I should be02/10 02:34
copumpkinit's so picky about module names and file names02/10 02:55
Mathnerd314is there a program such that replacing each occurence of SetX with Set(X+n) would cause an error where none existed previously?02/10 03:04
dolioMathnerd314: There shouldn't be.02/10 03:29
copumpkinedwinb: you know tristan henderson?02/10 03:51
copumpkinthis has got to be the most annoying reason to fail02/10 04:24
copumpkin(TopLevelModuleName {moduleNameParts = ["ASDF"]},AbsolutePath {filePath = "/var/folders/cV/cVW7rvVqGDGhFxG2w5e4u++++TI/-Tmp-/ASDF.agda"},AbsolutePath {filePath = "/private/var/folders/cV/cVW7rvVqGDGhFxG2w5e4u++++TI/-Tmp-/ASDF.agda"})02/10 04:24
copumpkinsince /var is a symlink to /private/var02/10 04:24
copumpkinokay, putting it in a non-symlink folder made it work02/10 04:29
* copumpkin shakes fist02/10 04:29
djahandariecopumpkin, heh02/10 04:48
copumpkinyay, I succeeded02/10 05:01
jonrafkinda winner is you02/10 05:03
djahandarie\o/02/10 05:03
copumpkinnow I just need to give it a nice interface02/10 05:05
copumpkinand ideally remove the damn temporary file business02/10 05:05
copumpkinI wish agda didn't make so many assumptions that the source code is a file02/10 05:05
edwinbcopumpkin: yes, he works in the same department02/10 13:03
pumpkinedwinb: ah, he gave me a bad grade several years ago :P02/10 15:47
pumpkinbut I like him and I kind of deserved it :)02/10 15:49
edwinbpumpkin: heh. you don't forget these things ;)02/10 15:51
edwinbthis was at Dartmouth presumably?02/10 15:52
pumpkinyeah02/10 15:52
pumpkinman, O(0) indexing02/10 16:12
copumpkinso a .lagda file only supports the TeX formatting, not the > delimeter?02/10 20:23
copumpkinlooks like it02/10 20:25
--- Day changed Sun Oct 03 2010
dolioOoo, stevan's (I think) code should now termination check with record sigma.03/10 03:08
pumpkinwhat code is that?03/10 03:09
dolioThe regular types thing.03/10 03:09
pumpkinoh03/10 03:09
dolioWhere it was failing because 'foo (x , y) = ...' was translated into projections that weren't known to be smaller.03/10 03:10
dolioBut now the termination checker knows that projected fields are smaller than the record.03/10 03:10
pumpkinah I see03/10 03:12
Saizanoh, clever, they are not-bigger rather than smaller03/10 03:19
Saizanhttp://code.google.com/p/agda/issues/detail?id=334&can=1&start=30003/10 03:19
dolioWhy don't we want foo to check?03/10 03:22
Saizantry to normalize foo :)03/10 03:22
dolioYeah, I guess.03/10 03:24
dolioI'm not big on recursive records.03/10 03:24
dolioThe way they behave is actually like codata, so that would obviously fail to be productive.03/10 03:25
dolioBut presumably they're supposed to be inductive.03/10 03:25
dolioSo that type should be empty.03/10 03:26
SaizanR should be empty, not sure if we can prove R -> _|_ though03/10 03:28
dolioYou can for the data equivalent. It's just foo with a different type.03/10 03:28
Saizanyeah03/10 03:29
dolioI was thinking about syntaxes for codata the other day, though, like 'data Stream a = Head :: a & Tail :: Stream a'.03/10 03:30
dolioAnd when you try to imagine a more GADT-like syntax, it looks just like records.03/10 03:31
doliodata Foo <t> where03/10 03:31
Saizanyeah, charity is similar, you've to specify projections03/10 03:31
dolio  D1 :: Foo <t> -> <T>03/10 03:31
dolio  D2 :: (r : Foo <t>) -> <T> -- D1 r is usable here...03/10 03:32
dolioOr something like that.03/10 03:32
dolioAnd the eta rule that you get for records kind of gets you extensional equality via 1-step bisimulation.03/10 03:35
doliop = q iff D1 p = D1 q && D2 p = D2 q && ...03/10 03:36
dolioI don't know what they do for directly recursive records. You can eta expand those forever.03/10 03:37
dolioI guess they avoid eta expanding for performance reasons these days.03/10 03:38
Saizanthey do seem to make sense only if the recursive occurrence is wrapped in something without eta rules.03/10 03:40
dolioAlso, it made me think about: 'codata T : Set where'.03/10 03:42
dolioWhat is that? It looks like bottom.03/10 03:42
dolioBut, on further thought, it might be top.03/10 03:42
dolioana-T : {A : Set} -> A -> T03/10 03:43
dolioIn fact, I'm pretty sure it is.03/10 03:43
dolioSame as 'record T : Set where' is top.03/10 03:43
pumpkinhow would you "construct' it?03/10 03:44
pumpkinbut I can see why03/10 03:44
Saizanwhat is the shape functor there?03/10 03:44
dolioYou construct it by ana-T, which is primitive.03/10 03:44
pumpkinoh ok03/10 03:44
dolioI don't know how you'd do it in (old) Agda, though.03/10 03:45
dolioSaizan: I'm not sure. Const Bot, maybe.03/10 03:45
Saizanana : {A : Set} -> (A -> F A) -> A -> nu F, so if F = Const Bot you'd have to construct a (A -> Bot), no?03/10 03:47
dolioHmm...03/10 03:48
dolioI think I'm mixing my ideas here.03/10 03:49
dolioGiven my 'codata T where <destructors>', the shape would be Const Top.03/10 03:50
dolioBecause it's "no destructors."03/10 03:50
dolioBut that isn't how Agda used to be, so 'codata T : Set where' would have still been empty, I guess.03/10 03:51
dolioBecause the things underneath weren't destructors, but the things you could observe when you destructed values.03/10 03:51
dolioAnyhow, I think records are essentially non-recursive codata.03/10 03:55
Saizani wonder if it was provably empty03/10 03:55
dolioAnd recursive records are a good match for codata in general.03/10 03:55
dolioThat even explains the p <= proj p.03/10 03:58
dolioBecause projections out of codata aren't necessarily smaller.03/10 03:58
dolioEr, proj p <= p.03/10 04:00
Saizanthis makes me think we should introduce something similar in the productivity checker03/10 04:01
dolioIt would mean that NAD's example would be inhabited, though.03/10 04:01
dolioBut that his function is an inadmissable fold over the infinite inhabitant.03/10 04:02
Saizanwhich kind of makes sense03/10 04:03
dolioYeah.03/10 04:03
dolioI suspect that isn't provably uninhabited.03/10 04:04
dolioI guess I'll mention this on the bug report. People still get notified even if the bug is closed, right?03/10 04:05
Saizani think so03/10 04:06
dolioDone.03/10 04:32
dolioI even thought of another link.03/10 04:32
dolioThe initial implementation of codata had subject reduction problems when it was thought of as constructors.03/10 04:32
dolioRecords had issues with subject reduction when constructors were introduced for them.03/10 04:33
Saizanit seems "record List (A : Set) : Set where field uncons : Maybe (A, List A)" would also make sense as an inductive tough03/10 04:36
dolioLots of record definitions make sense as either inductive or coinductive.03/10 04:44
dolioAnything non-recursive.03/10 04:44
dolioMaybe records are the (a) Right Way to introduce codata, though.03/10 04:45
dolioProbably better than the old codata.03/10 04:45
dolioIt's hard for me to imagine 'record List (A : Set) : Set where uncons : Maybe (A x List A)' being superior to the data version as an inductive definition.03/10 04:47
copumpkinafter several hours of struggle: http://pumpkinpat.ch/moo.html03/10 04:49
dolioOnly several hours to coax it to highlight bits of code without type checking it and such?03/10 04:54
copumpkinoh no, it's typechecking and all03/10 04:55
copumpkin:P03/10 04:55
dolioOh. But it does bits of code now.03/10 04:55
copumpkinyeah, it's taking the chunks and pasting them together and maintaining the highlighting information that agda spits out03/10 04:55
copumpkinwithout treating non-code as comments03/10 04:55
copumpkinit also handles the literate style I prefer03/10 04:56
copumpkinwhich is the > prefix03/10 04:56
copumpkinrather than \begin{code}03/10 04:56
copumpkinwhich is the only one agda likes03/10 04:56
dolioWe're still a while away from hpaste highlighting agda, though, I guess.03/10 04:56
copumpkinyeah03/10 04:57
copumpkinit's still a way away from actually being satisfactory, too03/10 04:57
copumpkinI hate writing shit out to a file and then asking the compiler to read it back in03/10 04:57
copumpkinbut not doing that would've required a lot more duplication of code03/10 04:57
copumpkinand when I do that, I can easily just call the parser and do a bit of highlighting without typechecking03/10 04:58
copumpkinthen I can have a deep highlighter and a shallow one, and chrisdone might prefer the shallow one03/10 04:58
copumpkinbut for now I'm just happy to get anything out of it at all03/10 04:59
--- Day changed Mon Oct 04 2010
aRcatani'm solving the exercises in Ulf Norell's Dependently Typed Programming in Agda: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf04/10 17:48
aRcatani'm stuck in the exercise 2.3 a (pdf page 20), where you have to prove transitivity of the sublist relation04/10 17:49
aRcatani don't know even where to start04/10 17:49
copumpkinpattern match on the parameters :)04/10 17:57
copumpkinpattern matching will generally introduce new knowledge about your goal04/10 17:58
copumpkinso things like trans stop stop will be trivial04/10 17:58
copumpkinand then you'll encounter recursive cases for some of them04/10 17:59
copumpkinif that makes sense :)04/10 17:59
copumpkinaRcatan: to help you, write trans x y = ?04/10 17:59
copumpkinand then C-c C-c x04/10 17:59
copumpkinand it'll break the cases up for you04/10 17:59
aRcatanwhat does the red background mean?04/10 18:06
copumpkinit means your function might not terminate04/10 18:06
copumpkintypically you're calling a recursive case that is not obviously smaller than the original parameter04/10 18:07
aRcatanyeah04/10 18:07
copumpkinare you using C-c C-, btw?04/10 18:09
aRcatanno, but looks handy04/10 18:09
copumpkinthat's probably the single most useful command04/10 18:09
copumpkinat least for me04/10 18:10
aRcatani've been already thinking there should be something like that04/10 18:10
copumpkinso unless I have an idea of how to go about proving something, I'll just casesplit on parameters that look like they'll let agda evaluate my goal more04/10 18:10
copumpkinand then look at the goal and context of the holes04/10 18:10
copumpkinand see what I can make progress on04/10 18:10
copumpkinC-c C-r on an empty hole that can only be refined to one constructor/lambda/record will also do that for you04/10 18:11
copumpkinotherwise, if you write in a function name that would fit, it'll give you a hole for each of its arguments04/10 18:12
aRcatanhmm04/10 18:15
aRcatani think i figured this out, though i have to think about it a bit04/10 18:16
aRcatanthank you copumpkin!04/10 18:16
copumpkinno problem, feel free to ask more04/10 18:16
copumpkinis there any way to get agda to infer an implicit that could only possibly have one value given other types (but isn't just a record)04/10 20:41
copumpkinlike data Moo : Set -> Set where A : Moo Nat; B : Moo Fin04/10 20:42
copumpkinf : {x : Moo Fin} -> ...04/10 20:42
copumpkinseems like it should be possible04/10 20:43
dantenit seems similar to constructor headed functions: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments04/10 20:45
Mathnerd314is someone around who can explain why Type : Type is a bad idea?04/10 22:37
pumpkinhave you heard of russell's paradox?04/10 22:37
pumpkinit's a similar idea04/10 22:38
pumpkinI think the usual construction is girard's paradox, and Saizan wrote an implementation of it recently04/10 22:38
Mathnerd314IIRC from when I looked at before, my problem was that I couldn't find a description of girard's paradox.04/10 22:41
Mathnerd314there was this, but I couldn't understand it: http://www.cs.chalmers.se/~coquand/paradox.ps04/10 22:47
dolioDo a google search for Hurkens.agda04/10 22:48
pumpkinhttp://www.cse.chalmers.se/~ulfn/darcs/Agda2/test/succeed/Hurkens.agda04/10 22:49
pumpkinI thought Saizan had made a separate one04/10 22:49
pumpkinbut I can't find it in the logs04/10 22:49
pumpkinmaybe I imagined it04/10 22:49
Saizanpumpkin: i'm pretty sure i made one too04/10 23:00
Saizanhttp://code.haskell.org/~Saizan/TypeInType.agda <- here it is04/10 23:03
--- Day changed Tue Oct 05 2010
wireshi05/10 12:04
wiresCan, and if so, how does one combine local definitions ('let' or 'where') and a 'with-expression'? what is the syntax for it...?05/10 12:04
wiresOh i'm sorry, I see now, just write05/10 12:15
wiresfoo f x y with f x05/10 12:15
wires... | true = bar x05/10 12:15
wires... | false = bar y05/10 12:15
wires    where bar z = z + z05/10 12:15
wiresOh, no.. actually that doesn't work: bar is not in scope of the "true" part of this expression05/10 12:17
wiresOk, so.. concretely: this works,05/10 12:25
wiresfoo : {A : Set} → (A → Bool) → A → A → A05/10 12:25
wiresfoo f x y with f x05/10 12:25
wires... | true = bar1 x05/10 12:25
wires    where bar1 : {X : Set} → X → X05/10 12:25
wires          bar1 z = z05/10 12:25
wires... | false = bar2 y05/10 12:25
wires    where bar2 : {X : Set} → X → X05/10 12:25
wires          bar2 z = z05/10 12:25
wiresbut I want to avoid repeating the definition of bar105/10 12:25
wiresany ideas?05/10 12:25
wiresuse nested where?05/10 12:26
freikhello05/10 13:38
freiksenetI am going through Agda tutorial by Ulf Norell05/10 13:39
freiksenetI got to the first exercise and seemingly wrote a correct function to do that (at least it loads with no errors). Is there a way to "test" it somehow? Like is there a REPL for agda in emacs?05/10 13:40
wiresfreiksenet: you can type ctrl-c ctrl-n and then type an expression, this evaluates the expression05/10 13:41
wiresfreiksenet: i've also managed to open the ghci panel in emacs once, this gives you a fully interactive agda so it seems, but I cannot open it again05/10 13:41
* wires confused05/10 13:42
freiksenetwires: oh, C-c C-n works nice.05/10 13:42
freiksenetI didn't like emacs ghci tbh, unlike Common Lisp emacs repl (slime) it's not better than terminal one and is buggy :|05/10 13:43
wiresyeah. and in fact, ghci is just haskell I think, not agda.. but i know nothing, i'm just starting with agda aswel05/10 13:45
wiresas well05/10 13:45
freiksenetC-c C-n is just what i need05/10 13:46
wiresgreat :)05/10 13:46
freiksenetwhat is the reason to have implicit N in that exercise (a) if for practical use you have to apply it explicitely?05/10 13:46
freiksenetexercise = "Define a function to compute a vector containing n copies of an ele-05/10 13:46
freiksenetment x.05/10 13:46
wiresthis one?05/10 13:51
wiresvec : {n : Nat}{A : Set} -> A -> Vec A n05/10 13:51
wiresvec {n} x = {! !}05/10 13:51
freiksenetyeah05/10 13:51
freiksenetn is implicit, so you don't specify it _usually_05/10 13:51
wiresstrange, yeah, i don't know...05/10 13:51
freiksenetfor any real use you do vec 5 0, for example05/10 13:51
freiksenetoops05/10 13:51
freiksenetvec {5} 005/10 13:51
wiresright..05/10 13:51
wiresyeah it's not like agda can infer that you want 5 there05/10 13:52
freiksenetyeah05/10 13:52
freiksenethttps://gist.github.com/e6dadeae8dc98ce692e305/10 13:53
freiksenetsecond exercise05/10 13:53
freiksenetsecond clause says "unreachable clause"05/10 13:53
freiksenetoh05/10 13:53
freiksenetnm05/10 13:53
freiksenet:D05/10 13:53
freiksenetforgot that n is the same for both05/10 13:53
freiksenetis there a compose function in Agda? Like haskells .05/10 14:42
aRcatanfreiksenet: in the standard library in Function there's _∘_ (i hope my unicode comes through)05/10 14:46
freiksenetaRcatan: thanks05/10 14:47
stevanwires: i think the only way to avoid bar1 in both wheres is to move it out :-/, i usually put it into a private block above05/10 16:44
--- Day changed Wed Oct 06 2010
copumpkindamn, I missed stevan again06/10 01:02
glguy_Are [agda --html] and [agda --compile] broken now?06/10 02:36
dolioI used --html like 3 or 4 days ago.06/10 02:37
dolioWith an Agda built that day or so.06/10 02:37
glguy_They don't seem to know about BUILTIN INFINITY or syntax06/10 02:37
glguy_from the standard library06/10 02:37
dolioDid you make sure to recompile the agda executable when recompiling the rest? It's not automatic.06/10 02:38
dolioThat said, I wasn't using the INFINITY stuff.06/10 02:38
glguy_I just did "cabal install"06/10 02:38
copumpkinglguy_: what do you want to do with the bitvector stuff, by the way? should we send it to NAD and ask him to unicodify it suitably?06/10 02:38
glguy_I'm not sure he has bandwidth to deal with it at the moment06/10 02:39
dolioWhen you recompile the main Agda stuff, you have to also go into src/main and cabal install there.06/10 02:39
glguy_but we could ask him if he was interested06/10 02:39
dolioThat's what generates the agda executable.06/10 02:39
copumpkinglguy_: sure, want me to email him and maybe CC you? or do you want to do anything more to it before showing him?06/10 02:40
glguy_Emailing him would be fine now06/10 02:41
dolioglguy_: That hit me a while back, because I hadn't been rebuilding the Agda executable, and I ran to a situation where the updated positivity checker accepted something that the old one didn't.06/10 02:42
copumpkinglguy_: what should I CC it to?06/10 02:42
glguy_thanks, that fixed it06/10 02:42
* glguy wonders if it makes sense to move the IO type into the world of universe-polymorphism06/10 03:29
glguyhttp://www.galois.com/~emertens/IO.agda/IO.html#147906/10 03:29
glguyColist being universe polymorphic means that we can replace an old comment about sequence requiring a new Colist and replace it with the definition06/10 03:29
glguybut perhaps it makes sense for [data http://www.galois.com/~emertens/IO.agda/IO.html#842 : Set → Set₁ where] to become more general06/10 03:30
glguyoops06/10 03:30
glguybut perhaps it makes sense for [data IO : Set → Set₁ where] to become more general06/10 03:30
copumpkinwhat if I want to build a custom universe and write it to a file?! :P06/10 03:31
copumpkinglguy: it looks like your type would still lead to the "pile o' sharps"?06/10 03:32
glguy[IO AbstractType] appears in Haskell regularly06/10 03:32
glguycopumpkin: The "pile of sharps" type is the current state of the standard library06/10 03:32
copumpkinyeah06/10 03:32
copumpkinI know06/10 03:32
copumpkinmaybe a custom syntax could avoid some of that06/10 03:34
copumpkinhmm06/10 03:34
glguyYuck! Who is doing the graphics for Wikipedia's Agda article? CNN? http://en.wikipedia.org/wiki/Agda_(theorem_prover)06/10 04:16
DegenerateMonadlol06/10 04:17
DegenerateMonad"Agda 2 is similar to Epigram."06/10 04:18
DegenerateMonadwhat does that even mean?06/10 04:18
Saizanthat excerpt is so edgy.06/10 04:18
SaizanDegenerateMonad: i'd say it's quite dissimilar, actually06/10 04:19
DegenerateMonadwell, compared to C, it's similar to epigram06/10 04:19
DegenerateMonadit just doesn't mean anything much without qualifiers06/10 04:20
dolioChocolate is similar to vanilla.06/10 04:22
dolioThat picture is pretty great, too.06/10 04:22
dolio"trLn . unwords . ma" <-- excerpt of Haskell code.06/10 04:23
DegenerateMonadwhat should go in its place?06/10 04:23
* DegenerateMonad chuckles06/10 04:23
Saizanhttp://en.wikipedia.org/w/index.php?title=Agda_(theorem_prover)&diff=323790412&oldid=322618365 <- !06/10 04:26
dolioI forgot to mention that you should put your eyeball right up to the screen to look at that excerpt.06/10 04:28
dolioThe Haskell one, that is.06/10 04:28
copumpkingwern killed it and someone put it back?06/10 04:28
copumpkinoh, he put it back06/10 04:28
freiksenetit's just that I am stuck at c) at first exersive, the transpose one. I know how to do that, but for some reason it doesn't type check06/10 08:47
freiksenetI can't head the matrix for some reason :|06/10 08:47
glguyWhich exercises?06/10 08:47
glguy2007 summer school?06/10 08:47
freiksenetyeah06/10 08:47
freiksenethttps://gist.github.com/303137c4b81e6c2230b3 here is test code. even this fails for some reason06/10 08:48
glguyDo you have a link to the original problem?06/10 08:49
glguyI don't know what your Matrix type is06/10 08:49
freiksenetadded matrix there06/10 08:49
glguyWhat is the type of head and tail? I'm going to guess that they only work on non-zero indexes06/10 08:50
glguy(non-empty vectors)06/10 08:50
freiksenetthey are from standard library06/10 08:50
freiksenetoh.06/10 08:50
freiksenetyou are right06/10 08:50
freiksenetthey indeed work only on non zero stuff06/10 08:51
freiksenetglguy: thanks, I'll try to figure it out myself after that06/10 08:52
freiksenetis there any alternative to C-c C-n? Like a REPL propmt? It's _really_ annoying to have to do C-c C-n every time you want to test how something would work06/10 09:20
stevancopumpkin: sup? :-)06/10 10:00
doliostevan: Your bug got fixed.06/10 10:10
stevanwhich are you thinking of? termination with inductive product vs record?06/10 10:13
dolioCorrect.06/10 10:14
stevanyeah i saw :-)06/10 10:21
stevanalso saw your interesting observation regarding codata and recursive records06/10 10:21
dolioI guess Anton Setzer came up with most of/all my ideas before.06/10 10:28
dolioI'd even read his overview that he subsequently posted, but I hadn't made the connection with records.06/10 10:28
stevanthe slides from last aim?06/10 10:29
dolioYes.06/10 10:29
stevanyeah, same here06/10 10:29
dolioSometimes you have to stumble around on your own, I guess.06/10 10:31
stevanbtw, did you solve the nils vs nisse problem? :-)06/10 10:31
dolioOh, yeah, he sent me a message.06/10 10:31
dolioApparently his first name is Nils Anders, and Nisse is his nickname.06/10 10:31
stevanyeah, people with the name nils are often called nisse here. like william and bill, i guess :-)06/10 10:32
dolioI see.06/10 10:32
stevanhere's a question: using the IFix from the slicing it presentation (http://strictlypositive.org/slicing-jpgs/ , last slide or so)  how does the pattern functor for, say, Nat look like?06/10 10:39
stevani can't get the bits to fit together...06/10 10:40
dolioI haven't looked at this in a while...06/10 10:40
dolioActually, this looks a lot like epigram's IDesc.06/10 10:41
dolioExcept, trying to do it in Haskell/SHE?06/10 10:42
stevanis epigram's IDesc the same IDesc that is presented in the levitation paper?06/10 10:45
dolioShould be similar.06/10 10:45
dolioNow that I look, this stuff is simpler.06/10 10:45
stevanthe levitation IDesc doesn't have both I and O indices (as the slicing it version has?)06/10 10:47
Saizanit applies t to (Case ..), isn't that ill-typed?06/10 10:49
dolioWell, I don't think you'd ever see general indexed functors in the IDesc stuff.06/10 10:50
dolioIDesc is a language for describing indexed endofunctors.06/10 10:50
dolioSo the i is the same as the o.06/10 10:50
dolioI think that's right, at least.06/10 10:51
dolioMaybe if/when they add mu and nu to the language directly, that'll change.06/10 10:53
dolioI'm not sure I follow what all is going on toward the end.06/10 10:55
dolioBut, the pattern functor should look like K () :+: I, I think.06/10 10:57
dolioExcept that () has the wrong kind.06/10 10:57
dolioYou need an indexed unit type instead.06/10 10:57
dolioWhere'd I leave off?06/10 11:01
Saizandolio : You need an indexed unit type instead.06/10 11:02
dolioOh, wow.06/10 11:02
dolioI thought for sure that wouldn't have gotten through.06/10 11:02
pigworkerStrictly, it's I -> IDesc I which describes indexed endofunctors; O -> IDesc I would give you (I -> Set) -> (O -> Set)06/10 11:06
dolioOh right. IMu takes I -> IDesc I, right?06/10 11:07
pigworkeryep06/10 11:07
pigworkerIf we went with *small* indexing (which perhaps we should anyway), we could add mu, nu : (O : Set) -> (O -> IDesc (I + O)) -> IDesc I and get on with it.06/10 11:09
npouillardpigworker: I'm looking at the models for Desc, and I would like to know if the extra "const Unit" are only for the lisp-ish syntax? Idem for the 'ind× in the paper.06/10 12:41
stevanhere's something that seems to work atleast: http://hpaste.org/40394/g06/10 13:03
freiksenetI am kinda confused by Agda comparison functions. For instance I want to filter list of Nats to include only Nats < 3. But < doesn't return a boolean. How do I use comparison to return boolean?06/10 13:11
stevanuse _<=?_ from Data.Nat together with the floor function from Data.Nullary.Decidable06/10 13:13
freiksenetmm, no module data.nullary. Do you mean Relation.Nullary?06/10 13:15
stevanyes, sorry06/10 13:15
freiksenetthanks06/10 13:18
freiksenetuh, how is floor symbol printed?06/10 13:20
freiksenettyped*06/10 13:20
stevan\lfloor and \rfloor i think06/10 13:20
freiksenetthanks :)06/10 13:21
stevanthere is some keyboard combination, which is impossible to remember, which when triggered above a symbol explains how to input it... C-u C-x =   it says on the wiki...06/10 13:23
freiksenetah, ok. missed that.06/10 13:23
freiksenetwhy there is only less equal command?06/10 13:24
stevanyou mean why there isn't a _<?_ ?06/10 13:24
freiksenetfor example, _>?_06/10 13:25
freiksenetor06/10 13:25
freiksenetI know you can express everything with only le?, but still, wouldn't it be convinient to have all of them?06/10 13:25
stevansure06/10 13:26
stevannot used that often i guess06/10 13:27
freiksenet%)06/10 13:27
freiksenetit just feels weird06/10 13:28
pigworkernpouillard: yes, that's to comply with the right-nested nil-terminated tuple structure which elaboration relies on; in the indexed case, it's right-nested proof-terminated tuples...06/10 13:30
pumpkin_stevan: oh, I wanted to make a couple of comments on the CT lib06/10 13:31
* pumpkin_ tries to remember what they are06/10 13:31
pumpkin_oh okay, so in the exponential object you only have one half of the natural isomorphism representing curry/uncurry06/10 13:33
pumpkin_and as far as I could tell, Product seems more like AllBinaryProducts than Product06/10 13:33
stevanfeel free to improve things :-)06/10 13:39
pumpkin_okay, I was just reluctant to make api-breaking changes :)06/10 13:39
pumpkin_so far all I've done is add new modules06/10 13:39
pumpkin_(at least without warning you before)06/10 13:39
npouillardpigworker: so nothing deep, just a syntactic consistency.06/10 13:42
pigworkersure06/10 13:43
ccasinI thought I read somewhere about new features to make sure you don't inspect Levels in scary ways (like use them non-parametrically)06/10 16:58
ccasinDoes anyone else remember where I might have seen this, or did I just dream it06/10 16:58
stevanperhaps you are thinking of this: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=AIMXII.Notes  ?06/10 17:06
ccasinstevan: hmm, lots of interesting stuff there but I don't see discussion of why pattern matching on levels might be bad.  Am I missing it?06/10 17:10
stevannope, that's the only thing about UP posted recently, as far as i remember06/10 17:13
ccasinstevan: ok - thanks anyway!06/10 17:14
glguy306/10 19:17
glguyWhile getContents : IO Costring, does it make sense that getLine : IO String (as it won't return a string until a newline is detected)?06/10 19:18
Saizanyes, to me06/10 19:19
contrapumpkinno bitvector yet!06/10 20:16
--- Day changed Thu Oct 07 2010
glguy__What does [* Changed the type of _≡_ to ∀ {a} {A : Set a} → A → A → Set a.] this allow for?07/10 05:00
dolioIt's less impredicative, at least.07/10 05:01
glguy__What does that mean?07/10 05:02
Saizanit was -> Set before?07/10 05:02
glguy_yes07/10 05:02
glguy_-  data _≡_ {a} {A : Set a} (x : A) : A → Set where07/10 05:03
glguy_+  data _≡_ {a} {A : Set a} (x : A) : A → Set a where07/10 05:03
dolioglguy_: Impredicativity is when a type is defined by quantifying over (or something of the sort) the universe of types it belongs to.07/10 05:04
dolioOr some higher universe or type.07/10 05:04
Saizanso we've gone from possibly higher to equal :)07/10 05:05
dolioSo, Sets being indexed by Sets, or by types in Set(suc i) is arguably impredicative.07/10 05:05
dolioNo. A : Set a, so it's indexed by a type in Set a, not by Set a, or by a type in a universe higher than Set a.07/10 05:06
glguy_I guess it allows for the following simplification07/10 05:07
glguy_] hunk ./src/Data/Container.agda 24107/10 05:07
glguy_-x ∈ xs = ◇ (Lift ⟨∘⟩ _≡_ x) xs07/10 05:07
glguy_+x ∈ xs = ◇ (_≡_ x) xs07/10 05:07
copumpkinthe fewer lifts, the better!07/10 05:07
dolioIf A, B[x] : Set a, (x : A) -> B[x] : Set a, but (A : Set a) -> T[A] is at least Set (suc a).07/10 05:08
Saizanglobular sets?07/10 16:02
dolioSaizan: Studying n-Category theory?07/10 17:14
Saizandolio: just reading the Coinductive Families thread07/10 17:17
dolioThere was something about globular sets in there?07/10 17:18
SaizanThorsten Altenkirch mentions them07/10 17:19
dolioOh.07/10 17:21
dolioOkay, that makes sense.07/10 17:21
dolioGlobular sets are a way of defining infinity categories, as I recall.07/10 17:22
dolioMy guess would be that what he's talking about is 'data Globular : Set1 where wrap : (A : Set) -> (eqv : A -> A -> Globular) -> Globular'.07/10 17:23
dolioSo, a set with an equivalence where proofs are up to a further equivalence, and so on.07/10 17:24
Saizanuh07/10 17:27
Saizanhttp://hpaste.org/40437/eq <- anyhow i was thinking that it's a shame that test1 and test2 don't typecheck07/10 17:28
dolioIt is a shame.07/10 17:29
dolioThat's why we need extensional equality.07/10 17:29
Saizando we?07/10 17:29
dolioYes.07/10 17:30
Saizanbut if one translated pattern matching to an eliminator f and g would have the same code07/10 17:30
dolioYes, it's possible that would work out.07/10 17:30
Saizansame if we translate .. \:: \# .. to unfolding07/10 17:31
dolioThat depends on how you rewrite xs and ys.07/10 17:31
dolioYou could rewrite one to 'unfold (\x -> just (x, x)) 1' and the other to 'unfold (\x -> just (1, x)) 0', for instance.07/10 17:32
dolioThere are arbitrary choices involved.07/10 17:32
Saizanthat's true, but i'd expect desugaring to be injective07/10 17:33
Saizans/injective/deterministic/07/10 17:33
Saizanit wouldn't be as good as extensional equality07/10 17:33
dolioMaybe it uses the name it's being bound to to choose what to desugar to. :)07/10 17:33
Saizanheh, true, i'd also expect alpha-equivalence though :)07/10 17:34
dolioIt's also conceivable that we could get some kind of genuine embedding of the universal property in the language that wouldn't exactly be extensionality.07/10 17:40
dolioBut I'm not holding my breath.07/10 17:40
dolioInductive types aren't treated precisely intensionally, in the strictest sense of the term.07/10 17:41
dolioSince we have (1 + n) = suc n, when those are not identical expressions.07/10 17:41
dolioBut there's no way to get normal forms for coinductive types, and normal forms for lambda terms aren't good enough.07/10 17:44
dolioInductive types also have the advantage of a strong inductive eliminator, and there's no equivalent for coinductive types, to my knowledge.07/10 17:45
dolioNo known equivalent, that is.07/10 17:46
Saizanyeah, but with definitional/propositional splitted like in OTT there's still something to be gained from making the former nicer07/10 17:47
dolioSure.07/10 17:48
Saizanbtw, if one looks at category-extras there's a zoo of unfoldings as well as folds, so i guess anamorphisms don't cover all the productive definitions?07/10 17:51
dolioAnamorphisms are (I think) sufficient to define the others, similar to catamorphisms.07/10 17:52
dolioIf you don't care about performance.07/10 17:52
Saizanah07/10 17:53
dolioInductive eliminators are paramorphisms, though, and with the expected evaluation strategy, can do some stuff asymptotically more efficiently.07/10 17:54
dolioAnd the same is true for the dual of paramorphisms, whose name I always forget.07/10 17:54
doliopred = indNat 0 (\n _ -> n)07/10 17:55
dolioFor instance.07/10 17:55
dolioThat's O(1) pred, whereas it's O(n) with a catamorphism.07/10 17:55
dolioWith an anamorphism, suc is ultimately O(n) if you examine the whole thing, because you have to re-unfold the original numer.07/10 17:56
copumpkinhylo?07/10 17:57
dolioHylo is cata g . ana f.07/10 17:58
dolioI think the dual is apo.07/10 17:58
copumpkinoh okay07/10 17:58
dolioAnyhow, with apo you can write something like 'suc n = apo (\_ -> just (right n)) _'.07/10 18:00
dolioWhich would work how you'd expect the constructors in Agda to work.07/10 18:00
* dolio goes to get some lunch.07/10 18:02
* copumpkin goes to get some dinner07/10 18:03
pumpkinare there any systems that allow you to have custom "sorts"?07/10 21:09
pumpkinI guess I'm not sure what I even mean by that, so I'll retract the question07/10 21:11
byorgey_pumpkin: Omega?07/10 21:49
pumpkinwhy is the paper for that a .ps despite being from 2010?07/10 21:51
pumpkin:(07/10 21:51
byorgeywhat's wrong with .ps ?07/10 21:52
pumpkinit's more painful to deal with on an ipad07/10 21:52
pumpkin:P07/10 21:52
edwinbOmega? 2010?07/10 21:55
* edwinb wonders what he's missed...07/10 21:55
pumpkinI dunno, http://web.cecs.pdx.edu/~sheard/papers/ claims it's 201007/10 21:55
pumpkin(LangOfTheFuture.ps)07/10 21:55
edwinbthere was a 2010 release apparently07/10 21:55
edwinbbut i thought that paper was around 200407/10 21:55
pumpkinI wouldn't know :)07/10 21:55
Adamantpumpkin: like for their library sort function?07/10 21:57
Adamantor in more Agda'y terms07/10 21:57
pumpkinnah, I mean Set/Set1/Set2 etc.07/10 21:57
Adamantah07/10 21:57
pumpkincustom universes still live in those sorts07/10 21:57
pumpkinI was wondering what would happen if you could instantiate your universes directly, without an eval function07/10 21:57
pumpkinif that makes any sense07/10 21:58
* edwinb turns a paper into pdf, following @copumpkin's orders ;)07/10 21:58
pumpkinedwinb: hey, I put a big please on it!07/10 21:58
pumpkinbut thanks :)07/10 21:58
edwinbhmm, on second thouhgs, it's now 10Mb rather than 200k07/10 21:58
pumpkinwow07/10 21:58
edwinbmayeb I should go back to the source07/10 21:59
pumpkinoh yeah07/10 21:59
pumpkinthat's my main issue07/10 21:59
edwinbI wonder where the source is...07/10 21:59
pumpkinI can convert a .ps to a .pdf in mac os using standard tools07/10 21:59
pumpkinbut they tend to blow up07/10 21:59
edwinbit irritates me too. As does not including a BibTeX (but I don't do that either so I can't complain...)07/10 22:00
pumpkinif I were still an academic, I'd publish all my paper sources! :P07/10 22:00
pumpkinalthough I often put embarrassing comments in the .tex so maybe I'd strip that first07/10 22:00
edwinbyes, that'd be my problem too ;)07/10 22:01
edwinbhello realazthat ;)07/10 22:45
realazthathi ;)07/10 22:45
--- Day changed Fri Oct 08 2010
dolioHey, I found something besides category theory that takes silly amounts of memory/cpu.08/10 11:46
stevando tell08/10 12:00
dolioI thought maybe I could formalize the reasoning behind the halting diagonal argument without doing much real work.08/10 12:02
dolioBy making a module with a bunch of parameters specifying all the necessary stuff.08/10 12:02
dolioBut that ate up quite a lot of memory.08/10 12:02
dolioI mean, it was a lot of parameters, but still.08/10 12:03
stevandidn't Saizan do something like that?08/10 12:03
dolioHe has some kind of diagonal argument module.08/10 12:04
dolioI was going a little more Turing machine specific.08/10 12:04
dolioTalking about tapes, and machines, and halting and stuff.08/10 12:04
dolioAnd a couple ways of sticking machines together, and how such machines halt and so on.08/10 12:05
stevanok08/10 12:06
dolioI don't really like waiting 3 or 4 minutes each time I C-c C-l, though.08/10 12:06
stevanit would be interesting to take those slow checking examples and do some profiling...08/10 12:17
Saizanhttp://code.haskell.org/~Saizan/halting/CompModel.agda <- i did something a little more specific about the halting problem, still without talking about tapes and machines though08/10 15:35
--- Day changed Sat Oct 09 2010
Saizan"Cannot have both universe polymorphism and type in type." :\09/10 00:59
dolioWhy would you need both?09/10 01:30
Saizani'm in the middle of moving from the latter to the former, but i guess it wouldn't be that useful anyhow09/10 01:33
dolioAh.09/10 01:35
glguyUsually when I notice Agda's termination checker it is because of frustration09/10 20:41
glguybut today it is awe... I don't know how it can tell that this definition terminates :)09/10 20:41
Saizaneheh09/10 20:46
Saizanlink?09/10 20:46
glguyyeah, one moment09/10 20:48
glguyits uploading now09/10 20:55
glguyhttp://www.galois.com/~emertens/simplelang/simpleeval.html09/10 20:56
glguyI was impressed that the definition of "one" passed09/10 20:56
* glguy acknowledges that the name choice isn't great in this file09/10 20:57
Saizani'd guess the Term is getting smaller09/10 21:00
glguyThe new auto tactic stuff is pretty cool09/10 21:04
glguy(C-c C-a)09/10 21:04
Saizani tried it a few times but it didn't help09/10 21:07
glguylispy: Do you know about the standard library’s Data.Star?09/10 21:23
lispyglguy: nope09/10 21:24
lispyglguy: Why do you ask?09/10 21:24
glguyhttp://www.galois.com/~emertens/simplelang/Data.Star.html09/10 21:24
glguybecause you were asking about just such a type at one point09/10 21:24
lispyoh, type index composition09/10 21:25
lispyThat is interesting, although I have a bit of trouble following it in paces09/10 21:27
lispyplaces*09/10 21:27
* glguy tries to decide if he likes the new syntax for sigma types: ∀ t → Σ[ v ∶ Value ] t ⟶⋆ val v09/10 21:39
glguyas compared to   ∀ t → Σ Value λ v →  t ⟶⋆ val v09/10 21:41
* Saizan likes it09/10 21:42
glguyor I could avoid the issue (in this case) and go with  ∀ t → ∃ λ v → t ⟶⋆ val v09/10 21:42
glguyWe need a new type  ⊥-elim : {Whatever : Set} → .⊥ → Whatever09/10 22:22
glguyfor bot-elim09/10 22:22
glguyoh no... we need functions that are polymorphic in their argument relevance now!09/10 22:24
glguyso that compose can work09/10 22:24
glguyI’m having to change [ ⊥-elim ∘′ ¬p]  to [λ x → ⊥-elim (¬p x)]09/10 22:25
glguyand then we can redo contradiction : ∀ {p w} {P : Set p} {Whatever : Set w} →09/10 22:30
glguy                .P → .(¬ P) → Whatever09/10 22:30
--- Day changed Sun Oct 10 2010
glguyWhat am I doing wrong that allows “one” to be defined like it is? http://www.galois.com/~emertens/simplelang/simpleeval.html#510610/10 02:32
glguyand subsequently allows for http://www.galois.com/~emertens/simplelang/simpleeval.html#634210/10 02:33
glguyit seems that I don’t understand proof irrelevance..10/10 02:33
dolioIt's rather hard for me to see the problem.10/10 02:41
glguyanything : ∀ {t u} {W : Set} → t ⟶ u → W10/10 02:42
glguyanything v = contradiction (e-if-true {true}{true}) term10/10 02:42
glguyI haven’t posulated anything10/10 02:42
glguyhave I?10/10 02:42
glguyanything : (W : Set) → W10/10 02:42
glguyanything = contradiction (e-if-true {true}{true}) term10/10 02:42
glguy  ⊥-elim′ : ∀ {a} {Whatever : Set a} → .⊥ → Whatever10/10 02:45
glguy  ⊥-elim′ ()10/10 02:45
glguythis seems to be the source of my being able to do anything10/10 02:45
dolioThat type for ⊥ is somewhat dubious, but I don't have an easy example of it causing problems.10/10 02:47
dolio⊥ elimination, that is.10/10 02:47
glguyI’m trying to narrow the test case to report the bug10/10 02:51
dolioAnyhow, the problem is it not evaluating to true, or something?10/10 02:51
glguyThe problem is that the logic is unsound :)10/10 02:51
dolioWhat logic?10/10 02:52
glguyagda10/10 02:52
glguyI’ve written a function that produces absolutely any value for free without posulating anything10/10 02:52
dolioWhat is expr's type?10/10 02:53
glguy(if if true then false else true then true else false) ⇓ false10/10 02:53
glguybut that doesn’t matter. the type of “anything” is the concerning thing10/10 02:53
glguyanything : ∀ {a} (W : Set a) → W10/10 02:53
glguyanything = contradiction (e-if-true {true}{true}) term10/10 02:53
dolioWell, the projection 'proof' implicitly uses a postulate.10/10 02:57
dolioAlthough, it isn't currently implemented that way.10/10 02:57
glguybut you agree that I shouldn’t be able to write “anything” in agda?10/10 02:58
dolioThere should be 'postulate .irrelevant : {A : Set) -> .A -> A'.10/10 02:58
dolioAnd 'proof x' should evaluate to 'irrelevant _'.10/10 02:58
dolioYes, but I'm not certain if it's that axiom, or ⊥-elim′, or if it wouldn't be possible if irrelevant projections were implemented 'properly'.10/10 02:59
glguyI’m having trouble making it work with: term′ : (t : Term) → .(IsValue t) → Normal t10/10 02:59
glguyterm′ _ vv n = ⊥-elim′ (terminal vv n)10/10 02:59
glguyso it might be the “.proof” field that is breaking things10/10 02:59
dolioWhat if you postulate that 'irrelevant' axiom I mentioned?10/10 03:03
dolioAnd use 'terminal (irrelevant vv) n', I think.10/10 03:03
dolioActually, no, I don't think that should matter...10/10 03:04
glguyis it related to using record constructor pattern matching to access the field?10/10 03:12
glguyI guess for now I’ll redo my proofs without the irrelevance so that they prove something10/10 03:13
dolioglguy: Are you sure anything doesn't have unsolved metas?10/10 03:36
glguyyes10/10 03:36
glguyemacs shows :   Agda:Checked10/10 03:36
glguyand the --html output mode didn’t require a special flag10/10 03:36
glguyand no metas were listed10/10 03:36
dolioHmm...10/10 03:38
dolioOkay, so, with the record with irrelevant projections, there are no unsolved metas.10/10 03:42
dolioWhen I implement it manually with a datatype and that irrelevance axiom, there are unsolved metas.10/10 03:42
dolioSo, something about the irrelevant projections implementation is doing something bad.10/10 03:43
glguyso does that mean that it is inferring some .\bot values?10/10 03:43
dolioThe unsolved meta is actually unfillable.10/10 03:43
dolioIt has to have type 'Subset (if true then true else true) IsValue'.10/10 03:43
dolioWhich is empty.10/10 03:43
glguyright10/10 03:44
glguyWhat did you say that irrelevance function was, again?10/10 03:45
dolio.irrelevant : {A : Set} -> .A -> A10/10 03:45
glguyso when A is \bot10/10 03:45
glguyhmm, nvm10/10 03:45
dolioNow to see if I can make a simpler example...10/10 03:48
dolioHopefully it can be done with something like Bool and T.10/10 03:48
dolioOh, I bet it's just not bothering to infer the proof.10/10 03:50
dolioBecause it's irrelevant. :)10/10 03:50
dolioJust infer the first, non-irrelevant argument, and call it a day.10/10 03:50
dolioHah! Done.10/10 03:56
glguyYou’ve written the simple test case or patched the type-checker? :)10/10 03:58
dolioyes.10/10 03:58
glguygreat. let me know when I can pull10/10 03:59
dolioOh, I read that wrong. :)10/10 04:00
dolioI wrote a simple test case.10/10 04:00
glguywell, that’s still great!10/10 04:02
dolioI'll file a bug.10/10 04:07
dolioOh wait, I thought of something that might be even simpler...10/10 04:09
dolioHah, yep.10/10 04:13
glguydo share!10/10 04:14
doliorecord ○ (A : Set) : Set where field .inflate : A10/10 04:15
dolioevil A = ⊥-elimⁱ (inflate _)10/10 04:15
glguythat is simple10/10 04:16
glguyproofs just got easier10/10 04:16
dolioIndeed.10/10 04:16
doliohttp://code.google.com/p/agda/issues/detail?id=34710/10 04:26
cads_So, I would like to begin to model the category of finite sets in agda.10/10 12:35
cads_I know some haskell, but I'm not very up to date on programming with types.10/10 12:36
realazthatanyone here familiar with smt solvers, I'm a newbie and could use some help10/10 18:33
--- Day changed Mon Oct 11 2010
* glguy is using the auto-solver to evaluate simple lambda calculus expressions :)11/10 02:18
glguytest3 : Star _⟶_ (app (app and tru) fls) fls11/10 02:18
glguytest3 = e-app₁ e-appabs ◅ e-appabs ◅ e-app₁ e-appabs ◅ e-appabs ◅ ε11/10 02:18
glguyC-c C-r ,  C-c C-a, C-c C-a   solved this definition :)11/10 02:19
Saizannice11/10 02:19
* Phantom_Hoover throws the letter 'Q' into a privet bush.11/10 16:37
pumpkinhm11/10 16:38
Phantom_Hoover"Is it a proof-assistant based on intuitionistic type theory?" No, it isn't.11/10 16:47
pumpkinPhantom_Hoover: care to elaborate, or are you just trolling?11/10 16:48
Phantom_HooverWell, the fact that proofs are written directly as functions makes actually proving complex things... painful.11/10 16:48
pumpkinyeah, it can be11/10 16:49
pumpkinthings will improve though11/10 16:49
Phantom_HooverAnd I suspect that the design of the proof kernel will make it very hard to take theorems on its word alone.11/10 16:50
* pumpkin shrugs11/10 16:50
Phantom_HooverI mean, it doesn't use small-kernel design, does it11/10 16:50
Phantom_Hoover*?11/10 16:50
pumpkina de bruijn criterionist amongst us!11/10 16:50
pumpkin:P11/10 16:50
pumpkinno, it doesn't11/10 16:51
pumpkinPhantom_Hoover: so what brings you here?11/10 16:51
Phantom_HooverInitially, a desire to see if anyone got that reference.11/10 16:51
pumpkinnot me :)11/10 16:52
Phantom_HooverI think Agda has merit as an experiment in dependently-typed languages, but experimental design does not a proof assistant make.11/10 16:53
ccasinOh, I don't know11/10 16:55
ccasinsure, one shouldn't have too much confidence in its consistency11/10 16:56
ccasinbut it has certainly helped me do proofs11/10 16:56
pumpkinword-order inversion does not an unpretentious sentence make11/10 16:56
pumpkinPhantom_Hoover: yeah, people prove false in it all the time :)11/10 16:56
pumpkinwell, not all the time, but there's another example of it up on the bug tracker right now11/10 16:56
ccasinoooh , how does it go?11/10 16:56
pumpkinapparently it will happily infer the values of irrelevant record fields if you omit them from the record constructor11/10 16:57
dolioIt goes _11/10 16:57
pumpkinincluding a value of \bot, and then you can write a .\bot -> A \bot-elim11/10 16:57
pumpkinand pull it back out as anything you want11/10 16:57
ccasinso it must not be really inferring a value so much as assuming one exists11/10 16:58
pumpkinyeah11/10 16:59
dolioEta expansion is probably a factor, too.11/10 17:00
dolioSince it doesn't work for data.11/10 17:00
* benmachine reads \bot-elim as lambdabot-elim and wonders what pumpkin has planned for the poor thing11/10 17:38
npouillarddoes anyone have some information (the date) of the XIII AIM?11/10 22:14
stevanthe one that just was?11/10 22:17
stevansorry, misread11/10 22:17
npouillardno the next one11/10 22:17
npouillardJean Philippe Bernardy told it will be at Chalmers if I remember correctly11/10 22:19
stevanyay :-)11/10 22:19
--- Day changed Thu Oct 14 2010
Saizanso i guess you can't prove a == b from a \x c == b \x d ?14/10 00:59
dolioNot in any easy way, at least.14/10 01:02
dolioYou could with --injective-type-constructors.14/10 01:03
Saizanhow would that look?14/10 01:11
dolioI hadn't thought about it...14/10 01:11
Saizanmaybe i just have to pattern match14/10 01:13
Saizanyep14/10 01:14
pumpkinSaizan: cong proj\_1 ?14/10 05:35
pumpkinoh14/10 05:35
pumpkinthe type :)14/10 05:35
--- Day changed Fri Oct 15 2010
bo_I have installed the emacs agda-mode, and it appears that the files are loaded in emacs (various agda2-* variables are defined), but there is no agda menu and no commands work. what could be wrong?15/10 09:49
stevanbo_: hi, do you have haskell-mode in place?15/10 12:42
bo_stevan: excellent. thank you. did not know I needed that as well. it works now.15/10 18:48
--- Day changed Sun Oct 17 2010
Spockzdoes anyone have an idea how to get highlighting of the latex in literate agda files?17/10 11:26
Spockz(with emacs)17/10 11:26
stevanSpockz: hi, i think you have to switch between latex-mode and agda-mode (possibily not if highlightning is part of some minor latex mode?). on the haskell wiki there is a section describing how this can be done automatically: http://www.haskell.org/haskellwiki/Literate_programming#Multi-mode_support_in_Emacs , i haven't tried it tho.17/10 12:31
Spockzstevan: trying17/10 12:40
Spockzwoosh17/10 12:52
Spockzit works :)17/10 12:52
stevan:-)17/10 12:53
stevanadd it to the agda wiki perhaps?  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda17/10 12:54
Spockzyep17/10 12:57
Spockzmainly it's s/haskell/agda2 :P17/10 12:57
Spockzoh, but now agda mode is broken17/10 13:12
stevanhow so?17/10 13:13
Spockzctrl - c - ctrl l doesn't work anymore17/10 13:14
Spockzbecause I'm in latex mode17/10 13:14
stevanbut when you enter a code block it should switch to agda-mode?17/10 13:15
Spockzit should, but it doesn't17/10 13:15
stevanthen something must be wrong in the way you setup mmm-mode?17/10 13:19
Spockzhmm do you have it working for haskell? As I don't get it working for haskell either, when copying the emacs config from the site17/10 13:27
stevani don't, i can try tho17/10 13:29
Spockzif you would please :)17/10 13:29
Spockzmaybe the emacs config was for some older versions17/10 13:29
stevani got it to work for haskell, had to run "You can activate mmm-mode by running "M-x mmm-ify-by-class" in the buffer. Emacs will prompt you for the class to use, to which should answer literate-haskell-bird or literate-haskell-latex, respectively. " manually tho17/10 13:39
Spockzah yes so far17/10 13:42
stevani get an error in the ghci buffer when tryingt to do it for agda however17/10 13:51
Spockzghci buffer? Should that still be used then?17/10 13:56
stevanwhat do you mean?17/10 13:58
SpockzI'd expect that the agda buffer is being used?17/10 13:58
stevanagda communicates with emacs thru a ghci buffer17/10 13:59
Spockzah ok :)17/10 14:00
stevanhere's the problem, i think: http://hpaste.org/40642/s17/10 14:03
Spockzhmm17/10 14:17
stevani don't know enough about agda2-mode nor mmm-mode... you can ask on the mailing list perhaps, or just create a function which toggle between the two modes and bind it to some key and do the toggling manually? :-)17/10 14:33
Spockzstevan: I did the latter, through a context menu17/10 14:40
Spockzbut I'm using two editors now, it actually works better17/10 14:40
Spockzeditting the latex (slides) in one editor and the code on them in aquamacs :)17/10 14:40
stevanhow do you reload the file each switch?17/10 14:41
Spockzwith the auto-revert-mode17/10 14:46
stevanok :-)17/10 14:46
Spockzouch17/10 15:02
SpockzNot implemented: type checking of with application17/10 15:02
Watermindwhich material would you recommend as theoretical foundations for someone wishing to get into Agda?17/10 17:08
WatermindI know plenty of haskell, but might need some type theory in particular haven't worked much with dependent types17/10 17:08
SpockzWatermind: have a look at this page: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials17/10 17:12
Watermindany thank you Spockz17/10 17:12
wiresWatermind: I recommend following both the tutorial by bove+dybjer and by ulf norell side by side (found on the page Spockz mentioned)17/10 17:14
Watermindwires: yes, I am downloading both17/10 17:14
wiresWatermind: as for theory, you might want to check out "Martin-Löf's Type Theory" by Nordström, Petersson and Smith17/10 17:15
wireshttp://www.cs.chalmers.se/Cs/Research/Logic/book/17/10 17:15
wiresand this one, it's very old, but useful: http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf17/10 17:16
wiresPer Martin-Löf, Intuitionistic type theory. Napoli, Bibliopolis, 198417/10 17:16
wireswell... "very old"17/10 17:16
Watermindoh nice wires17/10 17:16
Watermindthank you17/10 17:16
Watermindby the way, the link for Dybjer's book is wrong, an 'e' is missing after cs17/10 17:17
WatermindI tried editing it but needs password...17/10 17:17
Spockzyes17/10 17:17
Spockzthat's why it says17/10 17:17
Spockzbroken link. paper is available http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=DA0EF204DFF20BDFAB1492F07D23867B?doi=10.1.1.140.968&rep=rep1&type=pdf17/10 17:17
WatermindSpockz: yes I found it already17/10 17:18
Watermindthank you17/10 17:18
Watermindthe broken link is almost fine... just a letter missing I think17/10 17:18
stevani think the wiki passwd is "agda".17/10 17:54
Spockzit is17/10 17:56
Watermindwould you recommend source tar ball, or hackage source package?17/10 18:26
SpockzI installed from hackage17/10 18:26
Watermindok thanks17/10 18:27
Watermindoh my... darcs is taking quite a while to get  agda...17/10 19:28
Watermindquick question... is   {A : Set} -> ...  the same as (A : Set) -> ...17/10 22:25
WatermindI've seen both notations early in the manual and seem to be denotationally equivalent17/10 22:26
Watermindor maybe I should just continue reading :P17/10 22:26
dolio{} means the argument is implicit.17/10 22:27
dolioid : {A : Set} -> A -> A ; id x = x17/10 22:27
Watermindah got it... sorry should have just continued reading, I've noticed implicit arguments are coming right after this...17/10 22:28
Watermindhaving trouble installing Agda...17/10 23:33
WatermindI have ghc 6.10.4 (the one available in the opensuse repositories)17/10 23:33
Watermindand Cabal-1.6.0.317/10 23:34
dolioYou might need one newer than that.17/10 23:34
Watermindwell it did complain about Cabal17/10 23:34
Watermindbut then I did cabal install cabal-install17/10 23:34
Watermindand now cabal -V says:  1.8.0.2 of the Cabal library17/10 23:35
Watermindbut when I try to install agda I still get:17/10 23:35
Saizanthe problem is the dependency on QuickCheck, which depends on ghc, constraining the choices for Cabal17/10 23:36
Watermindcabal: dependencies conflict: ghc-6.10.4 requires Cabal ==1.6.0.3 however Cabal-1.6.0.3 was excluded because Agda-2.2.8 requires Cabal >=1.8.0.2 && <1.917/10 23:36
Saizanghc the library, not ghc the compiler, btw17/10 23:36
SaizanWatermind: a solution is to cabal unpack Agda; cd Agda-2.2.8; cabal configure; cabal build; cabal install --only17/10 23:37
Saizanthe configure step will print a warning that you can ignore17/10 23:37
Watermindok thank you Saizan17/10 23:37
Saizanor you can upgrade to ghc-6.1217/10 23:37
WatermindSaizan: I was hoping for the repositories to be updated :S17/10 23:38
WatermindSaizan: that seemed to work but it doesn't seem installed yet...17/10 23:41
SaizanWatermind: ghc-pkg list Agda ?17/10 23:41
WatermindSaizan: I did cd src to try and finish it but ther eis no main here17/10 23:41
Watermind /usr/lib/ghc-6.10.4/./package.conf:    and     /home/jadrian/.ghc/i386-linux-6.10.4/package.conf:17/10 23:42
Saizanok, so it seems it's not installed, if there was no line saying Agda17/10 23:43
Watermindshould I have done this has root? I thought this would just do a local installation17/10 23:43
Watermindthere was no error msg so I thought it would be fine17/10 23:44
Saizanno, you don't need to do it at root17/10 23:44
SaizanWatermind: can you paste the log of what you did to a pastebin?17/10 23:44
Saizane.g. pastebin.com17/10 23:44
WatermindSaizan: well I just pasted that line you gave me...17/10 23:44
SaizanWatermind: yeah, but i'd like to see the output :)17/10 23:45
Watermind2sorry internet connection :S17/10 23:49
Watermind2Saizan: http://pastebin.com/2DS1rqg817/10 23:49
Watermind2just noticed it complained about lacking a configure17/10 23:49
Saizanconfigure failed with "cabal: At least the following dependencies are missing: .."17/10 23:50
Saizanso the rest couldn't work17/10 23:50
Watermind2yes17/10 23:50
Watermind2but I thought that was the warning you mentioned that could be ignored17/10 23:51
Watermind2seems like I really need ghc 6.1217/10 23:51
Saizanah, sorry, no, the warning would be another one17/10 23:51
Saizanyou can probably progress further if you first run cabal install "QuickCheck >=2.1.0.2 && <2.2"17/10 23:52
Saizan(and the warning explicitly says it's a warning)17/10 23:52
Watermind2it did go further but stopped with an error cabal: Error: Could not find module: Agda.Main with any suffix: ["hi"] in the17/10 23:54
Watermind2search path: ["dist/build"]17/10 23:54
Saizanafter installing QuickCheck you need to rerun both "cabal configure" and "cabal build" before "cabal install --only"17/10 23:55
Watermind2ohh so maybe that's why it also still complains about my cabal verison even though I updated it17/10 23:56
Saizanno17/10 23:56
Watermind2nah still crashes with the same error... I also get a warning saying it might not work since Agda depends on multiple versions of cabal17/10 23:57
Saizanthat's because the dependencies force it to use two Cabal versions at the same time, and that can often cause build errors, not now though17/10 23:57
Watermind21.6 for ghc 6.10  and  1.8 for Agda 2.2.817/10 23:58
Saizanit still complains about QuickCheck?17/10 23:58
Watermind2nope not anymore17/10 23:58
Saizanso which error?17/10 23:58
Saizananyhow, with ghc-6.12 it should work out of the box, so it's probably easier to go that route17/10 23:58
Watermind2same as above...      cabal: Error: Could not find module: Agda.Main with any suffix: ["hi"] in the search path: ["dist/build"]17/10 23:59
--- Day changed Mon Oct 18 2010
Watermind2going to try on the source package instead of the hackage one18/10 00:00
Watermind2same thing18/10 00:01
SaizanWatermind2: what happens when you do "cabal build"? can you paste that log?18/10 00:01
Watermind2Saizan: http://pastebin.com/W3H8hX1D18/10 00:02
Saizanok, that's an error18/10 00:03
Watermind2and cabal build: http://pastebin.com/F4TjSMCZ18/10 00:03
Watermind2I mean cabal install18/10 00:03
Saizanunsupported extension: TupleSections <- means building failed, it requires an extension that's available only in ghc-6.1218/10 00:04
Watermind2oh well18/10 00:04
Saizansorry, i thought 2.2.6 still supported 6.1018/10 00:05
Watermind2I'll just get ghc 6.12 tehn18/10 00:05
Saizan*2.2.818/10 00:05
Watermind2Saizan: no worries thanks for all the tips18/10 00:05
Watermind2I'll get this running tomorrow18/10 00:05
Watermind2see you18/10 00:05
Saizancheers18/10 00:05
--- Log closed Tue Oct 19 10:49:34 2010
--- Log opened Tue Oct 19 10:49:41 2010
-!- Irssi: #agda: Total of 35 nicks [0 ops, 0 halfops, 0 voices, 35 normal]19/10 10:49
!barjavel.freenode.net [freenode-info] if you're at a conference and other people are having trouble connecting, please mention it to staff: http://freenode.net/faq.shtml#gettinghelp19/10 10:49
-!- Irssi: Join to #agda was synced in 82 secs19/10 10:50
--- Day changed Wed Oct 20 2010
st__hi20/10 15:19
Saizanhi20/10 15:19
st__I am a newbe and trying to write a simple hello world in agda20/10 15:20
Saizanhaving problems?20/10 15:20
st__I would like to execute plus (suc zero) (suc zero) and get a result20/10 15:21
Saizanif you're using the emacs mode you can use C-c C-n to get an expression normalized20/10 15:22
st__I get the following error when loading:  Missing type signature for left hand side plus (suc zero) (suc20/10 15:24
st__zero)20/10 15:24
st__thank you for providing help ... i am sitting at this for hours ;-)20/10 15:24
Saizanyou don't write the expression in the file, you load the module with the definition of plus, then C-c C-n and give "plus (suc zero) (suc zero)" when prompted for an expression20/10 15:25
Saizanyou could also have something like "test =  plus (suc zero) (suc zero)" in the file, so you just have to give "test" to C-c C-n20/10 15:26
st__WOW, I made it. thank you, that was the missing peace20/10 15:28
Saizangreat :)20/10 15:28
stevanhi, i don't like this: http://hpaste.org/40715/s  could someone explain why this is the case?20/10 17:07
ccasinare you curious about the reasons for positivity checking in general, or the reason this example fails the positivity checker?20/10 17:17
stevanit seems the positivity checker doesn't care about eta, yes?20/10 17:17
ccasinhow do you mean?20/10 17:19
stevanwell the only difference between the working and non-working version of [[_]] is a eta step?20/10 17:19
ccasinsorry, I didn't read your example carefully enough20/10 17:20
ccasinso using the first definition will pass the positivity checker?20/10 17:20
stevanyes20/10 17:20
ccasinyeah, OK, it seems the checker just isn't being smart enough20/10 17:21
stevanthis works also: http://hpaste.org/paste/40715/s#p4071620/10 17:21
ccasinI'd report it (though I also wouldn't be terribly surprised if someone on the list had a good reason for it)20/10 17:21
stevanit seems const is the function causing it, replacing it with \_ -> a makes it work20/10 17:22
ccasinyeah, it's just not unfolding id enough20/10 17:22
ccasinor, const20/10 17:23
stevanid is fine actually, const is the bad guy20/10 17:23
ccasinweird20/10 17:23
stevanhmm, if const x y = x rather than const x = \_ -> x (as in the stdlib) then it also works20/10 17:27
wiresHas anyone ever gotten emacs multi mode (mmm-mode) to work with literal agda?20/10 20:50
cadsWhat is "Hello, world!" when written in Adga?20/10 22:56
cadsAgda*20/10 22:56
pumpkinhmm20/10 22:56
pumpkinwe don't talk about IO around these here parts20/10 22:56
pumpkinbegone!20/10 22:56
pumpkin:)20/10 22:56
pumpkinbut you do have a binding to standard haskell IO functions in the standard library20/10 22:57
cadsFor example, the recursive version of the fibonacci function or the factorial function are commonly given as "hello world" in haskell :)20/10 22:57
pumpkinoh okay20/10 22:57
cadsHello world in ruby is often a webapp ;)20/10 22:57
pumpkinin that case I'd say it's probably something to do with sized vectors ;)20/10 22:57
cadsDependently typed vectors and functions on them?20/10 22:58
pumpkinyeah, probably with some Fin thrown in for indexing and stuff20/10 22:59
pumpkinalthough you can do most of that less elegantly in haskell20/10 22:59
cadsIt's actually the first kind of example I thought of which needed anything like dependent typing.20/10 22:59
cadsI guess in systems where IO is easy it's natural to want to make the machine say "hello"20/10 23:00
cadswhereas in haskell you're really itching to do something recursive20/10 23:01
cadsand in agda I'd itch to do something haskell can't easily do20/10 23:01
pumpkinthe nice thing about the sized vectors is that most of the definitions of functions are identical to those on lists20/10 23:01
pumpkinit's also an unnice thing20/10 23:01
pumpkinsince you're repeating code, which is why I hope much interesting work comes from the work pigworker was doing in that blog post a while back20/10 23:02
cadsWhat is he trying to accomplish?20/10 23:03
pumpkinhe's noting the similarity/deep connection between peano naturals, lists, and sized vectors (and various other variations on the theme)20/10 23:04
pumpkinand how lists are embellished forms of natural numbers, that carry additional information20/10 23:04
pumpkinso the length of a list is a natural characteristic that arises from that20/10 23:04
pumpkinand you get list append magically from nat addition (and probably a free proof that the length of the appended list is the sum of the lengths)20/10 23:05
pumpkinand also that sized vectors embellish the type of lists with their nat length20/10 23:05
pumpkinstuff like that20/10 23:05
cadsHmm, it seems like a list is a function from a von neumann ordinal to a certain domain.20/10 23:05
cadsOr can be seen as that20/10 23:05
cadscan you link me to his post?20/10 23:05
pumpkinwell, in agda and most dependently typed languages, lists are finite20/10 23:06
pumpkinyou can also see the Dec type for decidable predicates as an embellished Bool20/10 23:06
cadsyeah, I should say countable ordinals20/10 23:06
cadsgrrr20/10 23:06
cadsfinite.20/10 23:06
pumpkinhttp://www.e-pig.org/epilogue/?p=57720/10 23:06
cadsHeh20/10 23:09
cadswith posts like these I feel I have to look up a paper that introduces each term I read, or else have no hope of understanding a thing20/10 23:10
cadsWhat are sigma types?20/10 23:10
pumpkina dependent pair20/10 23:10
pumpkinlike (,) in haskell, but the type of the snd depends on the value of the fst20/10 23:10
pumpkin(can also be seen as existentials)20/10 23:10
pumpkin(pi types are the same idea on functions, where the type of the codomain depends on the input value)20/10 23:11
pumpkinthose two are the basic two ingredients for a dependent type system20/10 23:11
pumpkinyou can make Either (regular sums) out of a Sigma type, and you can make (,) out of a Sigma type or a Pi type20/10 23:12
cadsCan we express a Pi type in terms of a set of dependent pairs?20/10 23:12
pumpkina potentially infinite set of them20/10 23:13
cadssure20/10 23:13
Saizanthat is sort of why it's called Pi, it's a large product20/10 23:14
pumpkinSigma has the same relationship with Pi as (,) has to (->)20/10 23:14
cadsSaizan, that's why I thought of it - I wondered if there was an analogy there.20/10 23:15
pumpkinSigma for Sum, P for Product20/10 23:15
pumpkinPi20/10 23:15
pumpkinbut those terms are awfully confusing20/10 23:15
wiresyo, i've managed literate agda multi mode in aquamacs, yay http://agda.posterous.com/literate-agda-and-emacs-multimode20/10 23:16
wiresmeh, posterous screwed the markup...20/10 23:17
pumpkinspeaking of markup, I should clean up and release my agda highlighting code at some point20/10 23:17
cadsHaha, wires, there are no screenshots20/10 23:18
cadsis this to tempt us to follow the instructions to see for ourselves?20/10 23:18
cads(it is having this effect!)20/10 23:18
wirespumpkin: ya, that looked great20/10 23:18
wiresalright.. let me drop in a screencast ?20/10 23:18
pumpkinany ideas how I can force fixed-width on unicode characters? http://pumpkinpat.ch/moo.html20/10 23:19
wireslol.. no just kidding, let me work on my talk first20/10 23:19
cadswires, I'm gonna follow the recipe and see what comes out :)20/10 23:19
wirespumpkin: drop 'm in a pre block?20/10 23:19
pumpkinwires: it already is in one :P20/10 23:19
wirespumpkin: guess that doesn't work20/10 23:19
wiresya..20/10 23:19
wiresdamn, no idea; wrap each char in a div and size that... lol j/k20/10 23:20
wirescads: cool, let me know. there is this annoying issues with highlighting disappearing when you switch modes20/10 23:21
wirescads: and it seems quite heavy on cpu. Mind you I know next-to-nothing about emacs :)20/10 23:21
pumpkinwires: ugh :P I'll consider it though20/10 23:22
wirespumpkin: no, no, i was kidding. That's sick, although it should work.20/10 23:23
cadscopumpkin, can we break down the line "data Desc (I : Set) : Set1 where"? This seems like a datatype declaration like in haskell. But I don't understand what the Desc constructor does.20/10 23:24
cadsTell me if this is right.20/10 23:24
pumpkinit is just like a datatype declaration in haskell20/10 23:25
cadsDesc (I : Set) is a description of some set I, and its type is some finitely ramified type of set, Set1?20/10 23:25
pumpkinoh nope20/10 23:25
cads:)20/10 23:26
pumpkinDesc is a type constructor that takes a parameter (like data Desc i = ...) of type Set (like * in haskell), and the resulting datatype lives in Set120/10 23:26
pumpkinso you could have Desc Bool20/10 23:26
pumpkinor Desc Int20/10 23:26
pumpkinSet1 is the type of Set20/10 23:26
cadsWould it automatically know how to take Bool or Int parameters and represent that as an object in Set1?20/10 23:28
wirespumpkin: actually.. I think the problem is that your character spacing is to small20/10 23:28
cadsOh20/10 23:28
pumpkinwires: oh, maybe20/10 23:29
wirespumpkin:  ⇒ for instance is wider than a single char, and this pushes the rest of the line forward20/10 23:29
pumpkincads: that's just the type of the data. It's basically saying that Desc : Set -> Set1 (but that means something slightly different when written that way)20/10 23:29
cadsDoes the second line "say : I -> Desc I" show that we must define a function which gives a Desc of a parameter?20/10 23:30
pumpkinit's just like GADT syntax at that point20/10 23:30
pumpkindata Desc i where Say : i -> Desc i20/10 23:30
pumpkinin haskell syntax20/10 23:30
pumpkinwell, with ::20/10 23:30
pumpkinwires: let me try adjusting the css20/10 23:31
Saizancads: in Agda constructors are not required to start with an uppercase letter20/10 23:31
pumpkinwires: doesn't seem to fix it, at least using letter-spacing :/20/10 23:33
pumpkinoh, letter-spacing isn't what I want20/10 23:33
wiresno you want something else... kerning?20/10 23:33
pumpkinletter-spacing is similar to kerning, but what I really want is a fixed width for each character box, which I don't think is a property20/10 23:34
wiresyeah.. i was looking it up and you are right20/10 23:35
wiresi think20/10 23:35
wires:)20/10 23:35
wiresso.. put each char in boxes then :)20/10 23:35
cadsSaizan, I'm not familiar enough with haskell's higher level type stuff to really draw very much insight or confusion from what I already know.20/10 23:35
cadshehe, which may be a blessing, but more likely a curse20/10 23:36
pumpkinwires: ick20/10 23:37
pumpkincads: well, think of say as a constructor20/10 23:37
pumpkindata Desc i = Say i | ...20/10 23:37
pumpkindata Desc i = Say i | forall s. Sg (s -> Desc i) | Ask i (Desc i)20/10 23:39
cadsDamnit, dude. That should make sense to me.20/10 23:42
cadsI'm embarrassed with my haskell.20/10 23:42
cadsI don't even know how the existential type works, formally or practically.20/10 23:43
pumpkindata Moo = forall s. Moo s20/10 23:45
pumpkinthat means you can write20/10 23:45
pumpkinMoo 120/10 23:45
pumpkinor Moo True20/10 23:45
pumpkinor Moo [True, False]20/10 23:45
pumpkinthe constructor works "forall" parameters, but it always just gives you a Moo type in return20/10 23:45
pumpkinwhich means you can never pull anything out of it20/10 23:45
cadsAh20/10 23:45
pumpkinin agda in general you can pull knowledge of an existential out20/10 23:46
pumpkinbut in this case it's basically equivalent to haskell20/10 23:46
pumpkincause you can't pattern match on types20/10 23:46
cadswould you be able to pull data out of the existential type 'forall s. Sg (s -> Desc i)'?20/10 23:47
cadsin haskell, that is20/10 23:47
Saizanin haskell it'd be hard20/10 23:48
Saizanbecause haskell has what are called weak existentials, so you immediately forget what 's' is, even if you know the definition20/10 23:49
cadsokay. lemme try to understand what this thing is saying. We have that 'forall s. Sg (s -> Desc i)' must be one of the kinds of Desc i  for a parameter i. For any function from any s to Desc i, it can apply the Sg constructor to make this discription. The Sg constructor somehow makes a dependent pair?20/10 23:52
cadsThis is where I lose the line of reasoning. I don't know how exactly Sg makes a dependent pair, or if that's even what it does, and I am not sure how how whatever Sg makes stands in as equivalent to plain Say i.20/10 23:52
cadsThere, I tried to describe my thoughts as accurately as I could.. it reads like a mess though :)20/10 23:54
Saizanin the blog post there's both the sg data-constructor for Desc and the Sg type constructor20/10 23:54
wirescads: added screenshots :) http://agda.posterous.com/literate-agda-and-emacs-multimode20/10 23:54
Saizanso let's stick to lowercase for the data constructor20/10 23:54
cadsI swear, I should stop trying to beat this into my brain and find an article that introduces the thing from the tiniest building blocks20/10 23:54
Saizanan agda tutorial could help :)20/10 23:55
Saizananyhow, sg's type is isomorphic to "Sg Set (\S -> S -> Desc I) -> Desc I" which would basically be the uncurried version20/10 23:56
Saizanso it's unique field would be a dependent pair20/10 23:57
Saizans/it's/its/20/10 23:57
Saizanin addition to that [_] interprets sg as the description of a Sigma type :)20/10 23:57
Saizanso i guess it can get a bit muddy there20/10 23:57
Saizancads: have you followed any of the Agda tutorials, btw?20/10 23:58
cadshaven't been able to yet20/10 23:58
cadsI think I always got into deeper water than I knew how to swim in when I tried before20/10 23:58
--- Day changed Thu Oct 21 2010
cadsSaizan, I feel like pokoko here, constantly looking for some article that'll present things in a unified, englightening way that'll let me understand it without work21/10 00:00
cadsOkay. I will read Ulf Norell's tutorial.21/10 00:01
cads(if this is the most highly suggested one)21/10 00:02
Saizan(i think so)21/10 00:02
* Saizan doesn't remember from where he learned Agda21/10 00:04
Saizanjust that it got much easier once i learned how computation interacted with type checking21/10 00:05
cadsWhere did that specific insight come from? Something you just picked up?21/10 00:07
cadsOr was it something formal?21/10 00:07
Saizana bit from playing with the emacs mode, and a bit from seeing how the typechecking rules define equality for types: it normalizes both sides and then check for equality modulo alpha-equivalence21/10 00:10
Saizanwhich often means that you need to do case analysis just to make some function in your type compute further, since evaluation has to stop when it hits a case expression over a free variable21/10 00:13
Saizan(nvm that Agda doesn't have case expressions :)21/10 00:13
cads:)21/10 00:18
cadsI think I can dig playing around in emacs mode21/10 00:18
cadsOkay, once more I've worked my courage up.21/10 00:19
cadsIt's really interesting how sometimes you can try to learn something and flat out fail again and again.21/10 00:20
cadssometimes an epiphany leads to natural understanding, but usually it's a long process of building up to understand even the most basic terms of what you're learning21/10 00:22
cadsI wasn't comfortable with predicate calculus and boolean algebra comfortably until I made the connection with set algebras and was able to speak boolean algebra in terms of sets and venn diagrams.21/10 00:24
cadsHooray for half finished line editing.21/10 00:25
Saizanyeah, and it's quite good for probability theory too21/10 00:26
Saizananyhow, Cale likes to repeat that if you are not feeling confused you're not learning fast enough, so.. :)21/10 00:26
cadsSaizan, that's another example where the set algebra formalism really helped me get things21/10 00:26
cadsHmm.21/10 00:30
cadsI think I need to find a paper that uses sets or categories as a foundation to jam out a dependently typed theory.21/10 00:30
cadsSaizan, that's a good saying21/10 00:31
Saizanmy personal view of dep. typed theory is very syntactic, but i was raised as a logician21/10 00:39
pumpkinsorry, back21/10 00:41
pumpkinhas anyone thought about what laziness would mean in the presence of dependent types21/10 00:42
pumpkinwould proj\_2 force proj\_1 on a Sigma?21/10 00:43
pumpkinI know that since it's total the end effect is the same21/10 00:43
pumpkinbut just in terms of efficiency21/10 00:43
dolioAgda's evaluation is lazy-ish.21/10 00:44
Saizanwhen you normalize a term, do you also have to normalize the type?21/10 00:44
pumpkinwires: looks nice!21/10 00:44
Saizaneta-laws are type directed..21/10 00:45
pumpkinwires: feel like hacking the >-style literate agda into agda?21/10 00:45
pumpkin:P21/10 00:45
dolioYou only have to normalize types when checking equality.21/10 00:45
wiresyou mean like, take a markdown file or something and use > at beginning of line to start agda blocks?21/10 00:45
dolioAlthough, I don't know how that figures into Agda, since it does unification.21/10 00:46
pumpkinwires: well, literate haskell supports "> " as a prefix to each line as a literate code delimiter21/10 00:46
pumpkinwires: agda only supports the latex-style literate code21/10 00:46
wiresBird style it's called i think?21/10 00:46
wiresbut I shouldn't be hard, I'll look into it tomorrow.21/10 00:47
wiresI = it21/10 00:47
wiresps. I've also emailed a buddy who's deep into typing, the font kind, regarding your spacing issue21/10 00:48
wiresI'm going to bed now, cheers21/10 00:48
pumpkinoh cool, thanks21/10 00:48
pumpkinI support bird-style indirectly in my library, but it's ugly21/10 00:48
pumpkin(for highlighting only)21/10 00:48
stevanhi, i don't get why this piece has inference problems: http://hpaste.org/paste/40740/s#p40741   presumably something with irrelevance, but what exactly? thanks.21/10 13:40
stevan(the rest of the code: http://web.student.chalmers.se/~stevan/ctfp/html/Category.Categories.Alg.html )21/10 13:46
stevani'm trying to think of recent changes to irrelevance...21/10 13:49
doliostevan: See http://code.google.com/p/agda/issues/detail?id=35121/10 18:23
dolioAnd its links to other bugs.21/10 18:23
dolioIt's an eventual result of the bug that allowed proving false.21/10 18:23
dolioOr, the fixes to that bug.21/10 18:24
stevanah, thanks!21/10 23:40
--- Day changed Fri Oct 22 2010
st__hi22/10 18:28
st__Would it be possible to do a normalization in agda in parallel, e.g. on multiple computers at once?22/10 18:29
st__Agda would be used as a programming language and currently I am thinking about the performance of agda programs22/10 18:30
--- Day changed Sat Oct 23 2010
harulfI'm pretty much entirely new to agda and am trying to get it to work by ssh:ing to the chalmers computers and opening the .agda file in emacs, but I can't figure out how to activate agda-mode... how do you do that? or is that not installed on the computers?23/10 00:16
Saizanharulf: is there an agda-mode executable there?23/10 00:18
Saizansince "agda-mode setup" is how you normally activate it23/10 00:20
harulfit doesn't seem like there is23/10 00:20
harulfrunning agda-mode setup just tells me that it can't find the command23/10 00:20
harulfand asking cabal to install the agda-executable fails23/10 00:20
Saizanyou don't need agda-executable for the emacs mode23/10 00:22
harulfthen what do I need?23/10 00:22
Saizananyhow, have you seen these? http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.README-2-2-8 , though if you have ghc-6.10 there you probably want to use Agda-2.2.623/10 00:23
harulfhmm23/10 00:23
Saizanyou need the Agda haskell library + the .el files23/10 00:23
Saizanwhich are usually installed by the package Agda23/10 00:23
harulfI'll try that23/10 00:24
harulfthanks23/10 00:24
wiresharulf: can you run agda-mode on the CLI (i.e. outside emacs?)23/10 00:26
harulfwires: nope. it doesn't find it23/10 00:27
wirestry "locate agda-mode" ?23/10 00:28
Saizanyou could also check if "ghc-pkg list Agda" shows an Agda-<ver> package23/10 00:28
harulflocate didn't find anything23/10 00:31
wiresAnd Saizan's suggestion?23/10 00:31
harulfI get two packages23/10 00:31
harulfneither has agda in the title, though23/10 00:31
wires? i guess you get no packages, but two lines ending package.conf.d23/10 00:33
harulfyeah, exactly23/10 00:33
wiresyeah, so agda-mode is not installed :)23/10 00:33
Saizannor the Agda lib23/10 00:33
harulfmm23/10 00:33
wiresyou can install locally using cabal, for instance see here http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.MacOSX after "Installing Agda is much easier with Cabal."23/10 00:34
wiresi know this is for mac, but should work equally on unix machines also23/10 00:35
wiresIf you are on a wintendo machine, don't ask me ;)23/10 00:35
harulfI'll try that too23/10 00:38
wiresgood luck23/10 00:38
Saizanexcept you should never do "sudo cabal install"23/10 00:39
wiresgood point23/10 00:40
wirespumpkin: yo, regarding your unicode-monospacing issues23/10 00:40
Saizanthe guide i linked above should be enough if you already have ghc installed23/10 00:40
pumpkinhey23/10 00:40
wiressup23/10 00:40
pumpkinI still haven't gotten around to the boxy approach23/10 00:40
pumpkinthe code is on my other computer and I forgot to put it online so I can't get at it easily right now23/10 00:40
wiresyeah, screw that (boxing). My friend suggested using webfonts23/10 00:41
pumpkinwebfonts that support all the weird agda symbols? :O23/10 00:41
wiresthe <pre> font is in fact not entirely monospacesd23/10 00:41
pumpkinI've noticed :)23/10 00:41
wiresi've check some of the online foundries, but there are no nice fonts that support most unicode chars and are monospace23/10 00:41
pumpkin:(23/10 00:41
wiresso that leaves us with for instance computer modern or dejavu sans or the monospace font that is included on linux computer23/10 00:42
pumpkinknow of any freely licensed fonts that support that and that we could convert to web fontyness?23/10 00:42
wires^^ :)23/10 00:42
pumpkinah23/10 00:42
pumpkincomputer modern isn't my favorite font23/10 00:42
wiresno it's quite bad actually if it's not printed23/10 00:42
wiresdeja vu is okay23/10 00:43
pumpkinis there a webfonty version of it?23/10 00:43
wiresi'm not sure what font by default is shipped with debian for instance, but kosmikus uses that in emacs and it looks very good23/10 00:43
wiresi think you can just host the .tff fonts locally and embed them in you page23/10 00:43
wires.ttf23/10 00:43
pumpkinoh, that works? cool23/10 00:43
pumpkinI guess I want dejavu mono23/10 00:44
wiresor even .otf23/10 00:44
wireshm wait i just did this for my emacs locally, on moment23/10 00:44
wiresgrr can't find.. sorry23/10 00:47
pumpkinthat works nicely23/10 00:49
pumpkindejavu sans mono23/10 00:49
wiresI thought it missed some important characters23/10 00:49
pumpkinI dunno, I'm just testing it on my simple test page23/10 00:49
wireslike disjoint union23/10 00:49
pumpkinmy page has that23/10 00:50
pumpkinhttp://snapplr.com/5nad23/10 00:50
wiresy0 nice23/10 00:50
wiresjup that is much better23/10 00:51
pumpkinhttp://snapplr.com/8t4923/10 00:51
pumpkinnot a fan of the forall23/10 00:51
pumpkinbut whatever23/10 00:51
wireshow is "triple equals"?23/10 00:51
wiresbut this looks a lot better than before23/10 00:52
wiresi mean, at least it's monospaced :P23/10 00:52
pumpkinyeah :P23/10 00:52
pumpkinjust looking at triple equals in a glyph viewer looks fine to me23/10 00:53
pumpkinman, soon we'll have craploads of blogposts with pretty agda in them23/10 00:53
pumpkinI hope23/10 00:53
wireswhat did you write it in?23/10 00:53
pumpkinwrite what?23/10 00:53
wiresthat formatter23/10 00:53
pumpkinoh, it's haskell, using the agda API23/10 00:53
wiresk23/10 00:54
wiresare you sharing the code?23/10 00:54
pumpkinyeah, when I get back to my computer that has the code on it :)23/10 00:54
pumpkinsince I don't have it myself right now23/10 00:54
pumpkinjust the sample output I put up on my website23/10 00:54
wirescool23/10 00:54
pumpkinit's also horribly ugly code23/10 00:54
pumpkinsince the agda api loves using files23/10 00:55
pumpkinso you can only ask it to typecheck/highlight files23/10 00:55
pumpkinso I need to generate temporary files and so on23/10 00:55
pumpkin(and it likes to make sure the file name is correct)23/10 00:55
wiresno streams :( alright,  i'll put it in a container and use a stick to access it then23/10 00:55
pumpkinand removing that restriction requires lots of duplication of their code23/10 00:55
pumpkinoh no, I handle that for you23/10 00:55
pumpkinyou give it a string of agda code (or literate agda + markdown)23/10 00:56
pumpkinand it'll spit out the html or an intermediate format23/10 00:56
wiresnice23/10 00:56
pumpkinthe intermediate format is just [Either String Html] where the Strings represent non-code to be passed on to another formatter like markdown, and Html represents the highlighted code23/10 00:57
wiressweet. looking forward to using it23/10 00:57
pumpkin:)23/10 00:58
pumpkinI also want to make a lightweight version23/10 00:58
wiresin python? ;)23/10 00:58
pumpkinsince the current one requires full typechecking before it can highlight it23/10 00:58
pumpkinlol no23/10 00:58
wiresjust kidding, i'm running my site using python23/10 00:58
pumpkinthat's for the most accurate highlighting, since constructors can't be determined until typechecking23/10 00:58
pumpkinbut most people don't care and I could probably get away with just parsing23/10 00:58
pumpkinomg python23/10 00:59
pumpkinI've just been using hakyll23/10 00:59
wires*shrug*23/10 00:59
wiresis there a nice blog/cms in haskell?23/10 00:59
pumpkinI dunno, hakyll seems pretty nice to me23/10 00:59
pumpkinbut I'm a fan of static site generators23/10 00:59
wireshmm me too, just generate from your SCM23/10 01:00
pumpkinthat's what hakyll does23/10 01:00
pumpkinand quite nicely23/10 01:00
wiresdid you intergrate this with khakyll?23/10 01:00
pumpkinnot yet23/10 01:00
wiresbut you will.. alright nice23/10 01:00
pumpkinI basically hacked away at agda API for a few hours and spat out that page, then had to take a trip a couple of weeks ago and haven't worked on it since23/10 01:00
pumpkinbut yeah, I definitely intend to make a nice hakyll interface and another interface for things like wikis (or hpaste) to use23/10 01:01
wiresinteresting, i'll try hakyll later23/10 01:02
pumpkinjaspervdj, the main developer, is also very responsive and efficient :P23/10 01:02
wiresnice, pandoc23/10 01:03
wiresthis looks sweet..23/10 01:03
wiresthanks. now i need to get back to understanding observational equality :) ttyl later23/10 01:04
pumpkingood luck!23/10 01:04
wirescheers23/10 01:04
Spockzpumpkin: you made a highlighter based on the Agda code on hackage?23/10 10:29
pumpkinSpockz:not on hackage yet23/10 16:38
pumpkinbut the rest is right23/10 16:38
Spockzpumpkin: I did this for haskell: http://alessandrovermeulen.me/projects/lhs2texhl/23/10 16:39
pumpkincool23/10 16:41
Spockzand I want to do the same thing for agda, but then I need to talk to the agda lib in order to parse23/10 16:42
Spockzand I see that you have experience with that :)23/10 16:42
pumpkinit's not exactly pleasant23/10 16:43
Spockzthat's what I fear :P23/10 16:43
jmcarthuri don't like how syntax highlighters will treat some functions as special and others as not special23/10 17:26
Spockzjmcarthur: do you have an example?23/10 17:26
jmcarthur*some syntax highlighters23/10 17:27
pumpkinmine doesn't23/10 17:27
jmcarthurfor example: https://docs.google.com/viewer?url=http://alessandrovermeulen.me/wp-content/2010/10/LiterateHighlighter.pdf23/10 17:27
Spockzmine even reconises variables that are being used as functions23/10 17:27
jmcarthurwhy is length special but getArgs not?23/10 17:27
Spockzoh23/10 17:27
Spockzsorry :p23/10 17:27
pumpkinit isn't a function23/10 17:27
jmcarthuroh i see23/10 17:27
Spockzthat's because getArgs isn't used as a function, no application23/10 17:27
jmcarthurfunctions are special, values are not23/10 17:27
jmcarthurokay23/10 17:27
pumpkinbut I see what you mean23/10 17:27
Spockzbut main isn't highlighted because it has no binding and isn't used as a function so I can't recognise it23/10 17:28
Spockzthat's a bug in haskell-src-exts I think23/10 17:28
jmcarthurnow that i understand the method to the madness i think it's okay23/10 17:28
pumpkinjmcarthur: how about http://pumpkinpat.ch/moo.html :P23/10 17:28
jmcarthursome syntax highlighters do actually do that23/10 17:28
pumpkinyeah, the one in textmate does23/10 17:28
jmcarthuragda is probably really hard to get right23/10 17:28
pumpkinmy highlighter does get it right ;)23/10 17:29
pumpkinbut it can only highlight constructors green after a typechecking pass23/10 17:29
jmcarthurbut on the other hand, easy, because it's kind of pointless to treat certain functions as special :)23/10 17:29
jmcarthurah23/10 17:29
jmcarthuri like the highlighted constructors23/10 17:29
pumpkinbut that page is the result of a full typecheck highlighting23/10 17:29
pumpkinme too, but it's not feasible for general purpose highlighting23/10 17:29
pumpkinI often wish that haskell had the same feature23/10 17:30
jmcarthuri was thinking at some point in the past while looking at some syntax highlighting stuff that it could be nice if the rule was whether or not the variable was free23/10 17:30
jmcarthurbut i don't know23/10 17:30
jmcarthurlike, using a top level function would be different that using one bound by a pattern/lambda23/10 17:31
jmcarthur*than23/10 17:31
pumpkinah23/10 17:31
pumpkinI'm going to set up webfonts soon so we can get a true monospace font on that page too23/10 17:31
jmcarthurin haskell, types complicate that because there are actually *are* free variables (due to the usually implicit forall)23/10 17:31
Spockzthe one in textmate does what?23/10 17:32
jmcarthur*there actually23/10 17:32
pumpkinSpockz: highlights certain functions it knows about differently from other functions23/10 17:32
jmcarthurpumpkin: a "true" monospace font?23/10 17:32
jmcarthurwhat's not true about it as is?23/10 17:32
Spockzpumpkin: yes it highlights prelude functions differently23/10 17:32
pumpkinjmcarthur: the arrow in http://snapplr.com/bgeg is wider than the other constructors23/10 17:32
pumpkinyour browser font might be better23/10 17:33
jmcarthurah23/10 17:33
jmcarthurmine is set to menlo23/10 17:33
pumpkindoes it look okay?23/10 17:33
jmcarthurdoes the same thing you just said23/10 17:33
pumpkinah yeah23/10 17:33
pumpkinon the other hand, using something like dejavu sans mono23/10 17:33
jmcarthuri use menlo in emacs and it manages fine though23/10 17:33
jmcarthuri think it just resizes some things to fit23/10 17:33
SpockzI didn't find a font that is really good23/10 17:33
pumpkinworks fine and is nicely monospaced23/10 17:33
Spockzso I use courier now :)23/10 17:33
Spockzit has all the characters I encountered23/10 17:33
pumpkinhere, let me show you dejavu sans mono on the same code23/10 17:33
jmcarthurweird considering the origin of menlo23/10 17:33
pumpkinhttp://snapplr.com/5pa223/10 17:34
pumpkinthat's with dejavu sans mono23/10 17:34
Spockzpumpkin: but maybe I can encorporate some of your code in lhs2TeX-hl? :p23/10 17:34
pumpkinSpockz: sure, but it's mostly just hacks around the unfriendly agda API :P23/10 17:35
jmcarthuroh actually it looks fine with menlo23/10 17:35
pumpkinwhat part of it are you interested in?23/10 17:35
pumpkinis menlo free?23/10 17:35
pumpkinI'm mostly looking for stuff that I can webfontify23/10 17:35
jmcarthurpumpkin: i was thinking that what you just linked me to was text, not an image :P23/10 17:35
jmcarthurmenlo comes with os x23/10 17:35
pumpkin:P23/10 17:35
pumpkinah23/10 17:35
Spockzpumpkin: the part where I give it a .lagda file and that it compiles/checks that for me and gives me a parse tree or something23/10 17:35
jmcarthurit's apple's version of deja-vu, basically23/10 17:35
jmcarthurit's better, IMO23/10 17:36
Spockzdeja-vu misses a lot of chars23/10 17:36
jmcarthurnot for me23/10 17:36
pumpkinmenlo does look okay23/10 17:36
jmcarthurnot that i've noticed anyway23/10 17:36
pumpkinSpockz: really? I haven't noticed any missing23/10 17:36
pumpkinbut that's only on this small sample23/10 17:36
pumpkinmenlo seems to behave nicely too23/10 17:36
jmcarthuri use it as my main coding font. never had an issue23/10 17:36
pumpkinon this sample23/10 17:36
jmcarthurincluding with agda23/10 17:36
SpockzUnion, \—> \==> and some others23/10 17:36
jmcarthurum23/10 17:37
jmcarthurthose all work for me in menlo23/10 17:37
Spockzno not union23/10 17:37
SpockzUnion with a plus in it23/10 17:37
jmcarthurwhat is the agda string for that?23/10 17:37
jmcarthurif any23/10 17:37
pumpkindejavu sans mono works with \u+23/10 17:37
pumpkinfor me23/10 17:37
pumpkinit's even in this code23/10 17:37
pumpkinlet me screenshot it23/10 17:37
pumpkinoh it was in that screenshot23/10 17:37
jmcarthurSpockz: \u+ works for me with menlo23/10 17:38
pumpkinmaybe the browser is being friendly and fetching the glyph from another font though23/10 17:38
jmcarthuri'm in emacs23/10 17:38
jmcarthurworks23/10 17:38
jmcarthur⊎    <- that is correct, right?23/10 17:38
Spockzdon't know23/10 17:38
jmcarthurworks in my terminal too23/10 17:38
Spockz\|-23/10 17:39
Spockzhmm23/10 17:39
Spockzodd23/10 17:39
jmcarthurwell, anyway, i love menlo23/10 17:39
pumpkinhttp://snapplr.com/z0e423/10 17:40
jmcarthurhmm... my terminal still shows some sort of vector font for \u+ even if i change the font to a bit font, so i guess there is a chance it's being magical with menlo as well23/10 17:40
jmcarthurwhen i asked if that symbol was correct i meant is that the correct symbol i should be testing with, not is that symbol rendering correctly23/10 17:43
jmcarthurby the way23/10 17:43
Spockzbut yes that's the symbol23/10 17:43
Spockzhttp://alessandrovermeulen.me/wp-content/2010/10/Screen-shot-2010-10-23-at-18.41.00.png23/10 17:44
jmcarthuranyway, this is why menlo rocks http://typophile.com/files/menlovsdejavusansmono_6131.png23/10 17:44
jmcarthurSpockz: i like that23/10 17:44
Spockzyou can download it23/10 17:45
jmcarthuri want to get pandoc and lhs2tex to play nice together23/10 17:45
Spockzhmm23/10 17:45
Spockzdidn't look into that23/10 17:45
Spockzwould that be a better solution?.23/10 17:46
jmcarthurthan?23/10 17:46
Spockzlhs2TeX doesn't have that many formatting options23/10 17:46
Spockzthan what I presented?23/10 17:46
jmcarthurmy only reason is so i can use markdown instead of latex23/10 17:46
jmcarthurnot for highlighting23/10 17:46
Spockzaah23/10 17:46
jmcarthurpandoc by itself doesn't do highlighting, although i think for html at least it can use some library to add highlighting23/10 17:46
Spockzhscolour probably/23/10 17:47
jmcarthurno it's something else23/10 17:47
pumpkinI didn't realize menlo and dejavu sans were so similar23/10 17:47
pumpkinand had the common ancestor23/10 17:47
jmcarthurit's highlighting-kate23/10 17:47
pumpkinI'm not a fan of highlighting-kate23/10 17:47
jmcarthuri have only used it with pandoc. it was alright, but i didn't abuse it enough to pass final judgement23/10 17:48
jmcarthurthere was some talk about making pandoc and lhs2tex play nice together, but i don't know if any code was ever released23/10 17:49
jmcarthurthey speaker said it was a lot of work to do himself :\23/10 17:49
jmcarthur*the23/10 17:50
Spockzdo you know the speaker?23/10 17:50
jmcarthurno23/10 17:50
SpockzI don't know how hard it should bee23/10 17:51
jmcarthuroh but wait, i see an email from 2009 that claims it was possible even then...23/10 17:51
jmcarthurhttp://www.mail-archive.com/haskell@haskell.org/msg21788.html23/10 17:51
jmcarthurnow i don't know what that talk was actually about. i thought it was new and hard23/10 17:52
jmcarthurhttp://vimeo.com/1548173623/10 17:53
Spockzah malcolm wallace23/10 17:53
Spockzo, that's not malcolm wallace23/10 17:53
jmcarthuri tihnk just posted by him23/10 17:54
jmcarthur*think23/10 17:54
jmcarthurnot necessarily the speaker23/10 17:54
Spockzno the speaker is Tillmann Rendel23/10 17:56
kosmikusjmcarthur: Tillmann complained (and rightly so) that lhs2tex does not expose a library interface. The next release will probably do that.23/10 18:15
jmcarthurawesome!23/10 18:15
kosmikusactually, I'd rather rewrite lhs2tex completely though. if only I had the time.23/10 18:16
Spockzpumpkin: do you have the code for that interface somewhere I can look at it?23/10 18:36
pumpkinSpockz: let me dig it up23/10 20:35
pumpkinI warn you, it's horrible23/10 20:36
pumpkinSpockz: http://github.com/pumpkin/agda-highlight23/10 20:41
Spockzwooosh23/10 20:43
pumpkin?23/10 20:43
SpockzI was warned, but still23/10 20:45
pumpkinoh at how ugly it is23/10 20:45
pumpkinyeah, I even hardcoded my local path into it23/10 20:45
pumpkinit isn't intended for public consumption yet23/10 20:45
Spockzmaybe I should start over23/10 20:46
pumpkinyou're welcome to23/10 20:46
pumpkinor just wait a while and I'll have some more time to clean it up23/10 20:47
Spockzthe only thing I need is some extract23/10 20:47
Spockzproblem is that with lhs2tex you can only replace strings, so you don't have context23/10 20:48
pumpkinah23/10 20:49
Spockzso that's where lhs2tex 2.0 comes in :P23/10 20:50
pumpkinoh so you need it for haskell or agda?23/10 20:50
pumpkincause I'm not sure there's anything of value to haskell in there23/10 20:51
SpockzI've got the haskell part already23/10 20:51
Spockzso now I need the agda part23/10 20:51
pumpkinah23/10 20:53
Spockzmaybe import Agda.Syntax.Parser is enough23/10 20:54
pumpkincould be23/10 20:54
pumpkinthat has a fair amount of information and doesn't have unnecessary file-based IOo23/10 20:54
pumpkinor doesn't force you to use files, anyway23/10 20:55
Spockzhmm the agda syntax is a bit more complex23/10 21:05
Spockzbut maybe I can get a long way with just Expr23/10 21:07
--- Day changed Sun Oct 24 2010
MrAIHello24/10 20:22
pumpkinhi24/10 20:22
MrAIDo you know why I would keep getting a parse error in Agda? E.g. data List` (X::Set) = nil | con (x::X) (xs::List` X)24/10 20:23
MrAIThat keeps producing an error24/10 20:23
pumpkinyou probably want : and not :24/10 20:23
pumpkin::24/10 20:23
MrAIon all?24/10 20:24
pumpkinbut you also just need to look up the syntax :P24/10 20:24
pumpkinthat isn't valid syntax24/10 20:24
MrAISorry im new to Agda. Trying to get my head round it all :)24/10 20:24
pumpkindata List' (X : Set) : Set where Nil : List' X; Con : (x : X) -> (List' X) -> List' X24/10 20:25
pumpkinforgot the xs24/10 20:25
MrAIAh ok24/10 20:25
MrAIIs it ' or `? (Im not sure if you can see the difference there)24/10 20:26
pumpkinyou can put either in24/10 20:27
pumpkinthey're just different names24/10 20:27
pumpkinI used the wrong one :)24/10 20:27
MrAIIt keeps throwing me back: Perse error data<ERROR> List` (X : Set) where N....24/10 20:28
MrAIIm using emacs and went to Agda-> Load after typing that in24/10 20:29
pumpkinmaybe ` is reserved for something24/10 20:32
MrAIStill same problem. Is there a way to force emacs to do C-l instead of C-c?24/10 20:33
pumpkinI don't know what you mean24/10 20:33
pumpkinC-c C-l is what you do to load it24/10 20:33
MrAII see. I am doing that right then24/10 20:34
MrAIIm trying to follow the 'An Agda Tutorial' that was written in May 12, 2006. And I cant even get the examples to work :s lol24/10 20:36
copumpkinoh, that's probably agda124/10 20:38
copumpkinhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials24/10 20:38
MrAIAh ok. Thanks - Ill have a look there24/10 20:39
MrAII was forgetting the 'module ... where' part. But now I am faced with a: Parse error <EOF><ERROR>. All I have is :24/10 20:44
MrAImodule AgdaBasics where24/10 20:44
MrAIdata Bool : Set where24/10 20:44
MrAI true  : Bool24/10 20:44
MrAIfalse  : Bool24/10 20:44
MrAIDoes the program need to do something to load properly?24/10 20:45
MrAIExamples from http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/agdalectureexamples/ will not load either with a parse error24/10 20:54
pumpkinyou need indentation and so on24/10 20:54
MrAICould you give me the simplest Agda2 example you can think of please? I just want to get something loaded, lol24/10 20:59
pumpkinmodule Moo where24/10 21:02
pumpkindata X : Set where24/10 21:02
pumpkin<space><space>x : X24/10 21:02
MrAI*creates a Moo.agda file and types that in* *loads up emacs* *opens file*24/10 21:03
MrAIAgda -> Load. Success :D:D24/10 21:04
MrAIThanks24/10 21:04
MrAIReally thanks :D24/10 21:04
MrAIAnd if I understand that right... X is a set, where x is a type of X?24/10 21:05
pumpkinthe type of X is Set, the type of x is X24/10 21:05
pumpkinx is a constructor of X24/10 21:05
MrAIDoes the meaning of 'constructor' mean anything past: the type of x is X?24/10 21:07
benmachineyou can pattern match against constructors24/10 21:07
MrAII see24/10 21:07
MrAISo im assuming : is Adga2 and :: is Agda1?24/10 21:16
pumpkinprobably24/10 21:17
pumpkinI've never used Agda124/10 21:17
MrAIFair enough. I'm starting out and its not as easy as it would seem, lol24/10 21:17
MrAIHow did you learn?24/10 21:17
MrAIPersonally I wish I had done Mathematics first and the computing24/10 21:23
MrAI*then24/10 21:23
MrAIIs Haskell worth learning first, and then Agda?24/10 21:27
dschoepeMrAI: It would definitely help, imo.24/10 21:29
MrAIOk :D Thanks24/10 21:30
MrAII spent half an hour reading through Haskell basics but cleary I need to go revisit it24/10 21:31
pumpkinunless you're experienced in another functional language with an interesting type system, I'd recommend a few months of haskell at least24/10 21:33
MrAII dont have a few months. I have three weeks max to learn Haskell(maybe) and Agda224/10 21:35
MrAII've taken on a really ambitious project24/10 21:36
pumpkinwell, you'd better be willing to dedicate a lot of time to it :)24/10 21:43
pumpkinagda actually feels a bit cleaner than haskell in terms of the constructs it provides24/10 21:43
MrAIIm literally spending every waking for the next two weeks learning all this. And I dont have a functional programming past.24/10 21:44
pumpkinthe main advantage of haskell as a start for this is that it's easier to play with and see what it does24/10 21:45
pumpkinwe typically don't "run" agda programs24/10 21:45
pumpkinyou can ask emacs to normalize an expression for you, which has a similar effect for many things24/10 21:45
MrAIHaha yes I noticed that you dont 'run' agda programs :) Hard step that one24/10 21:45
pumpkinwell, you can do it24/10 21:46
pumpkinit just isn't ideal24/10 21:46
Saizanthere's also a repl apparently, agda -I24/10 21:46
pumpkinit's unsupported though24/10 21:47
MrAIYes pumpkin from what im finding - I do agree.24/10 21:47
dschoepepumpkin: On the other hand, the discussions with the type checker are a lot longer and more intricate than in Haskell though, in my experience24/10 21:47
dschoepeeven with all the "uncleanliness" :)24/10 21:48
MrAIThe one thing ive found coming from an OO background is I dont type as much, its alot more thinking24/10 21:48
benmachinehwo does agda claim to be (possibly) a dependently-typed programming language if you don't run things in it at all24/10 21:49
Saizanbecause you can24/10 21:50
pumpkinbenmachine: you can, but the users who typically write things in it don't usually24/10 21:50
Saizanand fairly easily24/10 21:50
benmachineso you *can* program with it but no-one does >_>24/10 21:51
pumpkinI program with it plenty24/10 21:51
pumpkinI just don't run the programs much24/10 21:51
benmachinehaha okay24/10 21:51
pumpkinif you choose to define programming as something you run, then I guess I don't program24/10 21:51
Saizani'm not sure if #agda is so representative, btw :)24/10 21:52
benmachinefor the purposes of this conversation I'm using program to mean doing stuff that exists for a reason other than to prove something24/10 21:52
benmachinecf. the dilemma in the topic24/10 21:52
pumpkinyou could easily run the programs we write too24/10 21:53
* benmachine hasn't yet done anything in agda that isn't proofs24/10 21:53
Saizando programs that compute proofs count?24/10 21:53
pumpkinwe just happen to be satisfied with proving them correct24/10 21:53
MrAISo what do you use Agda for then? If not to create programs you provide an input and expect an output?24/10 21:53
benmachinepumpkin: okay, that makes sense24/10 21:53
pumpkinMrAI: I usually write programs for something I care about, and then prove that they do what I want them to do24/10 21:54
pumpkinand then move on to something else24/10 21:54
benmachineMrAI: all the agda I've written is successful if it typechecks24/10 21:54
MrAIAh ok24/10 21:54
pumpkin(or fail to prove what I wanted to prove, and move on)24/10 21:54
pumpkin:P24/10 21:54
MrAII see now24/10 21:54
MrAII did read alot about how Agda can prove correctness24/10 21:54
* benmachine got as far as proving the commutativity and distributivity of multiplication on natural numbers24/10 21:55
* MrAI test24/10 21:56
benmachineI was considering starting a different tack though24/10 21:56
benmachineI proved multiplication was commutative by induction24/10 21:56
benmachinewhich is natural because the definition of multiplication was inductive24/10 21:56
MrAIProof by induction, proof by contradiction... I swear there was another24/10 21:56
pumpkingeneral proof by contradiction in agda doesn't work24/10 21:57
benmachinebut if I was doing a pen-and-paper mathematical proof, I would prove that m * n was the cardinality of A \times B and then prove a bijection between A \times B and B \times A24/10 21:57
MrAIAh ok24/10 21:57
benmachinethat would seem more natural, but I don't really know how to construct bijections and so forth in agda24/10 21:57
benmachineoffhand I guess you could construct a datatype containing f, a proof of surjectivity, and a proof of injectivity24/10 21:58
benmachineor it might be easier to provide f and g and prove f (g x) == x24/10 21:58
benmachineI dunno, anyone got any experience as to which is more sensible?24/10 21:58
Saizanprobably the latter24/10 21:59
MrAIIm sorry I cant help - my math stopped at high school 7 years ago.24/10 21:59
benmachineyeah I'm not sure what surjectivity proofs would even look like short of just providing an inverse24/10 21:59
Saizanbtw, maybe you don't even need to prove there's a bijection, just that the two sets are equipotent24/10 22:00
benmachinewhat's equipotence?24/10 22:00
dschoepebenmachine: my rusty latin skills suggest |A| = |B|24/10 22:01
Saizani'd represent it as just A -> B \x B -> A24/10 22:01
Saizanwithout any relation between the two functions24/10 22:02
benmachineSaizan: hmm24/10 22:03
Saizanmaybe i'm being silly, i'm not fully awake yet :P24/10 22:06
Saizanin fact you do need them to be inverses, otherwise it's easy to map multiple elements to just one24/10 22:09
benmachineyes24/10 22:09
benmachineor they could both be injections, I guess24/10 22:09
benmachineor both surjections24/10 22:09
Saizanyep, but the useful definitions of those properties involve partial inverses24/10 22:10
benmachine...indeed24/10 22:10
Saizanhow are you going to represent _has-cardinality_ ?24/10 22:13
benmachineiono24/10 22:13
* benmachine still new to this tbh24/10 22:13
SaizanX has-finite-cardinality n = bijection X (Fin n) :D24/10 22:14
benmachineheh24/10 22:15
benmachineveeery possibly.24/10 22:15
benmachineoh dang it I have to prove left and right inverse separately24/10 22:38
Saizanyeah, that's annoying24/10 22:40
--- Day changed Mon Oct 25 2010
glguyIs there any way for me to get rid of all of these [subst] calls without making a ton of top-level definitions? http://www.galois.com/~emertens/flag/flag.html25/10 08:27
glguyI need lambdas with rewrite syntax :)25/10 08:27
MrAIWhat is the best rescource for Agda2? I keep finding tutorials and documents relating to Agda125/10 15:12
SaizanMrAI: i'm pretty sure the ones here are about Agda2 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials25/10 15:14
MrAIWhich Set is bigger: Set1 or Set2 or Set3 ore... etc?25/10 15:47
MrAI*or25/10 15:47
Saizanfsvo bigger, Set (n+1) is bigger than Set n25/10 15:48
MrAIWhat does fsvo mean?25/10 15:48
Saizanfor some value of :)25/10 15:49
MrAIok thanks25/10 15:49
pumpkinMrAI: so what's the big project you've undertaken that needs agda?25/10 15:54
MrAIHow does "suc n + m = suc(n+m)" make the value smaller each time?  I know it takes in two arguments, but I dont see how it gets smaller25/10 16:02
MrAIIts my 4th Year University project - I've chosen one that uses Agda. The first step is to learn it :)25/10 16:02
MrAIWell the first is to learn functional programming - But I'm learning that along side Agda25/10 16:02
MrAIDoes suc reduce the value passed by one until the base case is reached?25/10 16:02
pumpkinsuc is a constructor25/10 16:02
pumpkinso if you pattern match on it25/10 16:02
pumpkinyou know that the parameter inside it is smaller, if you make some assumptions25/10 16:02
MrAII see25/10 16:02
Saizanyeah, n is smaller than suc n25/10 16:04
wiresoh wow, http://detexify.kirelabs.org/classify.html just scribble the symbol and it looks up the latex expression25/10 17:29
pumpkinthat's nice25/10 17:30
wiresI can easily find the type for propositional equality in agda, here http://www.cs.nott.ac.uk/~nad/listings/lib-0.4/Relation.Binary.Core.html#4612 but how is definitional equality represented in Agda?25/10 22:57
wiresIn addition, here http://www.cs.nott.ac.uk/~nad/listings/lib-0.4/Relation.Binary.PropositionalEquality.Core.html#574 what does {A = A} mean. Is that def. equality?25/10 22:58
pumpkinthat's just syntactic25/10 22:59
pumpkinjust means bind the implicit parameter named A to A25/10 22:59
wiresok.25/10 22:59
wireshttp://www.cs.nott.ac.uk/~nad/listings/lib-0.4/Relation.Binary.PropositionalEquality.TrustMe.html <-- is this def. equality?25/10 22:59
pumpkinno, that's a hack25/10 22:59
pumpkindefinitional equality is basically that type you linked to before25/10 23:00
wiresthe one that is called "propositional equality"? ;)25/10 23:00
wires"≡" that one25/10 23:00
wires?25/10 23:01
pumpkinactually, definitional equality is writing f x = f + 1, I think25/10 23:01
pumpkinjust any definition you write down25/10 23:01
wiresOk, that makes more sense.25/10 23:01
wiresAlright, thanks, I can go with that...25/10 23:01
wireswth... ??25/10 23:58
wirescabal install agda25/10 23:58
wiresResolving dependencies...25/10 23:58
wirescabal: dependencies conflict: ghc-6.12.3 requires directory ==1.0.1.1 however25/10 23:58
wiresdirectory-1.0.1.1 was excluded because ghc-6.12.3 requires directory ==1.0.1.225/10 23:58
wireswhat is that?25/10 23:58
--- Day changed Tue Oct 26 2010
Saizanwires: first Cabal FAQ26/10 00:08
wiresoops26/10 00:08
wiresok funny i'm having a hard time finding the FAQ :)26/10 00:10
Saizanhttp://www.haskell.org/cabal/FAQ.html26/10 00:11
wiresSaizan: ah.. haskell FAQ26/10 00:12
Saizanit says "Cabal FAQ" at the top :)26/10 00:13
wiresEven.. my brain is cooked ... maybe time to quit for today26/10 00:15
doliowires: Going back to earlier: "definitional equality" is the equality that is used internally to decide whether two expression are equal for the purposes of type checking.26/10 02:05
dolioAlthough, if you go back to Martin-Loef, it should probably be called "judgmental equality".26/10 02:06
wiresthanks26/10 02:06
dolioPropositional equality is equality as a datatype.26/10 02:06
dolioAnd it's called that because propositions are types in the Curry-Howard and Martin-Loef presentation, more or less.26/10 02:07
wiresI think I understand propositional equality26/10 02:07
wiresI'm trying to work out most of the details of the observational equality paper26/10 02:08
dolioWhereas "judgmental equality" is a judgment. If you look at Martin-Loef's stuff...26/10 02:08
wiresIt should be in the bibliopolis stuff, no?26/10 02:08
dolioJudgments have the form 'G |- J'26/10 02:09
wiresJ as in elimination rule?26/10 02:09
wiresor just random term?26/10 02:09
dolioAnd he has judgments like 'G |- T type' or 'G |- T prop'. 'G |- x : T' and 'G |- x = y : T', the last being an equality judgment.26/10 02:10
dolioJ being one of the judgment forms.26/10 02:10
dolioOr, things being judged.26/10 02:10
dolioAnyhow, his "definitional equality" is strictly used for meta-level abbreviations.26/10 02:10
dolioSo if you say "we'll write 'foo' instead of 'bar baz quux'," foo is definitionally equal to bar baz quux.26/10 02:11
dolioBut, I guess it's morphed over the years to mean the decidable equality used during type checking.26/10 02:12
wiresRight, but.. what is unclear to me; have you read the Observation equality now paper? They state on the second page: if |- a ==(def) b : A   blah blah. So this means the internal definition equality has a type itself?26/10 02:13
dolioAnyhow, in Agda, propositional equality is just kind of a capturing of definitional equality as a type, because you define it as an indexed type, inhabited only by 'refl', where the two indices must be definitionally equal.26/10 02:13
doliowires: Usually, definitional equality will only hold between two values of the same type. A is the type of a and b, in that notation.26/10 02:14
dolioIf the values have different types, they're trivially rejected as being definitionallly equal.26/10 02:15
dolioThat goes back to the equality judgment form I mentioned, too.26/10 02:16
dolio'x = y : T' means x and y are equal elements of type T.26/10 02:16
dolioIt's an operator to itself. _=_:_26/10 02:17
wireshm. I thought you could use def. equality to identify two types26/10 02:18
wireswell no26/10 02:18
wiresactually I didn't think that :)26/10 02:18
dolioAnyhow, observational type theory takes the separation seriously, by getting rid of the propositional-equality-captures-definitional-equality thing, and using a more permissive propositional equality.26/10 02:20
wireshmm. Yeah, I don't really get the paper... :-S26/10 02:22
dolioIt isn't easy.26/10 02:22
wiresI'm lacking a lot of prerequisite knowledge also...26/10 02:23
wirescould I ask you something about that paper?26/10 02:24
dolioSure.26/10 02:24
wiresSo, the paper says: as TT have nontrivial computations within types, the come with a notion of definitional equality, presented here as a typed equality judgement "===" Types are identified up to definitional equality as expressed by the conversion rule: |- s : S   |-  S === T     =>    |- s : T26/10 02:25
wiresThis doesn't mean one can state that S === T, right?26/10 02:26
wiresI mean it's only used internally during type checking... ie. follows from some rules?26/10 02:26
dolio|- s : S and |- S === T are premises.26/10 02:27
wiresyes26/10 02:27
dolioIf you can derive those two, you can derive |- s : T26/10 02:27
dolioSo it's an inference rule.26/10 02:27
wiresSo how does one derive S === T ?26/10 02:27
dolioWell, usually type equality is up to at least beta equality.26/10 02:28
dolioSo (\T -> T) S === S holds, for instance.26/10 02:28
dolioAnd so on.26/10 02:29
wiresAh ok...26/10 02:29
dolioAlso alpha equality. (x : A) -> B x === (y : A) -> B y26/10 02:29
dolioProvided x isn't free in B.26/10 02:29
dolioOTT/Epigram tries to go a few steps beyond that, in the section on "quoting" at the end of the paper, but that isn't crucial to understanding the rest.26/10 02:31
dolioLike, they try to make things definitionally eta-equal. For functions, that's f === \x -> f x.26/10 02:32
wiresAh, yes....26/10 02:32
dolioAnd they do simplifications of proofs and stuff.26/10 02:32
wiresCool, I didn't understand that section before...26/10 02:33
wiresthanks this helps a lot26/10 02:33
dolioYeah, it's kind of opaque unless you know what they're trying to accomplish.26/10 02:33
wiresespecially if you are new to the whole lambda-game26/10 02:33
wiresdifferent notations..26/10 02:34
wiresalso:   s[ Q:S=T > : T , do you happen to know how to read that notation?26/10 02:34
dolioThat looks like their notation for substitution/coercion.26/10 02:35
dolioGiven a term s : S, and a proof that S = T, that's a term with type T obtained by coercing by the proof of type equality.26/10 02:36
wiresYes, so that means Q is a proof object for S=T, then given Q i can coerce s to T ?26/10 02:36
dolioRight.26/10 02:36
wiresright26/10 02:36
wires:)26/10 02:36
wiresAlright, this should get me a bit further. Thanks for you help...26/10 02:37
dolioNo problem.26/10 02:37
freiksenet226/10 08:02
freiksenetsorry, misclick26/10 08:02
wiresIs there a specification somewhere of all the inference rules used in agda?26/10 10:31
wiresUm, heh, ok, in the source probably...26/10 10:32
Watermindemacs only applies syntax highlight to my files when I "Load" them using the menu26/10 12:54
Watermindand new contents are not highlighted, I must load again26/10 12:55
Watermindis this normal?26/10 12:55
ccasinWatermind: yes26/10 14:39
ccasinwires: the core is specified in ulf norell's thesis, though plenty has changed since then26/10 14:40
wiresccasin: thanks!26/10 14:40
ccasinin particular, the way universe levels work is a lot different than the way they are presented there26/10 14:42
ccasinin his thesis, there is no explicit quantification over levels, and things in lower universes are implicitly lifted up when the need to be26/10 14:43
ccasinnow we have the explicit universe polymorphism (and the lifting was never implemented)26/10 14:43
dolioMan, lifting was originally in?26/10 14:43
ccasinI'm sure lots of other things have changed too, but that's the one that comes to mind :)26/10 14:43
ccasindolio: well, I don't know if it was ever implemented.  but, it's in the paper26/10 14:44
dolioWell, I doubt it was implemented.26/10 14:44
dolioIt'd probably still be implemented if it were.26/10 14:44
dolioIt's a bummer that it wasn't, though.26/10 14:44
ccasinprobably (though, for example, the coq hackers have scaled back their universe polymorphism for efficiency reasons)26/10 14:45
ccasinyeah, it would be very nice26/10 14:45
dolioThat isn't really necessarily related to universe polymorphism.26/10 14:47
dolioFor instance, ECC has cumulative universes, but no universe polymorphism.26/10 14:47
ccasinyeah, you're right26/10 14:48
dolioAlthough universe polymorphism, I guess, allows you to do without, by carrying around more parameters.26/10 14:48
dolioAgda-style polymorphism, that is.26/10 14:48
ccasinthough luo works really hard for his cumulativity - he points out that the obvious naive way to add it breaks most general types26/10 14:48
ccasinI'm not sure it is as well thought out in ulf's thesis (certainly nothing is proved about it)26/10 14:49
ccasinyeah, but only if you define everything yourself.  If you want to use a non-polymorphic library or base type, you need it again26/10 14:50
dolioIn general you also need the unsatisfactory Lift type, too.26/10 14:50
Watermindccasin: so there's no way to get syntax highlight as you type? :S26/10 14:59
ccasinWatermind: I don't know of one, but maybe someone will correct me26/10 14:59
Watermindccasin: ok thanks26/10 15:00
Watermindthat's quite unusual26/10 15:00
Watermindno big deal anyway26/10 15:00
ccasinyes, though I almost never type more than a few lines without loading the file26/10 15:00
ccasinthat's the beauty of holes26/10 15:00
Watermindtrue26/10 15:00
Watermindis there a pre defined key binding to load the file?26/10 15:01
wiresCtrl-c Ctrl-l26/10 15:01
ccasinC-c C-l26/10 15:01
Watermindcool thanks guys26/10 15:01
wiresWatermind: check this one http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode26/10 15:02
wireshas most important commands in there26/10 15:02
Watermindnice thanks wires26/10 15:03
pumpkinyay26/10 19:06
pumpkin@ the Andreas Abel announcement on the list26/10 19:06
Watermindwhen you load a file in emacs, the bottom part seems the interpreter26/10 19:21
Watermindbut how do you input commands there?26/10 19:21
pumpkinit's not really an interpreter26/10 19:21
pumpkinbut you can ask it to evaluate terms for you26/10 19:21
pumpkinC-c C-n26/10 19:21
pumpkin(n for normalize)26/10 19:21
Watermindpumpkin: got it26/10 19:22
WatermindI was trying to write there26/10 19:22
Spockzpumpkin: I'm giving up doing something with the internal agda syntax representation. It might be easier to just parse the output for emacs..26/10 20:57
pumpkinaw really? the highlighting info it spits out isn't bad at all26/10 20:57
pumpkinI wouldn't touch the original syntax rep26/10 20:57
Spockzhmm maybe I should take another look again26/10 20:57
pumpkinthat's what I use in my highlighter26/10 20:58
pumpkinbut you need to duplicate a lot of their code to get that26/10 20:58
Spockzyeah26/10 20:58
pumpkinanyway, if you tell me what kind of output would be best from a highlighter, I can try to put an interface that works for you into my code once I clean it up26/10 21:02
pumpkinprobably tomorrow or the day after26/10 21:02
Spockzwell something that lists functions, constructors, datatypes and literals would be great26/10 21:03
pumpkinand you don't mind if the constructor knowledge costs you a full typecheck?26/10 21:04
Spockzno26/10 21:06
Spockzoh26/10 21:06
Spockzand operators separate26/10 21:06
pumpkinI'll see what I can do :P26/10 21:06
Spockzawesome :)26/10 21:07
--- Day changed Wed Oct 27 2010
wiresIn the Altenkirch/McBride/Swierstra  paper on observational equality, they use a notation T[s] when defining the W-types:  "...W for well-founded trees whose nodes [..] comprise a choise s of node shape from S and a 'child-function' f from recursive positions T[s] to subtrees".27/10 01:43
wiresHow should I read this notation T[s]27/10 01:44
wires?27/10 01:44
wiresLater it's also used in rules as     \Gamma |- t : T[s]    etc.27/10 01:44
wires(btw with \Gamma |- s : S as other premise)27/10 01:45
pumpkinT probably takes a shape and gives you a type27/10 01:45
Saizanyou can think of T as a function from S to Set, and T[s] is the result of applying that function to s27/10 01:45
Saizanthe notation T[x] often refers to a term T where x is a free variable, it's also called a "context"27/10 01:46
wiresOk, so its like substitution27/10 01:46
Saizanyep27/10 01:46
wiresK, clear. Thanks guys :)27/10 01:47
wires(crazy stuff this type theory...)27/10 01:47
pumpkinI quite liked http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ if you haven't read it yet27/10 01:47
pumpkiniirc it covers the W types too27/10 01:48
pumpkin(but not OTT)27/10 01:48
Saizannot sure why they don't just say T : S -> Set or similar, maybe that would complicate the system27/10 01:48
wiresSaizan: yeah, I think so27/10 01:49
wirespumpkin: ha, funny also just found that this morning, very nice reference!27/10 01:50
wirespumpkin: it's very rigorous and doesn't assume any prerequisite knowledge, unlike many other references27/10 01:51
pumpkinyeah27/10 01:52
pumpkinI was surprised at how I could follow just about all of it despite not knowing much :P27/10 01:52
wiresAlso, I really like Ulf Norell's thesis, it skips some bits but together with for example this ttfp.pdf one gets quite far27/10 01:53
wiresAnd Peter Selinger, "Lecture Notes on the Lambda Calculus" together with Barendregt/Barendsen "Introduction to Lambda Calculus" makes a really nice foundation I found.27/10 01:57
pigworkerwas reading logs earlier...27/10 09:21
Spockzpigworker: nice :)27/10 09:21
pigworkerthought I'd try to clear up the T[s] bit27/10 09:21
* Saizan hopes he's not got it wildly wrong27/10 09:22
pigworkersince wires, pumpkin and Saizan were trying to make sense of it27/10 09:22
pigworkerSaizan: your question of why not to write T : S -> Set is the relevant one27/10 09:23
pigworkerTo use such a notation rather suggests that the function space S -> Set exists. But in our tiny type theory, it does not.27/10 09:24
pigworkerHowever, we still need to bind variables: the range of Pi x:S. T should be some T such that x:S |- T : Set. We need that any instance T[s] (ie [s/x]T) is a Set if s:S, but we do not need T itself to be first-class, or to form \(x:S) -> T.27/10 09:27
dolioT[s] is useful notation, to, as I've more than once written something like Pi x:A. B, and had someone question me for several minutes about how that wasn't equivalent to A -> B, and so on.27/10 09:30
pigworkerThese sorts of artefact show up when you try to model just a one layer type theory: in a universe hierarchy, you get used to everything meta being object-one-layer-up, but when that's not available, you do end up needing a separate meta notation.27/10 09:31
Saizanmakes sense27/10 09:32
pigworkerWhen we model the universe in Agda as some inductive-recursive (U : Set; El : U -> Set), T becomes an Agda function in El S -> U, but that type is not the decoding of any element of U. So T is only a meta-level function.27/10 09:37
pigworkerdolio: I guess what's a bit fast and loose is writing T[s], not T[s/x]. But that does make sense in situations where T is introduced with x in scope and used out of x's scope. Not only can you but you must instantiate x.27/10 09:40
Saizanso you'd need to have U0, U1 , .. and El S -> U0 could be representable in U1 ?27/10 09:41
pigworkerSaizan: yes27/10 09:41
dolioWell, I meant, I'd write: Pi x:A. B[x], to make it clear that B[x] may make reference to x.27/10 09:41
dolioIn that case, B[s] makes sense to me.27/10 09:42
dolioLooking at B[-] as an expression with holes, or something.27/10 09:42
pigworkerYeah. I get too used to assumptions of maximum dependency. If I write Pi x:A. B, B had better be able to depend on x, so B[a] makes sense.27/10 09:43
dolioWell, the problem is that it's not always clear to people that B is a metavariable.27/10 09:44
dolioSince B may well be a valid object expression.27/10 09:45
dolioIn which case it would obviously not depend on x.27/10 09:45
dolioFonts might come in handy there.27/10 09:46
pigworkernow that is a context-sensitive issue27/10 09:46
dolioThat's the problem I've had, at least.27/10 09:47
pigworkerdolio: btw, thanks for your clarificatory remarks on LtU27/10 09:48
dolioNo problem.27/10 09:50
wirespigworker: thanks for further explanations!  While we are at it, there was one more bit of syntax /me couldn't parse. In some of the (value level) coercion rules '||' is used, e.g. { s || Q:S=} : ... and again later Q_T |--> (snd Q) s_0 s_1 {s_0 || Q_S : S_0 = S_1 }27/10 10:12
* edwinb is interested to read that the "to preserve the so-called phase distinction seems to be so important to make use of the usual compilation techniques"27/10 10:13
wires(and rest also thanks)27/10 10:13
pigworkerwires: it's invoking coherence, but let me find a copy and answer properly27/10 10:14
wirespigworker: awesome!27/10 10:16
pigworkerwires: yes {s_0 || Q_S : S_0 = S_1} is the proof that s_0 = s_1, which must exist because s_1 was made by coercion from s_027/10 10:17
pigworkerThis coherence property is used when we're coercing values between dependent sets T[-] (e.g. the range of a Pi, the second component of a Sigma, the positions in a W). We say that two dependent sets T0[-], T1[-] are equal if we get equal sets whenever we instantiate them with equal values. Here, we make one value from the other by coercion, so coherence makes them equal: job done!27/10 10:23
pigworkeredwinb: who is saying this?27/10 10:25
wiresAh, so  s[Q:S=T>  is notation for coerced value, where {s || Q:S=T} is notation for proof object that the value s:S and it's coercion are the same object?27/10 10:28
pigworkeredwinb: I googled it. I recall wondering how exactly they were going to handle inductive types with dependent elimination, especially if large elimination is included. Singleton translations tend to be problematic there. I'm not impressed by a selective translation which ignores the difficult bits.27/10 10:33
Saizanhttp://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.169.8065 <- btw of universes, i was reading this one and wondered if coming up with these seemingly ad-hoc "roles" is really worth it instead of an explicit datatype for codes and an interpretation function27/10 10:35
dolioActually, their roles seem similar to erasure tracking via modal types.27/10 10:39
pigworkerah, the newtype bug now has a paper solution? I'll check it out. I know they talk about "universes" in this context. But they're not trying to explain this stuff to dependent type theorists.27/10 10:39
dolioOnly the modes are coupled to the kind.27/10 10:40
edwinbpigworker: it's the draft Jean-Pierre posted to the Agda list27/10 10:41
pigworkerwires: yes s[Q:S=T> is s transported from S to T; {s || Q:S=T} is the proof that (s:S) = (s[Q:S=T>:T)27/10 10:41
pigworkeredwinb: It's reasonable to consider singleton translations when trying to compile to Haskell, but one should perhaps go further. And one should not let the desire to compile to Haskell have an undue influence on the language design.27/10 10:43
wiresthanks pigworker27/10 10:45
edwinbpigworker: I haven't read the draft in any depth yet, I was just a bit worried by the motivation...27/10 10:51
edwinbBut I agree, design the language first then worry about how you're going to make it go fast.27/10 10:52
* edwinb wanders off to make another attempt at learning about llvm27/10 10:53
edwinbIncidentally, I don't really understand the desire to compile to Haskell27/10 10:53
edwinbif it's about getting Haskell users to use it, isn't it better to compile to native code and give a Haskell interface?27/10 10:54
dolioIt might be that people think that'll make it possible to piggy back on GHC's optimizations.27/10 10:54
dolioI'm not sure I buy that, though.27/10 10:55
Saizani imagine it's also hard to interface with GHC's produced code at the native code level if you want an Haskell FFI27/10 10:58
Saizan..unless you go via C27/10 10:59
edwinbI'm not sure that's a big problem even if you go via, say, LLVM, since you can still get at the GHC run time system27/10 11:00
edwinbit would be a bit more work of course27/10 11:00
pigworkerTrying to piggy-back on GHC's optimizations seems fun in the short term, but I rather suspect it's possible to do better by retaining more information. And we can hardly beat GHC if we go via GHC, can we?27/10 12:00
dolioYeah.27/10 12:03
glguyTo jump into a discussion from 6 hours ago; compiling to Haskell via pages of unsafeCoerce# isn't particularly appealing to Haskell programmers.27/10 17:30
edwinbwhat about if all the unsafeCoerce# could be removed?27/10 17:30
glguyThen it might be at least *interesting*?27/10 17:30
glguyas it stands it seems a novelty27/10 17:31
edwinbThe only other advantage I could think of is that you'd generate readable, editable code. But if you're going to do that, I hope you'd want to do it in Agda instead...27/10 17:31
pumpkinit'd be nice to be able to export haskell interfaces, but not go via GHC :)27/10 17:33
glguyI'd like to see functions that *could* be typed in Haskell have Haskell types in their generated code. I think it is much more likely a usecase that Agda generated libraries could be used in a Haskell program27/10 17:34
edwinbyes, you'd just need to export an interface for that27/10 17:36
pigworkerI'd like to see Agda achieve an honourable escape from Haskell, whilst remaining friendly ties, like a Swedish version of the American revolution.27/10 17:40
pigworker*retaining27/10 17:40
glguyWhat does escaping Haskell enable Agda to do?27/10 17:41
pumpkinavoid tag checks on constructors when they aren't necessary!! :P27/10 17:42
pumpkin(just kidding)27/10 17:42
glguyWhy j/k?27/10 17:42
pumpkinwell, I'm not sure that's "haskell can't do it" as much as "GHC, in certain situations, can't see that tag checks are unnecessary, and none of the GHC gurus seems interested in fixing that"27/10 17:43
edwinbI'm not convinced that's a huge win in general, but I suppose it might enable further optimisations27/10 17:45
edwinbIn any case, we can't expect the GHC gurus to fix stuff just because it'll make some non-Haskell compiler faster...27/10 17:47
pumpkinyeah, I wasn't suggesting that :)27/10 17:47
pigworkerAgda should stand on its own feet (implementation in Agda, etc). Agda should look to Haskell for lessons to learn but not necessarily patterns to emulate. The Haskell community, lovely though it is, exerts a powerful groupthink which is not necessarily healthy for dependently typed language design.27/10 17:48
pumpkina self-hosting DT language implementation sounds like a lot of work (well, assuming it had proofs about the implementation) :) but I'd love to see one27/10 17:49
pigworkerI used to think it was a long way off, and then I wrote the Kipling paper.27/10 17:49
pumpkinwhich is that?27/10 17:50
pumpkinI don't think I've seen it27/10 17:50
pigworker"Outrageous but Meaningful Coincidences"27/10 17:50
edwinbSo we can have an implementation if we're willing to wait for it to run...27/10 17:51
pumpkinoh I see27/10 17:52
edwinbI expect the hardest parts would be the bits around the edges... the interface, parsing, etc27/10 17:52
pigworkerI think the big delay in using that code base isn't the interpreter: I think it arises from using Agda's constraint-solving machinery as a dependent typechecker. You have to wait for it to *start* running.27/10 17:53
edwinbbut that's probably just a Simple Matter Of Programming27/10 17:53
pigworkerSo, parser libraries are on their way. We need some constraint-solving tech now.27/10 17:54
glguyMaybe in getting off GHC, we can get away from code.haskell.org!27/10 18:08
glguy(and its uptime issues)27/10 18:08
pumpkinthat'd be nice :)27/10 19:00
danbrowncopumpkin: you're in boston now?27/10 20:43
pumpkindanbrown: not yet :/27/10 20:45
pumpkingoing to miss the bostonhaskell meeting27/10 20:46
danbrownare you moving here at some point?27/10 20:46
pumpkinyeah, a couple of weeks27/10 20:46
danbrowncool! we should grab drinks or something27/10 20:47
pumpkinsounds good! I'll let you know when I actually get there, as I don't even have a ticket yet :)27/10 20:47
danbrownalright27/10 20:48
danbrownfeel free to shoot me an email (jdanbrown@gmail.com)27/10 20:48
pumpkinwe should start up the bostonagda meetup! :P27/10 20:48
pumpkincool, will do27/10 20:48
danbrownprobably won't run into you at bostonhaskell—i tend not to go27/10 20:48
pumpkinah okay27/10 20:49
danbrownbut i probably should go :P27/10 20:49
pumpkinit can be fun27/10 20:49
djahandariepumpkin, you're going to miss the meeting??27/10 20:53
pumpkinyeah27/10 20:53
pumpkin:(27/10 20:53
djahandarieWhat27/10 20:53
djahandarieGrr27/10 20:53
pumpkin:P27/10 20:53
pumpkinI'll definitely be at the one afterwards though27/10 20:53
* djahandarie intimidates pumpkin into coming27/10 20:53
pumpkinhey, I'm in florida now27/10 20:53
pumpkinand don't have a plane ticket to boston27/10 20:53
pumpkinand need to be in florida at least until next week27/10 20:53
pumpkin:P27/10 20:53
djahandarieWho planned you talking on Friday exactly? :P27/10 20:54
pumpkinedwardk did :P27/10 20:54
pumpkinI said I might be in boston by the end of the month and next I knew I was on the email giving a talk about agda27/10 20:54
djahandarieHahaha27/10 20:54
pumpkinwell, I had told him I wouldn't mind giving a talk at some point27/10 20:55
pumpkinso it wasn't exactly a surprise :P27/10 20:55
djahandarieThere's no way I can come up with a good presentation within 2 days so I dunno what's going to happen after ddarius27/10 20:57
pumpkinI already told edwardk a few days ago I wouldn't make it27/10 20:58
pumpkinand he never has any trouble talking about things, so if he can't find anyone else I'm sure he'll talk about something of his own :)27/10 20:58
djahandarieAnd it'll be something incredibly complicated probably27/10 20:59
pumpkinnah, he's usually pretty clear27/10 20:59
djahandarieI didn't say otherwise27/10 20:59
pumpkinwell, I mean27/10 20:59
pumpkinhe doesn't do excessively esoteric stuff in his talks at bostonhaskell27/10 20:59
pumpkinin my experience27/10 20:59
djahandarieAh alright27/10 20:59
glguyAt one point weren't . patterns actually checked?27/10 21:57
Saizanthey aren't currently?27/10 21:58
glguysay: example : (i j : N) -> i == j -> Whatever ; example (.i) i refl = ?27/10 21:58
glguyit seems like you can type whatever you want in them27/10 21:58
glguyas long as the names are in scope27/10 21:58
pumpkin:O27/10 21:58
glguyoh, its only in some cases that it doesn't check them27/10 21:59
glguynot all27/10 21:59
glguyI'm having trouble simplifying my current case27/10 22:00
glguyhttp://hpaste.org/40929/unchecked__pattern27/10 22:02
glguyit seem slike I can type whatever I want in that last line27/10 22:02
glguyand while we are on that paste, what is the right way to pattern match on both i \le\' j and j \le\' k?27/10 22:07
Saizana lambda seems pretty weird in particular27/10 22:08
glguyI threw that in for maximum absurdity :)27/10 22:08
glguybut it doesn't have to be one27/10 22:09
pumpkinprobably a bug?27/10 22:11
glguyI have had many cases where . patterns weren't checked, so I typically just write them as ._ now to avoid depending on what value it claims27/10 22:12
--- Day changed Thu Oct 28 2010
Spockzcopumpkin: why are you sometimes named "copumpkin" and the other time "pumpkin"?28/10 14:09
edwinbMaybe it depends whether he's being productive or not28/10 14:49
copumpkin_anyone have agda running on GHC 7?28/10 23:40
dolioDoubtful.28/10 23:40
copumpkin_ugh, haskell-src depends on base 328/10 23:52
dolioYeah.28/10 23:53
copumpkin_and agda depends on haskell-src :(28/10 23:54
* copumpkin_ sighs28/10 23:54
dolioI know. I discovered that trying to install it on GHC 7.28/10 23:54
dolioI bumped the haskell-src dependency, and it seemed to compile fine.28/10 23:54
dolioBut I think I got stuck on something else, too.28/10 23:55
copumpkin_so you just went back to 6.12 for the mean time?28/10 23:55
dolioYeah.28/10 23:55
--- Day changed Fri Oct 29 2010
glguyname suggestions?29/10 05:35
glguy∀ n → Data.Sign.+ ◃ n ≡ + n29/10 05:35
glguy(n : ℤ) → Data.Sign.+ ◃ n ≡ + n29/10 05:36
lispyglguy: Bill and Ted29/10 05:54
Spockzcopumpkin: how are you today?29/10 10:20
Spockzhi copumpkin are you here?29/10 16:03
copumpki_yeah29/10 16:06
copumpki_I'm going to approach the highlighting problem differently29/10 16:06
copumpki_just patching agda to have a nicer interface, rather than working around it and duplicating code in my own module29/10 16:07
copumpki_it'll take a little longer but will be a lot nicer29/10 16:07
copumpki_frustrated that I can't use GHC 7 with agda though :(29/10 16:07
copumpki_Spockz1: :O29/10 16:10
Spockz1copumpki_: what's :O?29/10 16:11
Spockz1I mean, what's up?29/10 16:11
copumpki_:P29/10 16:11
copumpki_http://snapplr.com/mht629/10 16:11
Spockz1copumpki_: that sounds very good :)29/10 16:15
Spockz1Why can't you use ghc 7 anyways?29/10 16:15
copumpki_agda won't compile with it29/10 16:18
copumpki_its dependencies, rather29/10 16:18
Spockz1ah, that's said :(29/10 16:19
Spockz1*sad29/10 16:19
Spockz1which client are you using btw?29/10 16:20
copumpki_IRC client?29/10 16:20
copumpki_textual on mac29/10 16:20
pumpkinsrc/Data/Record/Label/TH.hs:5:1:29/10 21:35
pumpkin    Bad interface file: /Users/pumpkin/.cabal/lib/template-haskell-2.4.0.1/ghc-7.0.0.20101028/Language/Haskell/TH/Syntax.hi29/10 21:35
pumpkin 29/10 21:35
pumpkinwhen trying to build fclabels on 7.0 RC229/10 21:36
pumpkinit built TH before that, but for some reason doesn't like the .hi file29/10 21:36
pumpkinwhy did I ask that in here? it was meant for #ghc29/10 22:55
pumpkinlol29/10 22:55
--- Day changed Sat Oct 30 2010
cadsHow closely can agda be married to haskell?30/10 00:33
cadsMore to the point, how closesly has agda been married to haskell?30/10 00:34
Saizanwhat do you mean by married?30/10 00:34
Saizanhave you seen the haskell FFI?30/10 00:34
cadsI've seen it wrap c functions30/10 00:35
Saizanthat's the FFI in haskell for C, agda has its own FFI to import haskell libs :)30/10 00:36
cadsby married I just mean that there'd be facilities for writing programs that span between agda and haskell30/10 00:36
Saizanhttp://wiki.portal.chalmers.se/agda/agda.php?n=Docs.FFI30/10 00:36
cadsin a way that'd give a kind of programming synergy rather than being a less efficient than using purely one language30/10 00:37
cadsand I'm asking whether anyone's demonstrated haskell/agda hybrid systems30/10 00:37
cadsoooo30/10 00:38
cadsSaizan, I'm sorry, dude30/10 00:39
cadsI thought you were talking about haskell's FFI30/10 00:39
Saizanyeah, "haskell FFI" is pretty ambiguous30/10 00:41
Spockzpumpkin: ghc 7 troubles? :P30/10 09:37
--- Day changed Sun Oct 31 2010
benmachinesuppose I have f : A → B, g : B → A, is it possible to prove f (g x) == x without requiring A to be non-empty?31/10 01:09
benmachineI guess the concept doesn't make sense31/10 01:09
benmachinebut in principle there's a bijection between Unit \times A and A even if A is empty31/10 01:10
dolioIf A is empty, then so is B.31/10 01:11
dolioSo naturally f (g x) = x.31/10 01:12
benmachinedolio: right31/10 01:12
benmachinedolio: but I don't know how to produce an f (g x) == x without having an x first31/10 01:12
benmachineso it seems like my proof requires A nonempty31/10 01:13
dolioI'm not sure how you can hope to prove something like that without knowing what A, B, f and g are.31/10 01:13
benmachinedolio: neither am I :P31/10 01:13
dolioIt certainly is not true for all A, B, f and g.31/10 01:13
benmachineoh I know what f and g are31/10 01:13
benmachinef is A → Unit \times A, and g is vice versa31/10 01:14
* benmachine brb31/10 01:14
dolioYou only know the types?31/10 01:14
benmachineno31/10 01:17
benmachineok I will show you the whole thing, one sec :P31/10 01:18
benmachinehmm no I will make it typecheck first, then I will show you it and explain why I am dissatisfied31/10 01:18
benmachinehere we go http://hpaste.org/40999/benmachine31/10 01:20
benmachinethis is my proof that there is a bijection between (Unit \times A) and A31/10 01:21
benmachinebut it only works on non-empty A31/10 01:21
benmachineit would be nice if it worked on all A, given that it is trivially true for empty A31/10 01:21
benmachineis this possible31/10 01:21
benmachinealso I'm still new to agda so if I've done terrible things please tell me31/10 01:21
dolioI don't see anything there that requires A to be non-empty.31/10 01:22
benmachinedolio: the left identity proof has an implicit argument of type A, which I can't provide if it's empty31/10 01:22
benmachineor am I thinking about that in the wrong way31/10 01:22
dolioOh, yes, I see.31/10 01:23
dolioThe problem is that your definition of Bijection is wrong.31/10 01:23
benmachinemm I thought it might be31/10 01:23
benmachinehow could it be improved?31/10 01:24
dolioBijection is: exists f g x y. g (f x) = x /\ f (g y) = y31/10 01:24
dolioYou want: exists f g. (forall x. g (f x) = x) /\ (forall y. f (g y) = y)31/10 01:24
benmachineoh, yes I do31/10 01:25
dolioWhen you do that, injout and outinj will receive an A parameter.31/10 01:25
dolioOr, they already do.31/10 01:25
dolioBut you take my meaning.31/10 01:25
benmachineis this what I'm looking for?   bijection : (f : A → B)(g : B → A) → ((x : A) → g (f x) == x) → ((y : B) → f (g y) == y) → Bijection A B31/10 01:26
dolioYes.31/10 01:27
benmachineright, thanks31/10 01:27
* benmachine fiddles31/10 01:27
benmachineyesss, much better31/10 01:28
benmachinethanks again :)31/10 01:29
* benmachine moves on to trying to prove Bijection (Fin n) (Fin m) → n == m31/10 01:35
liyangAnyone awake? :-/31/10 04:06
* Saizan raises an hand31/10 04:07
liyangI'm sure there's an easy enough proof of foo : ∀ {xs : List ℕ} {x} → xs ≢ x ∷ xs , but I can't see it…31/10 04:07
Saizaninduction on xs?31/10 04:08
liyangTry it. :-/31/10 04:08
Saizanah, annoying.31/10 04:10
jmcarthurhttp://www.reddit.com/r/agda/    <-- "There doesn't seem to be anything here"31/10 04:12
jmcarthurthis must change31/10 04:12
jmcarthureverybody hype agda up with a bunch of blog posts31/10 04:13
jmcarthurmonad tutorials in agda anybody? ;)31/10 04:13
Saizanfoo : ∀ {xs : List ℕ} {x} → xs ≢ x ∷ xs31/10 04:14
Saizanfoo {[]} ()31/10 04:14
Saizanfoo {x ∷ xs} eq = foo (lemma eq) where lemma : ∀ {x : ℕ} { y xs ys} -> x ∷ xs ≡ y ∷ ys -> xs ≡ ys lemma refl = refl31/10 04:14
Saizanugh31/10 04:14
Saizanliyang: http://hpaste.org/41002/xs__x__xs31/10 04:14
Saizanjmcarthur: i think it was decided to keep Agda, Coq, ... all together as a big friendly family http://www.reddit.com/r/dependent_types31/10 04:17
dolioI don't really even understand why that was created, when r/types already existed.31/10 04:19
liyangSaizan: it's so fugly though. ;_;31/10 04:19
liyangIt already tells me that it “Cannot pattern match on constructor ≡.refl, since the inferred31/10 04:20
liyangindices [xs] cannot be unified with the expected indices [x ∷ xs]”31/10 04:20
dolioThere's also r/Coq, but that's pretty much dead.31/10 04:21
Saizanliyang: foo {x ∷ xs} eq = foo (cong (drop 1) eq), if you prefer31/10 04:21
Saizanliyang: anyhow, i think there's an issue on the bugtracker about making such equalities obviously empty31/10 04:22
pumpkinjmcarthur: I'm hoping to help with that when I finish my agda highlighter31/10 04:24
pumpkineveryone and their mom will be blogging about agda with beautiful, 100% accurate highlighting31/10 04:27
pumpkin;)31/10 04:27
jmcarthurhehe31/10 04:28
liyangSaizan: found it— http://code.google.com/p/agda/issues/detail?id=29131/10 04:34
liyang(or at least, one of them.)31/10 04:34
Saizanliyang: that's the one i was thinking of31/10 04:35
Saizanthe tricky part is that it's not necessarily empty for coinductive types, i guess?31/10 04:36

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