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

--- Log opened Fri May 01 00:00:04 2009
-!- dolio_ is now known as dolio01/05 01:46
-!- iago is now known as iago_01/05 10:29
--- Day changed Sat May 02 2009
-!- iago is now known as iago_02/05 10:27
-!- _dolio is now known as dolio02/05 17:14
-!- byorgey_ is now known as byorgey02/05 17:20
--- Day changed Sun May 03 2009
-!- Elly is now known as ThreAple03/05 09:59
-!- ThreAple is now known as THREAPLE03/05 09:59
-!- iago is now known as iago_03/05 11:05
-!- THREAPLE is now known as Elly03/05 11:31
-!- _dolio is now known as dolio03/05 15:33
-!- byorgey__ is now known as byorgey03/05 15:50
--- Day changed Mon May 04 2009
liyangMmmm... Futurama projections: http://blog.sigfpe.com/2009/05/three-projections-of-doctor-futamura.html04/05 13:07
-!- _dolio is now known as dolio04/05 20:38
--- Day changed Tue May 05 2009
-!- byorgey_ is now known as byorgey05/05 02:14
--- Day changed Wed May 06 2009
-!- badtruffle is now known as copumpkin06/05 02:33
-!- koninkje_away is now known as koninkje06/05 04:44
-!- koninkje is now known as koninkje_away06/05 06:10
-!- _dolio is now known as dolio06/05 09:12
-!- badtruffle is now known as copumpkin06/05 17:16
-!- _dolio is now known as dolio06/05 19:58
-!- badtruffle is now known as copumpkin06/05 20:39
-!- badtruffle is now known as copumpkin06/05 22:54
--- Day changed Thu May 07 2009
-!- byorgey_ is now known as byorgey07/05 01:29
-!- byorgey_ is now known as byorgey07/05 02:58
-!- badtruffle is now known as copumpkin07/05 04:21
-!- byorgey_ is now known as byorgey07/05 12:46
-!- byorgey_ is now known as byorgey07/05 15:34
-!- badtruffle is now known as copumpkin07/05 17:57
-!- _dolio is now known as dolio07/05 18:40
--- Day changed Fri May 08 2009
-!- badtruffl is now known as pumpkin_08/05 00:29
-!- e__ is now known as vixey08/05 01:29
-!- badtruffle is now known as pumpkin_08/05 05:16
-!- byorgey__ is now known as byorgey08/05 20:25
--- Day changed Sat May 09 2009
-!- byorgey_ is now known as byorgey09/05 12:52
--- Day changed Sun May 10 2009
-!- codolio is now known as dolio10/05 01:03
vixeyhttp://www.iis.sinica.edu.tw/~scm/2009/proof-irrelevance-extensional-equality-and-the-excluded-middle/10/05 02:55
vixeyyou might have already seen this10/05 02:55
vixeyanyone read it?10/05 04:23
vixeygot a question actually10/05 04:23
vixeynvm10/05 04:23
vixeyhow do you install happy?10/05 04:57
vixeyI just got loads of errors..10/05 04:57
-!- badtruffle is now known as copumpkin10/05 17:45
--- Day changed Mon May 11 2009
-!- badtruffle is now known as copumpkin11/05 00:47
-!- jfredett_ is now known as jfredett11/05 02:31
-!- badtruffle is now known as copumpkin11/05 03:21
-!- byorgey_ is now known as byorgey11/05 20:47
--- Day changed Tue May 12 2009
-!- badtruffle is now known as pumpkin_12/05 00:21
-!- badtruffle is now known as copumpkin12/05 01:56
-!- codolio is now known as dolio12/05 03:12
-!- badtruffle is now known as copumpkin12/05 07:11
-!- badtruffle is now known as copumpkin12/05 17:33
-!- Jerry_ is now known as XOO12/05 18:42
copumpkinis there an agda matrix library?12/05 20:08
swiertyes. but no one can be told about it.12/05 20:15
swiertyou have to see for yourself.12/05 20:15
copumpkin!12/05 20:16
copumpkinso it's a profound realization one comes to after playing with agda for a while? then you suddenly have a matrix library?12/05 20:16
swiert(It was a bad reference to the matrix movie).12/05 20:17
swiertBut there's some stuff in Data.Vec that should be useful.12/05 20:17
copumpkinoh :)12/05 20:22
copumpkinmaybe I'll play around with making a simple one myself to get a feel for the language12/05 20:22
copumpkinare there any plans to revive the --interactive mode?12/05 20:35
swiertI  think it may still work.12/05 20:35
swiertIt's just that it's no longer actively maintained.12/05 20:36
swiertThe emacs mode is quite nice once you get used to it.12/05 20:36
copumpkinI'm just not a big fan of emacs in general12/05 20:37
stevanlets hope somebody makes an agda mode for yi soon :-)12/05 20:40
-!- iago is now known as iago_12/05 21:08
cocopumpkinis there a specific way to "install" the standard library12/05 23:10
cocopumpkin?12/05 23:10
vixeyadd to agda2-include-dirs the path to the lib (in emacs  do M-x customize-mode and add to that)12/05 23:12
cocopumpkinagda2-include-dirs where? I'm not using emacs right now... (the only docs I can see mention agda2-include-dirs in .emacs)12/05 23:20
vixeywhat os12/05 23:21
cocopumpkinmac os12/05 23:21
vixeyyou should get Carbon Emacs12/05 23:21
cocopumpkinnot a big fan of emacs :/12/05 23:24
cocopumpkinI guess I could give in, but I'd prefer not to12/05 23:24
vixeyyour being really silly12/05 23:24
dolioYou want emacs.12/05 23:25
dolioProving non-trivial things without tool support is a pain.12/05 23:28
vixeyProving non-trivial things in Agda is a pain :p12/05 23:29
-!- byorgey_ is now known as byorgey12/05 23:30
cocopumpkinI just want to fool around with it, not do any substantial proving12/05 23:48
--- Day changed Wed May 13 2009
-!- koninkje1away is now known as koninkje13/05 04:04
-!- copumpkin is now known as pumpkin13/05 04:35
pumpkinhow does Monoid in http://www.cs.nott.ac.uk/~nad/listings/lib-0.1/Algebra.html#277 enforce associativity?13/05 04:51
pumpkinoh, I see13/05 04:52
pumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib-0.1/Algebra.FunctionProperties.html#78513/05 04:52
pumpkinwhoa, why is C-c C-l running GHC?13/05 05:21
pumpkinoh, it's running ghci13/05 05:22
pumpkinand it's pegging my CPU13/05 05:22
pumpkinwow, it took about a minute at 100% cpu for it to tell me my program was invalid13/05 05:23
pumpkinokay, I'm stuck on the most basic of problems13/05 05:47
pumpkinanyone around?13/05 06:11
-!- koninkje is now known as koninkje_away13/05 06:24
pumpkinis there something like a "Show instance" in agda?13/05 06:33
kosmikuspumpkin: well, all the values can be printed on screen13/05 06:38
pumpkinooh, how? it's not like I don't trust all the dependent magic, but I wanna "see" it! :P13/05 06:39
kosmikuspumpkin: just evaluate something13/05 06:39
pumpkinalso, I couldn't get my main function working without adding some pragmas into haskell13/05 06:39
kosmikusinto Haskell?13/05 06:39
kosmikusoh, you're compiling13/05 06:39
kosmikuswell, then I don't know if you can print13/05 06:40
pumpkinI had main : \forall {A} \r A; main = putStrLn "hello!"13/05 06:40
pumpkinI meant IO A13/05 06:40
pumpkinwhere IO came from the IO in the standard library13/05 06:40
pumpkinbut it complained that putStrLn had type IO \top13/05 06:40
kosmikusyes, that's true13/05 06:40
pumpkinso if I made main : IO \top, it complained that main had to be IO A13/05 06:41
kosmikusit does?13/05 06:41
kosmikuslet me check13/05 06:41
pumpkinfor compilation only13/05 06:41
pumpkinC-c C-l works fine13/05 06:41
kosmikushmmm13/05 06:44
pumpkinuser error? :P13/05 06:44
kosmikusseems like there are two IO types13/05 06:45
kosmikusa "primitive" IO type next to the one that "putStrLn" returns13/05 06:47
kosmikusand there seems to be a function "run" converting one into the other13/05 06:47
pumpkinah13/05 06:50
pumpkinis there something like "type" for type aliases in agda? I've made a custom matrix type, but it might be easier to work with as a Vec of Vecs13/05 06:50
dolioJust write a function.13/05 06:50
pumpkinoh, good point13/05 06:51
pumpkinhmm, actually I thought I knew how to do that :P13/05 06:55
pumpkinso I can write a function that takes a type and returns one13/05 06:56
dolioYes.13/05 06:56
pumpkinMat : ∀ {n m} → (a : Set) → Vec (Vec a n) m13/05 06:56
dolio'type Foo f = f Int' would be 'Foo : (Set -> Set) -> Set ; Foo f = f Int'.13/05 06:57
pumpkinwould that have to be Set1?13/05 06:57
dolioWhich?13/05 06:58
pumpkinthe last one13/05 06:58
pumpkin(Set -> Set) -> Set1 ?13/05 06:58
pumpkinor is that different?13/05 06:58
dolioNo.13/05 06:58
dolioSet : Set113/05 06:59
dolioSet1 : Set2, etc.13/05 06:59
dolio(Set -> Set) -> Set : Set1 as well.13/05 06:59
pumpkinhow is that : binding there? to the whole expression on the left, or only to the rightmost Set?13/05 07:00
dolio((Set -> Set) -> Set) : Set113/05 07:01
pumpkinaha13/05 07:01
dolioT -> T' : lub K K', where T : K and T' : K', as I recall.13/05 07:04
kosmikuslooks good13/05 07:04
dolioIf you think of Set3 being an upper bound of Set2 and Set3, for instance.13/05 07:04
pumpkinso, sorry for the stupid question, but what would the actual body of such a Mat function be?13/05 07:05
kosmikusquantifying over sets increases the universe level, though13/05 07:05
pumpkinwith the type I wrote above (assuming it makes sense)13/05 07:05
dolioWhat do you want your Mat to look like? Mat a m n?13/05 07:06
kosmikusMat n m = Vec (Vec a n) m13/05 07:06
kosmikusor something like that?13/05 07:06
kosmikusoh, well, Mat A n m = Vec (Vec A n) m13/05 07:06
kosmikusMat : Set -> \bn -> \bn -> Set13/05 07:07
dolioYeah, and the type is: Mat : Set -> Nat -> Nat -> Set13/05 07:07
pumpkinwhy does the Set come before the two Nats?13/05 07:07
dolioWell, whatever order you want.13/05 07:07
pumpkinah ok13/05 07:07
kosmikusbut it's compatible with Vec then13/05 07:08
kosmikusalso, Agda encourages parameters to come before indices13/05 07:08
pumpkinmakes sense13/05 07:08
dolioOpposite of GHC. :)13/05 07:09
pumpkinfor Mat a n m = Vec (Vec a n) m I'm getting "left hand side gives too many parameters to a function of type <type above>"13/05 07:09
kosmikusare you sure you got the right type?13/05 07:09
pumpkinMat : ∀ {n m} → (a : Set) → Vec (Vec a n) m Mat a n m = Vec (Vec a n) m13/05 07:10
pumpkinwhoops, it stuck them on same line13/05 07:10
pumpkinbut it doesn't like the Mat definition, given that type13/05 07:10
kosmikusnot implicit for n, m13/05 07:10
kosmikusalso, now you got different orders in the type and the def13/05 07:11
kosmikusand the type shouldn't mention Vec13/05 07:11
kosmikuswe gave the type above13/05 07:11
pumpkinoh, sorry13/05 07:11
pumpkinsometimes I see \forall {...} followed by \r and sometimes it isn't... is there a difference?13/05 07:13
dolio\r is ->?13/05 07:13
kosmikusI guess \r is ->13/05 07:14
kosmikuswell, there isn't really a difference13/05 07:14
pumpkinyeah, sorry13/05 07:14
dolioWhen you're listing several named pis in a row, you don't have to put ->.13/05 07:14
kosmikusif you have multiple function arguments that have names13/05 07:14
kosmikuswell, I'm too slow typing compared to dolio :)13/05 07:14
dolio:)13/05 07:14
pumpkinthank you so much! this is fun13/05 07:14
pumpkinis there a way to overload operators? Nat already took _+_ but I'd like to use it for Mat too13/05 07:15
pumpkinsorry if I sound totally clueless... it's probably because I am :/13/05 07:15
kosmikuspumpkin: only via modules/records13/05 07:15
dolioOddly enough, constructors can be overloaded.13/05 07:15
kosmikuspumpkin: but since you can locally open modules, it's actually quite ok13/05 07:15
pumpkinhmm, so my matrix addition is valid, but uses _+++_ which feels ugly :P13/05 07:17
kosmikusyou can rename the addition on natural numbers instead if you like13/05 07:18
pumpkinoh, I guess that's one option13/05 07:19
pumpkinhmm13/05 07:19
pumpkinso when you talk about records for overloading, is that a bit like explicitly dealing with haskell's typeclass dictionaries?13/05 07:19
pumpkinbut basically implementing them in the language itself?13/05 07:19
kosmikusyes13/05 07:20
pumpkinooh, fancy :)13/05 07:20
dolioKind of the opposite of fancy. :)13/05 07:22
dolioAside from the nicer modules and records-as-modules, which is fancy.13/05 07:22
pumpkinwell, it's fancy that we can do that, but not fancy in that we have to do it ourselves13/05 07:22
pumpkinunless there's some kind of fancy first-class typeclass abstraction defined somewhere?13/05 07:22
pumpkinwhat is agda's goal? is there an interest in making it a general-purpose programming language, or is it intended mainly as a theorem prover?13/05 07:26
pumpkinlike, would putting "practical" Num/Show records in there be useful, or just a distraction13/05 07:27
pumpkinwell, maybe not Num13/05 07:27
pumpkinI see there's lots of nice algebraic structures already13/05 07:27
dolioThe really fancy stuff is in EqReasoning or some such module.13/05 07:29
pumpkinhow would agda get around the Sum/Product newtypes for Monoid in haskell issue?13/05 07:30
dolioRelation.Binary.EqReasoning13/05 07:30
dolioAt least, I think that looks cool.13/05 07:30
kosmikusyes, it is quite cool13/05 07:31
pumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib-0.1/Relation.Binary.EqReasoning.html#453 can't see much i it?13/05 07:31
kosmikusI think the goal of Agda is to be more a programming language than a theorem prover13/05 07:31
pumpkinis the PreorderReasoning doing the work?13/05 07:31
kosmikusI have to leave now13/05 07:31
dolioYeah.13/05 07:31
pumpkincool :)13/05 07:31
dolioEqReasoning has an example of how to use it, though.13/05 07:31
pumpkinthanks for the help :)13/05 07:32
pumpkinyeah13/05 07:32
pumpkindammit, I need to go to sleep, but I want to keep playing with this13/05 07:33
pumpkinthis is making me want to contribute to the standard lib13/05 07:35
pumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib-0.1/Data.Vec.html#740 how does one write a Vec literal using that?13/05 07:43
dolio1 ∷ 2 ∷ 3 ∷ []13/05 07:44
pumpkinoh13/05 07:44
pumpkinwhat's that _[_]=_ thing?13/05 07:44
doliov [ i ]= x is a proof that the ith element of v is x.13/05 07:45
pumpkinoh13/05 07:46
dolioI need to redefine my alias for ℕ. \mathbb{N} is too much work.13/05 07:47
pumpkin\bn doesn't work?13/05 07:47
dolioDoes it?13/05 07:47
pumpkindoes for me, on a vanilla install13/05 07:47
dolioAh, nice.13/05 07:48
pumpkinwhee, I just added a matrix to itself!13/05 07:48
* pumpkin beams13/05 07:48
pumpkintomorrow, cholesky!13/05 07:48
pumpkin:P13/05 07:48
dolioMake sure you prove it correct.13/05 07:49
pumpkinI'm assuming it won't be as simple as saying that chol(A) chol(A)* = A13/05 07:51
dolioThat doesn't look like a proof. :)13/05 07:51
pumpkinI was hoping it would do all the work for me :P boo13/05 07:51
dolioTry Coq, maybe it will. :)13/05 07:52
pumpkinI guess it's just a proof assistant after all, not a proof master13/05 07:52
pumpkinso coq can do even more than agda?13/05 07:53
dolioCoq has automatic proving 'tactics' that you use.13/05 07:53
pumpkinI must say that compared to haskell, I feel all-powerful now :P but I've only been playing with agda for a little while13/05 07:53
dolioSo, in Agda, when you want to prove something, you give the type of the thing you want to prove, and write down a bunch of equations, like a haskell function.13/05 07:54
dolioYou can write stuff like 'proof input1 input2 = ?' and then say, "split input1 for me" and so on, but you're still figuring out the proof by hand.13/05 07:54
pumpkinI see13/05 07:54
dolioCoq lets you do stuff more like writing down the type of the proof and then saying, "try induction. Okay, we're done."13/05 07:55
pumpkinwow13/05 07:55
dolioAnd you can write new tactics and stuff.13/05 07:55
pumpkinsound awesome13/05 07:55
* pumpkin sings "a whole new world" from disney's aladdin13/05 07:56
dolioYeah, although the Agda way has its charms.13/05 07:56
dolioI've not really used Coq at all, though. Perhaps I'd feel differently if I had.13/05 07:56
pumpkinI wonder if a math prof would accept an agda program as a proof13/05 07:57
pumpkinI guess it depends on the math prof13/05 07:57
pumpkinI wonder at what point it would make sense to introduce a general _+_13/05 08:01
pumpkinas part of a semiring?13/05 08:01
pumpkinoh, I guess they already have that in Algebra13/05 08:02
pumpkinah well, thanks again for all your help :) bedtime now13/05 08:03
liyang(Oh wow. Activity!)13/05 08:03
pumpkinliyang: just me being a noob, nothing to get excited about :P13/05 08:04
* dolio hits the hay.13/05 08:06
liyangpumpkin: no, it was good.13/05 08:08
liyangThere needs to be an introduction to the standard library doc somewhere.13/05 08:08
liyangAnyone want to collaborate?13/05 08:09
liyangI don't think Nisse wants to write one (nor is he suited to writing an introduction from the perspective of someone who doesn't already know the stdlib)13/05 08:10
liyang(Oh, also, use the head libs if you can, rather than lib-0.1)13/05 08:11
kosmikusliyang: I would love to write some Agda documentation, but time is as always the problem13/05 12:02
kosmikusedwinb: ping13/05 12:02
edwinbhello13/05 12:02
kosmikushi there13/05 12:02
kosmikusI tried to install Idris13/05 12:02
edwinbyikes ;)13/05 12:02
edwinbwhat happened?13/05 12:02
kosmikusbut strangely enough, the binary segfaults13/05 12:02
edwinbweird13/05 12:02
kosmikusso you haven't actually seen this before, I guess13/05 12:03
edwinbwhich ghc?13/05 12:03
kosmikusI tested with 6.10.3 and 6.10.213/05 12:03
kosmikusI could also try 6.8.313/05 12:03
edwinbI'm using 6.10.113/05 12:03
edwinb6.8 is unlikely to work since I'm using some recent cabal stuff in the build13/05 12:04
kosmikusok13/05 12:04
kosmikusit's not unlikely that the actual problem is caused by me using Nix (www.nixos.org) rather than by Idris itself13/05 12:04
edwinbthis is the latest darcs version presumably?13/05 12:04
kosmikusbut I don't generally have segfaulting Haskell programs13/05 12:05
edwinbno, that's usually a bad sign with haskell programs...13/05 12:05
kosmikusyes, it's the latest darcs version13/05 12:05
edwinbI don't think it's doing anything at all strange on startup13/05 12:05
kosmikusyes, that's what I expected13/05 12:06
kosmikuslet me test it with 6.10.1 then13/05 12:06
edwinbjust reading command line arguments...13/05 12:06
edwinbI'm not really sure where to start here to be honest...13/05 12:06
kosmikusI mainly wanted to verify that this isn't a known problem13/05 12:06
edwinbno, it's new to me13/05 12:07
kosmikusok then13/05 12:07
edwinblet me know if you get any clues...13/05 12:07
kosmikusI'll let you know, yes13/05 12:07
kosmikusedwinb: what's the status of Prefix.hs13/05 13:09
kosmikusedwinb: I seem to have it in my darcs checkout, and it seems to be required(?), but it doesn't seem to actually be in the repo ...13/05 13:09
edwinbthat's generated by the Makefile13/05 13:25
edwinbit should shortly be superceded by some cabal magic13/05 13:25
edwinbit is an evil hack to get libraries in the right place...13/05 13:25
edwinbhmm, actually, it's not the only evil hack that needs fixing13/05 13:26
kosmikusah, but the Makefile isn't actually called by the cabal file13/05 13:46
kosmikusso you can't just build using cabal13/05 13:46
edwinbalas, not yet13/05 13:50
kosmikusI see13/05 13:55
kosmikusI think the segfault is solved though13/05 13:55
kosmikusproblem on my side13/05 13:55
kosmikususing incompatible library versions13/05 13:55
edwinbaha13/05 13:59
-!- byorgey_ is now known as byorgey13/05 15:59
kosmikusedwinb: ok, I got much further now13/05 16:29
kosmikusedwinb: now when I call idris, I get lots of output, and ultimately and index too large error13/05 16:29
edwinbthis is good!13/05 16:30
edwinbor rather, now it's my fault13/05 16:30
edwinbyou need to give a source file13/05 16:30
kosmikusah, ok13/05 16:32
kosmikusI was trying --help13/05 16:32
kosmikusbut that didn't work well13/05 16:32
kosmikusbut I'll play some more tonight13/05 16:32
doliodarcs ivor seems to have a rather funky .cabal file.13/05 16:34
kosmikushow so? I'm using the Hackage ivor, and haven't looked at the file. It seemed to just work.13/05 16:36
dolioIt's got some lines with "v v v v v v v" "^ ^ ^ ^ ^ ^ ^" and "*************" on them them. cabal doesn't like the last one.13/05 16:37
dolioHackage ivor works, yeah.13/05 16:37
kosmikusok13/05 16:37
kosmikusI'll not try darcs then13/05 16:37
doliodarcs has two different "Build-depends" lines, too. Maybe this is the result of a merge...13/05 16:39
byorgeyv v v v v and ^ ^ ^ ^ ^ ^ etc looks like an unresolved merge conflict.13/05 16:41
edwinbkosmikus: yes, helpful things like usage instructions would be nice13/05 16:41
edwinbI think I might take a but of time to make it more usable soon13/05 16:41
edwinbbit of time, even13/05 16:41
cocopumpkinis there a standard location for the standard lib? I have it in my agda search path, but was wondering where people usually put it13/05 20:45
kosmikuscocopumpkin: good question. I don't have it in any "standard" location ...13/05 20:48
cocopumpkinthere was talk about piggybacking on cabal for agda packages13/05 20:53
cocopumpkinmaybe ~/.agda/* somewhere?13/05 20:53
kosmikusI remember the talk, but I don't know if there was a conclusion13/05 20:59
kosmikusas a matter of fact, I'm not even using the released version of the stdlib right now, but still the darcs repo13/05 20:59
dolioThe patches to the standard library have some amusing descriptions.13/05 21:06
dolio"Made Everything boring"13/05 21:06
vixeyI like how half the stdlib is rewritting with Set replaced with Set113/05 21:07
vixeyand it comes up every few days on the mailing list13/05 21:07
vixeybut still nobody really knows a good way to do polymorphism?13/05 21:07
dolioThe Coq way isn't good?13/05 21:08
kosmikusbetter than the Agda way, in any case13/05 21:10
dolioCertainly.13/05 21:10
kosmikusI tend to use --type-in-type13/05 21:10
-!- koninkje_away is now known as koninkje13/05 21:58
-!- cocopumpkin is now known as copumpkin13/05 23:06
copumpkinhow does the compilation work in agda?13/05 23:19
copumpkindoes it pass through haskell?13/05 23:19
copumpkinwhy are head and tail private in Data.List?13/05 23:45
--- Day changed Thu May 14 2009
copumpkindoes Nat in the standard lib not have any algebraic structures defined on it?14/05 00:12
dolioAlgebraic stuff seems to be in Data.Nat.Properties.14/05 00:24
-!- koninkje is now known as koninkje_away14/05 04:26
pumpkinwould there be a problem with making syntactic sugar for records that looks like haskell typeclasses?14/05 04:38
vixeywhat do you mean exactly?14/05 04:40
pumpkinsorry14/05 04:40
pumpkinwell, as I understand it records (among other things) are exposing the dictionary behind typeclasses in haskell14/05 04:41
pumpkinbut I guess the syntax isn't a big deal really14/05 04:42
pumpkinso for simulating typeclass-like constraints on a type, you just ask for that record type?14/05 04:43
pumpkinbah, I don't think I'm being very clear, but I don't know the language yet :/14/05 04:43
vixeyno, it's not clear what you are saying14/05 04:43
pumpkinwell, on a high level, I'm wondering how I'd do the various things we do with typeclasses in haskell, in agda14/05 04:44
vixeyNot possible afaict14/05 04:44
vixeyThere's no way to define any 'open' object14/05 04:44
pumpkinoh14/05 04:44
pumpkinbut you could have similar behavior if you knew all the instances in advance?14/05 04:44
vixeyyes14/05 04:45
pumpkinlike, a record type definition would be the class ... bit, creating individual records would be the instance ... bits, and requesting the record type in a type signature would be the => constraints?14/05 04:45
vixeyhow do you make a record for monad?14/05 04:52
vixeyrecord Monad (m : Set -> Set) : Set1 where14/05 04:54
vixey field14/05 04:54
vixey  return : {A : Set} -> A -> m A14/05 04:54
pumpkinthey have http://www.cs.nott.ac.uk/~nad/listings/lib-0.1/Category.Functor.html#240 in the stdlib14/05 04:55
pumpkinit seems like you could do something similar for Monad14/05 04:55
vixey:/14/05 05:01
vixeyhow do you project out of a record14/05 05:01
vixeyopen Monad14/05 05:03
* vixey has trouble getting implicit parameters to solve enough here14/05 05:07
* pumpkin is totally clueless14/05 05:11
vixeyabout?14/05 05:12
pumpkinagda in general :) I just meant that I'm not much use14/05 05:13
vixeyI tried something out based on your idea but agdas implicit parameter solving isn't clever enough14/05 05:13
vixeyI thought it might do a bit of back-propagation though functions (so I could quote types), but it seems not14/05 05:14
* vixey has a look at Implicit.hs to see if what I wanted is possible14/05 05:22
vixeywhere can I find all the cool tricks with implicit parameters14/05 06:07
vixeyI couldn't do what I wanted with it14/05 06:08
* liyang wishes vixey could lurk moar so he can actually reply to him.14/05 10:45
* Laney lurks around liyang 14/05 12:38
-!- codolio is now known as dolio14/05 15:52
liyanghey Laney :314/05 16:27
-!- iago is now known as iago_14/05 18:02
-!- iago_ is now known as iago14/05 18:11
vixeyoh?14/05 20:19
vixeydid anyone find some more uses of implicit parameters?14/05 20:19
stevanmore than what uses?14/05 20:24
vixeymostly I have just used it like:  f : {T : Set} -> T -> ...14/05 20:25
stevanthe type checker can resolv trivial proofs that are passed as implicit arguments.14/05 20:28
vixeycan you show me some exmaples of it?14/05 20:29
stevanhttp://pastie.org/47835914/05 20:34
vixey:((14/05 20:35
vixeyagain with the broken formatting14/05 20:35
vixeyhmm14/05 20:35
vixeythis 'is not zero' is good14/05 20:36
vixeydo you know why it fills in ⊥? is it because it has only on constructor, or that it's a record ? or both14/05 20:36
vixeyseems to have to be a record14/05 20:38
vixey:/// this sucks14/05 20:45
vixeyhttp://pastie.org/47836914/05 20:45
vixeythat typechecks14/05 20:45
vixeybut if you uncomment it, adding a field to the record ... it doesn't typecheck14/05 20:45
vixeycan't do what I wanted14/05 20:48
vixeyI wonder why my code doesn't typecheck when the record has a field, should it really not?14/05 20:56
dolioIt checks, but it doesn't know what to fill in.14/05 21:04
dolioFor "record Q (T : Set) : Set where", all values are eta equal to each other, so it's trivial what it has to fill in, "record {}".14/05 21:05
dolioFor "record Q (T : Set) : Set where field name : Name", it could either fill in "record { name = `Bool`-name }" or "record { name = `ℕ`-name }".14/05 21:06
dolioBoth of which have type Q T, for any T.14/05 21:06
dolioThat you've named two records, `Bool` and `ℕ` isn't relevant.14/05 21:06
vixeyoh14/05 21:11
vixeyI was totally confused about how records work14/05 21:11
vixeyI thought it had to choose one of my instances14/05 21:11
--- Day changed Fri May 15 2009
--- Day changed Sat May 16 2009
-!- koninkje_away is now known as koninkje16/05 02:07
-!- koninkje is now known as koninkje_away16/05 06:31
copumpkinhi!16/05 06:46
copumpkinI was playing with something but agda doesn't like it, and I can't figure out why16/05 06:47
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=4923#a492316/05 06:49
copumpkinit was just a toy function to get a feel for things16/05 06:52
copumpkinobviously it's of no real use :)16/05 06:52
copumpkinI'll be back in a few :)16/05 06:54
dolioSo, if you think about it in terms of just the naturals...16/05 07:07
dolioIt's the difference between 'double n = n + n' and 'double z = z ; double (s n) = s (s (double n))'.16/05 07:07
dolioYou need to prove that those two functions are equal. It's non-obvious.16/05 07:07
copumpkinoh, I see! that makes sense16/05 07:08
copumpkinwhat would such a proof look like in agda? it seems like I could use induction, but I have no idea how to write real proofs in agda :P I've just been using it as a supercool typed haskell so far16/05 07:08
dolioYou'll need to look into equality. Generally people use something like 'data _==_ {a : Set} (x : a) : a -> Set where refl : x == x'.16/05 07:10
dolioThen you write something: 'double-proof : forall {n} -> double1 n == double2 n', which you'll do by induction.16/05 07:11
copumpkinthe propositional equality thing should help me here, right?16/05 07:12
dolioAnd to use it in map2, you'll probably need a function like: 'resp : forall {f x y} -> x == y -> f x == f y', which you'll use with f = \n -> Vec a n.16/05 07:12
copumpkinresp?16/05 07:13
dolioRespects.16/05 07:15
copumpkinoh16/05 07:15
dolioAnd, yes, propositional equality is the type you want to use.16/05 07:16
dolioTook me a while to find the definition.16/05 07:16
copumpkincool16/05 07:18
copumpkinso it seems like the fundamental thing it doesn't understand is that (suc n) + n === n + (suc n) ?16/05 07:55
dolioWell, (s n) + (s n) = s (n + (s n)), which it can tell from evaluation.16/05 07:57
dolioThen you're trying to give it 's (s (n + n))'.16/05 07:57
dolioSo it sees that the outermost constructor matches, but then it doesn't like 'n + (s n) = s (n + n)'.16/05 07:58
copumpkinI see16/05 07:59
copumpkindamn you agda for not being omniscient!16/05 07:59
copumpkin:)16/05 07:59
dolioIn general I'd try proving that (m * s n) = m + m * n.16/05 08:01
dolioThat probably gets you where you need to be.16/05 08:02
dolioI'm not sure how hard that is.16/05 08:02
copumpkinhmm16/05 08:03
copumpkinseems like that's most of what's missing to make a Semiring out of Nat16/05 08:05
copumpkinI'm surprised that isn't already in the std lib16/05 08:05
dolioIt's in Data.Nat.Properties.16/05 08:16
dolioMaybe not exported, though.16/05 08:16
copumpkinah, hmm16/05 08:18
kosmikusI think there's even a ring solver in the libs, but it's not very efficient (to typecheck)16/05 08:21
-!- codolio is now known as dolio16/05 17:03
-!- byorgey_ is now known as byorgey16/05 21:35
--- Day changed Sun May 17 2009
-!- codolio is now known as dolio17/05 01:45
copumpkinNat.Properties looks helpful, but it's all private17/05 06:12
-!- copumpki is now known as copumpkin17/05 06:18
dolioYou should prove some simple stuff yourself at first anyhow, to get the hang of it. :)17/05 06:21
copumpkinyeah, I should :) I've moved back to playing with my matrices, but I was wondering if there was such a notion as "class" constraints17/05 06:22
copumpkinI'd like to say that I want my matrices to contain anything that is a field17/05 06:23
vixeythat's what the module system is about17/05 06:23
dolioYeah, there's a couple ways to do similar things.17/05 06:28
copumpkinoh, I see, parametrized modules?17/05 06:28
dolioYou can either pass dictionaries to all your functions giving the field structure for the given type, or parameterize the module by the field.17/05 06:29
dolioIf you pass the dictionaries to a function, represented by records, you can open the record locally.17/05 06:29
dolioWhich is kind of like a type class you have to pass explicitly, with a little boilerplate.17/05 06:30
copumpkinso that requires the creation of a named dictionary for each instance of a type?17/05 06:30
copumpkin / record17/05 06:30
dolioParameterizing a whole module by it is probably nicer, though.17/05 06:31
dolioRight.17/05 06:31
copumpkinI haven't seen the std lib using the parameterized module thing, I guess they only took the record approach?17/05 06:31
dolioThey use it in setoid reasoning or something like that.17/05 06:32
vixeyI think the monads use it17/05 06:33
dolio'module Relation.Binary.PreorderReasoning (p : Preorder) where open Preorder p ...'.17/05 06:33
dolioThen all the stuff is defined in terms of 'carrier' which is in the Preorder record.17/05 06:34
dolioData.List.Equality uses it in a local module, too.17/05 06:35
copumpkinah, cool17/05 06:39
copumpkinis there any work for providing additional numeric types? reals, rationals, and so on?17/05 06:44
copumpkinI wonder if we could prove interesting things about continuous functions17/05 06:45
dolioThere's integers at least, right?17/05 06:45
copumpkinyeah, I think I saw them17/05 06:45
copumpkinI guess it'd be easy to make really slow reals17/05 06:46
copumpkinwell, not easy, but possible17/05 06:46
dolioYou could probably port whatever CReal does.17/05 06:47
copumpkinyeah17/05 06:47
dolioBut, yeah, it'd probably be slow.17/05 06:47
copumpkinproving stuff about that representation might be a little painful though17/05 06:47
dolioWell, technically, I don't even know if a straight port is possible, assuming you want to pass the termination checker.17/05 06:48
copumpkintrue17/05 06:48
copumpkinwow, even the : isn't primitive17/05 06:53
copumpkinor maybe it is17/05 06:53
copumpkincould Set be represented as a type dependent on a nat, to represent its cardinality?17/05 06:56
copumpkinto avoid Set1 etc.17/05 06:56
dolioI don't think so. But you can add something like that primitively to the type theory to get a similar effect.17/05 06:58
dolioThat's called universe polymorphism.17/05 06:58
copumpkinah17/05 06:59
dolioIf you think about doing it with Nat, you have to ask what type \i -> Set i is.17/05 07:02
copumpkinyeah, I guess you need a primitive somewhere17/05 07:02
dolioWhich I guess you can do, but then you have, like, an infinite tower Set i, and then something above all of them.17/05 07:02
dolioNat has to be built in, too.17/05 07:03
copumpkinyeah17/05 07:04
dolioMaybe similar questions come up with universe polymorphism, though. I'm not really familiar with its theoretical basis, or implementation.17/05 07:04
dolioCoq has it, though.17/05 07:05
copumpkinah17/05 07:06
dolioIt also hides the universe parameters most of the time, so it'll tell you things like "Type : Type", but it really means "Type[i] : Type[j] where j>i", but the former leads to cleaner looking stuff.17/05 07:06
copumpkinI see17/05 07:06
copumpkinit seems like coq has everything! :P17/05 07:06
dolioWell, it's been around somewhat longer, and has more people using/working on it.17/05 07:07
dolioI think, at least.17/05 07:08
copumpkinyeah, it seems more famous at least17/05 07:08
dolioIsabelle's another more established one, but it gets less press than Coq these days for some reason.17/05 07:08
copumpkinthat one has some haskell converter too, doesn't it?17/05 07:09
dolioI can't remember.17/05 07:09
copumpkinepigram and pi sigma are also roughly equivalent?17/05 07:45
copumpkinI guess there are no built-in matrix libs because we have no fields to use them on at this point17/05 07:48
copumpkinoh, and no fields type in the algebra module either17/05 07:49
copumpkinis there some way I can write the equivalent of ^{-1} in agda-mode? I need to define a multiplicative inverse for fields17/05 08:01
dolio\^-\^117/05 08:06
copumpkinoh, that's simple enough17/05 08:06
doliopi sigma is an intermediate language, isn't it?17/05 08:06
copumpkinoh, maybe17/05 08:07
-!- byorgey_ is now known as byorgey17/05 16:25
-!- codolio is now known as dolio17/05 18:26
-!- codolio is now known as dolio17/05 18:53
copumpkinwhy can't the law of excluded middle be represented in agda?17/05 23:41
kosmikuscopumpkin: it can be represented; it can't be proved17/05 23:44
copumpkinah17/05 23:46
vixeydo you understand what all the logical connectives mean?17/05 23:50
vixeylike 'or' and so on?17/05 23:50
copumpkime? yup, although I'm not sure how "formal" my knowledge of them is17/05 23:51
vixeyLEM proves  forall p : Program, halts p `or` not (halts p)17/05 23:54
copumpkiLEM?17/05 23:58
--- Day changed Mon May 18 2009
Laneylaw of the excluded middle18/05 00:05
copumpkioh, duh :)18/05 00:07
copumpkisorry, I'm not too fast today18/05 00:07
dolioWhat's halts look like? :)18/05 00:17
vixeyprobably like  eval p /= bot18/05 00:17
copumpkican I clear up some confusion I have that's not strictly related to agda, in here?18/05 00:19
copumpkiit has to do with halts18/05 00:19
vixey(that  eval _ /= _  would be one relation, not an 'eval' function btw)18/05 00:20
dolioAh.18/05 00:20
vixeywhat is it ?18/05 00:21
vixeyabout halts?18/05 00:21
copumpkiso I think the way I've been looking at it is wrong... I tend to see it as an inherently paradoxical function, a bit like how the premise of russell's paradox is the source of the paradox... but I'm not sure if that's correct, because people talk about the halting problem and not the halting paradox18/05 00:23
vixey'I tend to see it as an inherently paradoxical function' you're talkng about   halts : program -> bool  ?18/05 00:24
copumpkiyup18/05 00:24
dolio"Halting problem" gets its name because it's a decision problem about halting.18/05 00:24
vixeyhalts : program -> bool is fine you can write that in Haskell18/05 00:24
vixeythe problem is that  halts halts  isn't True18/05 00:25
copumpkiwell my problem with it is that if you assume the existence of the function, you can write a function that neither halts nor doesn't18/05 00:25
vixeythe really important issue I'm pointing out earlier is actually the meaning of 'o'r18/05 00:25
vixey'or'*18/05 00:25
vixeyyou can write halts in a strongly normalizing calculus too,  halts _ = True18/05 00:26
vixeyand we have  halts halts = True18/05 00:26
dolioHeh.18/05 00:26
dolioAnyhow, it's only if you assume that a Turing machine can decide halts for Turing machines that you get a problem.18/05 00:28
copumpkiyeah, that was the context I was thinking of18/05 00:28
vixeyoh sure, not arguing with that - Just Turing machines are kinda overdone18/05 00:28
dolioYou can have an oracle that decides halts for Turing machines, but you can't construct a Turing machine to defeat the oracle, because Turing machines don't have oracles.18/05 00:28
dolioOr, perhaps I should have worded that "you get a paradox".18/05 00:30
dolioOr contradiction.18/05 00:30
copumpkiyeah18/05 00:31
dolioI suppose it's a contradiction, because then you go on to conclude that Turing machines can't decide halts for Turing machines.18/05 00:31
dolioWhereas in Russel's paradox, your 'assumptions' are the axioms of naive set theory, so you have to amend those, which is a bit wider in scope.18/05 00:32
copumpkiyeah, I'm not saying it's analogous, but the kind of contradiction you get is similar18/05 00:33
vixeythe fun thing about halting is you can phrase any mathematical theorem as a question of whether a program halts or not18/05 00:34
vixeyif that's what 'turing complete' means - well you can do that in these logical frameworks/type theories too18/05 00:34
vixey(except instead of being about halting, it's about inhabitance)18/05 00:35
vixeyI don't see any relation of halting and russel18/05 00:35
copumpkithey're both like the "barber" paradox, if you've come across that18/05 00:37
vixeyneither of them seem like that if ask m18/05 00:38
vixeyme18/05 00:38
copumpkiif I have halts :: Program -> Input -> Bool, I can write f x = if halts f x then fix id else x18/05 00:38
copumpkiI can't really make a sophisticated argument showing them to be similar, but I can definitely see a similarity18/05 00:39
copumpkinot sure how else to show it though :)18/05 00:39
copumpkiI guess to be more correct, I should write halts :: (a -> a) -> a -> Bool, and f :: a -> a18/05 00:41
vixeythe usual formulation is  Nat -> Nat  actually18/05 00:42
vixeyand you work on the source of the program not the function itsself18/05 00:42
copumpkiwell yeah18/05 00:42
copumpkibut I couldn't write that succinctly18/05 00:42
vixeyof course programs are encoded as natural numbers so it's   halts :: Nat -> Bool18/05 00:42
copumpkianyway, that wasn't my point :P18/05 00:42
vixeyso what is?18/05 00:47
copumpkithat just like you don't know whether the barber who shaves people who don't shave themselves, shaves himself, you don't know whether the program that uses halts in the above way itself halts, and you don't know whether russell's set of sets that don't contain themselves contains itself18/05 00:49
* vixey thought the barber turned out to be a woman18/05 00:50
copumpkiI guess it could be made more clear in the halts case by making another intermediate function18/05 00:50
vixeyYou probably like that GEB book I hear it's all about this bullshit :p18/05 00:50
copumpkihah, my friends have recommended it to me but I haven't read it yet :)18/05 00:51
-!- copumpki is now known as pumpkin_18/05 01:42
-!- copumpki is now known as pumpkin18/05 18:50
-!- copumpki is now known as pumpkin18/05 20:19
--- Day changed Tue May 19 2009
copumpkiwhat are the "next steps" for agda? what are developers working on currently?19/05 07:04
solrizeis there some reason agate compiles to ghc instead of yhc core (which is already untyped)?  or even scheme?19/05 07:19
-!- copumpki is now known as pumpkin19/05 09:29
--- Day changed Wed May 20 2009
-!- copumpki is now known as hoggle20/05 20:31
-!- hoggle is now known as pumpkin_20/05 20:38
-!- codolio is now known as dolio20/05 20:57
British0zzyHi, I have some questions regarding parsing mixfix operators. Is agda's parser using the technique explained here: http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-mixfix.pdf ?20/05 23:36
--- Day changed Thu May 21 2009
dolioBritish0zzy: I just skimmed the paper, but I think the answer is "no". The paper is proposing a new way of defining mixfix operators.21/05 00:24
dolioBritish0zzy: Currently it uses Haskell-style "infix[lr]? N op" definitions.21/05 00:25
dolioN being an integer between 0 and 100, or something like that (rather than 0 to 9 like Haskell).21/05 00:27
copumpkinis the agda compiler using agate?21/05 00:27
British0zzyok, thanks.21/05 00:28
British0zzyDo you know of any examples of programming languages with precedence graphs?21/05 00:29
dolioNo. I've seen them proposed for Haskell as "what we should be doing," but I've not seen anyone do it. Maybe Agda will get it all nailed down, finally, if they're publishing papers on their progress.21/05 00:31
dolioOf course, there may be languages that do it that I don't know of.21/05 00:31
copumpkinsurely not!21/05 00:32
British0zzyI just want to get a feeling whether or not precedence graphs are nicer than a precedence table21/05 00:33
British0zzyin agda, can one define _! and have it bind greater than a prefix expression??21/05 00:34
dolioI think function application is always highest.21/05 00:35
dolioBut you can have _! bind tighter than some other operator ^_21/05 00:35
copumpkinwhat if I define !_, _!, and !_!21/05 00:36
British0zzyambiguity21/05 00:36
copumpkindoes it detect that one of them is impossible?21/05 00:36
dolioIf it can't figure it out, it will complain.21/05 00:36
British0zzyyou could get a warning when you define them, and a parsing error when it finds the ambiguity21/05 00:36
dolioBut I don't think it does any fancy type directed stuff or anything.21/05 00:36
British0zzyi think type directed stuff is the wrong way to go21/05 00:37
dolioIt would certainly allow for quite a bit of confusion. :)21/05 00:37
dolioI think I have a fancy natural number type around here somewhere, where I made 1+_ the successor.21/05 00:38
dolioSo you get to prove things like "m + 1+ n == 1+ m + n".21/05 00:38
copumpkinhah21/05 00:38
British0zzyi'm trying to develop a language where the compiler can recognize an expression like "1 + m" and convert it to "succ m" making for a much nicer proof assistant.21/05 00:41
copumpkinrewrite rules?21/05 00:41
British0zzyyea, but more powerful21/05 00:41
British0zzyuses the Rete matching algorithms21/05 00:42
British0zzyand it's dynamically typed, lol21/05 00:43
copumpkin:o21/05 00:43
British0zzywell, kinda21/05 00:44
British0zzyi guess it is "gradually typed"21/05 00:44
British0zzyi think that is the buzz word for it21/05 00:44
copumpkinah yeah21/05 00:44
British0zzyi've gotten it to do some cool type inference using the rete alg on ASTs21/05 00:45
British0zzybut whether or not it can verify a type is not guaranteed21/05 00:45
British0zzybut the cool thing is, if you have enough memory, and you let it sit there calculating long enough, it can do some pretty powerful inference21/05 00:47
British0zzyi still need to get it to where I can emit code.21/05 00:47
copumpkinI've thought about that for other optimizations21/05 00:48
copumpkinI think dons has mentioned it too21/05 00:48
copumpkinthe more compiler time you give it the more optimization it gets, it'd be pretty cool21/05 00:48
British0zzythe hardest part is writing a heuristic engine to determine the best code.21/05 00:50
British0zzybecause the rete alg will give the codegen numerous AST's representing the same program.21/05 00:50
British0zzyand i am trying to define a general language for defining rules.21/05 00:51
British0zzysuch as 1 + m => succ m21/05 00:51
British0zzybut m has to be a natural number21/05 00:52
British0zzy(or integer)21/05 00:52
British0zzyif you're interested, read this: http://cs.ucsd.edu/~ztatlock/publications/eqsat_tate_popl09.pdf21/05 00:53
copumpkin1 + (m : Nat) => succ m ?21/05 00:53
copumpkinooh thanks21/05 00:53
British0zzyyea, or: m : Nat, 1 + m => succ m21/05 00:53
British0zzywhere ',' represents that both must be true21/05 00:54
copumpkinwhy not just m : Nat => 1 + m = succ m21/05 00:54
copumpkinto use the => for constraints a bit like haskell does21/05 00:54
British0zzyi'm trying to develop a language based completely on equality saturation21/05 00:54
copumpkinah21/05 00:54
British0zzyI haven't determined a syntax for the rules yet, but as i get more accustomed to the rete alg and how rules are translated to it, hopefully I can create a general language for it21/05 00:56
British0zzyi want compiler optimizations to be written by the programmer21/05 00:56
British0zzyx : int, (2 ^ n) * x => x << n, could be a potential optimization. it's up to the heuristic engine to decide whether or not to apply it. You'd also need a rule like: k : int, (log k) : int => ∃ (n : int) s.t. k = 2 ^ n21/05 01:02
British0zzyis it proven that a dependently typed programming language is not turing complete?21/05 01:58
British0zzystatically typed21/05 01:59
copumpkindependent dynamic types seems like an odd concept :P21/05 02:00
British0zzylol, i guess, technically, when you mix values and types then a branch in a program represents a typecheck21/05 02:02
British0zzywhich is why completely general type checking is undecidable.21/05 02:04
British0zzycan one creat existential types in Agda?21/05 02:17
liyangBritish0zzy: yes. module Data.Product21/05 12:08
liyange.g. boring = \lambda x -> x & \equiv-refl : forall (x : X) -> \Sigma X (\lambda x -> x \equiv x)21/05 12:25
liyang(Where X can be inferred, you'd just write \exists \lambda x -> x \equiv x instead of \Sigma ...21/05 12:27
-!- copumpkin is now known as pumpkin21/05 19:09
-!- pumpkin is now known as copumpkin21/05 19:09
* liyang has conquered complete induction over ℕ! Really ought to stop naming things ‘cow’ though.21/05 21:01
liyangThat is all.21/05 21:01
liyangWhen I have the time, I'll write a gentle introduction to the Agda stdlib.21/05 21:02
liyangMaybe.21/05 21:02
Laneygood god please do21/05 21:05
stevanhow would you go about doing it? thru examples? theory?21/05 21:06
stevanfrom haskell as a starting point?21/05 21:08
Laneyyou'd have to explain too much then21/05 21:11
Laney"How to avoid reinventing the wheel using the standard library"21/05 21:12
Laney^by using21/05 21:12
-!- copumpki is now known as pumpkin21/05 23:47
--- Day changed Fri May 22 2009
-!- copumpki is now known as pumpkin22/05 02:04
liyangDunno lol. Haven't thought about it in much detail yet.22/05 08:55
liyangFollowing the style of learn you a haskell?22/05 08:55
-!- copumpki is now known as pumpkin22/05 16:09
-!- pumpkin is now known as Rianstradh22/05 23:32
-!- Rianstradh is now known as pumpkin22/05 23:32
-!- koninkje_away is now known as koninkje22/05 23:46
--- Day changed Sat May 23 2009
-!- codolio is now known as dolio23/05 01:56
-!- koninkje is now known as koninkje_away23/05 05:33
_shiftdear agda hackers, could you tell me what is wrong with the following code...?23/05 12:45
_shiftmymatch : ℕ → ℕ → ℕ23/05 12:46
_shiftmymatch k i with (compare k i)23/05 12:46
_shift... | equal _ = 123/05 12:46
_shift... | _       = 023/05 12:46
_shiftAFAICT, nothing is wrong, but agda complains:23/05 12:46
_shiftm != k of type ℕ23/05 12:46
_shiftwhen checking that the pattern equal _ has type Ordering k i23/05 12:46
_shiftversion: agda 2.2.2, lib-0.123/05 12:49
kosmikus_shift: first of all, shouldn't mymatch have a function type? where do the two arguments come from?23/05 13:02
kosmikus_shift: but I just see that perhaps my screen is messed up, because I can't correctly display unicode in my irc client23/05 13:03
_shiftah, ok, the signature is: mymatch : Nat -> Nat -> Nat23/05 13:05
kosmikusright23/05 13:05
kosmikusyou should try to replace the equal case with something like "mymatch k .k | equal _ = 1"23/05 13:06
_shifti don't get it23/05 13:08
kosmikusyou probably need "mymatch k .k | equal .k = 1", even23/05 13:12
kosmikusI can explain it later, but I first have to have lunch :)23/05 13:12
_shiftok, thanks:) i'll try23/05 13:14
stevanthe compare function in Data.Nat.Properties.strictTotalOrder is perhaps more suitable to do the thing you want, _shift.23/05 13:14
_shiftthanks, the 'cmp' from strictTotalOrder is a good example. i wonder what the dot is23/05 13:18
_shiftbtw, is there anywhere some documentation on the symtax of agda?23/05 13:19
_shiftthere is the reference manual draft, but the "dot" feature is not there23/05 13:34
byorgey_shift: the dot is for marking inaccessible patterns23/05 13:39
byorgeyarguments where you know what value the argument must have23/05 13:40
byorgeyin this case, Agda can just check for you that the second argument is also k (which is determined by the type of equal), instead of generating a fresh name for it23/05 13:41
byorgeyor something like that23/05 13:41
_shiftthanks. i'm a bit surprised that the first version without the dot didn't work, though...23/05 13:41
byorgeyI am too, actually, I don't really understand it well enough to know why the dotted version is required.23/05 13:42
copumpkinhmm, is it possible to have vararg functions in agda without wrapping the args up in a Vec or something similar?23/05 20:55
byorgeycopumpkin: I don't think so.23/05 21:05
byorgeynot unless you use tricks akin to the Haskell Printf stuff.23/05 21:06
byorgeyI'm not even sure how/if that would work in Agda without type classes.23/05 21:06
copumpkinyeah :/23/05 21:07
copumpkinalright ,thanks :)23/05 21:07
copumpkinI wasn't actually trying to do something in agda with varargs, was just curious if the dependent types allowed for something like that in an elegant manner23/05 21:07
edwinbyou could just compute the type of the funtion...23/05 21:14
edwinbwith printf, say, the format argument gives you the type of the rest of the function23/05 21:14
stevancopumpkin: something like this? http://pastie.org/48755923/05 21:19
copumpkininteresting23/05 21:20
stevanthere is a printf implementation in the cayenne paper also23/05 21:20
copumpkinthat's pretty neat :)23/05 21:21
byorgeyoh, I see, the typeclasses in Haskell's printf are just so that you can do computation at the type level23/05 21:30
byorgeyso of course you can do that directly in Agda =)23/05 21:31
byorgeystill, I think you have to be able to compute the type that you want from previous arguments, right?23/05 21:31
byorgeyyou couldn't just have a function that takes any number of Nats and returns their sum.23/05 21:31
kosmikusbyorgey: yes23/05 21:54
* kosmikus is just reading the log on #haskell to pick up on the hac phi discussion23/05 21:54
copumpkinhacking on agda at the hac phi could be neat!23/05 21:55
kosmikuscopumpkin: are you going to be at hac phi?23/05 21:55
copumpkinI'll do my best to be23/05 21:56
copumpkinI've put my name down23/05 21:56
kosmikushmm, it's so soon :)23/05 21:56
copumpkinnot sure I'd be much help for agda hacking, but I'd definitely be willing to try23/05 21:56
kosmikusI'm not sure if any of the Agda developers will be there23/05 21:57
kosmikusthat would certainly help23/05 21:57
kosmikusthere are AIMs though; next is in September in Gothenburg23/05 21:58
byorgeyAgda hacking at Hac phi is definitely welcome =)23/05 23:18
pumpkinbyorgey: how would accommodation and other boring things work? I've never been to something like this23/05 23:19
byorgeywe'll publish info on nearby hotels and such23/05 23:21
byorgeyunfortunately unless we get some really wealthy sponsor you'll have to pay for your own accomodation23/05 23:21
byorgeyalthough there may be a few local people willing to let others crash on their couch etc.23/05 23:22
pumpkinI can probably manage to pay for my own hotel room if I really try :P23/05 23:22
byorgeyok =)23/05 23:22
--- Day changed Sun May 24 2009
-!- pumpkin is now known as Gruppetto24/05 02:18
-!- Gruppetto is now known as pumpkin24/05 02:20
liyangcopumpkin: there's test/succeed/Printf.agda under the Agda source tree.24/05 17:23
liyangIn other news, I've registered http://learnyouanagda.org/ :324/05 17:23
stevan:-)24/05 17:34
liyangbut currently faffing with http://liyang.hu/ so I can use the same build system / UI for the pages. Nearly there...24/05 17:38
byorgeyparamorphisms are generalizations of catamorphisms.24/05 19:02
byorgeyer, sorry, wrong channel =)24/05 19:03
--- Day changed Mon May 25 2009
-!- byorgey_ is now known as byorgey25/05 12:41
endojellyhi there25/05 17:16
endojelly.n₁ + 0 != .n₁ of type ℕ25/05 17:16
endojellywhat can I do to resolve this, again?25/05 17:16
endojellynobody awake?25/05 21:25
liyangendojelly: oh hai.25/05 21:45
liyangendojelly: open import Data.Nat.Properties25/05 21:49
liyangendojelly: open CommutativeSemiring commutativeSemiring25/05 21:49
liyangendojelly: +-assoc : n + 0 \equiv n or something like that.25/05 21:50
liyangassoc? What am I on about?25/05 21:59
liyangSorry, rather full of dinner and watching Legally Blonde. I think it's infected me.25/05 21:59
liyangendojelly: here's something I prepared earl^Wjust a second ago -- http://liyang.hu/crap/AddZero.agda.html25/05 22:05
endojellyliyang, ah, thanks a lot! I just did it by hand by proving everything I needed myself, but I suspected it would already be in the standard library :P25/05 23:44
liyangIf you're just beginning Agda, the stdlib seems a bit overwhelming, so a lot of people get put off investigating further. D:25/05 23:47
liyangI do intend to do a tutorial of some sort on that. Time is always the problem though.25/05 23:48
--- Day changed Tue May 26 2009
endojellyliyang, thanks a lot again!26/05 08:35
endojelly_91 order !=< StrictTotalOrder26/05 10:23
endojellywhen checking that the expression i has type StrictTotalOrder26/05 10:23
endojellyokay, I have no idea why it wants a StrictTotalOrder at this place26/05 10:23
endojellyaah.26/05 10:27
endojellythat's why. I forgot to parameterize a parameterized module26/05 10:27
endojellyusing products makes everything really complicated :(26/05 12:58
endojellyI need to pattern match inside of a function type declaration26/05 15:44
endojellyif that makes sense26/05 15:44
endojellyis it possible?26/05 15:44
endojellyor am I thinking wrong? 8)26/05 15:44
endojellyI think somehow with-≡ is the answer26/05 16:24
endojellynow I just need to find the right substitution26/05 16:24
endojellythe product datatype makes life hard.26/05 16:24
--- Day changed Wed May 27 2009
-!- pumpkin is now known as Thwog27/05 00:48
-!- Thwog is now known as pumpkin27/05 00:52
liyangendojelly: could you show us the code? I'm not really sure exactly what you're trying to achieve...27/05 09:59
endojellyliyang, thanks, but the code is way different now27/05 12:15
liyangendojelly: hope you got your issue sorted out in any case. :327/05 18:21
endojellyliyang, I did, thanks! 8)27/05 18:22
liyangPS: content sought for http://learnyouanagda.org/ -- send me text; I'll make it suitable snarky and upload the finished work. Content under CC by-nc-sa.27/05 18:53
copumpkinawesome!27/05 18:53
copumpkinyou should get BONUS to contribute some art :P27/05 18:54
liyangI may steal some. :327/05 18:54
liyangOr take photos instead.27/05 18:54
liyangBecause I like my camera.27/05 18:54
copumpkinhah :) I'm sure he'd draw you some if you asked27/05 18:54
liyangAnd I have kittehz.27/05 18:54
copumpkinmaybe even a flaming unicorn with a rainbow27/05 18:54
stevanspeaking of art; it would be nice if agda had a logo27/05 18:55
copumpkina flaming unicorn!27/05 18:55
liyangstevan: take it up with the Agda mailing list. :327/05 18:56
liyangI tried thinking of a good domain name for the Agda Wiki which wasn't already taken, and failed. But then the idea of doing an informal (hah!) introduction to the language + stdlibs hit me...27/05 18:57
copumpkinagdawiki.org?27/05 18:57
copumpkinwikipagdia.org? :P27/05 18:58
liyangAgain, take it up with the mailing list. :)27/05 18:59
liyangI got slides to do before 15:00 tomorrow. :-/27/05 18:59
copumpkinjust throwing out random suggestions, am not being too serious :)27/05 18:59
liyangI do support wikipagdia.org though.27/05 19:00
--- Day changed Thu May 28 2009
-!- eelco_ is now known as eelco28/05 08:24
-!- Hennet_port is now known as Hennet_Port_Away28/05 11:24
-!- Hennet_Port_Away is now known as Hennet_port28/05 11:42
-!- Hennet_port is now known as Hennet_Port_Away28/05 16:43
-!- Hennet_Port_Away is now known as Hennet_port28/05 17:31
-!- Hennet_port is now known as Hennet_Port_Away28/05 18:01
-!- Hennet_Port_Away is now known as Hennet_port28/05 18:25
--- Day changed Fri May 29 2009
-!- jfredett_ is now known as jfredett29/05 06:07
-!- endojelly is now known as endo29/05 17:01
-!- endo is now known as endojelly29/05 17:01
--- Day changed Sat May 30 2009
-!- byorgey__ is now known as byorgey30/05 04:28
-!- byorgey_ is now known as byorgey30/05 17:55
-!- byorgey_ is now known as byorgey30/05 20:25
--- Day changed Sun May 31 2009

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