November.log

--- Log opened Sat Nov 01 00:00:43 2008
--- Day changed Sun Nov 02 2008
--- Day changed Mon Nov 03 2008
--- Day changed Tue Nov 04 2008
--- Day changed Wed Nov 05 2008
vixeyso agda 2 allows inductive-recursive definitions now?05/11 21:48
vixeyor doesn't it ?05/11 21:48
--- Day changed Thu Nov 06 2008
--- Day changed Fri Nov 07 2008
--- Day changed Sat Nov 08 2008
-!- vixey_ is now known as vixey08/11 16:48
--- Day changed Sun Nov 09 2008
--- Day changed Mon Nov 10 2008
--- Log closed Mon Nov 10 11:15:18 2008
--- Log opened Mon Nov 10 11:15:27 2008
-!- Irssi: #agda: Total of 5 nicks [0 ops, 0 halfops, 0 voices, 5 normal]10/11 11:15
-!- Irssi: Join to #agda was synced in 142 secs10/11 11:17
--- Day changed Tue Nov 11 2008
-!- Irssi: #agda: Total of 5 nicks [0 ops, 0 halfops, 0 voices, 5 normal]11/11 18:11
--- Day changed Wed Nov 12 2008
vixeywhat does this mean?12/11 15:48
vixeyhttp://article.gmane.org/gmane.comp.lang.agda/32412/11 15:48
vixey"Of course, not every occur-check failure corresponds to a disprovable equation"12/11 15:48
--- Log closed Thu Nov 13 06:59:39 2008
--- Log opened Fri Nov 21 15:05:12 2008
-!- Irssi: #agda: Total of 7 nicks [0 ops, 0 halfops, 0 voices, 7 normal]21/11 15:05
-!- Irssi: Join to #agda was synced in 0 secs21/11 15:05
vixeyapparently it's an open question whether or not type constructors are injective (?)21/11 19:15
vixeybut it is provable in Agda because of the unification21/11 19:15
vixeyfor example Fin n = Fin m -> n = m is provable just with reflexivity but in Coq you have to go through this whole fiasco of pigeonhole principle and so on21/11 19:16
vixeyis it a bug maybe?21/11 19:16
vixeynobody has any thougths about it?21/11 20:57
--- Day changed Sat Nov 22 2008
vixeywhat does OTT have that CIC + PI doesn't?22/11 18:41
stevanhi, i'm trying out agda for the first time. i've loaded a small example module into emacs using c-c c-x c-l, the code turned into pretty colors, but how do i play with it? is there any equivalent to ghci? agda --interactive was no longer supported it said. thanks.22/11 19:01
vixeystevan, you can compute normal forms of terms (that's sort of what ghci does I guess)22/11 19:06
vixeyI don't know the key combination for it though...22/11 19:06
vixeyCc Cx Cn maybe22/11 19:06
vixey(in the same emacs bit)22/11 19:07
stevanahh!22/11 19:09
vixeydoes anyone have a program that computes Zippers for a data type?22/11 20:49
vixey(one that I don't have to translate from Epigram into something that there exists an implementation of..)22/11 20:50
vixeyso quiet in Agda :(22/11 21:51
--- Day changed Sun Nov 23 2008
--- Day changed Mon Nov 24 2008
--- Day changed Tue Nov 25 2008
vixeyhello25/11 18:53
stevanhi :-)25/11 19:06
vixeyanyone saw this ? http://article.gmane.org/gmane.comp.lang.agda/32425/11 20:31
vixeyproving acyclicity25/11 20:31
vixeyI don't see the point why you would want to use a zipper or anything, it general if you have a function that give the size of a term,  the x = Foo (Bar ... x) ... should easily be proved contradictory just by size x = S (k + size x)25/11 20:32
vixeyis there something especially simple or what about it?25/11 20:32
--- Day changed Wed Nov 26 2008
--- Day changed Thu Nov 27 2008
stevanhi, how does one compute the normal form of a function that has a unicode name? the input mode in the minibuffer appears to be different than the input mode in the code buffer... thanks.27/11 15:22
--- Day changed Fri Nov 28 2008
--- Day changed Sat Nov 29 2008
--- Day changed Sun Nov 30 2008
SmerdyakovHeeeeelp30/11 14:53
SmerdyakovBuilding Agda-2.1.2...30/11 14:53
Smerdyakovsrc/full/AgdaMain.hs:15:17:30/11 14:53
Smerdyakov    Could not find module `Data.Map':30/11 14:53
Smerdyakov      it is a member of package containers-0.1.0.1, which is hidden30/11 14:53
SmerdyakovAgda really needs an official Debian package.30/11 15:09
SmerdyakovWow, finally built, after making about a dozen changes to the source code! :D30/11 15:31
SmerdyakovArgh!  The Emacs mode hangs!30/11 15:35
kosmikusSmerdyakov: are you using the released version, by any chance? you really should use the version from darcs.30/11 15:40
SmerdyakovI tried to use the version from darcs, but it was too hard getting all the dependencies installed.30/11 15:40
kosmikuscabal-install is your friend30/11 15:41
kosmikusit works quite well now30/11 15:41
SmerdyakovI have no Haskell experience, so learning those tools is extra cost.30/11 15:41
kosmikustrue, admittedly30/11 15:41
kosmikusbut in my experience, cabal-install pays off very quickly30/11 15:42
SmerdyakovNo 'cabal-install' program found in Debian unstable.30/11 15:42
SmerdyakovDo I need to build it manually?30/11 15:43
kosmikuswell, I really wouldn't know about Debian30/11 15:44
kosmikusbut you *can* build it manually30/11 15:44
kosmikushttp://hackage.haskell.org/cgi-bin/hackage-scripts/package/cabal-install30/11 15:44
kosmikusI have to leave, sorry. Good luck with your installation efforts. In general, this channel is still rather quiet. Usualy, the mailing list is the best address to get Agda help.30/11 15:45
vixeySmerdyakov, If Agda is hanging make sure you have the newer version of zlib.. this cause Agda to hang for me before30/11 17:34
vixey(in the emacs mode)30/11 17:34
SmerdyakovIt works for me now.30/11 17:35
vixeyok30/11 17:35
SmerdyakovHow do I introduce multiple "with"-analyzed expressions at once?30/11 18:04
vixeyI gave up trying to figure out the right indentation for "with" and just use helper functions defined in where clauses30/11 18:05
SmerdyakovAha.  They must be separated by pipes.30/11 18:07
* Smerdyakov ponders which Agda examples to go over in class.30/11 18:34
SmerdyakovHow do I use an equality proof in Agda?30/11 18:49
vixeypattern match on refl30/11 18:49
vixeythe reflexivity constructor30/11 18:49
SmerdyakovWhat type does [refl] go with?30/11 18:50
vixeyare you using the standard library?30/11 18:50
vixeyI tended to define everything myself30/11 18:50
SmerdyakovI'm just trying to reason with equality, however is the easiest way to do that.30/11 18:51
SmerdyakovI don't yet know how to use the standard library.30/11 18:51
vixeywell I think this is defined in the standard library, but I wrote,30/11 18:51
vixeydata _≡_ {a : Set} : a -> a -> Set where30/11 18:51
vixey  refl : forall {x} -> x ≡ x30/11 18:51
vixey≡sub : forall {a}{P : a -> Set}{x y : a} -> x ≡ y -> P x -> P y30/11 18:51
vixey≡sub refl Px = Px30/11 18:51
vixey≡symm : forall {a}{x y : a} -> x ≡ y -> y ≡ x30/11 18:52
vixey≡symm refl = refl30/11 18:52
vixeyetc30/11 18:52
SmerdyakovOh, so the argument to [refl] can't be a parameter, as it can in Coq.30/11 18:52
vixeyIf you wrote30/11 18:52
vixey  refl : forall x -> x ≡ x30/11 18:52
vixeyinstead of {x}30/11 18:52
vixeythen I think you could pass in a value x as a paremetr30/11 18:52
SmerdyakovThat's not what "parameter" means.30/11 18:53
vixeyoh not sure what you meant then30/11 18:53
vixeyI don't have Agda installed but to use the standard library I think you just   import Data.Nat  or whichever module30/11 18:54
SmerdyakovYour examples aren't working for me.30/11 18:56
SmerdyakovOops.  Transcribed wrong.30/11 18:56
vixey( http://pastie.org/327169 )30/11 18:58
vixey(that file should be self contained)30/11 18:58
SmerdyakovBizarre.  Things stop working when I switch arguments to explicit, but always match them with underscores in patterns.30/11 18:58
vixeyAgda pattern matching seems to work by some kind of ad-hoc constraint solver/unification algorithm30/11 18:59
vixeyit's roughly like Conors paper Eliminating Dependent Pattern Matching but you get type constructor injectivity (probably by accident of the implementor)30/11 18:59
SmerdyakovIt's roughly like a big ol' black box.30/11 19:04
vixeyyeah :)30/11 19:05
vixeyI'm not keen on it ..30/11 19:05
-!- Makedonier__ is now known as Makedonier30/11 19:08
SmerdyakovDoes anyone know how to do this without using "Seq" and "::eq"?  http://paste.lisp.org/display/7126730/11 19:21
SmerdyakovI.e., I though that Agda was magic and I would avoid needing to prove extra equality lemmas, but I'm not yet seeing how to achieve that.30/11 19:21
SmerdyakovWhat the heck does a message like this mean?30/11 19:34
Smerdyakov_132 : Set  [ at /home/adamc/hg/cpdt_f08/agda/Vec.agda:40,48-52 ]30/11 19:34
Smerdyakov_133 : _132 pf  [ at /home/adamc/hg/cpdt_f08/agda/Vec.agda:40,48-52 ]30/11 19:34
Smerdyakov_136 : refl == refl  [ at /home/adamc/hg/cpdt_f08/agda/Vec.agda:41,11-15 ]30/11 19:34
SmerdyakovIs it some kind of predicativity problem?30/11 19:34
SmerdyakovOh.  It means "I couldn't infer an implicit argument."30/11 19:37
--- Log closed Mon Dec 01 00:00:54 2008

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