October.log

--- Log opened Wed Oct 01 00:00:23 2008
-!- Jehst is now known as willone01/10 18:51
--- Day changed Thu Oct 02 2008
stepcutin, Dependently Typed Programming in Agda by Ulf Norell, he defines or like this:02/10 23:18
stepcut_or_ : Bool -> Bool -> Bool02/10 23:18
stepcuttrue or x = x02/10 23:18
stepcutfalse or _ = false02/10 23:18
stepcut 02/10 23:18
stepcutbut that seems like _and_ to me. Am I missing something ?02/10 23:18
rwbartonI agree02/10 23:29
stepcutok, just checking :)02/10 23:30
--- Day changed Fri Oct 03 2008
--- Day changed Sat Oct 04 2008
vixeycan you do induction-recursion in Agda?04/10 23:33
--- Day changed Sun Oct 05 2008
--- Day changed Mon Oct 06 2008
--- Day changed Tue Oct 07 2008
--- Day changed Wed Oct 08 2008
--- Day changed Thu Oct 09 2008
-!- dreixel_ is now known as dreixel09/10 13:11
--- Day changed Fri Oct 10 2008
-!- dreixel_ is now known as dreixel10/10 07:59
vixeyhi10/10 23:24
vixeydid anyone try encoding SPTs in Agda?10/10 23:24
vixeyyay10/10 23:33
vixeylots more people10/10 23:34
vixeyelliottt: well if you want something to try.. I am wondering how SPTs would turn out in AGda10/10 23:40
vixeyI wrote it up in Coq but it's very hard to write 'Nat'_ind with it10/10 23:41
elliotttoh, could i see your coq version?10/10 23:41
elliottti'm taking a coq class at psu this term :)10/10 23:41
* vixey is wondering if it wolud be loads easier with Agdas pattern matching10/10 23:41
vixeywow everyone is doing coq classes except me !10/10 23:41
elliotttwell, pattern matching ~~ inversion, right? :)10/10 23:41
* vixey jelous10/10 23:41
elliottthehe10/10 23:41
elliotttit's a fun class so far.10/10 23:42
vixeyhm I suppose yes it can be10/10 23:42
vixeyhttp://muaddibspace.blogspot.com/2008/10/i-suppose-i-better-take-different.html10/10 23:42
elliotttall the course materials are online, if you'd like to take a look10/10 23:42
vixeyyeah, that would be great10/10 23:42
vixeyIt's just directly taken out of http://www.cs.nott.ac.uk/~pwm/10/10 23:42
vixeyConstructing Universes for Generic Programming10/10 23:43
elliotttuh oh, admitted's :)10/10 23:44
vixeyI would go fill them in if my proof worked :)10/10 23:47
elliottt:)10/10 23:48
vixeywhat is the URL?10/10 23:54
elliottthttp://web.cecs.pdx.edu/~apt/cs510coq/10/10 23:55
vixeycool10/10 23:57
--- Day changed Sat Oct 11 2008
vixeyanyway11/10 00:11
vixeyif you try that SPT stuff do tell me :p11/10 00:11
vixeyI am not sure how it would go exactly but should be interesing11/10 00:11
vixeyI might have another stab at my version using some tools from the epigram papers11/10 00:11
kosmikusvixey: I've recently typed in some stuff from the "Universes for Generic Programs and Proofs" paper by Benke/Dybjer/Jansson which is vaguely related to SPTs by Morris11/10 14:44
vixeyoh I would really like to see that please11/10 14:45
kosmikusit's not very impressive11/10 14:51
kosmikusbut yeah, wait a minute11/10 14:51
kosmikusvixey: http://people.cs.uu.nl/andres/Universes.agda11/10 14:57
vixeyis this in UTF-8?11/10 14:58
kosmikusyes11/10 14:59
vixeyF⟦ NonRec A φ ⟧ X = Σ A (\x -> F⟦ φ x ⟧ X)11/10 15:01
vixeyI've got this11/10 15:01
vixeyF<question mark> NonRec A <phi> ...11/10 15:01
vixeyI guess it's my font missing some things11/10 15:01
vixeyoh is this W trees?11/10 15:05
kosmikusno, not quite, I think11/10 15:19
-!- kosmikus_ is now known as kosmikus11/10 15:40
cpfris this another channel you made?11/10 22:21
vixeynot me11/10 22:21
--- Day changed Sun Oct 12 2008
vixeyso what is everyone coding in Agda :)12/10 19:09
miakelhey vixey, I'm just doing the exercises in "Dependent Types at Work" (as homework)12/10 19:11
vixeyoh cool12/10 19:13
vixeyso you have a class with dependent type programming?12/10 19:14
miakelyeah, it's a course on types for programs and proofs at chalmers, these last few lectures are by ulf norell on agda12/10 19:15
miakelhttp://www.cs.chalmers.se/ComputingScience/Education/Courses/types/index.html12/10 19:15
vixeyI wish I could get on a course like that .. much more interesting that 'data structures and algorithms'12/10 19:17
vixeycool Krivine machine12/10 19:18
miakelyes, it's one of the more interesting courses I've taken - where do you study?12/10 19:18
vixeyheriot watt they like teaching people to play computer games12/10 19:19
vixeyit's a bit ridiculous12/10 19:19
vixeyhave you seen thoerems for free12/10 19:20
vixeythere's a link on that page about parametric polymorphism12/10 19:20
miakelplaying games can be a very lucrative business these days!  nope, haven't seen that12/10 19:20
vixeyif you plug in a type, you get a theorem back12/10 19:21
vixeye.g. length = length . $map f12/10 19:21
vixeyI was wondering about coding in something like Agda, to give a real theorem12/10 19:22
vixeysomething you could use in a proof12/10 19:22
vixeyhaven't tried but it seems like a fun idea12/10 19:22
vixeyare there any things you want to program in agda or similar12/10 19:24
vixey?12/10 19:24
miakelthe whole terms-as-proofs idea is extremely sexy, and I'm taking a course on logic also, but right now I'm just trying to learn the basics12/10 19:26
vixeyyeah It's wonderful that we might write programs that have _meaning_ :)12/10 19:26
miakelit's such an elegant and rich correspondence, it blows my mind :)12/10 19:30
* vixey nods 12/10 19:31
vixeyI am finding lots of new things too - like I just discovered this NoConfusion thing12/10 19:31
vixeyit's in a few Epigram papers, It's a really cool example of dependently typed programming12/10 19:31
miakelI'll have to check that out... so, given X : Set and P : X -> Set, shouldn't P be equivalent to (x : X) -> P x?12/10 19:47
miakelI'm trying to figure out how to write forall/exists predicates "inline" that are more complicated than just predicates I have in the environment, like "not P(x)" or "P(x) and Q(x)"12/10 19:49
miakelbut agda doesn't agree that (x : X) -> P x is of type X -> Set12/10 19:50
vixeyhuh I'm not sure what you mean12/10 20:00
vixeyP can't be equiv. to some expression containing P can ita12/10 20:00
vixeyHave you got a definition of  not ?12/10 20:03
miakelI'm thinking of how f is equivalent to \x -> f x, I want to name the parameter so I can apply stuff (like not) to it12/10 20:04
miakelyeah, it's just Not A = A -> False12/10 20:04
vixeyhmm12/10 20:04
vixeyf o equivalent to (\x -> f x) o12/10 20:05
vixeybut f equiv. to \x -> f x12/10 20:05
vixeyI'm not sure what equiv is12/10 20:05
vixeyinstead of using lambda what about composing thisg12/10 20:06
vixeylike  Not • P12/10 20:06
vixeyNot P x = P x -> False12/10 20:12
vixeynow  Not P  should be like with the previosu  \x -> Not P12/10 20:12
kosmikushi. anyone around?12/10 21:34
kosmikusI'm wondering whether we should formally found this channel. Register it etc ...12/10 21:35
kosmikusget lambdabot in here. write an Agda plugin for it and so on ...12/10 21:35
vixeywhat would an Agda plugin da?12/10 21:38
vixeydo*12/10 21:38
vixeyI am here now12/10 21:39
kosmikushi vixey12/10 21:44
kosmikuswell, an Agda plugin is not as important as registering the channel12/10 21:44
kosmikusan Agda plugin could be similar to a ghci plugin and allow to typecheck and/or evaluate Agda expressions from within irc12/10 21:45
kosmikusoh, I see that the channel *is* registered12/10 21:46
kosmikusthat's good12/10 21:46
kosmikusjfredett seems to have done it quite some time ago12/10 21:47
vixeyI woulb i12/10 21:53
vixeyIf someone wrote an IRC bot in Agda that would be nice12/10 21:53
kosmikushehe12/10 21:53
kosmikusthat would be better, of course12/10 21:53
kosmikusbut still quite a bit of work, given the lack of libraries12/10 21:54
vixeyI guess one could use a haskell IRC library exposed to Agda as a IRC monad12/10 21:55
vixeyIt's not something I'm interested in programming though12/10 21:55
vixeyAgda is the closest thing around to a metacircular proof assistant?12/10 22:55
kosmikusmetacircular?12/10 22:59
kosmikusI would assume that Epigram with * : * as a default is closer, and Coq with stratified universes is also not that much different.12/10 23:00
vixeyI think Epigram 2 will be much more but it seems only about 1/4 implemented12/10 23:01
kosmikusyes, it's taking a long time, unfortunately12/10 23:02
vixeyI wish I could help :p12/10 23:02
kosmikusmaybe you can. have you asked?12/10 23:02
vixeyno12/10 23:02
kosmikusI think it's probably difficult to do much because of the way Conor generally works.12/10 23:03
vixeyhow is that?12/10 23:03
kosmikusBut it certainly can do no harm to ask in a friendly way. Say that you're interested in Epigram and that you'd like to help with development. Ask if there's anything you can do.12/10 23:03
kosmikusWell, Conor is quite brilliant and has a lot of ideas, but that also leads to some strong opinions on how code should be written. I think he likes to have knowledge of every line of code that's in the project, and that can slow things down. I may be wrong though.12/10 23:04
vixeyhede12/10 23:05
kosmikusHe's recently started a new job, and probably has quite a few things to do there (teaching ...). I know the feeling ...12/10 23:05
--- Day changed Mon Oct 13 2008
--- Day changed Tue Oct 14 2008
--- Day changed Wed Oct 15 2008
-!- Irssi: #agda: Total of 6 nicks [0 ops, 0 halfops, 0 voices, 6 normal]15/10 13:53
vixeyhello15/10 19:04
--- Day changed Thu Oct 16 2008
--- Day changed Fri Oct 17 2008
jfredettPeople talked to me? on #agda?17/10 02:47
jfredettholy crap!17/10 02:47
jfredetthmm, maybe I should try my new idea out in agda17/10 02:47
jfredett...17/10 02:48
jfredettinstead of haskell..17/10 02:48
jfredett*ponders*17/10 02:48
kosmikusjfredett: why wouldn't we talk to you? :)17/10 07:46
vixeyhello17/10 20:38
jfredettkosmikus: there aren't just that many people on this channel17/10 23:14
jfredettusually no talking occurs17/10 23:14
vixeywhat did I miss17/10 23:17
vixeyso if agda emacs mode freezes do you know what to do?17/10 23:42
kosmikusCtrl-G usually works for me17/10 23:47
kosmikusyou can then switch to the *ghci* buffer and see what happened17/10 23:47
kosmikusvixey: ^^17/10 23:47
vixeyah thank you17/10 23:47
kosmikusjfredett: true, but that might change over time ;)17/10 23:47
--- Day changed Sat Oct 18 2008
vixeyno I can't build agda 2 this sucks18/10 00:00
vixeywell agda builds, agda-executable doesn't18/10 00:01
vixeyit fails because of zlib linking problems18/10 00:01
vixeyand that's why it crashes in emacs18/10 00:01
vixeyso irritating :/aoe18/10 00:01
--- Day changed Sun Oct 19 2008
--- Day changed Mon Oct 20 2008
--- Day changed Tue Oct 21 2008
--- Day changed Wed Oct 22 2008
--- Day changed Thu Oct 23 2008
--- Day changed Fri Oct 24 2008
--- Day changed Sat Oct 25 2008
vixeydoes anyone have any ideas how to make agda 2 faster?25/10 20:46
vixeynobody happens to have the ISPT universe in Agda?25/10 21:07
vixeySPF25/10 21:08
--- Day changed Sun Oct 26 2008
Saul_I'm having a bit of trouble with an assignment in agda26/10 07:18
Saul_I need to define the function shift : forall {m n} -> (Fin m -> Fin n) -> Fin (suc m) -> Fin (suc n)26/10 07:19
Saul_But I'm not sure what to do when m = zero26/10 07:19
Saul_since I can't feed an Fin 0 into the function26/10 07:20
Saul_Can anyone help me with this?26/10 07:20
vixeySaul_: What should the funcction do?26/10 08:44
vixeySaul_: i.e. shift _ _ = zero isn't very interesting26/10 08:44
Saul_as far as I can tell it should only change the type the function works on, not the values it returns26/10 08:55
vixeythat's impossible26/10 09:12
vixeyDo you have an interpretation of what Fin n means?26/10 09:12
Saul_It's the amount of bound variables in a lambda-esque datatype26/10 09:20
vixeythat's one application26/10 09:20
vixeyFin 0 = False, Fin 1 = Unit, Fin 2 = Bool, etc26/10 09:21
Saul_You mean that you want to know if I know what Fin means in general?26/10 09:21
vixeyso you can think of Fin m -> Fin n as a function from a set of m elements into a set of n elements26/10 09:22
Saul_I usually see Fin n as a number between 0 and n - 126/10 09:24
Saul_maybe that's not as useful on a type level though26/10 09:24
vixeyno that's a good interpretation of an arbirtary element of Fin n26/10 09:25
Saul_I think I got it :D26/10 09:53
Saul_I misinterpreted what the shift function should do26/10 09:53
Saul_that hole that I had with m = 0 is exactly the special case in the main function that I had to do differently26/10 09:54
Saul_Now I'll just have to get it to work26/10 09:54
vixeyyeah I think I see what you mean26/10 09:56
vixeyI can actually see two sensible definitions of lift though26/10 09:58
vixey4 infact26/10 09:59
vixey(not counting shift _ _ = zero)26/10 10:00
Saul_I needed shift f zero = zero26/10 10:00
Saul_shift f (suc x) = suc (f x)26/10 10:00
Saul_It was what you said about Fin n being a set with n elements26/10 10:01
vixeycool26/10 10:01
vixeyHave you seen thick and thin?26/10 10:01
Saul_there was an extra possible value in the input and output, which was exactly where my problems where in the main function that was supposed to use it26/10 10:02
* vixey nod26/10 10:02
Saul_no, what is it?26/10 10:02
vixeycheck out slides 9 & 1026/10 10:03
vixeyhttp://strictlypositive.org/dtp99/26/10 10:03
vixeythick and thin are very nice for proving stuff about Fin because they expose some good structure26/10 10:03
Saul_seems interesting26/10 10:08
Saul_What is your real name btw?26/10 10:09
vixeyvicky26/10 10:10
Saul_Yeah it said that in your whois, but what is your full name?26/10 10:11
vixey:////26/10 21:20
vixeywho wouldn't implement universe polymorphism26/10 21:20
vixeythis actually makes experimenting really difficult26/10 21:21
vixeyI guess I can just use --type-in-type and be realy careful..26/10 21:22
--- Day changed Mon Oct 27 2008
-!- Irssi: #agda: Total of 6 nicks [0 ops, 0 halfops, 0 voices, 6 normal]27/10 10:45
Laneyyo27/10 10:46
vixeyhttp://www.cs.nott.ac.uk/~nad/repos/simply-typed/27/10 18:52
vixeythis is very nice27/10 18:52
--- Day changed Tue Oct 28 2008
vixeyyou see papers where people write things like,28/10 23:27
vixeydata Ty : Ctxt -> * where28/10 23:28
vixey * : Ty Γ28/10 23:28
vixey ...28/10 23:28
vixeywhich of course Agda doesn't accept..28/10 23:28
vixeybut why not? couldn't it be made to work? (similary to implicit forall in haskell)28/10 23:28
vixey:(28/10 23:37
vixeyhttp://www.cs.nott.ac.uk/~nad/publications/danielsson-types2006.tgz28/10 23:37
vixeythis doesn't work with new Agda 228/10 23:37
--- Day changed Wed Oct 29 2008
kosmikusvixey: I don't get the message of what you posted before. The Ty example, what's the problem you're describing there?29/10 12:29
vixeyI can't remember what Ty is29/10 12:30
vixeycan you paste the message ?29/10 12:30
vixeyoh was it about the universe polymorphism?29/10 20:48
--- Day changed Thu Oct 30 2008
--- Day changed Fri Oct 31 2008
--- Log closed Sat Nov 01 00:00:43 2008

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