font is in fact not entirely monospacesd                                                                                                                                                                                                                                                                                                                                               23/10 00:41
I've noticed :)                                                                                                                                                                                                                                                                                                                                                                                  23/10 00:41
i've check some of the online foundries, but there are no nice fonts that support most unicode chars and are monospace                                                                                                                                                                                                                                                                           23/10 00:41
:(                                                                                                                                                                                                                                                                                                                                                                                               23/10 00:41
so that leaves us with for instance computer modern or dejavu sans or the monospace font that is included on linux computer                                                                                                                                                                                                                                                                      23/10 00:42
know of any freely licensed fonts that support that and that we could convert to web fontyness?                                                                                                                                                                                                                                                                                                  23/10 00:42
^^ :)                                                                                                                                                                                                                                                                                                                                                                                            23/10 00:42
ah                                                                                                                                                                                                                                                                                                                                                                                               23/10 00:42
computer modern isn't my favorite font                                                                                                                                                                                                                                                                                                                                                           23/10 00:42
no it's quite bad actually if it's not printed                                                                                                                                                                                                                                                                                                                                                   23/10 00:42
deja vu is okay                                                                                                                                                                                                                                                                                                                                                                                  23/10 00:43
is there a webfonty version of it?                                                                                                                                                                                                                                                                                                                                                               23/10 00:43
i'm not sure what font by default is shipped with debian for instance, but kosmikus uses that in emacs and it looks very good                                                                                                                                                                                                                                                                    23/10 00:43
i think you can just host the .tff fonts locally and embed them in you page                                                                                                                                                                                                                                                                                                                      23/10 00:43
.ttf                                                                                                                                                                                                                                                                                                                                                                                             23/10 00:43
oh, that works? cool                                                                                                                                                                                                                                                                                                                                                                             23/10 00:43
I guess I want dejavu mono                                                                                                                                                                                                                                                                                                                                                                       23/10 00:44
or even .otf                                                                                                                                                                                                                                                                                                                                                                                     23/10 00:44
hm wait i just did this for my emacs locally, on moment                                                                                                                                                                                                                                                                                                                                          23/10 00:44
grr can't find.. sorry                                                                                                                                                                                                                                                                                                                                                                           23/10 00:47
that works nicely                                                                                                                                                                                                                                                                                                                                                                                23/10 00:49
dejavu sans mono                                                                                                                                                                                                                                                                                                                                                                                 23/10 00:49
I thought it missed some important characters                                                                                                                                                                                                                                                                                                                                                    23/10 00:49
I dunno, I'm just testing it on my simple test page                                                                                                                                                                                                                                                                                                                                              23/10 00:49
like disjoint union                                                                                                                                                                                                                                                                                                                                                                              23/10 00:49
my page has that                                                                                                                                                                                                                                                                                                                                                                                 23/10 00:50
y0 nice                                                                                                                                                                                                                                                                                                                                                                                          23/10 00:50
jup that is much better                                                                                                                                                                                                                                                                                                                                                                          23/10 00:51
http://snapplr.com/8t49                                                                                                                                                                                                                                                                                                                                                                          23/10 00:51
not a fan of the forall                                                                                                                                                                                                                                                                                                                                                                          23/10 00:51
but whatever                                                                                                                                                                                                                                                                                                                                                                                     23/10 00:51
how is "triple equals"?                                                                                                                                                                                                                                                                                                                                                                          23/10 00:51
but this looks a lot better than before                                                                                                                                                                                                                                                                                                                                                          23/10 00:52
i mean, at least it's monospaced :P                                                                                                                                                                                                                                                                                                                                                              23/10 00:52
yeah :P                                                                                                                                                                                                                                                                                                                                                                                          23/10 00:52
just looking at triple equals in a glyph viewer looks fine to me                                                                                                                                                                                                                                                                                                                                 23/10 00:53
man, soon we'll have craploads of blogposts with pretty agda in them                                                                                                                                                                                                                                                                                                                             23/10 00:53
I hope                                                                                                                                                                                                                                                                                                                                                                                           23/10 00:53
what did you write it in?                                                                                                                                                                                                                                                                                                                                                                        23/10 00:53
write what?                                                                                                                                                                                                                                                                                                                                                                                      23/10 00:53
that formatter                                                                                                                                                                                                                                                                                                                                                                                   23/10 00:53
oh, it's haskell, using the agda API                                                                                                                                                                                                                                                                                                                                                             23/10 00:53
k                                                                                                                                                                                                                                                                                                                                                                                                23/10 00:54
are you sharing the code?                                                                                                                                                                                                                                                                                                                                                                        23/10 00:54
yeah, when I get back to my computer that has the code on it :)                                                                                                                                                                                                                                                                                                                                  23/10 00:54
since I don't have it myself right now                                                                                                                                                                                                                                                                                                                                                           23/10 00:54
just the sample output I put up on my website                                                                                                                                                                                                                                                                                                                                                    23/10 00:54
cool                                                                                                                                                                                                                                                                                                                                                                                             23/10 00:54
it's also horribly ugly code                                                                                                                                                                                                                                                                                                                                                                     23/10 00:54
since the agda api loves using files                                                                                                                                                                                                                                                                                                                                                             23/10 00:55
so you can only ask it to typecheck/highlight files                                                                                                                                                                                                                                                                                                                                              23/10 00:55
so I need to generate temporary files and so on                                                                                                                                                                                                                                                                                                                                                  23/10 00:55
(and it likes to make sure the file name is correct)                                                                                                                                                                                                                                                                                                                                             23/10 00:55
no streams :( alright,  i'll put it in a container and use a stick to access it then                                                                                                                                                                                                                                                                                                             23/10 00:55
and removing that restriction requires lots of duplication of their code                                                                                                                                                                                                                                                                                                                         23/10 00:55
oh no, I handle that for you                                                                                                                                                                                                                                                                                                                                                                     23/10 00:55
you give it a string of agda code (or literate agda + markdown)                                                                                                                                                                                                                                                                                                                                  23/10 00:56
and it'll spit out the html or an intermediate format                                                                                                                                                                                                                                                                                                                                            23/10 00:56
nice                                                                                                                                                                                                                                                                                                                                                                                             23/10 00:56
the 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 code                                                                                                                                                                                                           23/10 00:57
sweet. looking forward to using it                                                                                                                                                                                                                                                                                                                                                               23/10 00:57
:)                                                                                                                                                                                                                                                                                                                                                                                               23/10 00:58
I also want to make a lightweight version                                                                                                                                                                                                                                                                                                                                                        23/10 00:58
in python? ;)                                                                                                                                                                                                                                                                                                                                                                                    23/10 00:58
since the current one requires full typechecking before it can highlight it                                                                                                                                                                                                                                                                                                                      23/10 00:58
lol no                                                                                                                                                                                                                                                                                                                                                                                           23/10 00:58
just kidding, i'm running my site using python                                                                                                                                                                                                                                                                                                                                                   23/10 00:58
that's for the most accurate highlighting, since constructors can't be determined until typechecking                                                                                                                                                                                                                                                                                             23/10 00:58
but most people don't care and I could probably get away with just parsing                                                                                                                                                                                                                                                                                                                       23/10 00:58
omg python                                                                                                                                                                                                                                                                                                                                                                                       23/10 00:59
I've just been using hakyll                                                                                                                                                                                                                                                                                                                                                                      23/10 00:59
*shrug*                                                                                                                                                                                                                                                                                                                                                                                          23/10 00:59
is there a nice blog/cms in haskell?                                                                                                                                                                                                                                                                                                                                                             23/10 00:59
I dunno, hakyll seems pretty nice to me                                                                                                                                                                                                                                                                                                                                                          23/10 00:59
but I'm a fan of static site generators                                                                                                                                                                                                                                                                                                                                                          23/10 00:59
hmm me too, just generate from your SCM                                                                                                                                                                                                                                                                                                                                                          23/10 01:00
that's what hakyll does                                                                                                                                                                                                                                                                                                                                                                          23/10 01:00
and quite nicely                                                                                                                                                                                                                                                                                                                                                                                 23/10 01:00
did you intergrate this with khakyll?                                                                                                                                                                                                                                                                                                                                                            23/10 01:00
not yet                                                                                                                                                                                                                                                                                                                                                                                          23/10 01:00
but you will.. alright nice                                                                                                                                                                                                                                                                                                                                                                      23/10 01:00
I 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 since                                                                                                                                                                                                                                         23/10 01:00
but yeah, I definitely intend to make a nice hakyll interface and another interface for things like wikis (or hpaste) to use                                                                                                                                                                                                                                                                     23/10 01:01
interesting, i'll try hakyll later                                                                                                                                                                                                                                                                                                                                                               23/10 01:02
jaspervdj, the main developer, is also very responsive and efficient :P                                                                                                                                                                                                                                                                                                                          23/10 01:02
nice, pandoc                                                                                                                                                                                                                                                                                                                                                                                     23/10 01:03
this looks sweet..                                                                                                                                                                                                                                                                                                                                                                               23/10 01:03
thanks. now i need to get back to understanding observational equality :) ttyl later                                                                                                                                                                                                                                                                                                             23/10 01:04
good luck!                                                                                                                                                                                                                                                                                                                                                                                       23/10 01:04
cheers                                                                                                                                                                                                                                                                                                                                                                                           23/10 01:04
pumpkin: you made a highlighter based on the Agda code on hackage?                                                                                                                                                                                                                                                                                                                               23/10 10:29
Spockz:not on hackage yet                                                                                                                                                                                                                                                                                                                                                                        23/10 16:38
but the rest is right                                                                                                                                                                                                                                                                                                                                                                            23/10 16:38
pumpkin: I did this for haskell: http://alessandrovermeulen.me/projects/lhs2texhl/                                                                                                                                                                                                                                                                                                               23/10 16:39
cool                                                                                                                                                                                                                                                                                                                                                                                             23/10 16:41
and I want to do the same thing for agda, but then I need to talk to the agda lib in order to parse                                                                                                                                                                                                                                                                                              23/10 16:42
and I see that you have experience with that :)                                                                                                                                                                                                                                                                                                                                                  23/10 16:42
it's not exactly pleasant                                                                                                                                                                                                                                                                                                                                                                        23/10 16:43
that's what I fear :P                                                                                                                                                                                                                                                                                                                                                                            23/10 16:43
i don't like how syntax highlighters will treat some functions as special and others as not special                                                                                                                                                                                                                                                                                              23/10 17:26
jmcarthur: do you have an example?                                                                                                                                                                                                                                                                                                                                                               23/10 17:26
*some syntax highlighters                                                                                                                                                                                                                                                                                                                                                                        23/10 17:27
mine doesn't                                                                                                                                                                                                                                                                                                                                                                                     23/10 17:27
for example: https://docs.google.com/viewer?url=http://alessandrovermeulen.me/wp-content/2010/10/LiterateHighlighter.pdf                                                                                                                                                                                                                                                                         23/10 17:27
mine even reconises variables that are being used as functions                                                                                                                                                                                                                                                                                                                                   23/10 17:27
why is length special but getArgs not?                                                                                                                                                                                                                                                                                                                                                           23/10 17:27
oh                                                                                                                                                                                                                                                                                                                                                                                               23/10 17:27
sorry :p                                                                                                                                                                                                                                                                                                                                                                                         23/10 17:27
it isn't a function                                                                                                                                                                                                                                                                                                                                                                              23/10 17:27
oh i see                                                                                                                                                                                                                                                                                                                                                                                         23/10 17:27
that's because getArgs isn't used as a function, no application                                                                                                                                                                                                                                                                                                                                  23/10 17:27
functions are special, values are not                                                                                                                                                                                                                                                                                                                                                            23/10 17:27
okay                                                                                                                                                                                                                                                                                                                                                                                             23/10 17:27
but I see what you mean                                                                                                                                                                                                                                                                                                                                                                          23/10 17:27
but main isn't highlighted because it has no binding and isn't used as a function so I can't recognise it                                                                                                                                                                                                                                                                                        23/10 17:28
that's a bug in haskell-src-exts I think                                                                                                                                                                                                                                                                                                                                                         23/10 17:28
now that i understand the method to the madness i think it's okay                                                                                                                                                                                                                                                                                                                                23/10 17:28
jmcarthur: how about http://pumpkinpat.ch/moo.html :P                                                                                                                                                                                                                                                                                                                                            23/10 17:28
some syntax highlighters do actually do that                                                                                                                                                                                                                                                                                                                                                     23/10 17:28
yeah, the one in textmate does                                                                                                                                                                                                                                                                                                                                                                   23/10 17:28
agda is probably really hard to get right                                                                                                                                                                                                                                                                                                                                                        23/10 17:28
my highlighter does get it right ;)                                                                                                                                                                                                                                                                                                                                                              23/10 17:29
but it can only highlight constructors green after a typechecking pass                                                                                                                                                                                                                                                                                                                           23/10 17:29
but on the other hand, easy, because it's kind of pointless to treat certain functions as special :)                                                                                                                                                                                                                                                                                             23/10 17:29
ah                                                                                                                                                                                                                                                                                                                                                                                               23/10 17:29
i like the highlighted constructors                                                                                                                                                                                                                                                                                                                                                              23/10 17:29
but that page is the result of a full typecheck highlighting                                                                                                                                                                                                                                                                                                                                     23/10 17:29
me too, but it's not feasible for general purpose highlighting                                                                                                                                                                                                                                                                                                                                   23/10 17:29
I often wish that haskell had the same feature                                                                                                                                                                                                                                                                                                                                                   23/10 17:30
i 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 free                                                                                                                                                                                                                              23/10 17:30
but i don't know                                                                                                                                                                                                                                                                                                                                                                                 23/10 17:30
like, using a top level function would be different that using one bound by a pattern/lambda                                                                                                                                                                                                                                                                                                     23/10 17:31
*than                                                                                                                                                                                                                                                                                                                                                                                            23/10 17:31
ah                                                                                                                                                                                                                                                                                                                                                                                               23/10 17:31
I'm going to set up webfonts soon so we can get a true monospace font on that page too                                                                                                                                                                                                                                                                                                           23/10 17:31
in haskell, types complicate that because there are actually *are* free variables (due to the usually implicit forall)                                                                                                                                                                                                                                                                           23/10 17:31
the one in textmate does what?                                                                                                                                                                                                                                                                                                                                                                   23/10 17:32
*there actually                                                                                                                                                                                                                                                                                                                                                                                  23/10 17:32
Spockz: highlights certain functions it knows about differently from other functions                                                                                                                                                                                                                                                                                                             23/10 17:32
pumpkin: a "true" monospace font?                                                                                                                                                                                                                                                                                                                                                                23/10 17:32
what's not true about it as is?                                                                                                                                                                                                                                                                                                                                                                  23/10 17:32
pumpkin: yes it highlights prelude functions differently                                                                                                                                                                                                                                                                                                                                         23/10 17:32
jmcarthur: the arrow in http://snapplr.com/bgeg is wider than the other constructors                                                                                                                                                                                                                                                                                                             23/10 17:32
your browser font might be better                                                                                                                                                                                                                                                                                                                                                                23/10 17:33
ah                                                                                                                                                                                                                                                                                                                                                                                               23/10 17:33
mine is set to menlo                                                                                                                                                                                                                                                                                                                                                                             23/10 17:33
does it look okay?                                                                                                                                                                                                                                                                                                                                                                               23/10 17:33
does the same thing you just said                                                                                                                                                                                                                                                                                                                                                                23/10 17:33
ah yeah                                                                                                                                                                                                                                                                                                                                                                                          23/10 17:33
on the other hand, using something like dejavu sans mono                                                                                                                                                                                                                                                                                                                                         23/10 17:33
i use menlo in emacs and it manages fine though                                                                                                                                                                                                                                                                                                                                                  23/10 17:33
i think it just resizes some things to fit                                                                                                                                                                                                                                                                                                                                                       23/10 17:33
I didn't find a font that is really good                                                                                                                                                                                                                                                                                                                                                         23/10 17:33
works fine and is nicely monospaced                                                                                                                                                                                                                                                                                                                                                              23/10 17:33
so I use courier now :)                                                                                                                                                                                                                                                                                                                                                                          23/10 17:33
it has all the characters I encountered                                                                                                                                                                                                                                                                                                                                                          23/10 17:33
here, let me show you dejavu sans mono on the same code                                                                                                                                                                                                                                                                                                                                          23/10 17:33
weird considering the origin of menlo                                                                                                                                                                                                                                                                                                                                                            23/10 17:33
http://snapplr.com/5pa2                                                                                                                                                                                                                                                                                                                                                                          23/10 17:34
that's with dejavu sans mono                                                                                                                                                                                                                                                                                                                                                                     23/10 17:34
pumpkin: but maybe I can encorporate some of your code in lhs2TeX-hl? :p                                                                                                                                                                                                                                                                                                                         23/10 17:34
Spockz: sure, but it's mostly just hacks around the unfriendly agda API :P                                                                                                                                                                                                                                                                                                                       23/10 17:35
oh actually it looks fine with menlo                                                                                                                                                                                                                                                                                                                                                             23/10 17:35
what part of it are you interested in?                                                                                                                                                                                                                                                                                                                                                           23/10 17:35
is menlo free?                                                                                                                                                                                                                                                                                                                                                                                   23/10 17:35
I'm mostly looking for stuff that I can webfontify                                                                                                                                                                                                                                                                                                                                               23/10 17:35
pumpkin: i was thinking that what you just linked me to was text, not an image :P                                                                                                                                                                                                                                                                                                                23/10 17:35
menlo comes with os x                                                                                                                                                                                                                                                                                                                                                                            23/10 17:35
:P                                                                                                                                                                                                                                                                                                                                                                                               23/10 17:35
ah                                                                                                                                                                                                                                                                                                                                                                                               23/10 17:35
pumpkin: the part where I give it a .lagda file and that it compiles/checks that for me and gives me a parse tree or something                                                                                                                                                                                                                                                                   23/10 17:35
it's apple's version of deja-vu, basically                                                                                                                                                                                                                                                                                                                                                       23/10 17:35
it's better, IMO                                                                                                                                                                                                                                                                                                                                                                                 23/10 17:36
deja-vu misses a lot of chars                                                                                                                                                                                                                                                                                                                                                                    23/10 17:36
not for me                                                                                                                                                                                                                                                                                                                                                                                       23/10 17:36
menlo does look okay                                                                                                                                                                                                                                                                                                                                                                             23/10 17:36
not that i've noticed anyway                                                                                                                                                                                                                                                                                                                                                                     23/10 17:36
Spockz: really? I haven't noticed any missing                                                                                                                                                                                                                                                                                                                                                    23/10 17:36
but that's only on this small sample                                                                                                                                                                                                                                                                                                                                                             23/10 17:36
menlo seems to behave nicely too                                                                                                                                                                                                                                                                                                                                                                 23/10 17:36
i use it as my main coding font. never had an issue                                                                                                                                                                                                                                                                                                                                              23/10 17:36
on this sample                                                                                                                                                                                                                                                                                                                                                                                   23/10 17:36
including with agda                                                                                                                                                                                                                                                                                                                                                                              23/10 17:36
Union, \—> \==> and some others                                                                                                                                                                                                                                                                                                                                                                  23/10 17:36
um                                                                                                                                                                                                                                                                                                                                                                                               23/10 17:37
those all work for me in menlo                                                                                                                                                                                                                                                                                                                                                                   23/10 17:37
no not union                                                                                                                                                                                                                                                                                                                                                                                     23/10 17:37
Union with a plus in it                                                                                                                                                                                                                                                                                                                                                                          23/10 17:37
what is the agda string for that?                                                                                                                                                                                                                                                                                                                                                                23/10 17:37
if any                                                                                                                                                                                                                                                                                                                                                                                           23/10 17:37
dejavu sans mono works with \u+                                                                                                                                                                                                                                                                                                                                                                  23/10 17:37
for me                                                                                                                                                                                                                                                                                                                                                                                           23/10 17:37
it's even in this code                                                                                                                                                                                                                                                                                                                                                                           23/10 17:37
let me screenshot it                                                                                                                                                                                                                                                                                                                                                                             23/10 17:37
oh it was in that screenshot                                                                                                                                                                                                                                                                                                                                                                     23/10 17:37
Spockz: \u+ works for me with menlo                                                                                                                                                                                                                                                                                                                                                              23/10 17:38
maybe the browser is being friendly and fetching the glyph from another font though                                                                                                                                                                                                                                                                                                              23/10 17:38
i'm in emacs                                                                                                                                                                                                                                                                                                                                                                                     23/10 17:38
works                                                                                                                                                                                                                                                                                                                                                                                            23/10 17:38
⊎    <- that is correct, right?                                                                                                                                                                                                                                                                                                                                                                  23/10 17:38
don't know                                                                                                                                                                                                                                                                                                                                                                                       23/10 17:38
works in my terminal too                                                                                                                                                                                                                                                                                                                                                                         23/10 17:38
\|-                                                                                                                                                                                                                                                                                                                                                                                              23/10 17:39
hmm                                                                                                                                                                                                                                                                                                                                                                                              23/10 17:39
odd                                                                                                                                                                                                                                                                                                                                                                                              23/10 17:39
well, anyway, i love menlo                                                                                                                                                                                                                                                                                                                                                                       23/10 17:39
http://snapplr.com/z0e4                                                                                                                                                                                                                                                                                                                                                                          23/10 17:40
hmm... 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 well                                                                                                                                                                                                                      23/10 17:40
when i asked if that symbol was correct i meant is that the correct symbol i should be testing with, not is that symbol rendering correctly                                                                                                                                                                                                                                                      23/10 17:43
by the way                                                                                                                                                                                                                                                                                                                                                                                       23/10 17:43
but yes that's the symbol                                                                                                                                                                                                                                                                                                                                                                        23/10 17:43
http://alessandrovermeulen.me/wp-content/2010/10/Screen-shot-2010-10-23-at-18.41.00.png                                                                                                                                                                                                                                                                                                          23/10 17:44
anyway, this is why menlo rocks http://typophile.com/files/menlovsdejavusansmono_6131.png                                                                                                                                                                                                                                                                                                        23/10 17:44
Spockz: i like that                                                                                                                                                                                                                                                                                                                                                                              23/10 17:44
i want to get pandoc and lhs2tex to play nice together                                                                                                                                                                                                                                                                                                                                           23/10 17:45
hmm                                                                                                                                                                                                                                                                                                                                                                                              23/10 17:45
didn't look into that                                                                                                                                                                                                                                                                                                                                                                            23/10 17:45
would that be a better solution?.                                                                                                                                                                                                                                                                                                                                                                23/10 17:46
than?                                                                                                                                                                                                                                                                                                                                                                                            23/10 17:46
lhs2TeX doesn't have that many formatting options                                                                                                                                                                                                                                                                                                                                                23/10 17:46
than what I presented?                                                                                                                                                                                                                                                                                                                                                                           23/10 17:46
my only reason is so i can use markdown instead of latex                                                                                                                                                                                                                                                                                                                                         23/10 17:46
not for highlighting                                                                                                                                                                                                                                                                                                                                                                             23/10 17:46
aah                                                                                                                                                                                                                                                                                                                                                                                              23/10 17:46
pandoc by itself doesn't do highlighting, although i think for html at least it can use some library to add highlighting                                                                                                                                                                                                                                                                         23/10 17:46
hscolour probably/                                                                                                                                                                                                                                                                                                                                                                               23/10 17:47
no it's something else                                                                                                                                                                                                                                                                                                                                                                           23/10 17:47
I didn't realize menlo and dejavu sans were so similar                                                                                                                                                                                                                                                                                                                                           23/10 17:47
and had the common ancestor                                                                                                                                                                                                                                                                                                                                                                      23/10 17:47
it's highlighting-kate                                                                                                                                                                                                                                                                                                                                                                           23/10 17:47
I'm not a fan of highlighting-kate                                                                                                                                                                                                                                                                                                                                                               23/10 17:47
i have only used it with pandoc. it was alright, but i didn't abuse it enough to pass final judgement                                                                                                                                                                                                                                                                                            23/10 17:48
there was some talk about making pandoc and lhs2tex play nice together, but i don't know if any code was ever released                                                                                                                                                                                                                                                                           23/10 17:49
they speaker said it was a lot of work to do himself :\                                                                                                                                                                                                                                                                                                                                          23/10 17:49
*the                                                                                                                                                                                                                                                                                                                                                                                             23/10 17:50
do you know the speaker?                                                                                                                                                                                                                                                                                                                                                                         23/10 17:50
no                                                                                                                                                                                                                                                                                                                                                                                               23/10 17:50
I don't know how hard it should bee                                                                                                                                                                                                                                                                                                                                                              23/10 17:51
oh but wait, i see an email from 2009 that claims it was possible even then...                                                                                                                                                                                                                                                                                                                   23/10 17:51
now i don't know what that talk was actually about. i thought it was new and hard                                                                                                                                                                                                                                                                                                                23/10 17:52
http://vimeo.com/15481736                                                                                                                                                                                                                                                                                                                                                                        23/10 17:53
ah malcolm wallace                                                                                                                                                                                                                                                                                                                                                                               23/10 17:53
o, that's not malcolm wallace                                                                                                                                                                                                                                                                                                                                                                    23/10 17:53
i tihnk just posted by him                                                                                                                                                                                                                                                                                                                                                                       23/10 17:54
*think                                                                                                                                                                                                                                                                                                                                                                                           23/10 17:54
not necessarily the speaker                                                                                                                                                                                                                                                                                                                                                                      23/10 17:54
no the speaker is Tillmann Rendel                                                                                                                                                                                                                                                                                                                                                                23/10 17:56
jmcarthur: Tillmann complained (and rightly so) that lhs2tex does not expose a library interface. The next release will probably do that.                                                                                                                                                                                                                                                        23/10 18:15
awesome!                                                                                                                                                                                                                                                                                                                                                                                         23/10 18:15
actually, I'd rather rewrite lhs2tex completely though. if only I had the time.                                                                                                                                                                                                                                                                                                                  23/10 18:16
pumpkin: do you have the code for that interface somewhere I can look at it?                                                                                                                                                                                                                                                                                                                     23/10 18:36
Spockz: let me dig it up                                                                                                                                                                                                                                                                                                                                                                         23/10 20:35
I warn you, it's horrible                                                                                                                                                                                                                                                                                                                                                                        23/10 20:36
Spockz: http://github.com/pumpkin/agda-highlight                                                                                                                                                                                                                                                                                                                                                 23/10 20:41
wooosh                                                                                                                                                                                                                                                                                                                                                                                           23/10 20:43
?                                                                                                                                                                                                                                                                                                                                                                                                23/10 20:43
I was warned, but still                                                                                                                                                                                                                                                                                                                                                                          23/10 20:45
oh at how ugly it is                                                                                                                                                                                                                                                                                                                                                                             23/10 20:45
yeah, I even hardcoded my local path into it                                                                                                                                                                                                                                                                                                                                                     23/10 20:45
it isn't intended for public consumption yet                                                                                                                                                                                                                                                                                                                                                     23/10 20:45
maybe I should start over                                                                                                                                                                                                                                                                                                                                                                        23/10 20:46
you're welcome to                                                                                                                                                                                                                                                                                                                                                                                23/10 20:46
or just wait a while and I'll have some more time to clean it up                                                                                                                                                                                                                                                                                                                                 23/10 20:47
the only thing I need is some extract                                                                                                                                                                                                                                                                                                                                                            23/10 20:47
problem is that with lhs2tex you can only replace strings, so you don't have context                                                                                                                                                                                                                                                                                                             23/10 20:48
ah                                                                                                                                                                                                                                                                                                                                                                                               23/10 20:49
so that's where lhs2tex 2.0 comes in :P                                                                                                                                                                                                                                                                                                                                                          23/10 20:50
oh so you need it for haskell or agda?                                                                                                                                                                                                                                                                                                                                                           23/10 20:50
cause I'm not sure there's anything of value to haskell in there                                                                                                                                                                                                                                                                                                                                 23/10 20:51
I've got the haskell part already                                                                                                                                                                                                                                                                                                                                                                23/10 20:51
so now I need the agda part                                                                                                                                                                                                                                                                                                                                                                      23/10 20:51
ah                                                                                                                                                                                                                                                                                                                                                                                               23/10 20:53
maybe import Agda.Syntax.Parser is enough                                                                                                                                                                                                                                                                                                                                                        23/10 20:54
could be                                                                                                                                                                                                                                                                                                                                                                                         23/10 20:54
that has a fair amount of information and doesn't have unnecessary file-based IOo                                                                                                                                                                                                                                                                                                                23/10 20:54
or doesn't force you to use files, anyway                                                                                                                                                                                                                                                                                                                                                        23/10 20:55
hmm the agda syntax is a bit more complex                                                                                                                                                                                                                                                                                                                                                        23/10 21:05
but maybe I can get a long way with just Expr                                                                                                                                                                                                                                                                                                                                                    23/10 21:07
--- Day changed Sun Oct 24 2010
Hello                                                                                                                                                                                                                                                                                                                                                                                            24/10 20:22
hi                                                                                                                                                                                                                                                                                                                                                                                               24/10 20:22
Do 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
That keeps producing an error                                                                                                                                                                                                                                                                                                                                                                    24/10 20:23
you probably want : and not :                                                                                                                                                                                                                                                                                                                                                                    24/10 20:23
::                                                                                                                                                                                                                                                                                                                                                                                               24/10 20:23
on all?                                                                                                                                                                                                                                                                                                                                                                                          24/10 20:24
but you also just need to look up the syntax :P                                                                                                                                                                                                                                                                                                                                                  24/10 20:24
that isn't valid syntax                                                                                                                                                                                                                                                                                                                                                                          24/10 20:24
Sorry im new to Agda. Trying to get my head round it all :)                                                                                                                                                                                                                                                                                                                                      24/10 20:24
data List' (X : Set) : Set where Nil : List' X; Con : (x : X) -> (List' X) -> List' X                                                                                                                                                                                                                                                                                                            24/10 20:25
forgot the xs                                                                                                                                                                                                                                                                                                                                                                                    24/10 20:25
Ah ok                                                                                                                                                                                                                                                                                                                                                                                            24/10 20:25
Is it ' or ? (Im not sure if you can see the difference there)                                                                                                                                                                                                                                                                                                                                  24/10 20:26
you can put either in                                                                                                                                                                                                                                                                                                                                                                            24/10 20:27
they're just different names                                                                                                                                                                                                                                                                                                                                                                     24/10 20:27
I used the wrong one :)                                                                                                                                                                                                                                                                                                                                                                          24/10 20:27
It keeps throwing me back: Perse error data List (X : Set) where N....                                                                                                                                                                                                                                                                                                                   24/10 20:28
Im using emacs and went to Agda-> Load after typing that in                                                                                                                                                                                                                                                                                                                                      24/10 20:29
maybe ` is reserved for something                                                                                                                                                                                                                                                                                                                                                                24/10 20:32
Still same problem. Is there a way to force emacs to do C-l instead of C-c?                                                                                                                                                                                                                                                                                                                      24/10 20:33
I don't know what you mean                                                                                                                                                                                                                                                                                                                                                                       24/10 20:33
C-c C-l is what you do to load it                                                                                                                                                                                                                                                                                                                                                                24/10 20:33
I see. I am doing that right then                                                                                                                                                                                                                                                                                                                                                                24/10 20:34
Im trying to follow the 'An Agda Tutorial' that was written in May 12, 2006. And I cant even get the examples to work :s lol                                                                                                                                                                                                                                                                     24/10 20:36
oh, that's probably agda1                                                                                                                                                                                                                                                                                                                                                                        24/10 20:38
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials                                                                                                                                                                                                                                                                                                                             24/10 20:38
Ah ok. Thanks - Ill have a look there                                                                                                                                                                                                                                                                                                                                                            24/10 20:39
I was forgetting the 'module ... where' part. But now I am faced with a: Parse error . All I have is :                                                                                                                                                                                                                                                                               24/10 20:44
module AgdaBasics where                                                                                                                                                                                                                                                                                                                                                                          24/10 20:44
data Bool : Set where                                                                                                                                                                                                                                                                                                                                                                            24/10 20:44
true  : Bool                                                                                                                                                                                                                                                                                                                                                                                     24/10 20:44
false  : Bool                                                                                                                                                                                                                                                                                                                                                                                    24/10 20:44
Does the program need to do something to load properly?                                                                                                                                                                                                                                                                                                                                          24/10 20:45
Examples from http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/agdalectureexamples/ will not load either with a parse error                                                                                                                                                                                                                                                               24/10 20:54
you need indentation and so on                                                                                                                                                                                                                                                                                                                                                                   24/10 20:54
Could you give me the simplest Agda2 example you can think of please? I just want to get something loaded, lol                                                                                                                                                                                                                                                                                   24/10 20:59
module Moo where                                                                                                                                                                                                                                                                                                                                                                                 24/10 21:02
data X : Set where                                                                                                                                                                                                                                                                                                                                                                               24/10 21:02
x : X                                                                                                                                                                                                                                                                                                                                                                              24/10 21:02
*creates a Moo.agda file and types that in* *loads up emacs* *opens file*                                                                                                                                                                                                                                                                                                                        24/10 21:03
Agda -> Load. Success :D:D                                                                                                                                                                                                                                                                                                                                                                       24/10 21:04
Thanks                                                                                                                                                                                                                                                                                                                                                                                           24/10 21:04
Really thanks :D                                                                                                                                                                                                                                                                                                                                                                                 24/10 21:04
And if I understand that right... X is a set, where x is a type of X?                                                                                                                                                                                                                                                                                                                            24/10 21:05
the type of X is Set, the type of x is X                                                                                                                                                                                                                                                                                                                                                         24/10 21:05
x is a constructor of X                                                                                                                                                                                                                                                                                                                                                                          24/10 21:05
Does the meaning of 'constructor' mean anything past: the type of x is X?                                                                                                                                                                                                                                                                                                                        24/10 21:07
you can pattern match against constructors                                                                                                                                                                                                                                                                                                                                                       24/10 21:07
I see                                                                                                                                                                                                                                                                                                                                                                                            24/10 21:07
So im assuming : is Adga2 and :: is Agda1?                                                                                                                                                                                                                                                                                                                                                       24/10 21:16
probably                                                                                                                                                                                                                                                                                                                                                                                         24/10 21:17
I've never used Agda1                                                                                                                                                                                                                                                                                                                                                                            24/10 21:17
Fair enough. I'm starting out and its not as easy as it would seem, lol                                                                                                                                                                                                                                                                                                                          24/10 21:17
How did you learn?                                                                                                                                                                                                                                                                                                                                                                               24/10 21:17
Personally I wish I had done Mathematics first and the computing                                                                                                                                                                                                                                                                                                                                 24/10 21:23
*then                                                                                                                                                                                                                                                                                                                                                                                            24/10 21:23
Is Haskell worth learning first, and then Agda?                                                                                                                                                                                                                                                                                                                                                  24/10 21:27
MrAI: It would definitely help, imo.                                                                                                                                                                                                                                                                                                                                                             24/10 21:29
Ok :D Thanks                                                                                                                                                                                                                                                                                                                                                                                     24/10 21:30
I spent half an hour reading through Haskell basics but cleary I need to go revisit it                                                                                                                                                                                                                                                                                                           24/10 21:31
unless you're experienced in another functional language with an interesting type system, I'd recommend a few months of haskell at least                                                                                                                                                                                                                                                         24/10 21:33
I dont have a few months. I have three weeks max to learn Haskell(maybe) and Agda2                                                                                                                                                                                                                                                                                                               24/10 21:35
I've taken on a really ambitious project                                                                                                                                                                                                                                                                                                                                                         24/10 21:36
well, you'd better be willing to dedicate a lot of time to it :)                                                                                                                                                                                                                                                                                                                                 24/10 21:43
agda actually feels a bit cleaner than haskell in terms of the constructs it provides                                                                                                                                                                                                                                                                                                            24/10 21:43
Im literally spending every waking for the next two weeks learning all this. And I dont have a functional programming past.                                                                                                                                                                                                                                                                      24/10 21:44
the main advantage of haskell as a start for this is that it's easier to play with and see what it does                                                                                                                                                                                                                                                                                          24/10 21:45
we typically don't "run" agda programs                                                                                                                                                                                                                                                                                                                                                           24/10 21:45
you can ask emacs to normalize an expression for you, which has a similar effect for many things                                                                                                                                                                                                                                                                                                 24/10 21:45
Haha yes I noticed that you dont 'run' agda programs :) Hard step that one                                                                                                                                                                                                                                                                                                                       24/10 21:45
well, you can do it                                                                                                                                                                                                                                                                                                                                                                              24/10 21:46
it just isn't ideal                                                                                                                                                                                                                                                                                                                                                                              24/10 21:46
there's also a repl apparently, agda -I                                                                                                                                                                                                                                                                                                                                                          24/10 21:46
it's unsupported though                                                                                                                                                                                                                                                                                                                                                                          24/10 21:47
Yes pumpkin from what im finding - I do agree.                                                                                                                                                                                                                                                                                                                                                   24/10 21:47
pumpkin: On the other hand, the discussions with the type checker are a lot longer and more intricate than in Haskell though, in my experience                                                                                                                                                                                                                                                   24/10 21:47
even with all the "uncleanliness" :)                                                                                                                                                                                                                                                                                                                                                             24/10 21:48
The one thing ive found coming from an OO background is I dont type as much, its alot more thinking                                                                                                                                                                                                                                                                                              24/10 21:48
hwo does agda claim to be (possibly) a dependently-typed programming language if you don't run things in it at all                                                                                                                                                                                                                                                                               24/10 21:49
because you can                                                                                                                                                                                                                                                                                                                                                                                  24/10 21:50
benmachine: you can, but the users who typically write things in it don't usually                                                                                                                                                                                                                                                                                                                24/10 21:50
and fairly easily                                                                                                                                                                                                                                                                                                                                                                                24/10 21:50
so you *can* program with it but no-one does >_>                                                                                                                                                                                                                                                                                                                                                 24/10 21:51
I program with it plenty                                                                                                                                                                                                                                                                                                                                                                         24/10 21:51
I just don't run the programs much                                                                                                                                                                                                                                                                                                                                                               24/10 21:51
haha okay                                                                                                                                                                                                                                                                                                                                                                                        24/10 21:51
if you choose to define programming as something you run, then I guess I don't program                                                                                                                                                                                                                                                                                                           24/10 21:51
i'm not sure if #agda is so representative, btw :)                                                                                                                                                                                                                                                                                                                                               24/10 21:52
for the purposes of this conversation I'm using program to mean doing stuff that exists for a reason other than to prove something                                                                                                                                                                                                                                                               24/10 21:52
cf. the dilemma in the topic                                                                                                                                                                                                                                                                                                                                                                     24/10 21:52
you could easily run the programs we write too                                                                                                                                                                                                                                                                                                                                                   24/10 21:53
* benmachine hasn't yet done anything in agda that isn't proofs                                                                                                                                                                                                                                                                                                                                               24/10 21:53
do programs that compute proofs count?                                                                                                                                                                                                                                                                                                                                                           24/10 21:53
we just happen to be satisfied with proving them correct                                                                                                                                                                                                                                                                                                                                         24/10 21:53
So what do you use Agda for then? If not to create programs you provide an input and expect an output?                                                                                                                                                                                                                                                                                           24/10 21:53
pumpkin: okay, that makes sense                                                                                                                                                                                                                                                                                                                                                                  24/10 21:53
MrAI: I usually write programs for something I care about, and then prove that they do what I want them to do                                                                                                                                                                                                                                                                                    24/10 21:54
and then move on to something else                                                                                                                                                                                                                                                                                                                                                               24/10 21:54
MrAI: all the agda I've written is successful if it typechecks                                                                                                                                                                                                                                                                                                                                   24/10 21:54
Ah ok                                                                                                                                                                                                                                                                                                                                                                                            24/10 21:54
(or fail to prove what I wanted to prove, and move on)                                                                                                                                                                                                                                                                                                                                           24/10 21:54
:P                                                                                                                                                                                                                                                                                                                                                                                               24/10 21:54
I see now                                                                                                                                                                                                                                                                                                                                                                                        24/10 21:54
I did read alot about how Agda can prove correctness                                                                                                                                                                                                                                                                                                                                             24/10 21:54
* benmachine got as far as proving the commutativity and distributivity of multiplication on natural numbers                                                                                                                                                                                                                                                                                                  24/10 21:55
* MrAI test                                                                                                                                                                                                                                                                                                                                                                                                   24/10 21:56
I was considering starting a different tack though                                                                                                                                                                                                                                                                                                                                               24/10 21:56
I proved multiplication was commutative by induction                                                                                                                                                                                                                                                                                                                                             24/10 21:56
which is natural because the definition of multiplication was inductive                                                                                                                                                                                                                                                                                                                          24/10 21:56
Proof by induction, proof by contradiction... I swear there was another                                                                                                                                                                                                                                                                                                                          24/10 21:56
general proof by contradiction in agda doesn't work                                                                                                                                                                                                                                                                                                                                              24/10 21:57
but 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 A                                                                                                                                                                                                                   24/10 21:57
Ah ok                                                                                                                                                                                                                                                                                                                                                                                            24/10 21:57
that would seem more natural, but I don't really know how to construct bijections and so forth in agda                                                                                                                                                                                                                                                                                           24/10 21:57
offhand I guess you could construct a datatype containing f, a proof of surjectivity, and a proof of injectivity                                                                                                                                                                                                                                                                                 24/10 21:58
or it might be easier to provide f and g and prove f (g x) == x                                                                                                                                                                                                                                                                                                                                  24/10 21:58
I dunno, anyone got any experience as to which is more sensible?                                                                                                                                                                                                                                                                                                                                 24/10 21:58
probably the latter                                                                                                                                                                                                                                                                                                                                                                              24/10 21:59
Im sorry I cant help - my math stopped at high school 7 years ago.                                                                                                                                                                                                                                                                                                                               24/10 21:59
yeah I'm not sure what surjectivity proofs would even look like short of just providing an inverse                                                                                                                                                                                                                                                                                               24/10 21:59
btw, maybe you don't even need to prove there's a bijection, just that the two sets are equipotent                                                                                                                                                                                                                                                                                               24/10 22:00
what's equipotence?                                                                                                                                                                                                                                                                                                                                                                              24/10 22:00
benmachine: my rusty latin skills suggest |A| = |B|                                                                                                                                                                                                                                                                                                                                              24/10 22:01
i'd represent it as just A -> B \x B -> A                                                                                                                                                                                                                                                                                                                                                        24/10 22:01
without any relation between the two functions                                                                                                                                                                                                                                                                                                                                                   24/10 22:02
Saizan: hmm                                                                                                                                                                                                                                                                                                                                                                                      24/10 22:03
maybe i'm being silly, i'm not fully awake yet :P                                                                                                                                                                                                                                                                                                                                                24/10 22:06
in fact you do need them to be inverses, otherwise it's easy to map multiple elements to just one                                                                                                                                                                                                                                                                                                24/10 22:09
yes                                                                                                                                                                                                                                                                                                                                                                                              24/10 22:09
or they could both be injections, I guess                                                                                                                                                                                                                                                                                                                                                        24/10 22:09
or both surjections                                                                                                                                                                                                                                                                                                                                                                              24/10 22:09
yep, but the useful definitions of those properties involve partial inverses                                                                                                                                                                                                                                                                                                                     24/10 22:10
...indeed                                                                                                                                                                                                                                                                                                                                                                                        24/10 22:10
how are you going to represent _has-cardinality_ ?                                                                                                                                                                                                                                                                                                                                               24/10 22:13
iono                                                                                                                                                                                                                                                                                                                                                                                             24/10 22:13
* benmachine still new to this tbh                                                                                                                                                                                                                                                                                                                                                                            24/10 22:13
X has-finite-cardinality n = bijection X (Fin n) :D                                                                                                                                                                                                                                                                                                                                              24/10 22:14
heh                                                                                                                                                                                                                                                                                                                                                                                              24/10 22:15
veeery possibly.                                                                                                                                                                                                                                                                                                                                                                                 24/10 22:15
oh dang it I have to prove left and right inverse separately                                                                                                                                                                                                                                                                                                                                     24/10 22:38
yeah, that's annoying                                                                                                                                                                                                                                                                                                                                                                            24/10 22:40
--- Day changed Mon Oct 25 2010
Is 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.html                                                                                                                                                                                                                                   25/10 08:27
I need lambdas with rewrite syntax :)                                                                                                                                                                                                                                                                                                                                                            25/10 08:27
What is the best rescource for Agda2? I keep finding tutorials and documents relating to Agda1                                                                                                                                                                                                                                                                                                   25/10 15:12
MrAI: i'm pretty sure the ones here are about Agda2 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials                                                                                                                                                                                                                                                                         25/10 15:14
Which Set is bigger: Set1 or Set2 or Set3 ore... etc?                                                                                                                                                                                                                                                                                                                                            25/10 15:47
*or                                                                                                                                                                                                                                                                                                                                                                                              25/10 15:47
fsvo bigger, Set (n+1) is bigger than Set n                                                                                                                                                                                                                                                                                                                                                      25/10 15:48
What does fsvo mean?                                                                                                                                                                                                                                                                                                                                                                             25/10 15:48
for some value of :)                                                                                                                                                                                                                                                                                                                                                                             25/10 15:49
ok thanks                                                                                                                                                                                                                                                                                                                                                                                        25/10 15:49
MrAI: so what's the big project you've undertaken that needs agda?                                                                                                                                                                                                                                                                                                                               25/10 15:54
How 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 smaller                                                                                                                                                                                                                                                          25/10 16:02
Its my 4th Year University project - I've chosen one that uses Agda. The first step is to learn it :)                                                                                                                                                                                                                                                                                            25/10 16:02
Well the first is to learn functional programming - But I'm learning that along side Agda                                                                                                                                                                                                                                                                                                        25/10 16:02
Does suc reduce the value passed by one until the base case is reached?                                                                                                                                                                                                                                                                                                                          25/10 16:02
suc is a constructor                                                                                                                                                                                                                                                                                                                                                                             25/10 16:02
so if you pattern match on it                                                                                                                                                                                                                                                                                                                                                                    25/10 16:02
you know that the parameter inside it is smaller, if you make some assumptions                                                                                                                                                                                                                                                                                                                   25/10 16:02
I see                                                                                                                                                                                                                                                                                                                                                                                            25/10 16:02
yeah, n is smaller than suc n                                                                                                                                                                                                                                                                                                                                                                    25/10 16:04
oh wow, http://detexify.kirelabs.org/classify.html just scribble the symbol and it looks up the latex expression                                                                                                                                                                                                                                                                                 25/10 17:29
that's nice                                                                                                                                                                                                                                                                                                                                                                                      25/10 17:30
I 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
In 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
that's just syntactic                                                                                                                                                                                                                                                                                                                                                                            25/10 22:59
just means bind the implicit parameter named A to A                                                                                                                                                                                                                                                                                                                                              25/10 22:59
ok.                                                                                                                                                                                                                                                                                                                                                                                              25/10 22:59
http://www.cs.nott.ac.uk/~nad/listings/lib-0.4/Relation.Binary.PropositionalEquality.TrustMe.html <-- is this def. equality?                                                                                                                                                                                                                                                                     25/10 22:59
no, that's a hack                                                                                                                                                                                                                                                                                                                                                                                25/10 22:59
definitional equality is basically that type you linked to before                                                                                                                                                                                                                                                                                                                                25/10 23:00
the one that is called "propositional equality"? ;)                                                                                                                                                                                                                                                                                                                                              25/10 23:00
"≡" that one                                                                                                                                                                                                                                                                                                                                                                                     25/10 23:00
?                                                                                                                                                                                                                                                                                                                                                                                                25/10 23:01
actually, definitional equality is writing f x = f + 1, I think                                                                                                                                                                                                                                                                                                                                  25/10 23:01
just any definition you write down                                                                                                                                                                                                                                                                                                                                                               25/10 23:01
Ok, that makes more sense.                                                                                                                                                                                                                                                                                                                                                                       25/10 23:01
Alright, thanks, I can go with that...                                                                                                                                                                                                                                                                                                                                                           25/10 23:01
wth... ??                                                                                                                                                                                                                                                                                                                                                                                        25/10 23:58
cabal install agda                                                                                                                                                                                                                                                                                                                                                                               25/10 23:58
Resolving dependencies...                                                                                                                                                                                                                                                                                                                                                                        25/10 23:58
cabal: dependencies conflict: ghc-6.12.3 requires directory ==1.0.1.1 however                                                                                                                                                                                                                                                                                                                    25/10 23:58
directory-1.0.1.1 was excluded because ghc-6.12.3 requires directory ==1.0.1.2                                                                                                                                                                                                                                                                                                                   25/10 23:58
what is that?                                                                                                                                                                                                                                                                                                                                                                                    25/10 23:58
--- Day changed Tue Oct 26 2010
wires: first Cabal FAQ                                                                                                                                                                                                                                                                                                                                                                           26/10 00:08
oops                                                                                                                                                                                                                                                                                                                                                                                             26/10 00:08
ok funny i'm having a hard time finding the FAQ :)                                                                                                                                                                                                                                                                                                                                               26/10 00:10
Saizan: ah.. haskell FAQ                                                                                                                                                                                                                                                                                                                                                                         26/10 00:12
it says "Cabal FAQ" at the top :)                                                                                                                                                                                                                                                                                                                                                                26/10 00:13
Even.. my brain is cooked ... maybe time to quit for today                                                                                                                                                                                                                                                                                                                                       26/10 00:15
wires: 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
Although, if you go back to Martin-Loef, it should probably be called "judgmental equality".                                                                                                                                                                                                                                                                                                     26/10 02:06
thanks                                                                                                                                                                                                                                                                                                                                                                                           26/10 02:06
Propositional equality is equality as a datatype.                                                                                                                                                                                                                                                                                                                                                26/10 02:06
And it's called that because propositions are types in the Curry-Howard and Martin-Loef presentation, more or less.                                                                                                                                                                                                                                                                              26/10 02:07
I think I understand propositional equality                                                                                                                                                                                                                                                                                                                                                      26/10 02:07
I'm trying to work out most of the details of the observational equality paper                                                                                                                                                                                                                                                                                                                   26/10 02:08
Whereas "judgmental equality" is a judgment. If you look at Martin-Loef's stuff...                                                                                                                                                                                                                                                                                                               26/10 02:08
It should be in the bibliopolis stuff, no?                                                                                                                                                                                                                                                                                                                                                       26/10 02:08
Judgments have the form 'G |- J'                                                                                                                                                                                                                                                                                                                                                                 26/10 02:09
J as in elimination rule?                                                                                                                                                                                                                                                                                                                                                                        26/10 02:09
or just random term?                                                                                                                                                                                                                                                                                                                                                                             26/10 02:09
And 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
J being one of the judgment forms.                                                                                                                                                                                                                                                                                                                                                               26/10 02:10
Or, things being judged.                                                                                                                                                                                                                                                                                                                                                                         26/10 02:10
Anyhow, his "definitional equality" is strictly used for meta-level abbreviations.                                                                                                                                                                                                                                                                                                               26/10 02:10
So if you say "we'll write 'foo' instead of 'bar baz quux'," foo is definitionally equal to bar baz quux.                                                                                                                                                                                                                                                                                        26/10 02:11
But, I guess it's morphed over the years to mean the decidable equality used during type checking.                                                                                                                                                                                                                                                                                               26/10 02:12
Right, 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
Anyhow, 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
wires: 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
If the values have different types, they're trivially rejected as being definitionallly equal.                                                                                                                                                                                                                                                                                                   26/10 02:15
That goes back to the equality judgment form I mentioned, too.                                                                                                                                                                                                                                                                                                                                   26/10 02:16
'x = y : T' means x and y are equal elements of type T.                                                                                                                                                                                                                                                                                                                                          26/10 02:16
It's an operator to itself. _=_:_                                                                                                                                                                                                                                                                                                                                                                26/10 02:17
hm. I thought you could use def. equality to identify two types                                                                                                                                                                                                                                                                                                                                  26/10 02:18
well no                                                                                                                                                                                                                                                                                                                                                                                          26/10 02:18
actually I didn't think that :)                                                                                                                                                                                                                                                                                                                                                                  26/10 02:18
Anyhow, 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
hmm. Yeah, I don't really get the paper... :-S                                                                                                                                                                                                                                                                                                                                                   26/10 02:22
It isn't easy.                                                                                                                                                                                                                                                                                                                                                                                   26/10 02:22
I'm lacking a lot of prerequisite knowledge also...                                                                                                                                                                                                                                                                                                                                              26/10 02:23
could I ask you something about that paper?                                                                                                                                                                                                                                                                                                                                                      26/10 02:24
Sure.                                                                                                                                                                                                                                                                                                                                                                                            26/10 02:24
So, 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 : T                                                                                         26/10 02:25
This doesn't mean one can state that S === T, right?                                                                                                                                                                                                                                                                                                                                             26/10 02:26
I mean it's only used internally during type checking... ie. follows from some rules?                                                                                                                                                                                                                                                                                                            26/10 02:26
|- s : S and |- S === T are premises.                                                                                                                                                                                                                                                                                                                                                            26/10 02:27
yes                                                                                                                                                                                                                                                                                                                                                                                              26/10 02:27
If you can derive those two, you can derive |- s : T                                                                                                                                                                                                                                                                                                                                             26/10 02:27
So it's an inference rule.                                                                                                                                                                                                                                                                                                                                                                       26/10 02:27
So how does one derive S === T ?                                                                                                                                                                                                                                                                                                                                                                 26/10 02:27
Well, usually type equality is up to at least beta equality.                                                                                                                                                                                                                                                                                                                                     26/10 02:28
So (\T -> T) S === S holds, for instance.                                                                                                                                                                                                                                                                                                                                                        26/10 02:28
And so on.                                                                                                                                                                                                                                                                                                                                                                                       26/10 02:29
Ah ok...                                                                                                                                                                                                                                                                                                                                                                                         26/10 02:29
Also alpha equality. (x : A) -> B x === (y : A) -> B y                                                                                                                                                                                                                                                                                                                                           26/10 02:29
Provided x isn't free in B.                                                                                                                                                                                                                                                                                                                                                                      26/10 02:29
OTT/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
Like, they try to make things definitionally eta-equal. For functions, that's f === \x -> f x.                                                                                                                                                                                                                                                                                                   26/10 02:32
Ah, yes....                                                                                                                                                                                                                                                                                                                                                                                      26/10 02:32
And they do simplifications of proofs and stuff.                                                                                                                                                                                                                                                                                                                                                 26/10 02:32
Cool, I didn't understand that section before...                                                                                                                                                                                                                                                                                                                                                 26/10 02:33
thanks this helps a lot                                                                                                                                                                                                                                                                                                                                                                          26/10 02:33
Yeah, it's kind of opaque unless you know what they're trying to accomplish.                                                                                                                                                                                                                                                                                                                     26/10 02:33
especially if you are new to the whole lambda-game                                                                                                                                                                                                                                                                                                                                               26/10 02:33
different notations..                                                                                                                                                                                                                                                                                                                                                                            26/10 02:34
also:   s[ Q:S=T > : T , do you happen to know how to read that notation?                                                                                                                                                                                                                                                                                                                        26/10 02:34
That looks like their notation for substitution/coercion.                                                                                                                                                                                                                                                                                                                                        26/10 02:35
Given 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
Yes, so that means Q is a proof object for S=T, then given Q i can coerce s to T ?                                                                                                                                                                                                                                                                                                               26/10 02:36
Right.                                                                                                                                                                                                                                                                                                                                                                                           26/10 02:36
right                                                                                                                                                                                                                                                                                                                                                                                            26/10 02:36
:)                                                                                                                                                                                                                                                                                                                                                                                               26/10 02:36
Alright, this should get me a bit further. Thanks for you help...                                                                                                                                                                                                                                                                                                                                26/10 02:37
No problem.                                                                                                                                                                                                                                                                                                                                                                                      26/10 02:37
2                                                                                                                                                                                                                                                                                                                                                                                                26/10 08:02
sorry, misclick                                                                                                                                                                                                                                                                                                                                                                                  26/10 08:02
Is there a specification somewhere of all the inference rules used in agda?                                                                                                                                                                                                                                                                                                                      26/10 10:31
Um, heh, ok, in the source probably...                                                                                                                                                                                                                                                                                                                                                           26/10 10:32
emacs only applies syntax highlight to my files when I "Load" them using the menu                                                                                                                                                                                                                                                                                                                26/10 12:54
and new contents are not highlighted, I must load again                                                                                                                                                                                                                                                                                                                                          26/10 12:55
is this normal?                                                                                                                                                                                                                                                                                                                                                                                  26/10 12:55
Watermind: yes                                                                                                                                                                                                                                                                                                                                                                                   26/10 14:39
wires: the core is specified in ulf norell's thesis, though plenty has changed since then                                                                                                                                                                                                                                                                                                        26/10 14:40
ccasin: thanks!                                                                                                                                                                                                                                                                                                                                                                                  26/10 14:40
in particular, the way universe levels work is a lot different than the way they are presented there                                                                                                                                                                                                                                                                                             26/10 14:42
in his thesis, there is no explicit quantification over levels, and things in lower universes are implicitly lifted up when the need to be                                                                                                                                                                                                                                                       26/10 14:43
now we have the explicit universe polymorphism (and the lifting was never implemented)                                                                                                                                                                                                                                                                                                           26/10 14:43
Man, lifting was originally in?                                                                                                                                                                                                                                                                                                                                                                  26/10 14:43
I'm sure lots of other things have changed too, but that's the one that comes to mind :)                                                                                                                                                                                                                                                                                                         26/10 14:43
dolio: well, I don't know if it was ever implemented.  but, it's in the paper                                                                                                                                                                                                                                                                                                                    26/10 14:44
Well, I doubt it was implemented.                                                                                                                                                                                                                                                                                                                                                                26/10 14:44
It'd probably still be implemented if it were.                                                                                                                                                                                                                                                                                                                                                   26/10 14:44
It's a bummer that it wasn't, though.                                                                                                                                                                                                                                                                                                                                                            26/10 14:44
probably (though, for example, the coq hackers have scaled back their universe polymorphism for efficiency reasons)                                                                                                                                                                                                                                                                              26/10 14:45
yeah, it would be very nice                                                                                                                                                                                                                                                                                                                                                                      26/10 14:45
That isn't really necessarily related to universe polymorphism.                                                                                                                                                                                                                                                                                                                                  26/10 14:47
For instance, ECC has cumulative universes, but no universe polymorphism.                                                                                                                                                                                                                                                                                                                        26/10 14:47
yeah, you're right                                                                                                                                                                                                                                                                                                                                                                               26/10 14:48
Although universe polymorphism, I guess, allows you to do without, by carrying around more parameters.                                                                                                                                                                                                                                                                                           26/10 14:48
Agda-style polymorphism, that is.                                                                                                                                                                                                                                                                                                                                                                26/10 14:48
though luo works really hard for his cumulativity - he points out that the obvious naive way to add it breaks most general types                                                                                                                                                                                                                                                                 26/10 14:48
I'm not sure it is as well thought out in ulf's thesis (certainly nothing is proved about it)                                                                                                                                                                                                                                                                                                    26/10 14:49
yeah, but only if you define everything yourself.  If you want to use a non-polymorphic library or base type, you need it again                                                                                                                                                                                                                                                                  26/10 14:50
In general you also need the unsatisfactory Lift type, too.                                                                                                                                                                                                                                                                                                                                      26/10 14:50
ccasin: so there's no way to get syntax highlight as you type? :S                                                                                                                                                                                                                                                                                                                                26/10 14:59
Watermind: I don't know of one, but maybe someone will correct me                                                                                                                                                                                                                                                                                                                                26/10 14:59
ccasin: ok thanks                                                                                                                                                                                                                                                                                                                                                                                26/10 15:00
that's quite unusual                                                                                                                                                                                                                                                                                                                                                                             26/10 15:00
no big deal anyway                                                                                                                                                                                                                                                                                                                                                                               26/10 15:00
yes, though I almost never type more than a few lines without loading the file                                                                                                                                                                                                                                                                                                                   26/10 15:00
that's the beauty of holes                                                                                                                                                                                                                                                                                                                                                                       26/10 15:00
true                                                                                                                                                                                                                                                                                                                                                                                             26/10 15:00
is there a pre defined key binding to load the file?                                                                                                                                                                                                                                                                                                                                             26/10 15:01
Ctrl-c Ctrl-l                                                                                                                                                                                                                                                                                                                                                                                    26/10 15:01
C-c C-l                                                                                                                                                                                                                                                                                                                                                                                          26/10 15:01
cool thanks guys                                                                                                                                                                                                                                                                                                                                                                                 26/10 15:01
Watermind: check this one http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode                                                                                                                                                                                                                                                              26/10 15:02
has most important commands in there                                                                                                                                                                                                                                                                                                                                                             26/10 15:02
nice thanks wires                                                                                                                                                                                                                                                                                                                                                                                26/10 15:03
yay                                                                                                                                                                                                                                                                                                                                                                                              26/10 19:06
@ the Andreas Abel announcement on the list                                                                                                                                                                                                                                                                                                                                                      26/10 19:06
when you load a file in emacs, the bottom part seems the interpreter                                                                                                                                                                                                                                                                                                                             26/10 19:21
but how do you input commands there?                                                                                                                                                                                                                                                                                                                                                             26/10 19:21
it's not really an interpreter                                                                                                                                                                                                                                                                                                                                                                   26/10 19:21
but you can ask it to evaluate terms for you                                                                                                                                                                                                                                                                                                                                                     26/10 19:21
C-c C-n                                                                                                                                                                                                                                                                                                                                                                                          26/10 19:21
(n for normalize)                                                                                                                                                                                                                                                                                                                                                                                26/10 19:21
pumpkin: got it                                                                                                                                                                                                                                                                                                                                                                                  26/10 19:22
I was trying to write there                                                                                                                                                                                                                                                                                                                                                                      26/10 19:22
pumpkin: 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
aw really? the highlighting info it spits out isn't bad at all                                                                                                                                                                                                                                                                                                                                   26/10 20:57
I wouldn't touch the original syntax rep                                                                                                                                                                                                                                                                                                                                                         26/10 20:57
hmm maybe I should take another look again                                                                                                                                                                                                                                                                                                                                                       26/10 20:57
that's what I use in my highlighter                                                                                                                                                                                                                                                                                                                                                              26/10 20:58
but you need to duplicate a lot of their code to get that                                                                                                                                                                                                                                                                                                                                        26/10 20:58
yeah                                                                                                                                                                                                                                                                                                                                                                                             26/10 20:58
anyway, 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 up                                                                                                                                                                                                                                    26/10 21:02
probably tomorrow or the day after                                                                                                                                                                                                                                                                                                                                                               26/10 21:02
well something that lists functions, constructors, datatypes and literals would be great                                                                                                                                                                                                                                                                                                         26/10 21:03
and you don't mind if the constructor knowledge costs you a full typecheck?                                                                                                                                                                                                                                                                                                                      26/10 21:04
no                                                                                                                                                                                                                                                                                                                                                                                               26/10 21:06
oh                                                                                                                                                                                                                                                                                                                                                                                               26/10 21:06
and operators separate                                                                                                                                                                                                                                                                                                                                                                           26/10 21:06
I'll see what I can do :P                                                                                                                                                                                                                                                                                                                                                                        26/10 21:06
awesome :)                                                                                                                                                                                                                                                                                                                                                                                       26/10 21:07
--- Day changed Wed Oct 27 2010
In 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
How should I read this notation T[s]                                                                                                                                                                                                                                                                                                                                                             27/10 01:44
?                                                                                                                                                                                                                                                                                                                                                                                                27/10 01:44
Later it's also used in rules as     \Gamma |- t : T[s]    etc.                                                                                                                                                                                                                                                                                                                                  27/10 01:44
(btw with \Gamma |- s : S as other premise)                                                                                                                                                                                                                                                                                                                                                      27/10 01:45
T probably takes a shape and gives you a type                                                                                                                                                                                                                                                                                                                                                    27/10 01:45
you can think of T as a function from S to Set, and T[s] is the result of applying that function to s                                                                                                                                                                                                                                                                                            27/10 01:45
the 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
Ok, so its like substitution                                                                                                                                                                                                                                                                                                                                                                     27/10 01:46
yep                                                                                                                                                                                                                                                                                                                                                                                              27/10 01:46
K, clear. Thanks guys :)                                                                                                                                                                                                                                                                                                                                                                         27/10 01:47
(crazy stuff this type theory...)                                                                                                                                                                                                                                                                                                                                                                27/10 01:47
I quite liked http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ if you haven't read it yet                                                                                                                                                                                                                                                                                                         27/10 01:47
iirc it covers the W types too                                                                                                                                                                                                                                                                                                                                                                   27/10 01:48
(but not OTT)                                                                                                                                                                                                                                                                                                                                                                                    27/10 01:48
not sure why they don't just say T : S -> Set or similar, maybe that would complicate the system                                                                                                                                                                                                                                                                                                 27/10 01:48
Saizan: yeah, I think so                                                                                                                                                                                                                                                                                                                                                                         27/10 01:49
pumpkin: ha, funny also just found that this morning, very nice reference!                                                                                                                                                                                                                                                                                                                       27/10 01:50
pumpkin: it's very rigorous and doesn't assume any prerequisite knowledge, unlike many other references                                                                                                                                                                                                                                                                                          27/10 01:51
yeah                                                                                                                                                                                                                                                                                                                                                                                             27/10 01:52
I was surprised at how I could follow just about all of it despite not knowing much :P                                                                                                                                                                                                                                                                                                           27/10 01:52
Also, I really like Ulf Norell's thesis, it skips some bits but together with for example this ttfp.pdf one gets quite far                                                                                                                                                                                                                                                                       27/10 01:53
And 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
was reading logs earlier...                                                                                                                                                                                                                                                                                                                                                                      27/10 09:21
pigworker: nice :)                                                                                                                                                                                                                                                                                                                                                                               27/10 09:21
thought I'd try to clear up the T[s] bit                                                                                                                                                                                                                                                                                                                                                         27/10 09:21
* Saizan hopes he's not got it wildly wrong                                                                                                                                                                                                                                                                                                                                                                   27/10 09:22
since wires, pumpkin and Saizan were trying to make sense of it                                                                                                                                                                                                                                                                                                                                  27/10 09:22
Saizan: your question of why not to write T : S -> Set is the relevant one                                                                                                                                                                                                                                                                                                                       27/10 09:23
To 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
However, 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
T[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
These 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
makes sense                                                                                                                                                                                                                                                                                                                                                                                      27/10 09:32
When 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
dolio: 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
so you'd need to have U0, U1 , .. and El S -> U0 could be representable in U1 ?                                                                                                                                                                                                                                                                                                                  27/10 09:41
Saizan: yes                                                                                                                                                                                                                                                                                                                                                                                      27/10 09:41
Well, 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
In that case, B[s] makes sense to me.                                                                                                                                                                                                                                                                                                                                                            27/10 09:42
Looking at B[-] as an expression with holes, or something.                                                                                                                                                                                                                                                                                                                                       27/10 09:42
Yeah. 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
Well, the problem is that it's not always clear to people that B is a metavariable.                                                                                                                                                                                                                                                                                                              27/10 09:44
Since B may well be a valid object expression.                                                                                                                                                                                                                                                                                                                                                   27/10 09:45
In which case it would obviously not depend on x.                                                                                                                                                                                                                                                                                                                                                27/10 09:45
Fonts might come in handy there.                                                                                                                                                                                                                                                                                                                                                                 27/10 09:46
now that is a context-sensitive issue                                                                                                                                                                                                                                                                                                                                                            27/10 09:46
That's the problem I've had, at least.                                                                                                                                                                                                                                                                                                                                                           27/10 09:47
dolio: btw, thanks for your clarificatory remarks on LtU                                                                                                                                                                                                                                                                                                                                         27/10 09:48
No problem.                                                                                                                                                                                                                                                                                                                                                                                      27/10 09:50
pigworker: 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
(and rest also thanks)                                                                                                                                                                                                                                                                                                                                                                           27/10 10:13
wires: it's invoking coherence, but let me find a copy and answer properly                                                                                                                                                                                                                                                                                                                       27/10 10:14
pigworker: awesome!                                                                                                                                                                                                                                                                                                                                                                              27/10 10:16
wires: 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_0                                                                                                                                                                                                                                                                      27/10 10:17
This 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
edwinb: who is saying this?                                                                                                                                                                                                                                                                                                                                                                      27/10 10:25
Ah, 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
edwinb: 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
http://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 function                                                                                                                           27/10 10:35
Actually, their roles seem similar to erasure tracking via modal types.                                                                                                                                                                                                                                                                                                                          27/10 10:39
ah, 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
Only the modes are coupled to the kind.                                                                                                                                                                                                                                                                                                                                                          27/10 10:40
pigworker: it's the draft Jean-Pierre posted to the Agda list                                                                                                                                                                                                                                                                                                                                    27/10 10:41
wires: 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
edwinb: 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
thanks pigworker                                                                                                                                                                                                                                                                                                                                                                                 27/10 10:45
pigworker: I haven't read the draft in any depth yet, I was just a bit worried by the motivation...                                                                                                                                                                                                                                                                                              27/10 10:51
But 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 llvm                                                                                                                                                                                                                                                                                                                                           27/10 10:53
Incidentally, I don't really understand the desire to compile to Haskell                                                                                                                                                                                                                                                                                                                         27/10 10:53
if 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
It might be that people think that'll make it possible to piggy back on GHC's optimizations.                                                                                                                                                                                                                                                                                                     27/10 10:54
I'm not sure I buy that, though.                                                                                                                                                                                                                                                                                                                                                                 27/10 10:55
i imagine it's also hard to interface with GHC's produced code at the native code level if you want an Haskell FFI                                                                                                                                                                                                                                                                               27/10 10:58
..unless you go via C                                                                                                                                                                                                                                                                                                                                                                            27/10 10:59
I'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 system                                                                                                                                                                                                                                                                              27/10 11:00
it would be a bit more work of course                                                                                                                                                                                                                                                                                                                                                            27/10 11:00
Trying 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
Yeah.                                                                                                                                                                                                                                                                                                                                                                                            27/10 12:03
To 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
what about if all the unsafeCoerce# could be removed?                                                                                                                                                                                                                                                                                                                                            27/10 17:30
Then it might be at least *interesting*?                                                                                                                                                                                                                                                                                                                                                         27/10 17:30
as it stands it seems a novelty                                                                                                                                                                                                                                                                                                                                                                  27/10 17:31
The 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
it'd be nice to be able to export haskell interfaces, but not go via GHC :)                                                                                                                                                                                                                                                                                                                      27/10 17:33
I'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 program                                                                                                                                                                                 27/10 17:34
yes, you'd just need to export an interface for that                                                                                                                                                                                                                                                                                                                                             27/10 17:36
I'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
*retaining                                                                                                                                                                                                                                                                                                                                                                                       27/10 17:40
What does escaping Haskell enable Agda to do?                                                                                                                                                                                                                                                                                                                                                    27/10 17:41
avoid tag checks on constructors when they aren't necessary!! :P                                                                                                                                                                                                                                                                                                                                 27/10 17:42
(just kidding)                                                                                                                                                                                                                                                                                                                                                                                   27/10 17:42
Why j/k?                                                                                                                                                                                                                                                                                                                                                                                         27/10 17:42
well, 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
I'm not convinced that's a huge win in general, but I suppose it might enable further optimisations                                                                                                                                                                                                                                                                                              27/10 17:45
In 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
yeah, I wasn't suggesting that :)                                                                                                                                                                                                                                                                                                                                                                27/10 17:47
Agda 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
a 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 one                                                                                                                                                                                                                                           27/10 17:49
I used to think it was a long way off, and then I wrote the Kipling paper.                                                                                                                                                                                                                                                                                                                       27/10 17:49
which is that?                                                                                                                                                                                                                                                                                                                                                                                   27/10 17:50
I don't think I've seen it                                                                                                                                                                                                                                                                                                                                                                       27/10 17:50
"Outrageous but Meaningful Coincidences"                                                                                                                                                                                                                                                                                                                                                         27/10 17:50
So we can have an implementation if we're willing to wait for it to run...                                                                                                                                                                                                                                                                                                                       27/10 17:51
oh I see                                                                                                                                                                                                                                                                                                                                                                                         27/10 17:52
I expect the hardest parts would be the bits around the edges... the interface, parsing, etc                                                                                                                                                                                                                                                                                                     27/10 17:52
I 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
but that's probably just a Simple Matter Of Programming                                                                                                                                                                                                                                                                                                                                          27/10 17:53
So, parser libraries are on their way. We need some constraint-solving tech now.                                                                                                                                                                                                                                                                                                                 27/10 17:54
Maybe in getting off GHC, we can get away from code.haskell.org!                                                                                                                                                                                                                                                                                                                                 27/10 18:08
(and its uptime issues)                                                                                                                                                                                                                                                                                                                                                                          27/10 18:08
that'd be nice :)                                                                                                                                                                                                                                                                                                                                                                                27/10 19:00
copumpkin: you're in boston now?                                                                                                                                                                                                                                                                                                                                                                 27/10 20:43
danbrown: not yet :/                                                                                                                                                                                                                                                                                                                                                                             27/10 20:45
going to miss the bostonhaskell meeting                                                                                                                                                                                                                                                                                                                                                          27/10 20:46
are you moving here at some point?                                                                                                                                                                                                                                                                                                                                                               27/10 20:46
yeah, a couple of weeks                                                                                                                                                                                                                                                                                                                                                                          27/10 20:46
cool! we should grab drinks or something                                                                                                                                                                                                                                                                                                                                                         27/10 20:47
sounds good! I'll let you know when I actually get there, as I don't even have a ticket yet :)                                                                                                                                                                                                                                                                                                   27/10 20:47
alright                                                                                                                                                                                                                                                                                                                                                                                          27/10 20:48
feel free to shoot me an email (jdanbrown@gmail.com)                                                                                                                                                                                                                                                                                                                                             27/10 20:48
we should start up the bostonagda meetup! :P                                                                                                                                                                                                                                                                                                                                                     27/10 20:48
cool, will do                                                                                                                                                                                                                                                                                                                                                                                    27/10 20:48
probably won't run into you at bostonhaskell—i tend not to go                                                                                                                                                                                                                                                                                                                                    27/10 20:48
ah okay                                                                                                                                                                                                                                                                                                                                                                                          27/10 20:49
but i probably should go :P                                                                                                                                                                                                                                                                                                                                                                      27/10 20:49
it can be fun                                                                                                                                                                                                                                                                                                                                                                                    27/10 20:49
pumpkin, you're going to miss the meeting??                                                                                                                                                                                                                                                                                                                                                      27/10 20:53
yeah                                                                                                                                                                                                                                                                                                                                                                                             27/10 20:53
:(                                                                                                                                                                                                                                                                                                                                                                                               27/10 20:53
What                                                                                                                                                                                                                                                                                                                                                                                             27/10 20:53
Grr                                                                                                                                                                                                                                                                                                                                                                                              27/10 20:53
:P                                                                                                                                                                                                                                                                                                                                                                                               27/10 20:53
I'll definitely be at the one afterwards though                                                                                                                                                                                                                                                                                                                                                  27/10 20:53
* djahandarie intimidates pumpkin into coming                                                                                                                                                                                                                                                                                                                                                                 27/10 20:53
hey, I'm in florida now                                                                                                                                                                                                                                                                                                                                                                          27/10 20:53
and don't have a plane ticket to boston                                                                                                                                                                                                                                                                                                                                                          27/10 20:53
and need to be in florida at least until next week                                                                                                                                                                                                                                                                                                                                               27/10 20:53
:P                                                                                                                                                                                                                                                                                                                                                                                               27/10 20:53
Who planned you talking on Friday exactly? :P                                                                                                                                                                                                                                                                                                                                                    27/10 20:54
edwardk did :P                                                                                                                                                                                                                                                                                                                                                                                   27/10 20:54
I 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 agda                                                                                                                                                                                                                                                                                  27/10 20:54
Hahaha                                                                                                                                                                                                                                                                                                                                                                                           27/10 20:54
well, I had told him I wouldn't mind giving a talk at some point                                                                                                                                                                                                                                                                                                                                 27/10 20:55
so it wasn't exactly a surprise :P                                                                                                                                                                                                                                                                                                                                                               27/10 20:55
There's no way I can come up with a good presentation within 2 days so I dunno what's going to happen after ddarius                                                                                                                                                                                                                                                                              27/10 20:57
I already told edwardk a few days ago I wouldn't make it                                                                                                                                                                                                                                                                                                                                         27/10 20:58
and 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
And it'll be something incredibly complicated probably                                                                                                                                                                                                                                                                                                                                           27/10 20:59
nah, he's usually pretty clear                                                                                                                                                                                                                                                                                                                                                                   27/10 20:59
I didn't say otherwise                                                                                                                                                                                                                                                                                                                                                                           27/10 20:59
well, I mean                                                                                                                                                                                                                                                                                                                                                                                     27/10 20:59
he doesn't do excessively esoteric stuff in his talks at bostonhaskell                                                                                                                                                                                                                                                                                                                           27/10 20:59
in my experience                                                                                                                                                                                                                                                                                                                                                                                 27/10 20:59
Ah alright                                                                                                                                                                                                                                                                                                                                                                                       27/10 20:59
At one point weren't . patterns actually checked?                                                                                                                                                                                                                                                                                                                                                27/10 21:57
they aren't currently?                                                                                                                                                                                                                                                                                                                                                                           27/10 21:58
say: example : (i j : N) -> i == j -> Whatever ; example (.i) i refl = ?                                                                                                                                                                                                                                                                                                                         27/10 21:58
it seems like you can type whatever you want in them                                                                                                                                                                                                                                                                                                                                             27/10 21:58
as long as the names are in scope                                                                                                                                                                                                                                                                                                                                                                27/10 21:58
:O                                                                                                                                                                                                                                                                                                                                                                                               27/10 21:58
oh, its only in some cases that it doesn't check them                                                                                                                                                                                                                                                                                                                                            27/10 21:59
not all                                                                                                                                                                                                                                                                                                                                                                                          27/10 21:59
I'm having trouble simplifying my current case                                                                                                                                                                                                                                                                                                                                                   27/10 22:00
http://hpaste.org/40929/unchecked__pattern                                                                                                                                                                                                                                                                                                                                                       27/10 22:02
it seem slike I can type whatever I want in that last line                                                                                                                                                                                                                                                                                                                                       27/10 22:02
and 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
a lambda seems pretty weird in particular                                                                                                                                                                                                                                                                                                                                                        27/10 22:08
I threw that in for maximum absurdity :)                                                                                                                                                                                                                                                                                                                                                         27/10 22:08
but it doesn't have to be one                                                                                                                                                                                                                                                                                                                                                                    27/10 22:09
probably a bug?                                                                                                                                                                                                                                                                                                                                                                                  27/10 22:11
I have had many cases where . patterns weren't checked, so I typically just write them as ._ now to avoid depending on what value it claims                                                                                                                                                                                                                                                      27/10 22:12
--- Day changed Thu Oct 28 2010
copumpkin: why are you sometimes named "copumpkin" and the other time "pumpkin"?                                                                                                                                                                                                                                                                                                                 28/10 14:09
Maybe it depends whether he's being productive or not                                                                                                                                                                                                                                                                                                                                            28/10 14:49
anyone have agda running on GHC 7?                                                                                                                                                                                                                                                                                                                                                               28/10 23:40
Doubtful.                                                                                                                                                                                                                                                                                                                                                                                        28/10 23:40
ugh, haskell-src depends on base 3                                                                                                                                                                                                                                                                                                                                                               28/10 23:52
Yeah.                                                                                                                                                                                                                                                                                                                                                                                            28/10 23:53
and agda depends on haskell-src :(                                                                                                                                                                                                                                                                                                                                                               28/10 23:54
* copumpkin_ sighs                                                                                                                                                                                                                                                                                                                                                                                            28/10 23:54
I know. I discovered that trying to install it on GHC 7.                                                                                                                                                                                                                                                                                                                                         28/10 23:54
I bumped the haskell-src dependency, and it seemed to compile fine.                                                                                                                                                                                                                                                                                                                              28/10 23:54
But I think I got stuck on something else, too.                                                                                                                                                                                                                                                                                                                                                  28/10 23:55
so you just went back to 6.12 for the mean time?                                                                                                                                                                                                                                                                                                                                                 28/10 23:55
Yeah.                                                                                                                                                                                                                                                                                                                                                                                            28/10 23:55
--- Day changed Fri Oct 29 2010
name suggestions?                                                                                                                                                                                                                                                                                                                                                                                29/10 05:35
∀ n → Data.Sign.+ ◃ n ≡ + n                                                                                                                                                                                                                                                                                                                                                                      29/10 05:35
(n : ℤ) → Data.Sign.+ ◃ n ≡ + n                                                                                                                                                                                                                                                                                                                                                                  29/10 05:36
glguy: Bill and Ted                                                                                                                                                                                                                                                                                                                                                                              29/10 05:54
copumpkin: how are you today?                                                                                                                                                                                                                                                                                                                                                                    29/10 10:20
hi copumpkin are you here?                                                                                                                                                                                                                                                                                                                                                                       29/10 16:03
yeah                                                                                                                                                                                                                                                                                                                                                                                             29/10 16:06
I'm going to approach the highlighting problem differently                                                                                                                                                                                                                                                                                                                                       29/10 16:06
just patching agda to have a nicer interface, rather than working around it and duplicating code in my own module                                                                                                                                                                                                                                                                                29/10 16:07
it'll take a little longer but will be a lot nicer                                                                                                                                                                                                                                                                                                                                               29/10 16:07
frustrated that I can't use GHC 7 with agda though :(                                                                                                                                                                                                                                                                                                                                            29/10 16:07
Spockz1: :O                                                                                                                                                                                                                                                                                                                                                                                      29/10 16:10
copumpki_: what's :O?                                                                                                                                                                                                                                                                                                                                                                            29/10 16:11
I mean, what's up?                                                                                                                                                                                                                                                                                                                                                                               29/10 16:11
:P                                                                                                                                                                                                                                                                                                                                                                                               29/10 16:11
http://snapplr.com/mht6                                                                                                                                                                                                                                                                                                                                                                          29/10 16:11
copumpki_: that sounds very good :)                                                                                                                                                                                                                                                                                                                                                              29/10 16:15
Why can't you use ghc 7 anyways?                                                                                                                                                                                                                                                                                                                                                                 29/10 16:15
agda won't compile with it                                                                                                                                                                                                                                                                                                                                                                       29/10 16:18
its dependencies, rather                                                                                                                                                                                                                                                                                                                                                                         29/10 16:18
ah, that's said :(                                                                                                                                                                                                                                                                                                                                                                               29/10 16:19
which client are you using btw?                                                                                                                                                                                                                                                                                                                                                                  29/10 16:20
IRC client?                                                                                                                                                                                                                                                                                                                                                                                      29/10 16:20
textual on mac                                                                                                                                                                                                                                                                                                                                                                                   29/10 16:20
src/Data/Record/Label/TH.hs:5:1:                                                                                                                                                                                                                                                                                                                                                                 29/10 21:35
29/10 21:35
when trying to build fclabels on 7.0 RC2                                                                                                                                                                                                                                                                                                                                                         29/10 21:36
it built TH before that, but for some reason doesn't like the .hi file                                                                                                                                                                                                                                                                                                                           29/10 21:36
why did I ask that in here? it was meant for #ghc                                                                                                                                                                                                                                                                                                                                                29/10 22:55
lol                                                                                                                                                                                                                                                                                                                                                                                              29/10 22:55
--- Day changed Sat Oct 30 2010
How closely can agda be married to haskell?                                                                                                                                                                                                                                                                                                                                                      30/10 00:33
More to the point, how closesly has agda been married to haskell?                                                                                                                                                                                                                                                                                                                                30/10 00:34
what do you mean by married?                                                                                                                                                                                                                                                                                                                                                                     30/10 00:34
have you seen the haskell FFI?                                                                                                                                                                                                                                                                                                                                                                   30/10 00:34
I've seen it wrap c functions                                                                                                                                                                                                                                                                                                                                                                    30/10 00:35
that's the FFI in haskell for C, agda has its own FFI to import haskell libs :)                                                                                                                                                                                                                                                                                                                  30/10 00:36
by married I just mean that there'd be facilities for writing programs that span between agda and haskell                                                                                                                                                                                                                                                                                        30/10 00:36
http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.FFI                                                                                                                                                                                                                                                                                                                                          30/10 00:36
in a way that'd give a kind of programming synergy rather than being a less efficient than using purely one language                                                                                                                                                                                                                                                                             30/10 00:37
and I'm asking whether anyone's demonstrated haskell/agda hybrid systems                                                                                                                                                                                                                                                                                                                         30/10 00:37
oooo                                                                                                                                                                                                                                                                                                                                                                                             30/10 00:38
Saizan, I'm sorry, dude                                                                                                                                                                                                                                                                                                                                                                          30/10 00:39
I thought you were talking about haskell's FFI                                                                                                                                                                                                                                                                                                                                                   30/10 00:39
yeah, "haskell FFI" is pretty ambiguous                                                                                                                                                                                                                                                                                                                                                          30/10 00:41
pumpkin: ghc 7 troubles? :P                                                                                                                                                                                                                                                                                                                                                                      30/10 09:37
--- Day changed Sun Oct 31 2010
suppose 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
I guess the concept doesn't make sense                                                                                                                                                                                                                                                                                                                                                           31/10 01:09
but in principle there's a bijection between Unit \times A and A even if A is empty                                                                                                                                                                                                                                                                                                              31/10 01:10
If A is empty, then so is B.                                                                                                                                                                                                                                                                                                                                                                     31/10 01:11
So naturally f (g x) = x.                                                                                                                                                                                                                                                                                                                                                                        31/10 01:12
dolio: right                                                                                                                                                                                                                                                                                                                                                                                     31/10 01:12
dolio: but I don't know how to produce an f (g x) == x without having an x first                                                                                                                                                                                                                                                                                                                 31/10 01:12
so it seems like my proof requires A nonempty                                                                                                                                                                                                                                                                                                                                                    31/10 01:13
I'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
dolio: neither am I :P                                                                                                                                                                                                                                                                                                                                                                           31/10 01:13
It certainly is not true for all A, B, f and g.                                                                                                                                                                                                                                                                                                                                                  31/10 01:13
oh I know what f and g are                                                                                                                                                                                                                                                                                                                                                                       31/10 01:13
f is A → Unit \times A, and g is vice versa                                                                                                                                                                                                                                                                                                                                                      31/10 01:14
* benmachine brb                                                                                                                                                                                                                                                                                                                                                                                              31/10 01:14
You only know the types?                                                                                                                                                                                                                                                                                                                                                                         31/10 01:14
no                                                                                                                                                                                                                                                                                                                                                                                               31/10 01:17
ok I will show you the whole thing, one sec :P                                                                                                                                                                                                                                                                                                                                                   31/10 01:18
hmm no I will make it typecheck first, then I will show you it and explain why I am dissatisfied                                                                                                                                                                                                                                                                                                 31/10 01:18
here we go http://hpaste.org/40999/benmachine                                                                                                                                                                                                                                                                                                                                                    31/10 01:20
this is my proof that there is a bijection between (Unit \times A) and A                                                                                                                                                                                                                                                                                                                         31/10 01:21
but it only works on non-empty A                                                                                                                                                                                                                                                                                                                                                                 31/10 01:21
it would be nice if it worked on all A, given that it is trivially true for empty A                                                                                                                                                                                                                                                                                                              31/10 01:21
is this possible                                                                                                                                                                                                                                                                                                                                                                                 31/10 01:21
also I'm still new to agda so if I've done terrible things please tell me                                                                                                                                                                                                                                                                                                                        31/10 01:21
I don't see anything there that requires A to be non-empty.                                                                                                                                                                                                                                                                                                                                      31/10 01:22
dolio: the left identity proof has an implicit argument of type A, which I can't provide if it's empty                                                                                                                                                                                                                                                                                           31/10 01:22
or am I thinking about that in the wrong way                                                                                                                                                                                                                                                                                                                                                     31/10 01:22
Oh, yes, I see.                                                                                                                                                                                                                                                                                                                                                                                  31/10 01:23
The problem is that your definition of Bijection is wrong.                                                                                                                                                                                                                                                                                                                                       31/10 01:23
mm I thought it might be                                                                                                                                                                                                                                                                                                                                                                         31/10 01:23
how could it be improved?                                                                                                                                                                                                                                                                                                                                                                        31/10 01:24
Bijection is: exists f g x y. g (f x) = x /\ f (g y) = y                                                                                                                                                                                                                                                                                                                                         31/10 01:24
You want: exists f g. (forall x. g (f x) = x) /\ (forall y. f (g y) = y)                                                                                                                                                                                                                                                                                                                         31/10 01:24
oh, yes I do                                                                                                                                                                                                                                                                                                                                                                                     31/10 01:25
When you do that, injout and outinj will receive an A parameter.                                                                                                                                                                                                                                                                                                                                 31/10 01:25
Or, they already do.                                                                                                                                                                                                                                                                                                                                                                             31/10 01:25
But you take my meaning.                                                                                                                                                                                                                                                                                                                                                                         31/10 01:25
is 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 B                                                                                                                                                                                                                                                         31/10 01:26
Yes.                                                                                                                                                                                                                                                                                                                                                                                             31/10 01:27
right, thanks                                                                                                                                                                                                                                                                                                                                                                                    31/10 01:27
* benmachine fiddles                                                                                                                                                                                                                                                                                                                                                                                          31/10 01:27
yesss, much better                                                                                                                                                                                                                                                                                                                                                                               31/10 01:28
thanks again :)                                                                                                                                                                                                                                                                                                                                                                                  31/10 01:29
* benmachine moves on to trying to prove Bijection (Fin n) (Fin m) → n == m                                                                                                                                                                                                                                                                                                                                   31/10 01:35
Anyone awake? :-/                                                                                                                                                                                                                                                                                                                                                                                31/10 04:06
* Saizan raises an hand                                                                                                                                                                                                                                                                                                                                                                                       31/10 04:07
I'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
induction on xs?                                                                                                                                                                                                                                                                                                                                                                                 31/10 04:08
Try it. :-/                                                                                                                                                                                                                                                                                                                                                                                      31/10 04:08
ah, annoying.                                                                                                                                                                                                                                                                                                                                                                                    31/10 04:10
http://www.reddit.com/r/agda/    <-- "There doesn't seem to be anything here"                                                                                                                                                                                                                                                                                                                    31/10 04:12
this must change                                                                                                                                                                                                                                                                                                                                                                                 31/10 04:12
everybody hype agda up with a bunch of blog posts                                                                                                                                                                                                                                                                                                                                                31/10 04:13
monad tutorials in agda anybody? ;)                                                                                                                                                                                                                                                                                                                                                              31/10 04:13
foo : ∀ {xs : List ℕ} {x} → xs ≢ x ∷ xs                                                                                                                                                                                                                                                                                                                                                          31/10 04:14
foo {[]} ()                                                                                                                                                                                                                                                                                                                                                                                      31/10 04:14
foo {x ∷ xs} eq = foo (lemma eq) where lemma : ∀ {x : ℕ} { y xs ys} -> x ∷ xs ≡ y ∷ ys -> xs ≡ ys lemma refl = refl                                                                                                                                                                                                                                                                              31/10 04:14
ugh                                                                                                                                                                                                                                                                                                                                                                                              31/10 04:14
liyang: http://hpaste.org/41002/xs__x__xs                                                                                                                                                                                                                                                                                                                                                        31/10 04:14
jmcarthur: i think it was decided to keep Agda, Coq, ... all together as a big friendly family http://www.reddit.com/r/dependent_types                                                                                                                                                                                                                                                           31/10 04:17
I don't really even understand why that was created, when r/types already existed.                                                                                                                                                                                                                                                                                                               31/10 04:19
Saizan: it's so fugly though. ;_;                                                                                                                                                                                                                                                                                                                                                                31/10 04:19
It already tells me that it “Cannot pattern match on constructor ≡.refl, since the inferred                                                                                                                                                                                                                                                                                                      31/10 04:20
indices [xs] cannot be unified with the expected indices [x ∷ xs]”                                                                                                                                                                                                                                                                                                                               31/10 04:20
There's also r/Coq, but that's pretty much dead.                                                                                                                                                                                                                                                                                                                                                 31/10 04:21
liyang: foo {x ∷ xs} eq = foo (cong (drop 1) eq), if you prefer                                                                                                                                                                                                                                                                                                                                  31/10 04:21
liyang: anyhow, i think there's an issue on the bugtracker about making such equalities obviously empty                                                                                                                                                                                                                                                                                          31/10 04:22
jmcarthur: I'm hoping to help with that when I finish my agda highlighter                                                                                                                                                                                                                                                                                                                        31/10 04:24
everyone and their mom will be blogging about agda with beautiful, 100% accurate highlighting                                                                                                                                                                                                                                                                                                    31/10 04:27
;)                                                                                                                                                                                                                                                                                                                                                                                               31/10 04:27
hehe                                                                                                                                                                                                                                                                                                                                                                                             31/10 04:28
Saizan: found it— http://code.google.com/p/agda/issues/detail?id=291                                                                                                                                                                                                                                                                                                                             31/10 04:34
(or at least, one of them.)                                                                                                                                                                                                                                                                                                                                                                      31/10 04:34
liyang: that's the one i was thinking of                                                                                                                                                                                                                                                                                                                                                         31/10 04:35
the 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!