/home/laney/.irssi/irclogs/Freenode/2009/#agda/April.log

--- Log opened Wed Apr 01 00:00:39 2009
-!- byorgey__ is now known as byorgey01/04 01:13
stevanhi, what's the proper way of nesting withs using the ... shorthand? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=3169#a3169  indenting the | doesn't seem to help and indenting the ... causes a parse error. or do i need to define the function apa on each line, ie. not use the ... shorthand? thanks.01/04 10:35
-!- byorgey_ is now known as byorgey01/04 13:34
liyangstevan: I've never figured that one out either. http://hpaste.org/fastcgi/hpaste.fcgi/view?id=3169#a317901/04 18:30
vixeywith is the most horrible confusing abomination01/04 19:27
vixeyI'm complaining because I can't think of any better alternative..01/04 19:28
iagoyou don't like guards01/04 19:29
iagoin pattern matching01/04 19:29
iago?01/04 19:29
vixeyiago: It's the only thing had to trawl through pages of source code  for basic use01/04 19:33
liyangit's non-obvious at first until you realise it's necessary in a dependently-typed context.01/04 20:33
vixey:S01/04 20:34
vixeyI use  where  clauses with type annotations01/04 20:34
liyangYes, but when your with-pattern matches refine one of your existing arguments?01/04 20:58
liyangWhat then?01/04 20:58
--- Day changed Thu Apr 02 2009
byorgeyhi all, I'm trying to get the emacs mode working, and the README says to add something like (load-file (let (......  )  (shell-command-to-string "agda --emacs-mode")) to my .emacs02/04 03:42
byorgeybut that just causes an error when I try to load a .agda file.02/04 03:42
byorgeyI've installed Agda 2.2.0 via cabal-install, as well as Agda-executable.02/04 03:42
byorgeyany ideas?02/04 03:42
byorgeyin particular the agda executable doesn't seem to actually take a --emacs-mode option02/04 03:43
Laneybyorgey: is --emacs-mode there when you run agda --help?02/04 09:05
byorgeyLaney: no, it isn't02/04 13:09
byorgeyI've gotten it to work now, seems like the instructions in the README are just incomplete02/04 13:10
byorgeythe Makefile that comes with the source does some magic that doesn't happen when you install via cabal-install, and the README doesn't explain that02/04 13:11
LaneyI didn't have to do anything special, but I'm using the darcs version02/04 13:12
zernyHi guys. I just installed Agda (via cabal install) but can not get the emacs mode working as described in the readme. The command "agda --emacs-mode" just gives an error. Any hints as to what I am doing wrong?02/04 13:45
byorgeyhehe, zerny, I just had the exact same problem =)02/04 13:46
zerny:)02/04 13:46
byorgeyzerny: I ended up just downloading the source .tgz and installing that way (doing make install, then cabal install in a couple places, as described in the README)02/04 13:46
zernythe tar ball on hackage does not seem to contain any emacs stuff.02/04 13:46
zernybyorgey:02/04 13:46
zernyok02/04 13:46
byorgeyyeah, get the tarball from the Agda wiki instead02/04 13:47
byorgeythat 'load-file' line still gives me errors, but the installation process added other stuff to my .emacs02/04 13:47
byorgeyand it seems to work now02/04 13:47
LaneyI'm guessing there's a mismatch between the README in the tarball and reality02/04 13:48
Laneypreviously the .emacs incantation was different02/04 13:48
zernybyorgey: I will check it out. Does it look like it is possible to just keep the cabal install and install  the .el stuff manually?02/04 13:48
byorgeyzerny: well, it's definitely possible, but I wasn't able to find any instructions for doing so02/04 13:51
zernybyorgey: could I ask what it has appended to your .emacs?02/04 13:52
byorgeyzerny: sure, let me check02/04 13:53
byorgey(add-to-list 'load-path "/home/brent/local/share/emacs/site-lisp/agda2-mode")02/04 13:53
byorgey(require 'agda2)02/04 13:53
byorgeythat's all02/04 13:54
byorgeyso maybe you can just stick something like that in your .emacs, and copy the emacs mode .el files to some appropriate place02/04 13:54
byorgeyyou can find those here: http://code.haskell.org/Agda/src/data/02/04 13:55
zernybyorgey: it looks like it works :)02/04 13:55
byorgeygreat =)02/04 13:55
zernythanks for your help :)02/04 13:56
LaneyDoes ~/.cabal/share/Agda*/emacs-mode/ exist?02/04 13:56
Laneythat's where the new version puts it02/04 13:56
zernyLaney: nope. First place I looked02/04 13:56
zernyI only have an Agda.css file there02/04 13:57
Laneyweird02/04 13:57
LaneyI'd suggest mailing the list to get it fixed02/04 13:57
zernybut I am using the version on hackage02/04 13:57
Laneyif it has incorrect instructions then that's a bug02/04 13:57
zernyit might be a bit older. agda --version gives me 2.2.002/04 13:58
zernyLaney: ok. need to go, but thanks for the help02/04 13:58
Laneynp02/04 13:58
Laneybye02/04 13:58
byorgey2.2.0 is the latest stable version, I think02/04 14:03
-!- pumpkin- is now known as ackbar02/04 23:14
-!- ackbar is now known as pumpkin02/04 23:14
--- Day changed Fri Apr 03 2009
-!- byorgey_ is now known as byorgey03/04 23:53
--- Day changed Sat Apr 04 2009
vixey:S04/04 00:19
vixeyyou define a function which has got some cases by = some cases by ~04/04 00:19
-!- byorgey__ is now known as byorgey04/04 15:32
* liyang wonders what vixey's last comment on = / ~ is about.04/04 18:51
vixeymy dad said "StructurallyRecursiveDescentParsing... wow"04/04 18:54
vixeyliyang, page 15 of http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-parser-combinators.pdf04/04 18:57
* liyang is staying away from codata until they figure out exactly how they want to implement it. It used to be case that you had to use ~ in all cases and weren't allowed to mutually recurse ~ and = definitions.04/04 19:04
liyang(By used to be, I mean, earlier this year.)04/04 19:05
vixeycodata is like04/04 19:05
vixeyI don't know.. but it sucks :/04/04 19:05
vixeyyou can't decide equality for it04/04 19:05
--- Day changed Sun Apr 05 2009
yakovhey05/04 20:12
vixeyhi05/04 20:15
vixey:/05/04 20:17
--- Day changed Mon Apr 06 2009
-!- byorgey_ is now known as byorgey06/04 13:09
--- Log closed Mon Apr 06 18:28:31 2009
--- Log opened Mon Apr 06 18:33:34 2009
-!- Irssi: #agda: Total of 18 nicks [0 ops, 0 halfops, 0 voices, 18 normal]06/04 18:33
-!- Irssi: Join to #agda was synced in 106 secs06/04 18:35
vixeyliyang, mrff...06/04 20:51
vixeydo you know when/if james chapman will put his thesis online ?06/04 20:51
* vixey really wants to read it because it's probably going ot have something to do with Type Theory should eat itself06/04 20:53
--- Day changed Tue Apr 07 2009
vixeyhi07/04 00:07
-!- byorgey_ is now known as byorgey07/04 02:37
-!- jfredett_ is now known as jfredett07/04 04:15
stepcutdoes Agda have a mode similar to that Coq mode that spits out valid Haskell from a proof?07/04 22:16
vixeyI thin kso07/04 22:43
liyangstepcut: sort of. --compile will spit out a Haskell program, which you can compile using GHC.07/04 22:52
--- Day changed Wed Apr 08 2009
ccasinHi all08/04 15:51
ccasinI'm trying to get the agda emacs mode installed08/04 15:51
ccasinI was able to successfully "cabal install Agda-executable"08/04 15:51
ccasinthe readme says I should now do "agda-mode setup"08/04 15:51
ccasinbut the agda-mode binary doesn't appear to have been installed by cabal08/04 15:51
ccasinI also don't see any .el files anywhere in the stuff cabal installed and downloaded08/04 15:52
ccasinany tips?08/04 15:52
stevanhi, there been others complaining about not finding the agda mode... might be a bug. I had the darcs version on the system already so i just copied the needed files out from there, you could always do the same if you don't find a better solution.08/04 15:54
ccasinthanks, I will take a look at the darcs version08/04 15:56
ccasincool, this worked08/04 16:23
ccasinthanks for the help08/04 16:23
stevan:-)08/04 16:23
ccasinstrange that the tarball downloaded by cabal doesn't even contain the emacs mode though08/04 16:24
-!- iago is now known as iago_08/04 19:35
--- Day changed Thu Apr 09 2009
-!- eelco_ is now known as eelco09/04 07:01
liyangvixey: http://www.cs.ioc.ee/~james/thesis.pdf09/04 15:29
vixeywoo!!09/04 15:29
liyangvixey: James says: I imagine it isn't exactly what he's hoping for as it doesn't go any further than the papers on my webpage. It improves on them hopefully, but that is all.09/04 15:30
--- Day changed Fri Apr 10 2009
--- Day changed Sat Apr 11 2009
-!- anyfoo is now known as endojelly11/04 16:14
--- Day changed Sun Apr 12 2009
-!- byorgey_ is now known as byorgey12/04 00:40
Ellyagda from darcs does not install properly if the install target is not in your path - it attempts to invoke `agda-mode` with no path12/04 09:02
-!- kosmikus_ is now known as kosmikus12/04 21:22
-!- byorgey_ is now known as byorgey12/04 23:32
--- Day changed Mon Apr 13 2009
-!- Elly is now known as Gruelly13/04 05:03
vixeyoh Elly you are here!13/04 05:08
-!- Gruelly is now known as Elly13/04 05:14
EllyI am!13/04 05:14
Ellyso are you :O13/04 05:14
vixeydid you code anything neat in agda13/04 05:14
vixey?13/04 05:14
Ellynope13/04 05:31
EllyI was just looking at it and joined here to complain about the build process :P13/04 05:32
EllyI'm kind of a linguistic jack of all trades13/04 05:32
Ellybut master of none :(13/04 05:32
endojellywith a DecTotalOrder, I only have ≤, and I have to define > myself, right?13/04 16:01
endojellywhy isn't > predefined (it's just ¬ (a ≤ b) after all)?13/04 16:02
endojellyand another thing:13/04 16:04
endojellyapparently I can install agda's libraries and the executable via cabal, but not the emacs lisp files?13/04 16:05
endojellyhmm13/04 18:54
endojellyI have something of type (StrictTotalOrder._≈_ order x y)13/04 18:54
endojelly(x ≈ y)13/04 18:55
endojellyhow do I get type x ≡ y out of it?13/04 18:55
vixeyI don't know the definitions of these things13/04 18:57
endojellyso, anybody familiar with the standard library having any idea?13/04 18:57
vixeyok...13/04 18:58
endojellyI'm poking around but my head hurts from all those record layers13/04 18:58
vixeykinda wondering where StrictTotalOrder is defined13/04 18:59
endojellyRelation/Binary.agda13/04 18:59
vixeyby ≡ you mean the identity type? looks like it could be any equivalence though13/04 19:00
stevanyour earlier question about _>_; m < n = suc m <= n. and m > n = n < m.13/04 19:00
endojellystevan, for Nat, yes, but I was talking about the much much more general definitions in Relation.Binary13/04 19:01
stevanah, ok13/04 19:01
endojellyvixey, yes, I mean the one defined in Relation.Binary.PropositionalEquality so that I can use subst13/04 19:01
vixeyare the projections here http://www.cs.nott.ac.uk/~nad/repos/lib/Relation/Binary/PropositionalEquality/Core.agda13/04 19:01
endojellyalternatively, I'd like to have a subst involving ≈13/04 19:02
-!- pumpkin_ is now known as coedwardk13/04 20:40
-!- coedwardk is now known as copumpkin13/04 20:49
--- Day changed Tue Apr 14 2009
-!- pumpkin is now known as copumpkin14/04 03:53
-!- e__ is now known as vixey14/04 16:16
ccasinis there any way to lift things from Set to Set1?14/04 19:30
ccasinI mean, generally, if I have some (e : Set), is there any way I can use it where a Set1 is expected14/04 19:31
--- Day changed Wed Apr 15 2009
-!- pumpkin_ is now known as copumpkin15/04 01:47
-!- byorgey_ is now known as byorgey15/04 02:37
vixey"is there any way to lift things from Set to Set1?" -- you might be able to use a universe construction to do that sort of thing15/04 18:31
--- Day changed Thu Apr 16 2009
ccasinis there any way to pattern match in a lambda?16/04 04:48
ccasin(forgive the newbie questions)16/04 04:48
ccasinI guess I'm meant to use a where expression?16/04 04:57
ccasinhmm, but I can't seem to put one of those inside a lambda?16/04 05:05
--- Day changed Fri Apr 17 2009
-!- byorgey_ is now known as byorgey17/04 10:28
-!- pumpkin is now known as uniqueness17/04 14:37
-!- uniqueness is now known as copumpkin17/04 14:38
--- Day changed Sat Apr 18 2009
--- Day changed Sun Apr 19 2009
-!- stepcut` is now known as stepcut19/04 16:26
--- Day changed Mon Apr 20 2009
stevanhi, could someone throw an eye on this piece of code? i can't figure out why it doesn't work... http://pastie.org/452595  thanks.20/04 19:08
vixeystevan sorry don't have a clue since it's got 'with' in it but is the formatting correct?20/04 20:06
stevani believe so; test' works and its has the same formatting...20/04 20:11
vixeytest : ℕ →20/04 20:13
vixey20/04 20:13
vixeytest n with n ≟ \20/04 20:13
vixey020/04 20:13
vixeythat's how it looks because of all the whitespace20/04 20:13
vixeyhttp://pastie.org/452595.txt works though20/04 20:14
vixey(for me)20/04 20:14
stevanyour paste has just as much whitespace? emacs adds it for some reason?20/04 20:15
vixeyweird20/04 20:16
stevandoes the test function work for you? (the one that is commented out)20/04 20:16
vixeybtw it's your paste20/04 20:16
stevanah ok :-)20/04 20:16
vixeydoes anyone know how to get unicode working in the emacs mode though? :/20/04 21:38
vixeyany non ASCII symbols are just boxes for me20/04 21:38
vixeyI did change the agda emacs font file to make it do that... before it wouldn't even load20/04 21:38
stevando you use the lastest release? with the recommended .emacs initialization line? and emacs in gui mode rather than terminal?20/04 21:42
-!- eelco_ is now known as eelco20/04 23:03
--- Day changed Tue Apr 21 2009
-!- byorgey_ is now known as byorgey21/04 01:43
--- Day changed Wed Apr 22 2009
--- Day changed Thu Apr 23 2009
-!- pumpkin is now known as copumpkin23/04 05:41
liyangWhat do people think about getting a domain name for the Agda project?23/04 13:29
liyang(Unfortunately all the top .com/.org/.net names are taken.)23/04 13:30
vixeyI aint paying!23/04 13:35
vixeyisn't http://wiki.portal.chalmers.se/agda/ just fine?23/04 13:35
vixey..23/04 13:39
vixeythis is bizarre btw23/04 13:39
vixeyIf F is injective and the type checker knows that F i = F j it could conclude i = j to solve further constraints. For examples if F is a name of an inductive family or a constructor, it is injective. If F is defined then it is not injective in general, but in some important cases it is. For instance, define Vectors by recursion.23/04 13:39
vixeywho says that the names of type families are injective23/04 13:39
vixeyit's not normally provable23/04 13:39
stevanvixey: i think i implemented the Coq Program type you talked about in Agda: http://pastie.org/45577123/04 14:34
vixeyUGH23/04 14:34
vixeythe formatting again23/04 14:35
stevan:-/23/04 14:35
vixeyIt's called ExistsT btw, Program is the name of thing that figures out coercions between ExistsT T P and T23/04 14:36
stevanhttp://pastie.org/455771 better formating; seems like copying in console emacs includes the trailing white spaces...23/04 14:37
stevanah ok23/04 14:37
vixeyif you're on linux or mac then there is a much better emacs than the console one23/04 14:39
vixeystevan: Sometimes yuo have a program23/04 14:39
vixeyA -> B23/04 14:39
vixeybut it's recursive and the recursion is not obvious23/04 14:40
vixeybut with  A -> Program B (\b -> P b)23/04 14:40
vixeythen you can have a good hypothesis for recursion23/04 14:40
stevanok23/04 14:45
-!- iago is now known as iago_23/04 15:21
-!- iago is now known as iago_23/04 17:47
-!- pumpkin_ is now known as pumpkin23/04 20:36
--- Day changed Fri Apr 24 2009
-!- Elly is now known as Elly|silent24/04 05:00
-!- iago is now known as iago_24/04 14:33
--- Day changed Sat Apr 25 2009
-!- Elly|silent is now known as Elly25/04 05:00
--- Day changed Sun Apr 26 2009
-!- pumpkin_ is now known as copumpkin26/04 07:49
-!- dolio_ is now known as dolio26/04 11:53
-!- copumpkin is now known as ackbar26/04 20:47
-!- ackbar is now known as copumpkin26/04 20:47
--- Day changed Mon Apr 27 2009
-!- pumpkin_ is now known as copumpkin27/04 03:50
--- Day changed Tue Apr 28 2009
-!- pumpkin_ is now known as copumpkin28/04 00:26
-!- byorgey_ is now known as byorgey28/04 15:31
-!- iago is now known as iago_28/04 21:21
--- Day changed Wed Apr 29 2009
-!- dolio_ is now known as dolio29/04 00:12
liyangI seem to remember a while ago Bjork wrote a song about this channel.29/04 10:11
Ellyreally?29/04 10:28
liyangIt's oh so quiet.29/04 10:30
* edwinb jumps up and down and shouts a bit29/04 10:31
* edwinb decides this is tiring so shuts up and goes for coffee29/04 10:32
-!- pumpkin is now known as zygohistomorphic29/04 16:59
-!- zygohistomorphic is now known as pumpkin29/04 17:00
vixeyHas anyone studied metatheory of injectivity of type constructors29/04 22:40
vixeyI don't understand the justification for adding that to Agda theory29/04 22:41
byorgeyvixey: ? I always thought it was simply something that we want to be true, hence we require it.29/04 23:32
byorgeymaybe there is some deeper justification I'm not aware of though.29/04 23:32
edwinbhmm29/04 23:58
edwinbhttp://healf.blogspot.com/ may have what you're after29/04 23:58
edwinbMcBride, Goguen and McKinna, TYPES 2004, "A few constructions on constructors"29/04 23:59
vixeysorry I meant like29/04 23:59
vixeysay you have  Fin : Nat -> Set, with constructors fz and fs29/04 23:59
vixeyAgda seems to give you  Fin n = Fin m -> n = m  as part of typechecking29/04 23:59
--- Day changed Thu Apr 30 2009
edwinbindeed30/04 00:00
vixeyin something like Coq to prove that you would have to give a cardinality argument30/04 00:00
vixey(and use decidable equality of Nat to let you prove the contrapositive)30/04 00:01
edwinbbut you can prove it for all constructors30/04 00:01
edwinbthe paper I quoted has all the details30/04 00:01
edwinband Conor's thesis30/04 00:01
edwinbEpigram generates all the proofs when you declare a datatype30/04 00:01
edwinbAgda, as far as I understand it, just takes them as understood30/04 00:02
vixeyI think those papers talk about injectivity of the fz and fsconstructors, but Agda also gives you injectivity of Fin30/04 00:02
vixeywhich is not a conservative extension30/04 00:02
edwinbah, I see, you mean the type constructors too30/04 00:02
edwinbTo be honest, I didn't know Agda allowed that...30/04 00:07
vixeyIt'd be really interesting to see who is making use of this in programs30/04 00:08
vixeyI'd probably have to stick a  trace  in the typechecker and run through pages of source code though30/04 00:09
edwinbI can't immediately imagine why it's useful, but it's always fun to see why these things are ;)30/04 00:09
vixeyyeah I really have no idea more specific than "it makes more things typecheck"30/04 00:10
vixeymaybe there is a thread on the mailing list about why they added it..30/04 00:10
edwinbI'm sure Ulf would be delighted to explain if you asked...30/04 00:10
vixeyapparently OTT has type constructor injectivity too30/04 00:15
edwinbinteresting...30/04 00:17
edwinbif I remember I will ask Conor when I see him next week...30/04 00:17
-!- dolio_ is now known as dolio30/04 06:20
-!- eelco_ is now known as eelco30/04 10:41
-!- iago is now known as iago_30/04 21:00

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