--- Log opened Mon Jun 01 00:00:32 2009
--- Day changed Tue Jun 02 2009
-!- koninkje is now known as koninkje_away02/06 08:31
-!- codolio is now known as dolio02/06 10:05
titusgI just upgraded ubuntu and agda mode stopped working -- .agda files open as fundamental. I ran agda-mode setup again but it said it was already done.02/06 13:30
titusgAh, never mind, emacs wasn;t finding agda-mode. cabal should give you the option to install it in a standard place IMO.02/06 13:36
titusgBTW, the default monospaced truetype font in emacs-snapshot on jaunty is great -- symbols for nearly everything in agda-input-show-etc. I think it's Deja Vu. Bitmapped fonts make my hair stand on end :-)02/06 13:42
Laneyyeah it's pretty nice02/06 13:48
Laneybtw, a little bird told me that there are easily installable packages for Ubuntu Karmic ;)02/06 13:49
--- Day changed Wed Jun 03 2009
-!- eelco_ is now known as eelco03/06 13:07
titusghi, how do I input superscripts in agda mode? Thinking it would be like LaTeX I expected x\^y to work but that gives me x-hat y03/06 15:21
kosmikuswell, I think the problem is that not all letters exist as superscripts03/06 15:23
kosmikusx\^2 works, for instance03/06 15:23
-!- anyfoo is now known as endojelly03/06 15:26
titusgso it does, thanks.03/06 15:26
--- Day changed Thu Jun 04 2009
-!- koninkje_away is now known as koninkje04/06 04:19
-!- koninkje is now known as koninkje_away04/06 06:32
soupdragonhttp://learnyouanagda.org/ *lol*04/06 13:48
soupdragonliyang: Суупер?04/06 13:54
soupdragonanyone else reading conors coinduction note?04/06 13:59
soupdragonsnoozeville04/06 14:06
--- Day changed Fri Jun 05 2009
-!- eelco_ is now known as eelco05/06 14:34
--- Day changed Sat Jun 06 2009
-!- koninkje_away is now known as koninkje06/06 06:27
--- Log closed Sat Jun 06 10:09:51 2009
--- Log opened Sat Jun 06 10:13:42 2009
-!- Irssi: #agda: Total of 17 nicks [0 ops, 0 halfops, 0 voices, 17 normal]06/06 10:13
-!- Irssi: Join to #agda was synced in 89 secs06/06 10:15
-!- f_ is now known as soupdragon06/06 15:16
-!- byorgey_ is now known as byorgey06/06 19:03
--- Day changed Sun Jun 07 2009
-!- pumpkin is now known as c0w07/06 21:12
-!- c0w is now known as pumpkin07/06 21:12
--- Day changed Mon Jun 08 2009
-!- jfredett_ is now known as jfredett08/06 13:11
--- Day changed Tue Jun 09 2009
-!- byorgey_ is now known as byorgey09/06 04:48
-!- liyang` is now known as liyang09/06 09:20
-!- f__ is now known as soupdragon09/06 12:52
-!- byorgey_ is now known as byorgey09/06 14:23
-!- endojelly is now known as explicitjelly09/06 17:19
-!- explicitjelly is now known as anyfoo09/06 17:21
-!- anyfoo is now known as tricorexplicido09/06 17:21
-!- tricorexplicido is now known as efficientjelly09/06 17:22
-!- efficientjelly is now known as explisixjelly09/06 17:22
-!- explisixjelly is now known as enticingjelly09/06 17:23
-!- enticingjelly is now known as arrogantjelly09/06 17:23
-!- arrogantjelly is now known as effluentjelly09/06 17:23
-!- effluentjelly is now known as brokenjelly09/06 17:23
-!- brokenjelly is now known as crashedjelly09/06 17:24
-!- crashedjelly is now known as endojelly09/06 17:24
-!- pumpkin is now known as ceilingcat09/06 22:27
-!- ceilingcat is now known as pumpkin09/06 22:27
--- Day changed Wed Jun 10 2009
-!- byorgey_ is now known as byorgey10/06 03:33
-!- pumpkin is now known as ceilingcat10/06 03:56
-!- ceilingcat is now known as pumpkin10/06 03:58
-!- byorgey_ is now known as byorgey10/06 14:21
-!- byorgey_ is now known as byorgey10/06 14:38
stevando we really need both: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Publications   and   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation ?  seems to me they largly overlap?10/06 15:31
soupdragonstevan: no10/06 15:44
soupdragonit's silly having them both but don't make one of the URLs before a 40410/06 15:45
soupdragonbecome*10/06 15:45
-!- byorgey__ is now known as byorgey10/06 16:18
-!- byorgey_ is now known as byorgey10/06 19:41
liyangsoupdragon: Cyynep?10/06 22:39
soupdragonyea!!10/06 22:39
liyangsoupdragon: Sorry, was at TFP, then the extended weekend caught up with me.10/06 22:40
soupdragonI was going to ask: What would you write about induction-recursion in your tutorial10/06 22:40
soupdragonno worries this is IRC :)10/06 22:40
soupdragonwhat's TFP10/06 22:40
liyangTrends in Functional Programming; was in Hungary / Slovakia last week.10/06 22:42
soupdragonoooo10/06 22:42
soupdragoncool10/06 22:42
liyangsoupdragon: don't know what to write about ind-rec. Not entirely sure I understand it. :-/10/06 22:43
soupdragonme neither :P10/06 22:43
soupdragonI donno it seems really cool though10/06 22:43
liyangBut knowing that I don't understand it is a good first step, I reckon.10/06 22:43
soupdragonI think they got some PhD at notts working on 'what the hell do you do with induction-recursion'10/06 22:43
soupdragonnot me :(10/06 22:43
liyangOTOH I do know who to ask. :310/06 22:44
soupdragon:310/06 22:46
soupdragonhehe10/06 22:46
soupdragonthere is a couple of examples that come up again and again but yeah10/06 22:46
soupdragonI would never think: Oh I should use induction recursion for this10/06 22:46
-!- byorgey__ is now known as byorgey10/06 23:09
liyangsoupdragon: http://www.cs.chalmers.se/~peterd/papers/Indexed_IR.pdf has a paragraph on what IRDs are. (Though I'm sure it's more subtle than that.)10/06 23:15
liyanghttp://www.cs.chalmers.se/~peterd/papers/Finite_IR.pdf10/06 23:28
soupdragonit's too hard :((10/06 23:28
--- Day changed Thu Jun 11 2009
-!- byorgey_ is now known as byorgey11/06 00:52
soupdragonon agda mailing list, nobody considered proof irrelevence via the Prf modality :(11/06 19:26
soupdragonhuge long thread about it .. not one mention of my favorite method11/06 19:27
codolioMaybe you should write a mail about it. :)11/06 20:02
--- Day changed Fri Jun 12 2009
--- Log closed Fri Jun 12 14:38:00 2009
--- Log opened Fri Jun 12 14:42:23 2009
-!- Irssi: #agda: Total of 16 nicks [0 ops, 0 halfops, 0 voices, 16 normal]12/06 14:42
-!- Irssi: Join to #agda was synced in 101 secs12/06 14:43
--- Day changed Sat Jun 13 2009
-!- pumpkin is now known as liquidsnack13/06 01:57
-!- liquidsnack is now known as pumpkin13/06 01:58
-!- byorgey_ is now known as byorgey13/06 13:55
-!- byorgey_ is now known as byorgey13/06 14:52
-!- byorgey_ is now known as byorgey13/06 18:14
-!- liquidsnack is now known as pumpkin13/06 18:44
-!- liquidsnack is now known as pumpkin13/06 19:28
-!- pumpkin is now known as hunp13/06 19:53
-!- hunp is now known as pumpkin13/06 19:53
-!- byorgey_ is now known as byorgey13/06 21:01
-!- byorgey__ is now known as byorgey13/06 22:35
--- Day changed Sun Jun 14 2009
-!- soupdragon is now known as vixey14/06 00:22
-!- vixey is now known as soupdragon14/06 00:23
maxotehi guys14/06 11:18
maxotecan Agda gives me the answers of x * y = 15 being x,y natural?14/06 11:18
--- Day changed Mon Jun 15 2009
--- Day changed Tue Jun 16 2009
--- Day changed Wed Jun 17 2009
-!- byorgey_ is now known as byorgey17/06 12:58
--- Day changed Thu Jun 18 2009
PeakerWorkHey, I'm reading AgdaIntro.pdf and it seems _or_ is defined to actually be and, not or?18/06 12:09
stevan:-) yeah18/06 12:11
PeakerWorkheh, who can fix that?18/06 12:18
stevanyou could email the author i guess; ulfn at chalmers dot se18/06 12:21
kosmikusI think this is known18/06 13:19
kosmikusit's a test for the reader :)18/06 13:19
PeakerWorkheh18/06 14:40
--- Day changed Fri Jun 19 2009
-!- dwm__ is now known as darinm19/06 00:05
-!- byorgey_ is now known as byorgey19/06 15:05
--- Day changed Sat Jun 20 2009
-!- byorgey_ is now known as byorgey20/06 23:34
--- Day changed Sun Jun 21 2009
-!- koninkje is now known as koninkje_away21/06 04:07
--- Day changed Mon Jun 22 2009
--- Day changed Tue Jun 23 2009
-!- faXx is now known as _nano23/06 12:01
-!- _nano is now known as faXx23/06 12:02
--- Day changed Wed Jun 24 2009
--- Day changed Thu Jun 25 2009
acowleyHello, can someone please help me getting basic IO to compile correctly?25/06 00:18
acowleyagda -c is giving me the error: The type of main should be .IO.Primitive.IO A, for some A. The25/06 00:19
acowleygiven type is .IO.IO .Data.Unit.⊤25/06 00:19
acowleyI've tried using IO.Primitive instead of IO, but I end up chasing down the Costring vs String type, so I'm wondering if there's an easy way to get IO itself working.25/06 00:19
acowleySince it seems to handle all that25/06 00:20
liyanger, I've never tried compiling my programs. Could have a look for you, if you're willing to wait a few hours.25/06 00:22
liyangWhich version (i.e. date?) of the compiler / stdlibs are you using, out of interest?25/06 00:23
acowleyAgda 2 version 2.2.2 from hackage, and the StdLib 0.1 stable release25/06 00:24
acowleyI'd never tried before, either25/06 00:24
acowleyI've got a program that is hideously slow, so I am trying to figure out ways of dealing with that25/06 00:25
acowleyI thought perhaps a batch compilation and execute workflow would be an option, but quickly ran into this trouble25/06 00:25
liyangacowley: I'm not sure why we bother with these so-called `stable' releases. They're stable in the sense that stuff are known not to work.25/06 01:14
acowleyAh.25/06 01:14
acowleyWhat is the recommended installation strategy? I used to use a darcs build, but after really fighting to get GHC 10.3 built on a PPC Mac (10.4), I was relieved to find Agda in hackage. However, I didn't see a standard lib there, so I tried the darcs StdLib, and found that it didn't work my Agda from hackage. Finally I tried the 0.1 release with my hackage Agda, and that seemed happy in that all my other code works.25/06 01:16
liyangWell, as long as you have GHC and Cabal installed, it's generally straightforward.25/06 01:17
liyangthe darcs stdlib usually works best with the darcs agda plus or minus a week or two. When I upgrade I do both at the same time.25/06 01:18
acowleySo my mistake was relief at seeing Agda finally in hackage? :)25/06 01:18
soupdragonyeah putting Agda on hackage was a weird move25/06 01:19
liyangacowley: yes.25/06 01:20
acowleyI thought it was a positive sign of impending stability, so perhaps soupdragon is right.25/06 01:20
soupdragonWell I find Agda 'works' most of the time, but installing it is really hard work25/06 01:21
liyangBut once you've built the thing from hackage, you'll have most, if not all of the dependencies already installed, which makes migrating to the darcs versions more straightforward.25/06 01:21
soupdragonI hope they do a rewrite or something, but probably not going to happen25/06 01:21
liyangsoupdragon: upgrading is a lot easier. =)25/06 01:21
acowleyRight, and after days of compiling and recompiling GHC on a slow computer I was all too eager to avoid another difficult install.25/06 01:21
liyangThe `stable' release is known to install, if you will. If it doesn't, it's likely your own fault.25/06 01:22
liyangThe darcs versions are known to work at known points in time, but if it fails to install, well, *shrug*.25/06 01:22
liyangacowley: technically that's a problem with GHC. :325/06 01:22
acowleyliyang: fair enough :)25/06 01:24
liyangacowley: so, this works for me -- http://liyang.hu/crap/Hai.agda.html25/06 01:32
liyangThere's a short paragraph in IO.agda explaining the IO.IO / IO.Primitive.IO distinction.25/06 01:36
acowley_liyang: I saw that, but didn't pay enough attention to figure out the necessary invocations.25/06 01:40
acowley_I'm giving your suggestion a shot, but I've got two agda compilations running simultaneously now, so it will probably take a while :P25/06 01:42
acowley_Thanks for the help!25/06 01:42
acowley_liyang: That strategy worked with my hodgepodge version of Agda+StdLib, too!25/06 02:00
acowley_I'm just about up to a working darcs version now, too.25/06 02:00
acowley_Shoot, still having problems with the standard lib.25/06 02:02
acowley_This is the same trouble I had before actually, when trying a darcs standard lib with the hackage agda: Note in scope Set_1 in Function.agda25/06 02:03
acowley_s/Note/Not25/06 02:03
acowley_After an emacs bounce, things are back to normal. Except that changes to the definition of the divides relation have now risen up to bite me. Ouch.25/06 02:35
-!- jfredett_ is now known as jfredett25/06 15:22
--- Day changed Fri Jun 26 2009
ehirdcabal: happy version >=1.15 && <2 is required but it could not be found.26/06 00:24
ehird;_;26/06 00:24
* ehird 'stalls26/06 00:24
ccasinyeah, I've also had to install happy and alex manually26/06 00:27
ccasinnot sure why cabal can't get them itself26/06 00:27
ehirdmm26/06 00:27
ehirdNow, uh, how do I get an agda REPL without using emacs?26/06 00:29
ehird:\26/06 00:30
stevana repl alone won't get you far... when things get a bit more complicated you really need the interactivness which agda mode in emacs gives you.26/06 00:31
ccasindon't know, I'm afraid26/06 00:31
ehirdstevan: but I can't stand using emacs :(26/06 00:31
stevanvi user?26/06 00:31
ehirdif those are the two choices, yes.26/06 00:31
ccasinehird: it really is worth it - the way the emacs mode let you leave holes in programs and fill them in incrementally is pretty key if you're doing anything with fancy types26/06 00:32
ehirdCan't I switch to emacs when I stop just playing around with hello-world level examples? :-)26/06 00:33
ehirdIs there a compiler binary, at least?26/06 00:33
ccasinI believe the Agda-executable cabal package has one26/06 00:33
stevani didn't like the emacs idea either, being a vi user, but i find it ok when using viper to emulate vi bindings in emacs :-)26/06 00:33
ccasinbut better to start learning the emacs mode commands early on26/06 00:33
ccasin(with the vi bindings, if you like)26/06 00:34
ehirdperhaps i'll write a crazy vi mode with loads of shell commands to do the same thing :-)26/06 00:34
ehirdif I ever overcome my cronic laziness26/06 00:34
Laneythe emacs mode just passes stuff to ghci26/06 00:34
ehird*chronic, even.26/06 00:34
stevanthere is agda --interactive also, but it's not supported anymore26/06 00:35
ehirdMehhhhhhh, fine I'll use emacs ;-) how should I set it up?26/06 00:35
ccasinI think the wiki has instructions26/06 00:36
ehirdOK26/06 00:36
ccasinor at least a link to the readme, which does have instructions26/06 00:37
ehirdIncidentally, I haven't seen + in any of the few Agda files I've looked at so far. No operators?26/06 00:40
stevanhttp://www.cs.nott.ac.uk/~nad/listings/lib/Data.Nat.html26/06 00:42
ccasinIt live sin the standard library26/06 00:42
ccasinwhich doesn't come with agda, I think - you'll have to download it and put it somewhere26/06 00:42
ccasinand then probably tell emacs where it is26/06 00:43
ehirdI take it, then, that Agda is pretty much the fastest language for arithmetic out there. Not ;-)26/06 00:43
ehirdAlso, do I really have to type all that unicode? :\26/06 00:43
ccasinactually there are ways to tell it to use the primitive addition26/06 00:43
stevanemacs takes care of that too26/06 00:43
ehirdDoes it? How?26/06 00:43
ccasinyou can type latex26/06 00:43
ccasinhit \26/06 00:43
ehirdAh.26/06 00:43
ccasinthen the latex for the thing26/06 00:43
ehirdTodo list: Learn LaTeX, for real.26/06 00:43
ccasinsome of them have other shortcuts too26/06 00:43
ccasinthere is a page on the wiki with common symbols26/06 00:44
ehirdI don't see anything about adding it to emacs, but agda-mode(1) seems to have a magic mode for doing it?26/06 00:48
ccasinadding agda-mode to emacs, or the standard library?26/06 00:49
ehirdHuh?26/06 00:49
ccasinare you trying to add agda mode to emacs, or trying to tell agda mode about the standard library?26/06 00:49
ehirdWell, gee... both I guess?26/06 00:50
ccasinhttp://code.haskell.org/Agda/README26/06 00:51
ccasinunder 2b26/06 00:51
ccasinyou want to put the agda-mode binary somewhere in your path26/06 00:51
ccasinthen add invocation to your .emacs file26/06 00:51
ehirdAlready in my path, so.26/06 00:52
ehird  The program tries to add setup code for Agda's Emacs mode to the26/06 00:52
ehird  current user's .emacs file.26/06 00:52
ehirdI wonder if that works.26/06 00:52
ccasincheck your .emacs file26/06 00:53
ccasinthen to add the standard library (after you have agda-mode up and running), follow the instructions near the top here:26/06 00:53
ccasinhttp://www.cs.nott.ac.uk/~nad/listings/lib-0.1/README.html26/06 00:53
stevanyou also need haskell-mode26/06 00:53
ehirdI have haskell-mode.26/06 00:54
stevanok26/06 00:54
ehird"standard" ← does this mean it doesn't ship with agda?26/06 00:54
ccasinheh, yes26/06 00:54
ccasinit's hard to design good standard libraries for dependently typed languages26/06 00:55
ehird...but it includes IO, so I guess I'll take it.26/06 00:55
ccasinthe "visible plumbing" problem26/06 00:55
ehirdAny nice cabal magic to get this thing?26/06 00:55
ccasinnot to my knowledge26/06 00:55
ehirdAww.26/06 00:56
ehirdSo I have to, like, download it? Using, like, a web client? Laaame ;-)26/06 00:56
ccasin:)26/06 00:56
ccasinthat's what you get for using a research language26/06 00:56
ehirdOnly by virtue of wanting the closest thing to Haskell + -XDependentTypes ;-)26/06 00:57
* ehird attempts to find lib-0.1's download.26/06 00:57
ccasinhttp://www.cs.nott.ac.uk/~nad/software/lib-0.1.tar.gz26/06 00:58
ehirdyay26/06 00:59
* ehird makes sure agda-mode works first th— wait, what's the Agda file extension?26/06 00:59
ccasin.agda26/06 01:00
ehirdWell, that's far too logical.26/06 01:00
ehirdI am disappointed.26/06 01:00
ehirdWelp, loading an .agda file doesn't start any magic mode of love.26/06 01:00
ehirdIndeed, I have no agda commands.26/06 01:01
ccasinlet's see your .emacs26/06 01:01
ccasinalso, are there any errors in the *Messages* buffer?26/06 01:01
ehirdFile error: Cannot open load file, /Users/ehird/zsh:1: command not found: agda-mode26/06 01:01
ehird% grep '.cabal' ~/.profile26/06 01:02
ehird/Users/ehird/.cabal/bin:\26/06 01:02
ehird:\26/06 01:02
ehird(load-file (let ((coding-system-for-read 'utf-8))26/06 01:02
ehird             (shell-command-to-string "agda-mode locate")))26/06 01:02
ehirdare the only relevant .emacs lines.26/06 01:02
ccasinwell26/06 01:03
ccasinaltenatively, write:26/06 01:03
ccasin(load-file "/path/to/agda2.el")26/06 01:04
ccasinsince the binary isn't showing up, for whatever eason26/06 01:04
ccasin*reason26/06 01:04
ehirdSo, uh... does agda-mode have syntax highlighting...?26/06 01:06
ccasinyes, but you need to load the buffer first26/06 01:07
ehird... and automatic indentation ...?26/06 01:07
ccasinC-c C-l26/06 01:07
ehirdccasin: Ah.26/06 01:07
ehirdlol, the blank file doesn't parse :)26/06 01:07
ccasinthe indentation is a bit weaker26/06 01:07
ehirdwait, you mean it can't highlight as I type?26/06 01:07
ehirdnow that's weak :-(26/06 01:07
ccasinyeah, research language and all26/06 01:08
ccasinthere may be a way, I'm not sure26/06 01:08
ehird:-)26/06 01:08
ehirdWell, it's working. How can I evaluate a given expression to test the things I'm writing?26/06 01:09
ccasinI think C-c C-n26/06 01:09
ccasinbut I might be misremembering26/06 01:09
ccasinhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode26/06 01:09
ccasinis helpful26/06 01:09
ccasinit's in the sidebar of the wiki26/06 01:09
ehirdThanks.26/06 01:09
ehirdDon't suppose there's a way not involving a dinky minibuffer window? :-)26/06 01:10
copumpkin:o ehird26/06 01:10
ccasinI think if you are typing in a hole, it will do the expression in that hole?26/06 01:10
ehirdCommand :o not recognized.26/06 01:10
ehirdccasin: Todo list appended: learn what agda holes are.26/06 01:10
ehird:-)26/06 01:10
ccasin:)26/06 01:11
ccasintype ? somewhere26/06 01:11
ccasinwhere you want eventually to fill in an expression26/06 01:11
ccasinthen load the buffer26/06 01:11
ccasinand you'll get a hole26/06 01:11
ehirdcute26/06 01:11
ccasinonce in the hold you can C-c C-, to see what type should go there26/06 01:11
ccasinand C-c C-r to replace the hole with what you've written (maybe generating some smaller holes) if it's well typed26/06 01:11
ccasin*hole26/06 01:12
ehirdIt works, hoorah.26/06 01:12
ccasinone tends to use it like undefined or error in haskell - leaving a well typed gap to come back to later26/06 01:13
ccasinbut it happens a lot more in agda, because you need help to think about the complicated intermediate types26/06 01:14
stevani think there was some effort of porting holes to haskell at some hackathon, but i havn't heard anything since26/06 01:15
* ehird implements Nat, plus, minus.26/06 01:15
ehirdid : (A : Set) -> A -> A-- the dependent function space is written (x : A) -> B26/06 01:19
ehirdid A x = x26/06 01:19
ehirdIn this, what is "A"?26/06 01:19
ehirdA variable that is a set?26/06 01:20
ehirdWell, argument.26/06 01:20
ccasinwell, in the type, it's a type variable26/06 01:20
ehirdright26/06 01:20
ccasinyes, in both cases, sorry, I was distracted26/06 01:20
ehird:-)26/06 01:20
ccasinyou're just explicitly writing the type variable that haskell would write for you26/06 01:21
ehirdright26/06 01:21
ccasinyou can make it impicit by writing {A : Set} in the type26/06 01:21
ccasininstead of (A : Set)26/06 01:21
ccasinthen you won't have to mention it in the definition26/06 01:21
ccasin*implicit26/06 01:21
* ehird defines booleans and attempts to make a function that takes any non-zero Nat. "Any caller can pass any argument with any value that he wants so long as it is not zero."26/06 01:21
ehird;-)26/06 01:21
ccasinof course, you can name any argument to a function - it doesn't have to be a type like in id26/06 01:22
ccasinsince we have full dependent functions26/06 01:22
ehirdyar26/06 01:23
ehird_==_ : Nat -> Nat -> Set                -- is this really the best type for this, instead of -> Bool with one Bool type?26/06 01:23
ccasinWell, they are different26/06 01:24
ccasinyou could define a _==_ for any type26/06 01:25
ccasinbut the -> Bool version26/06 01:25
ccasinonly for types with decidable equality26/06 01:25
ccasinI believe there is an equality check on booleans that does what you want, though26/06 01:25
ccasinI think it's = with a question mark over it26/06 01:25
ccasin\?=   maybe26/06 01:25
ccasinerr26/06 01:25
ccasinan equality check on nats, I mean26/06 01:25
ccasinit's return type isn't Bool though, but it's equivalent26/06 01:26
ehirdBut I'm making my own nats :)26/06 01:26
ccasinSure, well, you can write the version you want26/06 01:26
ccasinyou might want to have both, in fact26/06 01:26
ccasinthe refl version is useful, because you can match on refl and get refinement in your types26/06 01:27
stevanfor doing the division thing; the simplest would be to have a function isZero : N -> Set26/06 01:27
ccasin(Like with GADTs)26/06 01:27
ccasinno26/06 01:27
ccasinerr26/06 01:27
ccasinignore me26/06 01:27
ehirdrefl?26/06 01:28
ccasinas in the definition of equality here26/06 01:28
ccasinhttp://www.cs.nott.ac.uk/~nad/listings/lib-0.1/Relation.Binary.Core.html26/06 01:28
ccasinor, have you programmed with GADTs?26/06 01:28
ccasinit comes up there too26/06 01:29
stevanisNotZero would be better yet26/06 01:29
ccasinby the refl version, I meant the -> Set version, as opposed to the -> Bool version26/06 01:29
ehirdah.26/06 01:29
ehirdI think I'll go with the refl one, since what I'm really trying to do is make that noZeroesAllowed function26/06 01:30
ccasinyeah - then you'll be able to pattern match on it in the function definition, and agda will know not to worry about 0s26/06 01:30
ehirdHmm, I'll have to define "not".26/06 01:31
ehirdNow to figure out how to make a function that takes either the set True or the set False and returns one of them too.26/06 01:32
ccasinNot quite what you want I think26/06 01:35
ehirdPerhaps not.26/06 01:35
ccasinthis is a constructive logic26/06 01:35
ehirdNow I have "zeroOnly : (n : Nat) -> n == zero -> Nat", and the function is half the battle to call it. Or something.26/06 01:35
ccasinyou want not to be Set -> BOTTOM26/06 01:35
ehirdright26/06 01:35
ccasinwhere BOTTOM is some empty type26/06 01:35
ccasinthat seems like an odd function - what are you trying to do with it?26/06 01:36
ehirdccasin: You can call it with zero and a proof that you're giving it zero and nothing else.26/06 01:36
ehirdi.e., a dependent type useless test function.26/06 01:36
copumpkinhas anyone written a Field "typeclass" for agda?26/06 01:36
copumpkinthere are lots of algebraic structures in the std lib but I didn't see Field26/06 01:37
stevana record you mean?26/06 01:37
copumpkinyeah :)26/06 01:37
copumpkinbut I think of them as doing typeclasses by hand26/06 01:37
ccasinehird: yeah26/06 01:37
ehirdBut I can't figure how to get a value of type (n == zero)26/06 01:38
ccasinwell, the value will be "refl"26/06 01:38
ccasinwhen n is 026/06 01:38
ehirdwhat does "refl" mean?26/06 01:38
ccasinhow did you define _==_?26/06 01:38
ehirdhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=6262#a626226/06 01:39
ccasintraditionally, it's a data type with one constructor, called refl26/06 01:39
ehirdwhere26/06 01:39
ehirddata True : Set where26/06 01:39
ehird  tt : True26/06 01:39
ehirddata False : Set where26/06 01:39
copumpkinSet :o26/06 01:39
ehirdAha.26/06 01:39
ehird"tt".26/06 01:39
ehirdPassing tt works.26/06 01:39
ehird\o/26/06 01:39
ccasinah, I see26/06 01:39
ehirdCan't say I understand it but yay.26/06 01:39
ccasinsorry, I thought you had a different sort of equality26/06 01:39
ehirdhehe26/06 01:39
ehirdzeroOnly (succ zero) tt indeed fails.26/06 01:40
ehirdIf I make it {n == zero}, will that pass tt for me?26/06 01:40
ehirdSomehow.26/06 01:40
ccasinin agda, anything can be an implicit argument26/06 01:40
ehirdwell, I guess an actual proof goes there when it's not trivial26/06 01:40
ehirdright?26/06 01:40
ehirdeg when it's from user input26/06 01:40
ccasinsure, then you'd probably have to write something26/06 01:40
ccasinyou can fill in implicit arguments explicitly with { }26/06 01:40
ehirddo I have to do {_ : n == zero}?26/06 01:40
ehirdor is there a shortcut26/06 01:41
ccasinyou shouldn't have to write anything at all, if it's implicit26/06 01:41
copumpkinso does anyone know of a Field implementation anywhere?26/06 01:41
ehirdzeroOnly : (n : Nat) -> {_ : n == zero} -> Nat26/06 01:41
ehirdzeroOnly n = n26/06 01:41
ehirdHow could I avoid writing that...?26/06 01:41
ccasinwell, you didn't need to use the proof of n == zero at all26/06 01:42
ehirdIn the call, no.26/06 01:42
ehirdccasin: but if I omit that, any old grubby Nat can be passed.26/06 01:42
ehirdInstead of just classy zero.26/06 01:42
ccasinwell, it's still there, it's just implicit26/06 01:43
ccasinlike in haskell every function has a bunch of type arguments26/06 01:43
ehirdyeah26/06 01:43
ccasinthey are all implicit, but it doesn't mean they don't get passed26/06 01:43
ehirdit's just the {_ : ...} I was talking about vs {...}26/06 01:43
ehirdit'd seem like {n == zero} would work but nope26/06 01:43
ccasinwell {n == zero} is a type26/06 01:43
ehirdyeah26/06 01:43
ccasinyou need a value of that type26/06 01:43
ccasinyou could also just write nothing26/06 01:44
ccasinand since the argument is implicit, agda should be able to infer it26/06 01:44
ccasinif the thing is actually 026/06 01:44
ehirdokay, now I need to figure out how to do nonZeroOnly... so I need an arugment of not (n == zero), where I define "not".26/06 01:44
ehirdWell, that's for tomorrow26/06 01:44
ccasinhave fun!26/06 01:45
-!- ehird is now known as ehird_26/06 16:02
-!- ehird_ is now known as ehird26/06 16:04
ehirdHmm.26/06 16:39
ehirdSo if I have "zeroOnly : (n : Nat) -> {_ : n == zero} -> Nat" where "_==_ : Nat -> Nat -> Set" of either True w/ tt or False w/ nothing and I want to make nonZeroOnly, I guess I'd have to make "not : Set -> Set", right? Or something26/06 16:39
ehird.26/06 16:39
stevanyea, but in constructive logic the resulting set should always be False... so you can't do it that way.26/06 16:48
stevanan other way to see it is that you can't pattern-match on what kind of set the first set it...26/06 16:50
stevans/it.../is.../26/06 16:50
stevanin the definition: not False = True, False will just be a variable... and then if you define not True = False on the next line it will never be reached, because the above case will match all input.26/06 16:55
ehirdmm...26/06 17:04
ehirdstevan: Maybe I should change =='s type, since this Set thing isn't working26/06 17:04
* ehird finds out what the Prop/refl thing is and does that26/06 17:04
stevanthe way to think of it is you need to convince the typechecker that if div : (m n : N) -> N... and n is zero then the function doesn't make sense and the right hand side should be left out (this is called an absurd pattern in agda)26/06 17:06
ehirdright26/06 17:07
ehirdoh, (m n : N) is sugar for (m:N)→(n:N)?26/06 17:07
ehird(well, with a trailing →)26/06 17:07
stevanand the way to do that is to carry a proof around that if n is zero is a contradiction; that's why i suggested the isNonZero approach yesterday26/06 17:07
soupdragonstevan: what ?26/06 17:08
ehirdstevan: sorry, I don't recall that; maybe I disconnected just before you said it?26/06 17:08
soupdragon <stevan> yea, but in constructive logic the resulting set should always be False... so you can't do it that way.26/06 17:08
soupdragoncan't you just define not the usual way and it works fine?26/06 17:08
soupdragonnot . not = id _in this case_ since nat equality is decidable26/06 17:08
stevanehird: isNonZero : N -> Set26/06 17:09
ehirdstevan: ah26/06 17:09
ehirdstevan: so basically specializing a not-equal function26/06 17:09
ehirdinstead of negating an equality one26/06 17:09
ehirdthat works, I guess; doesn't feel to clean but I guess dependent types require it26/06 17:09
stevanyeah26/06 17:09
ehird*too26/06 17:09
ehirdstevan: and then a separate isZero, I presume?26/06 17:09
stevanto do what?26/06 17:11
stevansoupdragon: the way ehird had defined his functions, i'm pretty sure it was impossible to do what he was trying to26/06 17:11
ehirdwell, having "zeroOnly : (n : Nat) -> {_ : n == zero} -> Nat" but "nonZeroOnly : (n : Nat) -> {_ : isNonZero n} -> Nat" is a bit odd26/06 17:11
ehird/shrug26/06 17:11
soupdragonstevan: but I think that,  not (n == zero)  would have the correct interpretation26/06 17:12
stevanehird: something liket his: div : (m n : N) -> {p : isNonZero n} -> N26/06 17:13
ehirdmm26/06 17:13
ehirdstevan: it's just that doing (n == zero) for one case and (isNonZero n) isn't terribly symmetric/general26/06 17:13
ehirdi was just wondering if there was another way26/06 17:14
stevansoupdragon: could you show the code for it?26/06 17:14
stevanwell you could have a function satisfies : (A -> Bool) -> Set i guess and then write == in terms of bool?26/06 17:16
soupdragonstevan: Code for what?26/06 17:17
ehirdi'm not actually tied to the True/False as sets approach if it isn't useful to work with :p26/06 17:17
stevanhow not would work in that case, soupdragon? if == : N -> N -> Set26/06 17:18
copumpkinehird: I was wondering why you'd done that :)26/06 17:18
soupdragonThe usual definition26/06 17:18
soupdragonnot P = P -> False26/06 17:18
ehirdcopumpkin: it was in one of the examples :-P26/06 17:18
copumpkinah :)26/06 17:19
stevansoupdragon: the problem is how do you show that if n is zero in div : (m n : N) -> {p : not (n == 0)} -> N that the function doesn't make sense?26/06 17:22
soupdragonif n = 0 then in the implementation of div you can use the contradiction from that hypothesis to fill in the case with a vacuous program26/06 17:23
ehirderm, because (not (n == 0)) is False26/06 17:23
ehirdthe same way zeroOnly works?26/06 17:23
stevansoupdragon: i don't think i ever seen anything like that, could you show the code for it?26/06 17:26
soupdragonhttp://www.pasteit4me.com/1401226/06 17:33
stevancool, i didn't know that. time to revisit some code where i needed just that thing!26/06 17:37
soupdragonbtw26/06 17:39
soupdragondiv : (n m : N) -> not (zero? n) -> N26/06 17:39
soupdragonin this part, if we have used something other than 'not (zero? n)' that actually reduces to False when n = 0.. then you could avoid using false-elim (or with)26/06 17:40
soupdragonjust div O m ()26/06 17:40
stevanyeah, that's how i've been doing it... thus suggesting isNonZero26/06 17:42
stevanwell ehird, now you got two problems instead of one! :-)26/06 17:46
ehirdstevan: I thought only regexps did that!26/06 17:47
ehird" if we have used something other than 'not (zero? n)' that actually reduces to False when n = 0"26/06 17:47
ehirdWell, yeah, that's the idea :P26/06 17:47
ehirdWhat is the prop thing for True? The google did nothing.26/06 17:47
stevanprop thing?26/06 17:48
ehirdRefl.26/06 17:49
stevanthat something which would actually reduce to False, could be isNonZero for example btw.26/06 17:49
ehirdInstead of making True a Set.26/06 17:49
stevannot quite sure what you mean... you wanna know what refl is?26/06 17:50
ehirdYes :-)26/06 17:53
stevanit's the constructor of the proof that two elements are equal26/06 17:56
ehirdah.26/06 17:58
ehirdSo unrelated, then, to the thing I read about making True a prop instead of a Set?26/06 17:58
stevanagain, not quite sure i follow :-p, a prop? example?26/06 17:59
ehirdEr. Maybe I misread.26/06 18:00
ehirddata True : Set where-- Here it would make sense to declare True to be a26/06 18:00
ehird  tt : True-- Prop (the universe of propositions) rather than a26/06 18:00
ehird-- Set. See 'Introduction.Universes' for more26/06 18:00
ehird-- information.26/06 18:00
ehirdI guess I should see that :-)26/06 18:02
stevanProp is some Coq thing, not part of agda as far as i know... perhaps something they defined earlier?26/06 18:04
soupdragonstevan: I think they have an crappy ad-hoc version in Agda :)26/06 18:05
soupdragonlike most of the crap they pile in26/06 18:06
soupdragonthey have pattern matching as primitive but I think objects in prop not convertible..26/06 18:06
stevanis that the reference manual or something ehird ?26/06 18:07
ehirdHuh. What happened there.26/06 18:07
ehirdstevan: It's:26/06 18:08
ehirdIntroductory examples from the Agda distribution. Further examples. →26/06 18:08
ehirdhttp://www.cs.chalmers.se/~ulfn/darcs/Agda2/examples/Introduction/26/06 18:08
ehirdhttp://www.cs.chalmers.se/~ulfn/darcs/Agda2/examples/Introduction/Basics.agda26/06 18:08
stevanok26/06 18:09
stevanhmm26/06 18:10
stevanthe first two tutorials on the main page of the wiki are good introductions btw26/06 18:11
ehirdOK26/06 18:11
stevanwith exercises and so on26/06 18:12
-!- hesselink_ is now known as hesselink26/06 18:13
stevantoo bad none of them shows the false-elim thing tho! damn it :-p26/06 18:24
stevanicfp soon, lets make an agda submission!26/06 18:46
soupdragonwhen do they say what the problem is?26/06 18:54
ehirdT-0D00H04M23S26/06 18:55
ehirdhttp://icfpcontest.org/countdown.php26/06 18:55
ehird:P26/06 18:56
ehirdHeh.26/06 19:04
ehirdIt's been started for four minutes and yet, clicking Specifications:26/06 19:05
ehird"Quit rattling your packages and put them back under the tree.  It hasn't started yet."26/06 19:05
--- Day changed Sat Jun 27 2009
-!- copumpkin is now known as EnglishGentv227/06 22:36
-!- EnglishGentv2 is now known as copumpkin27/06 22:37
--- Day changed Sun Jun 28 2009
-!- byorgey__ is now known as byorgey28/06 14:33
stevanhi28/06 19:29
stevanif i'd like to do the soundness reasoning using Relation.Binary.EqReasoning in this example: http://www.cs.chalmers.se/~ulfn/darcs/Agda2/examples/outdated-and-incorrect/StackLanguage.agda   how could i go about making the Prog setoid? what would the carrier be? carrier = Prog n? but where do i get the n from? thanks.28/06 19:32
soupdragonwhere's setoid?28/06 19:34
soupdragonhttp://www.cs.nott.ac.uk/~nad/repos/lib/src/Relation/Binary.agda28/06 19:35
soupdragonI think you would use something like  Prog' A = exists t, Prog A n  and then the carrier could be Prog' A28/06 19:36
stevanexists n, right?28/06 19:36
soupdragonoops yes28/06 19:37
stevanhmm, ok28/06 19:37
soupdragon_≅_ : forall {A n} -> Prog A n -> Prog A n -> Set28/06 19:37
soupdragonp₁ ≅ p₂ = ⟦ p₁ ⟧ == ⟦ p₂ ⟧28/06 19:37
soupdragonyou want to use that equivelance?28/06 19:37
stevanyeah28/06 19:37
soupdragonyou could use  Prog A n  as the carrier but I have a feeling like hiding the n would be more useful28/06 19:38
stevanhow could i do it without hiding it?28/06 19:40
stevanwould the soundess proof still be as strong if the n is hidden?28/06 19:40
stevanhmm, i'm not sure if i actually need a Prog setoid, it might be that an A setoid is enough...28/06 19:49
stevanor a Vec setoid... hmm28/06 19:51
stevanVec makes most sense; cause eval returns a Vec, right? same problem there with the n index tho...28/06 20:03
soupdragonwhy is that a problem28/06 20:04
stevanwell, i need a setoid of whatever i'm eq reasoning about, yes? i think Vec in this case; so VecSetoid = record { carrier = Vec A n ; ... there module could be parametrized over A, so i get the A from there, but the n?28/06 20:06
soupdragonI don't think so28/06 20:06
stevanwhat do you reckon?28/06 20:07
soupdragonyou just need one per equivalence relation, congruence quotiented by a function is what you're really using (with the function [[ _ ]])28/06 20:11
stevani'm sorry, but i don't quite follow. could you please explain a bit further?28/06 20:14
--- Day changed Mon Jun 29 2009
-!- byorgey_ is now known as byorgey29/06 19:13
* edwinb attempts to install agda, and finds that version 2.3.1 of Alex is not between 2.0.1 and 3...29/06 22:39
edwinboh, no, it turns out it's because cabal install doesn't29/06 22:42
edwinbI'm sure I used to know how to use computers29/06 22:42
kosmikusso you solved it?29/06 22:45
edwinbYes, it just turns out I'm an idiot ;)29/06 22:45
edwinbMove along, nothing to see here...29/06 22:45
edwinb(I forgot that cabal puts things in ~/.cabal/bin)29/06 22:46
kosmikusthat's a common mistake. I've been confused by this several times already.29/06 22:47
edwinbI had it all set up nicely, but I'm setting up a new computer and finding out what I've forgotten29/06 22:47
kosmikusright, exactly29/06 22:47
kosmikusI'm getting confused once I'm not sitting in front of my own machine29/06 22:48
edwinbI wish I'd written down all the things I've had to do to set this up neatly...29/06 22:48
kosmikuswhat OS are you using?29/06 22:49
edwinbLeopard29/06 22:49
kosmikusisn't that outdated already? :)29/06 22:50
edwinbprobably ;)29/06 22:50
edwinbI was using Tiger until today!29/06 22:50
edwinbI was scared to upgrade since I had the machine set up right29/06 22:50
kosmikushah29/06 22:50
kosmikusyou should use NixOS29/06 22:50
edwinbthat'd probably give me a whole new set of problems ;)29/06 22:56
--- Day changed Tue Jun 30 2009
-!- byorgey_ is now known as byorgey30/06 14:55
-!- copumpkin is now known as coPumpkin30/06 18:53
-!- coPumpkin is now known as copumpkin30/06 18:53

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