| --- Log opened Mon Dec 01 00:00:54 2008 | ||
| --- Day changed Tue Dec 02 2008 | ||
| * Smerdyakov has a hard time coming up with good examples distinguishing Agda from Coq. | 02/12 21:05 | |
| Smerdyakov | I have examples of pattern matching on terms in inductive types with indices that have structure; I have a simple K example; and I have an inductive-recursive definition. | 02/12 21:05 |
|---|---|---|
| vixey | I did a comparison | 02/12 21:06 |
| vixey | http://pastie.org/329164 if you like | 02/12 21:07 |
| vixey | it's a universe of types then a view defined on them | 02/12 21:07 |
| vixey | it's orders of magnitude easier in Agda .. | 02/12 21:07 |
| vixey | (basically typed out from Peter Morris Universes papers) | 02/12 21:09 |
| Smerdyakov | vixey, what does this development "do"? | 02/12 21:12 |
| vixey | it typechecks :) | 02/12 21:12 |
| Smerdyakov | But why should I care? | 02/12 21:12 |
| * vixey thinks it's a good example that distinguished Agda and Coq, the idea in the paper is that you can do generic programming over inductives or inductive families in this way | 02/12 21:14 | |
| vixey | Smerdyakov, (I posted it because you seemed to be looking for examples like that .. maybe I mixed up what you meant?) | 02/12 21:18 |
| Smerdyakov | I'm still trying to understand what is going on in it. | 02/12 21:18 |
| Smerdyakov | So you build up this machinery and only put it to use in converting between representations of naturals? | 02/12 21:20 |
| vixey | yes | 02/12 21:20 |
| vixey | well it doesn't really convert between representations | 02/12 21:21 |
| vixey | it's just that the names like “succ” get unfolded | 02/12 21:21 |
| vixey | I think it's possible to make an intepretation into 'real' agda types and write generic programs over them though | 02/12 21:23 |
| --- Day changed Wed Dec 03 2008 | ||
| -!- jfredett_ is now known as jfredett | 03/12 05:03 | |
| * Smerdyakov is failing again to get Agda built on a different machine, after spending a few hours on it. :( | 03/12 15:44 | |
| Smerdyakov | I think Agda needs a lot more documentation on building, to the point where it seems fair to consider that there hasn't yet been a "real" public release. | 03/12 15:46 |
| stevan | they updated the documentation on building yesterday | 03/12 15:56 |
| stevan | http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.InstallationOfAgdaFromSourceForNonprogrammers | 03/12 15:57 |
| Smerdyakov | Those instructions are, to me, obviously insufficient. | 03/12 15:59 |
| Smerdyakov | Configuration fails because of missing packages. | 03/12 15:59 |
| Smerdyakov | In general, I refuse to use packages that need more than one command line to install. | 03/12 16:00 |
| Smerdyakov | Unfortunately, I already committed to doing an Agda demo in class today. :P | 03/12 16:00 |
| Smerdyakov | What the heck.... somehow I ended up with an old Cabal version. I followed the download link from the first Google hit. | 03/12 16:09 |
| vixey | I did that too | 03/12 16:09 |
| vixey | that's why I had the wrong zlib version | 03/12 16:10 |
| vixey | so I patched it and gave the author a patch and he was like: " I fixed this last year" | 03/12 16:10 |
| Smerdyakov | Haskell is such a mess. | 03/12 16:10 |
| vixey | so is Agda ... | 03/12 16:18 |
| vixey | have you read tried to the source code? :p | 03/12 16:19 |
| Smerdyakov | No. | 03/12 16:19 |
| Laney | I swear I just did "cabal install" to install agda | 03/12 17:45 |
| Laney | then added the load path to my .emacs file | 03/12 17:45 |
| Laney | (obviously this requires the right cabal) | 03/12 17:45 |
| kosmikus | same here | 03/12 18:35 |
| --- Day changed Thu Dec 04 2008 | ||
| --- Day changed Fri Dec 05 2008 | ||
| --- Day changed Sat Dec 06 2008 | ||
| --- Day changed Sun Dec 07 2008 | ||
| --- Day changed Mon Dec 08 2008 | ||
| --- Day changed Tue Dec 09 2008 | ||
| --- Day changed Wed Dec 10 2008 | ||
| --- Day changed Thu Dec 11 2008 | ||
| --- Day changed Fri Dec 12 2008 | ||
| ksf | Warning: -fallow-undecidable-instances is deprecated: use -XUndecidableInstances or pragma {-# LANGUAGE UndecidableInstances#-} instead | 12/12 14:43 |
| ksf | Failing due to -Werror. | 12/12 14:43 |
| ksf | oh, come on. | 12/12 14:43 |
| * ksf gives up installing agda via portage | 12/12 14:44 | |
| vixey | yeah get the darcs repo and compile it | 12/12 14:50 |
| vixey | all the automatic installer stuff is broken | 12/12 14:50 |
| kosmikus | ksf: does portage have an up-to-date version anyway? | 12/12 14:58 |
| kosmikus | the last release of agda was ages ago | 12/12 14:58 |
| ksf | there's a darcs package, but it seems to pull a tagged version. | 12/12 14:59 |
| --- Day changed Sat Dec 13 2008 | ||
| -!- jfredett_ is now known as jfredett | 13/12 04:26 | |
| --- Day changed Sun Dec 14 2008 | ||
| kosmikus | ok, let's continue here then ;) | 14/12 18:59 |
| mmorrow | heh | 14/12 18:59 |
| SamB | what do you know, there is one | 14/12 19:00 |
| mmorrow | so i'm trying to get started and want to eval something (anything) in the interpreter (agda -I) | 14/12 19:00 |
| kosmikus | you need to import a module for natural number literals to be available | 14/12 19:00 |
| mmorrow | (w/ loading any files at first) | 14/12 19:00 |
| mmorrow | kosmikus: ah, ok. | 14/12 19:00 |
| mmorrow | so there's not something like a Prelude or equiv then i take it | 14/12 19:01 |
| SamB | um ... why are you using that thing ? | 14/12 19:01 |
| kosmikus | basically the only thing that's predefined is Set | 14/12 19:01 |
| kosmikus | and of course you can type in closed terms | 14/12 19:01 |
| kosmikus | \ x -> x | 14/12 19:01 |
| kosmikus | (\ x -> x) Set | 14/12 19:02 |
| SamB | are you going to be using a library ? | 14/12 19:02 |
| mmorrow | perfect! that's what i wanted. to successfuly eval at least one thing. :) | 14/12 19:02 |
| SamB | and ... what about Emacs ? | 14/12 19:03 |
| mmorrow | SamB: that's the next step. i want to eventually get to where i can ffi import haskell function and write (say) an echo server in Agda | 14/12 19:03 |
| mmorrow | ;) | 14/12 19:03 |
| SamB | huh | 14/12 19:03 |
| mmorrow | oh yes | 14/12 19:03 |
| SamB | how do you prove things with Haskell functions in the picture | 14/12 19:03 |
| SamB | ? | 14/12 19:04 |
| mmorrow | SamB: well, if i have to sacrifice some things to write an echo server, then so be it | 14/12 19:04 |
| kosmikus | well, you can assume some behaviour | 14/12 19:04 |
| kosmikus | there's no problem in proving things | 14/12 19:04 |
| mmorrow | i could still have isolated parts of the code which aren't "infected"? | 14/12 19:04 |
| kosmikus | the question is whether they're actually ture | 14/12 19:04 |
| kosmikus | s/ture/true/ | 14/12 19:04 |
| mmorrow | heh, yeah. | 14/12 19:05 |
| SamB | kosmikus: oh ? | 14/12 19:05 |
| kosmikus | SamB: you can postulate functions in Agda, for example | 14/12 19:05 |
| SamB | I wish haddock comments COULD be given for instances ... | 14/12 19:05 |
| kosmikus | hm? is this related? | 14/12 19:05 |
| SamB | I often wish to READ such | 14/12 19:05 |
| * mmorrow looks over the example code and reads a few tutorial | 14/12 19:06 | |
| * SamB is pulling and was talking about this patch: | 14/12 19:10 | |
| SamB | Fri Jul 18 11:01:53 EDT 2008 Liyang HU | 14/12 19:10 |
| SamB | * fixed documentation for Haddock 0.8 | 14/12 19:10 |
| mmorrow | what's the type of Set? like as in # in Cayenne. | 14/12 19:28 |
| mmorrow | (\(x : ?) -> x) Set | 14/12 19:28 |
| SamB | Main> :typeOf Set | 14/12 19:30 |
| SamB | Set1 | 14/12 19:30 |
| mmorrow | oh nice. thx | 14/12 19:31 |
| SamB | I tried :t but there were 3 commands that matched ;-P | 14/12 19:31 |
| mmorrow | heh | 14/12 19:32 |
| mmorrow | cool, so #_i === Set_(i-1) , i `elem` [1..] | 14/12 19:35 |
| mmorrow | (where #_i is the equivalent Cayenne concept) | 14/12 19:35 |
| * SamB wonders if agda has stopped inappropriately using the *ghci* buffer yet | 14/12 19:49 | |
| kosmikus | what's inappropriate? | 14/12 19:58 |
| mmorrow | is an expression of type (x' : x) -> x possible to write with a let expression alone? (i haven't figured out how to get where-expressions working at the prompt yet) | 14/12 20:04 |
| vixey | hey what's going on in here? | 14/12 20:04 |
| mmorrow | vixey: hey vixey | 14/12 20:04 |
| mmorrow | i just built agda | 14/12 20:04 |
| vixey | mmorrow you should try the emacs mode | 14/12 20:04 |
| mmorrow | vixey: i would if i didn't use vim (well, yi now sorta) | 14/12 20:05 |
| SamB | well, it's more of an Agda UI than an Emacs mode IMO | 14/12 20:05 |
| SamB | or rather, the Agda UI | 14/12 20:05 |
| vixey | it's the agda UI ... | 14/12 20:05 |
| vixey | yeah | 14/12 20:05 |
| vixey | nobody is writing a different one | 14/12 20:05 |
| mmorrow | hmm, ok. i should try that. | 14/12 20:05 |
| vixey | except I think you can get vim syntax coloring from the agda binary.. | 14/12 20:06 |
| vixey | not sure how but iirc that is at least possible | 14/12 20:06 |
| mmorrow | cool | 14/12 20:06 |
| SamB | why isn't the UI written in Agda ;-P | 14/12 20:06 |
| mmorrow | do either of you know how to write a one-liner expression of type (x' : x) -> x (assuming only basic syntax and Set{0..})? | 14/12 20:06 |
| vixey | yeah just \(x' : x) -> x' | 14/12 20:07 |
| mmorrow | \(x':x) -> x | 14/12 20:08 |
| vixey | no | 14/12 20:08 |
| mmorrow | let f : (t : Set1)(x : t) -> t; f (x:t) = t in f Set | 14/12 20:08 |
| mmorrow | that doesn't work though | 14/12 20:08 |
| vixey | you must put lots of spaces in | 14/12 20:08 |
| mmorrow | hmm | 14/12 20:08 |
| mmorrow | it says that `t' isn't in scope though | 14/12 20:08 |
| mmorrow | i think i can't pattern match on the type in "f (x:t)" | 14/12 20:09 |
| * mmorrow reads more | 14/12 20:09 | |
| vixey | f : (t : Set1)(x : t) -> t | 14/12 20:10 |
| vixey | f t x = x | 14/12 20:10 |
| mmorrow | ohhh | 14/12 20:10 |
| vixey | f : {t : Set1} (x : t) -> t | 14/12 20:10 |
| vixey | f x = x | 14/12 20:10 |
| mmorrow | ah, nice | 14/12 20:10 |
| vixey | f : (t : Set1)(x : t) -> t | 14/12 20:11 |
| vixey | f = \(t : Set1)(x : t) -> x | 14/12 20:11 |
| mmorrow | nice | 14/12 20:11 |
| mmorrow | Main> let f : {t : Set2}(x : t) -> t; f x = x in f Set | 14/12 20:11 |
| mmorrow | Set | 14/12 20:11 |
| mmorrow | exactly what i wanted to do :) | 14/12 20:12 |
| vixey | I realy hate this Set1 Set2 crap.. | 14/12 20:12 |
| mmorrow | i guess it has to be so for soundness | 14/12 20:12 |
| mmorrow | (or so i've read, but i don't know the precise argument) | 14/12 20:13 |
| vixey | the alternative is to write Set everywhere and have the computer place numbers on them | 14/12 20:13 |
| mmorrow | ah, yeah | 14/12 20:13 |
| mmorrow | i believe cayenne does that | 14/12 20:13 |
| vixey | anyway that's not in Agda so.. | 14/12 20:13 |
| mmorrow | Cayenne uses # for Set | 14/12 20:13 |
| mmorrow | ooh, i think i messed that up before | 14/12 20:14 |
| mmorrow | no, # := #_1 | 14/12 20:14 |
| mmorrow | #_i === Set_(i-1) , i `elem` [1..] | 14/12 20:14 |
| vixey | I had a brief look at Cayennes implementation | 14/12 20:15 |
| mmorrow | but i think you just always type # (i haven't used Cayenne enough to know if you ever have to be explicit about which # you're using) | 14/12 20:15 |
| mmorrow | vixey: what'd you think of it? | 14/12 20:15 |
| mmorrow | i've looked over the code a bunch. neat. | 14/12 20:15 |
| vixey | you can tell they were having fun hacking when they wrote it :) | 14/12 20:16 |
| mmorrow | heh | 14/12 20:16 |
| mmorrow | i bet | 14/12 20:16 |
| SamB | okay, library-test is failing | 14/12 20:20 |
| vixey | is that like make test? | 14/12 20:21 |
| SamB | vixey: maybe! | 14/12 20:21 |
| vixey | hey SamB | 14/12 20:24 |
| vixey | you were doing something with explicit substitutions in Agda right? | 14/12 20:24 |
| SamB | was I? | 14/12 20:25 |
| vixey | I guess I made it up then | 14/12 20:25 |
| SamB | either that or I didn't know what I was doing | 14/12 20:25 |
| mmorrow | there needs to be an agda evalbot for sure | 14/12 20:25 |
| vixey | http://www.citeulike.org/user/SamB/article/2711074 | 14/12 20:25 |
| vixey | http://naesten.dyndns.org:8080/repos/agda-lambda/Subst.agda | 14/12 20:27 |
| SamB | oh, maybe I was then ;-) | 14/12 20:30 |
| vixey | ;p | 14/12 20:30 |
| vixey | mmorrow but it's a bit awkward with the multiline definitions | 14/12 20:31 |
| SamB | but just saying "explicit substitutions" somehow made me think of the rewrite tactics in Coq ;-) | 14/12 20:31 |
| vixey | like I think most code is a few lines long with pattern matches? | 14/12 20:31 |
| vixey | Coq is giving me a sore arm :/ | 14/12 20:32 |
| vixey | holding left control for so long | 14/12 20:32 |
| vixey | well proof-general not Coq | 14/12 20:32 |
| mmorrow | vixey | 14/12 20:32 |
| vixey | yes? | 14/12 20:33 |
| mmorrow | : it should be doable though as long as you can put semis in between stuff | 14/12 20:33 |
| mmorrow | to stick it on one line | 14/12 20:33 |
| mmorrow | or else i guess you'd have to use some illegal/appropriate char to denote a linebreak for the purpose of the bot | 14/12 20:34 |
| mmorrow | then preproc the incoming string | 14/12 20:34 |
| SamB | ¶? | 14/12 20:39 |
| vixey | mmorrow, hey | 14/12 20:41 |
| vixey | that timber thing is in haskell right | 14/12 20:41 |
| vixey | you could hook it up with agda | 14/12 20:41 |
| vixey | for doing the server | 14/12 20:42 |
| vixey | but proving things in Agda ... ? how do you do it | 14/12 20:42 |
| vixey | I mean just writing out huge proof terms is not really a good way | 14/12 20:42 |
| mmorrow | yeah, timber's in haskell | 14/12 20:43 |
| vixey | other methods than reflective proofs? | 14/12 20:43 |
| mmorrow | that's an interesting thought. what do you ave in mind when you say "hook it up" to agda? | 14/12 20:44 |
| mmorrow | like as in, what part do you see as being the part that agda would be the best use for? | 14/12 20:46 |
| mmorrow | *to use for | 14/12 20:47 |
| vixey | I don't really know it just occured to me | 14/12 20:47 |
| vixey | I don't really program anything in Agda actually | 14/12 20:47 |
| mmorrow | vixey: me neither yet ;) | 14/12 20:47 |
| mmorrow | vixey: i want to as an experiment write something along the lines of an echo server (the important part being communicating over the network) in agda to see if i'd want to use agda for such things. (and along the way learn agda) | 14/12 20:50 |
| mmorrow | (and to see the extent to which writing such a thing in agda defeats the purpose of using the languge in the first place) | 14/12 20:52 |
| mmorrow | or if at all | 14/12 20:52 |
| mmorrow | *or if it defeats the purpose at all | 14/12 20:53 |
| mmorrow | how would one get across that this is well-typed? | 14/12 22:15 |
| mmorrow | map typeOf (2 :: 4 :: []) | 14/12 22:15 |
| mmorrow | i tried annotations in various places (in agda -I), but came up with syntax errors | 14/12 22:16 |
| mmorrow | (ignoring the fact that that would better be done another way) | 14/12 22:17 |
| mmorrow | n/m | 14/12 22:17 |
| vixey | typeOf ??! | 14/12 22:19 |
| vixey | is that a function | 14/12 22:19 |
| mmorrow | vixey: yeah, it's in examples/lib/Prelude.agda | 14/12 22:26 |
| mmorrow | i'm currently assembling my stdlib | 14/12 22:26 |
| mmorrow | Main> 41 + 1 | 14/12 22:29 |
| mmorrow | 42 | 14/12 22:29 |
| vixey | you got the actual stdlib? | 14/12 22:29 |
| vixey | of Agda | 14/12 22:29 |
| mmorrow | Main> pi | 14/12 22:29 |
| mmorrow | 3.141592653589793 | 14/12 22:29 |
| mmorrow | i had to define pi | 14/12 22:29 |
| mmorrow | vixey: kinda. i took everything under examples/lib/ and am picking out what i want and making a "personal" stdlib | 14/12 22:30 |
| mmorrow | :) | 14/12 22:30 |
| mmorrow | plus adding stuff that i want that isn't there | 14/12 22:30 |
| mmorrow | vixey: http://moonpatio.com:8080/fastcgi/hpaste.fcgi/view?id=574#a574 | 14/12 22:32 |
| mmorrow | typeOf is in there | 14/12 22:32 |
| mmorrow | looks like i'll have to figure out how to add Agda syntax highlighting to hpaste2 now | 14/12 22:32 |
| mmorrow | http://code.haskell.org/Agda/examples/lib/ | 14/12 22:33 |
| mmorrow | vixey: oh, and re: Set_i, looks like there's a flag to | 14/12 22:35 |
| mmorrow | --type-in-type ignore universe levels (this makes Agda inconsistent) | 14/12 22:35 |
| mmorrow | but.. | 14/12 22:35 |
| vixey | omg that was frustrating I couldn't find this thing | 14/12 22:35 |
| vixey | http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Libraries.StandardLibrary | 14/12 22:35 |
| vixey | This is the one I meant though | 14/12 22:35 |
| mmorrow | whoa | 14/12 22:35 |
| mmorrow | nice | 14/12 22:35 |
| * mmorrow looks | 14/12 22:35 | |
| vixey | IT's got some very interesting dependently typed things | 14/12 22:35 |
| mmorrow | very cool. that's gonna save me a ton of work :) | 14/12 22:36 |
| vixey | I want it to act like type-in-type but also topological sort the types (or give a universe inconsistency error) | 14/12 22:36 |
| mmorrow | interesting. do you know yet if it's possible to infer the levels of types or under what conditions it is? | 14/12 22:37 |
| mmorrow | because it'd be great if it was | 14/12 22:38 |
| vixey | so if you have this term | 14/12 22:39 |
| vixey | foo x = f x Set (g Set) h x | 14/12 22:39 |
| vixey | you can just put a fresh name to each one | 14/12 22:39 |
| vixey | foo x = f x Set[#g0] (g Set[#g1]) h x | 14/12 22:39 |
| vixey | then as you typecheck you build up a bunch of constraints like, { #g0 < #g7, #g3 < #g1, ... } | 14/12 22:39 |
| mmorrow | ah i see | 14/12 22:40 |
| mmorrow | then topo sort and voila | 14/12 22:40 |
| vixey | so it's always decidable if there is a mapping from there to the nats that make the (<)'s true | 14/12 22:40 |
| mmorrow | cool | 14/12 22:40 |
| mmorrow | that'd be interesting too if you allowed a /partial/ ordering on the #g_i (i'm not sure what this would mean off the top of my head) | 14/12 22:42 |
| SamB | isn't that what vixey just said though ? | 14/12 22:43 |
| mmorrow | SamB: i'm trying to figure that out | 14/12 22:43 |
| mmorrow | (i'm not sure) | 14/12 22:44 |
| SamB | those constraints form a partial order relation, do they not ? | 14/12 22:44 |
| SamB | I mean, when the code is right ;-) | 14/12 22:45 |
| mmorrow | to clarify (to make sure we're using the same defs), i'm using totally ordered as in Z (or N), and partially ordered as in C (complex nums) | 14/12 22:45 |
| SamB | huh, and I was thinking partially ordered like modules that aren't allowed to recursively import eachother ... | 14/12 22:46 |
| mmorrow | heh | 14/12 22:46 |
| mmorrow | yeah, so a partial odering would be a dag | 14/12 22:46 |
| mmorrow | so i guess the fact that she's topologically sorting things means that she's talking about a partial ordering | 14/12 22:47 |
| SamB | mmorrow: what did you define pi to be ? | 14/12 22:48 |
| mmorrow | but since Set_i is indexed by N, which is not a dag (well, a trivial on), but has a total ordering | 14/12 22:48 |
| mmorrow | i'm confused | 14/12 22:48 |
| mmorrow | SamB: i just used ghci> pi::Double | 14/12 22:48 |
| mmorrow | and copy/pasted | 14/12 22:48 |
| SamB | that doesn't sound too good somehow | 14/12 22:48 |
| mmorrow | apparently agda's using ghc's Double, so that's the best you can do | 14/12 22:49 |
| mmorrow | {-# BUILTIN FLOAT Float #-} | 14/12 22:49 |
| SamB | am I the only one who doesn't see how that's useful ? | 14/12 22:49 |
| mmorrow | type Float = Prelude.Double | 14/12 22:50 |
| mmorrow | SamB: yes :) | 14/12 22:50 |
| mmorrow | what if i wanted to code up a FFT in agda? | 14/12 22:50 |
| vixey | do you know Fin? | 14/12 22:50 |
| mmorrow | vixey: i saw that module, but didn't look at it yet | 14/12 22:50 |
| SamB | mmorrow: you can't say yes, you could say no if you didn't either though | 14/12 22:50 |
| mmorrow | heh | 14/12 22:51 |
| vixey | mmorrow, with total correctness proof? | 14/12 22:51 |
| SamB | you can't code correct FFT with floating point can you ? | 14/12 22:51 |
| vixey | if not .. just like you would in haskell I gues... | 14/12 22:51 |
| mmorrow | vixey: that'd be cool | 14/12 22:51 |
| vixey | SamB: well somebody did it http://www.cs.ru.nl/~venanzio/publications/FFT_TPHOLs_2001.pdf | 14/12 22:51 |
| mmorrow | SamB: the correctness isn't at the level of rounding | 14/12 22:51 |
| SamB | mmorrow: um, I beg to differ! | 14/12 22:52 |
| mmorrow | SamB: and anyone using floating point for numerical analysis (which is everyone) always bounds their error | 14/12 22:52 |
| SamB | okay, I suppose that's good enough, but how are you going to prove stuff like that using native floats ??? | 14/12 22:52 |
| vixey | Fin 0 has no elements, Fin 1 ~ (), Fin 2 ~ Bool, Fin 3 ~ Either () (Either () ()) ... | 14/12 22:53 |
| mmorrow | SamB: i don't know | 14/12 22:53 |
| vixey | Fin n ~ { i : nat | i < n } | 14/12 22:53 |
| mmorrow | SamB: also, i'm assuming that i'd actually use agda to /execute/ the fft as well | 14/12 22:53 |
| mmorrow | which would suck if it was realllllly slow | 14/12 22:54 |
| mmorrow | anyhow, i just threw that out there. i haven't really thought about it | 14/12 22:54 |
| * mmorrow looks at Fin | 14/12 22:56 | |
| SamB | hmm, perhaps http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.90.1712 holds the answer | 14/12 23:05 |
| SamB | (total coincidence that I bumped into it -- I was just correcting stuff in vicinity of C-CoRN ...) | 14/12 23:05 |
| mmorrow | interesting | 14/12 23:07 |
| vixey | SamB, do you work in C-CoRN by the way? | 14/12 23:09 |
| SamB | not really | 14/12 23:09 |
| SamB | the thing I tried to use it for seems to be really hard ... | 14/12 23:09 |
| vixey | "Our high-level formalization of floats: pairs" lol | 14/12 23:10 |
| vixey | what was that? | 14/12 23:10 |
| SamB | perhaps impossible ? | 14/12 23:10 |
| SamB | I was trying to lift a ring structure pointwise | 14/12 23:11 |
| vixey | I don't know what that means :( | 14/12 23:11 |
| SamB | instance Num n => Num (a -> n) | 14/12 23:12 |
| SamB | only, you know, with the ring axioms carrying over too ;-) | 14/12 23:12 |
| vixey | oh | 14/12 23:13 |
| vixey | it's const? | 14/12 23:13 |
| SamB | what the ? | 14/12 23:13 |
| vixey | 9 gets lifted to const 9 ? | 14/12 23:13 |
| SamB | oh, sure | 14/12 23:13 |
| vixey | with x + y = \o -> x o + y o | 14/12 23:13 |
| SamB | but I was trying to lift the structure, not the elements | 14/12 23:13 |
| * vixey I guess I really don't understand | 14/12 23:13 | |
| SamB | actually you seem to have it | 14/12 23:14 |
| SamB | but I was having trouble with some stuff trying to do it with equivalence as the primitive, so I decided to try the apartness-as-primitive approach | 14/12 23:15 |
| vixey | (=) is a tricky thing | 14/12 23:16 |
| SamB | but then I couldn't find a way to represent apartness that satisfied the ... er ... cotransitive property without requiring something of the argument type | 14/12 23:17 |
| SamB | http://c-corn.cs.ru.nl/documentation/CoRN.algebra.CSetoids.html#lab35 | 14/12 23:18 |
| vixey | I haven't read about how setoids work yet | 14/12 23:20 |
| SamB | where ? | 14/12 23:20 |
| vixey | anywhere | 14/12 23:20 |
| SamB | basically, it's a first-class equivalence relation | 14/12 23:21 |
| SamB | hmm, make test fails too :-( | 14/12 23:22 |
| * mmorrow just figured out how to import arbitrary haskell functions. <sys/socket.h>-via-haskell-ffi-via-agda-ffi here i come | 14/12 23:50 | |
| * mmorrow meant here he comes | 14/12 23:51 | |
| vixey | hehe | 14/12 23:51 |
| vixey | you know the IO definition as a GADT and as a Cont IOTree? | 14/12 23:51 |
| vixey | do you think you will do it like that? | 14/12 23:51 |
| vixey | I guess there are already some monads in the stdlib but | 14/12 23:52 |
| mmorrow | i do. the first time i saw the IOTree def was the other day, but it makes sense i guess. | 14/12 23:52 |
| mmorrow | vixey: yeah, i'm not sure how i'm gonna do it yet. | 14/12 23:52 |
| mmorrow | IO.agda is pretty minimal | 14/12 23:52 |
| mmorrow | and IO could always be split up into Net, Disk, ... (whatever) | 14/12 23:54 |
| mmorrow | vixey: have you seen IOSpec? it's pretty cool. | 14/12 23:54 |
| vixey | have seen the papers about it | 14/12 23:54 |
| mmorrow | oleg's ZFS is cool as well | 14/12 23:55 |
| vixey | I wish I could stay on a bit but I have to go | 14/12 23:55 |
| vixey | later | 14/12 23:55 |
| mmorrow | vixey: oh, check out the code on hackage. | 14/12 23:55 |
| mmorrow | later | 14/12 23:55 |
| --- Day changed Mon Dec 15 2008 | ||
| mmorrow | ByteString.agda http://moonpatio.com:8080/fastcgi/hpaste.fcgi/view?id=584 | 15/12 04:32 |
| -!- kosmikus_ is now known as kosmikus | 15/12 13:55 | |
| --- Day changed Tue Dec 16 2008 | ||
| --- Day changed Wed Dec 17 2008 | ||
| --- Day changed Thu Dec 18 2008 | ||
| --- Day changed Fri Dec 19 2008 | ||
| --- Day changed Sat Dec 20 2008 | ||
| --- Day changed Sun Dec 21 2008 | ||
| --- Day changed Mon Dec 22 2008 | ||
| --- Day changed Tue Dec 23 2008 | ||
| --- Day changed Wed Dec 24 2008 | ||
| --- Day changed Thu Dec 25 2008 | ||
| --- Day changed Fri Dec 26 2008 | ||
| --- Day changed Sat Dec 27 2008 | ||
| --- Day changed Sun Dec 28 2008 | ||
| --- Day changed Mon Dec 29 2008 | ||
| --- Day changed Tue Dec 30 2008 | ||
| --- Day changed Wed Dec 31 2008 | ||
| --- Log closed Thu Jan 01 00:00:36 2009 | ||
Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!