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

--- Log opened Sun Mar 01 00:00:24 2009
--- Day changed Mon Mar 02 2009
--- Day changed Tue Mar 03 2009
-!- pumpkin_ is now known as pumpkin03/03 04:09
--- Day changed Wed Mar 04 2009
--- Day changed Thu Mar 05 2009
-!- Cheshire is now known as vixey05/03 18:43
--- Day changed Fri Mar 06 2009
-!- pumpkin- is now known as pumpkin--06/03 04:21
vixeythis is cool http://www.lmcs-online.org/ojs/viewarticle.php?id=38&layout=abstract & http://www.math.uu.se/~palmgren/modif/06/03 17:53
--- Day changed Sat Mar 07 2009
--- Day changed Sun Mar 08 2009
-!- jfredett2 is now known as jfredett08/03 07:23
--- Day changed Mon Mar 09 2009
--- Day changed Tue Mar 10 2009
-!- jfredett2 is now known as jfredett10/03 23:56
--- Day changed Wed Mar 11 2009
-!- jfredett2 is now known as jfredett11/03 01:13
--- Day changed Thu Mar 12 2009
-!- _nano is now known as faXx12/03 22:41
--- Day changed Fri Mar 13 2009
--- Day changed Sat Mar 14 2009
iago_hello, there is some good/best "point" to start with agda2?14/03 19:59
vixeyright now14/03 20:00
iago_uhm... well, my English is not very good... but I was asking for some paper/book/etc that is a good start-point for agda14/03 20:01
--- Day changed Sun Mar 15 2009
endojellyhi15/03 21:14
vixeyhi15/03 21:14
stevanhello15/03 21:19
pumpkinhi!15/03 21:20
--- Day changed Mon Mar 16 2009
endojellystupid question, but can someone tell me again when I would need a dot pattern16/03 13:54
endojellyinstead of a pattern without a .?16/03 13:54
swiertendojelly: when you pattern match on a proof, for example.16/03 14:15
swiertsuppose you want to define trans : (x y : Nat) -> (x == y) -> y == x16/03 14:16
swiertwhen you pattern match on "x==y" you learn that x and y are really definitionally equal/convertible.16/03 14:17
swiertso what patterns should you write on the left-hand side of the function definition?16/03 14:17
swiertAny pattern you write should reflect that x and y must be equal.16/03 14:17
swiertIn Agda you write this as "trans x .x Refl = ..."16/03 14:17
endojellyswiert, ah, thanks!16/03 14:58
swiertendojelly: np. Hope my explanation helped.16/03 14:58
endojellyit did. without dot patterns you could use each variable only once?16/03 14:59
swiertendojelly: I think so - otherwise agda will complain about repeated occurrences of the same variable.16/03 15:09
endojellyagda is nice.16/03 15:10
swiertyep :)16/03 15:10
endojellyI really like the goals, they're helpful.16/03 15:13
swiertyeah. Once you get used to them, you start to miss them in Haskell.16/03 15:16
endojellyheh, haven't used haskell since playing around with agda (I only started to do so Saturday), but I think you may be right 8)16/03 15:17
endojellydo you think it's good style to give parameters of e.g. type a ≤ x names according to their type, i.e. a≤x ?16/03 15:24
endojellyI'm doing that, but I'm wondering if someone might think it's confusing.16/03 15:25
endojellya≤x is a proof that a ≤ x16/03 15:25
endojellyor what conventions do you use for naming your proofs?16/03 15:25
swiertI try to give them some ascii representation: a_lt_x/aLtx but that quickly becomes rather painful to work with as well.16/03 15:27
stevanendojelly: that's the way i do it too, i find it more helpful when reading than just calling the proof "p".16/03 15:31
endojellystevan, yes, me too. I started with giving it names like "pax" for a proof of type a ≤ x but I think a≤x is just most readable16/03 15:37
stevani find it even better when you use unicode :-)16/03 15:38
endojellyyes :P16/03 15:43
endojellywell, standard library forces you to use unicode anyway16/03 15:43
-!- eelco_ is now known as eelco16/03 15:47
endojellyΣ ⊤ (λ _ → ⊤) !=< ⊤ of type Set16/03 17:52
endojellywhen checking that the expression tt has type ⊤16/03 17:52
endojellyhuh?16/03 17:52
vixeyyeah that didn't make sense16/03 17:52
vixeyit seems like you just pasted an error message and said "huh"16/03 17:53
endojellyGoal: ⊤16/03 17:53
endojellyHave: Σ ⊤ (λ _ → ⊤)16/03 17:53
endojellybut I just typed in "tt"16/03 17:53
endojellywhy do I have Σ ⊤ (λ _ → ⊤) instead of ⊤?16/03 17:53
endojellyah!16/03 17:53
endojellybecause I'm stupid and shadowed stuff.16/03 17:53
endojellyhmm16/03 18:48
endojellyhow do I use DecTotalOrder?16/03 18:49
endojellyI made some function which use ≤16/03 18:49
endojellythey work fine with Nat but I would like them to work with any type having a total order16/03 18:49
endojellyso, how do I say "any type that has a total order"?16/03 18:49
endojellythings like a : DecTotalOrder -> a -> a -> Set don't work16/03 18:50
vixeydon't you mean (a : DecTotalOrder) -> a -> a -> Set16/03 18:50
endojellyyes, but doesn't work anyway16/03 18:50
endojellybecause DecTotalOrder ist of type Set116/03 18:50
vixeya : DecTotalOrder -> a -> a -> Set is a lot different16/03 18:50
endojellyI typed it with parantheses16/03 18:51
vixeyno you didn't16/03 18:51
endojellyin my code16/03 18:51
vixeyok16/03 18:51
endojelly{ a : DecTotalOrder} → a → a → Set16/03 18:51
endojellyanyway, doesn't work16/03 18:51
endojellyDecTotalOrder !=< _75 of type Set116/03 18:51
endojellywhen checking that the expression a has type _7516/03 18:51
endojellyso that's obviously not how to use that stuff16/03 18:51
endojellyso how do I?16/03 18:52
endojellyah, I have an idea16/03 18:52
endojellysince it's a Set116/03 18:52
endojellyno, doesn't work :(16/03 18:56
vixeyYou should post more code than one (erroneous) snippet16/03 18:57
endojellyI just want to know how to say that I want a type which has a decidable total order16/03 18:57
endojellynever mind, I found out16/03 19:00
stevanhow did you solve it? :-)16/03 19:03
endojellyhmm, didn't really solve it yet %)16/03 19:03
endojelly_foo_ : { t : DecTotalOrder } → DecTotalOrder.carrier t → DecTotalOrder.carrier t → Set16/03 19:03
endojellythis may be the right direction?16/03 19:03
stevanan inner parametrized module might work also?16/03 19:06
endojellyhow?16/03 19:07
endojellyright now I think I got it working16/03 19:07
endojellybut it's uglyyy16/03 19:07
endojellya function foo that does the same as  ≤16/03 19:07
endojellylooks like this:16/03 19:07
endojellyfoo : (t : DecTotalOrder) → DecTotalOrder.carrier t → DecTotalOrder.carrier t → Set16/03 19:07
endojellyfoo t a b = (t ≤ a) b16/03 19:07
endojellycan that be it?!16/03 19:07
endojelly(t ≤ a) b16/03 19:08
endojellythat's strange16/03 19:08
endojelly(_≤_ t) a b16/03 19:08
endojellythat's a bit better, but hmm16/03 19:08
endojellyfoo : {t : DecTotalOrder} → DecTotalOrder.carrier t → DecTotalOrder.carrier t → Set16/03 19:11
endojellyfoo {t} a b = let _≤_ = (_≤_ t) in a ≤ b16/03 19:11
endojellyis that how you do that?16/03 19:11
endojellystevan, what is an inner parametrized module?16/03 19:13
stevanyou can define a new module inside the one you are working in which takes as parameters the things you need inside it and then you provide those things when you open it16/03 19:15
stevanbut i'm not sure if that helps in your case16/03 19:16
endojellystevan, it might. I will try that out.16/03 19:22
endojellystevan, I think that's exactly it16/03 19:23
endojellystevan, yes, that's great, thanks16/03 19:28
endojellydamn, those parameterized modules are nice.16/03 20:09
stevan:-)16/03 20:13
--- Day changed Tue Mar 17 2009
endojellyby the way, which font do you use for math symbols?17/03 00:09
pumpkin_"The interactive mode is no longer supported. Don't complain if it doesn't work." aw17/03 20:29
endojellywas it good?17/03 22:15
endojellybut the announcement reads nicely. i only started this weekend, but i took every single feature announced for 2.2.0 for granted %)17/03 22:16
endojellyImportant changes since 2.1.2 (which17/03 22:18
endojellywas released 2007-08-16)17/03 22:18
endojellyok, I guess that explains it %)17/03 22:19
--- Day changed Wed Mar 18 2009
--- Day changed Thu Mar 19 2009
-!- jfredett2 is now known as jfredett19/03 23:31
--- Day changed Fri Mar 20 2009
--- Day changed Sat Mar 21 2009
endojellylookup (rbr k v l _ r _) k' with k ≟ k'21/03 20:11
endojellyist that common?21/03 20:11
endojellywhen I just want to check if k == k'?21/03 20:11
--- Day changed Sun Mar 22 2009
stepcutthis agda tutorial (AFP08) makes a lot more sense if implement everything with out using implicit arguments22/03 22:52
kosmikusstepcut: why?22/03 22:59
kosmikuswithout implicit arguments, everything becomes horribly verbose22/03 22:59
stepcutkosmikus: exactly!22/03 23:14
stepcutkosmikus: I'm not saying it is better to write code that way. Just that it is a good way to understand what is going on when you are first getting started22/03 23:15
kosmikusstepcut: ah ok22/03 23:31
kosmikusI agree that it can be instructive22/03 23:32
stepcutyeah22/03 23:32
--- Day changed Mon Mar 23 2009
stepcuthow do I make agda happy about the :: on the RHS:23/03 01:09
stepcuttranspose (xs :: xss) = ((vec ::) $ xs) $ (transpose xss)23/03 01:09
kosmikusstepcut: _::_ vec ?23/03 07:27
stepcutkosmikus: thanks, this seems to work, transpose (xs :: xss) = ((vec _::_) $ xs) $ (transpose xss)23/03 13:16
kosmikusoh sorry, I thought vec was a parameter, but it's a function you want to apply to the operator _::_, right?23/03 13:29
kosmikusthen yes, what you said. _::_ is like (::) in Haskell.23/03 13:29
kosmikusstepcut: ^^23/03 13:29
stepcutyeah23/03 13:30
stepcutvec is just 'replicate' except it can infer how many times to repeat something from the type23/03 13:32
kosmikusyes, I see that now23/03 13:32
kosmikusI originally thought that (vec ::) was supposed to be an operator section23/03 13:33
kosmikusthat's why I translated to _::_ vec23/03 13:33
kosmikusI don't think Agda has sections yet23/03 13:33
stepcutah I see, that is useful to know how to do as well23/03 13:33
stepcutso, If I have, data Vec (A : Set) : Nat -> Set where  _::_ : (n : Nat) -> A -> Vec A n -> Vec A  (suc n)23/03 13:38
stepcutthat compiles, but there are more arguments than _, so I am not sure how to apply it23/03 13:38
stepcutmabye, _::_ arg1 arg2 arg3 is the only option?23/03 13:38
kosmikus(arg1 :: arg2) arg3 should work23/03 13:46
kosmikusbut it's not what you want here, of course23/03 13:46
kosmikusyou want n to be implicit23/03 13:47
stepcutkosmikus: yeah, when I was experimenting with making everything explicit I ran into that problem23/03 13:57
-!- eelco_ is now known as eelco23/03 15:29
-!- anyfoo is now known as efficientjelly23/03 18:49
-!- efficientjelly is now known as endojelly23/03 18:49
--- Day changed Tue Mar 24 2009
stepcutI wonder how hard it would be to add algebraic data types and  pattern matching to LamdadPi24/03 22:02
vixeystepcut: general algebraic types is very easy24/03 22:04
vixeybut pattern matching is very difficult :)24/03 22:04
vixeywell the way I think about implementing it is difficult24/03 22:04
vixeyif you just did the sort of direct implementation like Agda does, it would be easier24/03 22:04
stepcutvixey: could you do anything useful with general algebraic types with out pattern matching?24/03 22:05
kosmikusdepends a bit on whether you want to continue to guarantee totality24/03 22:05
stepcutI need totality and termination24/03 22:06
kosmikusstepcut: what's relatively easy is to add datatypes and have the eliminator being generated automatically24/03 22:06
vixeystepcut: You can do everything with eliminators (and K) you can do with pattern matching24/03 22:06
kosmikusadding a translation from pattern matching to eliminators is a bit tricky24/03 22:06
vixeyI would implement pattern matching by compiling into eliminators24/03 22:06
stepcutvixey: ok. I will work towards understanding what that means :)24/03 22:06
kosmikusbut not really difficult either24/03 22:06
vixeykosmikus, it is difficult to me :p24/03 22:07
vixeyhave you implement this?24/03 22:07
kosmikusit's the combination of things; if you want pattern matching and implicit parameters and modules and this and that, you sooner or later end up with Agda again24/03 22:07
kosmikusno, I haven't. but I've looked a bit at the Agda and Epigram implementations24/03 22:07
kosmikusI think it's doable, and I'd like to implement it for LambdaPi24/03 22:08
vixeyI wanted to give a reflective implementation24/03 22:08
kosmikusthe main reason I haven't is that I don't quite like Agda's approach. I'd rather have Epigram's.24/03 22:08
kosmikusbut Epigram's approach is hard to do non-interactively.24/03 22:08
kosmikusif you don't need totality, the PiSigma paper draft by Altenkirch and Oury is interesting24/03 22:09
kosmikusthey describe a comparatively simple constraint-based pattern matching algorithm24/03 22:09
stepcuttotality means that for every input, there is a valid output?24/03 22:09
vixeywell24/03 22:10
vixeytotal means for every input there is an output24/03 22:10
vixeypartial, you could have an infinite loop (undefined values)24/03 22:10
stepcuttermination is essential24/03 22:10
vixeystepcut: what do you plan on doing ?24/03 22:12
stepcutvixey: a puzzle game rooted in logic and programming. Since users will be constructing proofs and programs which are run by centralized server, termination is somewhat important24/03 22:13
stepcutvixey: I could use timeouts, etc. But, I am hoping to avoid that by avoiding general recursion, etc.24/03 22:13
stepcutvixey: that's also why I am interested in something like LambdaPi. At the core I need something very simple and adaptable.24/03 22:15
vixeytermination is somewhat important24/03 22:15
stepcutvixey: :)24/03 22:15
vixeybut do you know the kind of algorithmic complexity of programs you could write in this context is *huge*24/03 22:15
vixey(You probably did know this)24/03 22:16
vixeybtw sounds cool24/03 22:16
stepcutvixey: yes. I am still working out the details of making it practical.24/03 22:16
vixeydid you write anything about it yet? What is the puzzle24/03 22:16
stepcutvixey: it will be a myst-ish type game, where you have to solve increasing difficult puzzles to reach your final destiny.24/03 22:17
vixeygreat!24/03 22:17
vixeyit will be the #1 way to learn dependent types24/03 22:18
stepcutvixey: I am still working on the plot, but it will be something like: you get trapped in a derelict alien space ship and you need to escape. But most of the computer technology is broken. Fortunately, you find a bizzare but simple devices with weird symbols on it. At first it seems to primitive to do anything useful. But, you will use it to 'hotwire' broken parts of the computer on your journey.24/03 22:19
stepcutover time you will start to build up a library of more powerful routines.24/03 22:19
stepcutthe 'simple machine' is, of course, the lambapi calculator, which doesn't even know what a number is.24/03 22:20
stepcutso, the puzzles will involve things like simple proofs, building up natural numbers, etc.24/03 22:21
vixeyreally this sounds great :)24/03 22:21
stepcutof course, it has to start really simple. Like, introducing the concept of a set ;)24/03 22:21
kosmikushey, this sounds like a lot of fun24/03 22:22
vixeyset as in set theory?24/03 22:22
kosmikusI actually had a similar idea once, but I never even came close to implementing it24/03 22:22
stepcutvixey: as much as is required to understand types24/03 22:22
kosmikusso I'd really like to see this game :)24/03 22:22
stepcutkosmikus: :)24/03 22:22
kosmikusanyway, I have to leave for tonight24/03 22:23
kosmikustalk to you again tomorrow or some other day24/03 22:23
stepcutkosmikus: cool, see you around24/03 22:23
vixeybye24/03 22:23
vixeystepcut: Have you read  To Mock a Mockingbird?24/03 22:25
stepcutvixey: no24/03 22:28
vixeyit's about combinatory logic24/03 22:28
vixeyit's a lot of fun, just your idea reminds me of it a little24/03 22:28
stepcutvixey: cool, I'll check it out24/03 22:28
stevanstepcut: you might find this paper interesting as well: http://www.cs.chalmers.se/~bengt/papers/GKminiTT.pdf24/03 22:31
stepcutstevan: cool!24/03 22:31
stepcutI don't think I have actually run an agda program yet -- just getting them to compile is enough of a learning experience24/03 22:51
vixeydid you do some reflective proofs?24/03 22:51
stepcutvixey: I'm just doing the AFP08 tutorial24/03 22:52
stepcutI don't even know how to do I/O in agda yet (assuming it can be done), so I don't even know what I would run :)24/03 22:54
vixeyyeah I'm sure you can do IO24/03 22:54
stevanactually IO is explained at the end of the AFP08 tutorial :-)24/03 22:55
stepcutstevan: yeah, I am still at the equality section24/03 22:55
stepcutthough, I did skip ahead a bit24/03 22:55
--- Day changed Wed Mar 25 2009
stepcutlets says I have:25/03 01:36
stepcutdata Nat : Set where zero : Nat ;  suc  : Nat -> Nat25/03 01:37
stepcutdata _==_ {A : Set} (x : A) : A -> Set where refl : x == x25/03 01:37
stepcutnow I want to write:25/03 01:37
stepcutlem-sub : (m : Nat) -> (n : Nat) -> (suc m) == (suc n) -> m == n25/03 01:37
stepcutlem-sub (suc m) (suc n) sm==sn = ...25/03 01:37
stepcutI'm a bit lost here...25/03 01:37
stepcutor, going the other way,25/03 01:38
stepcutlem-add : (m : Nat) -> (n : Nat) -> m == n -> (suc m) == (suc n)25/03 01:38
stepcutI tried this:25/03 01:40
stepcutlem-add : (m : Nat) -> (n : Nat) -> m == n -> (suc m) == (suc n)25/03 01:40
stepcutlem-add m n m==n with refl25/03 01:40
stepcutlem-add m n m==n | proof = refl25/03 01:40
stepcutbut, I got this:25/03 01:40
stepcutAn internal error has occurred. Please report this as a bug.25/03 01:40
stepcutoh... hrm25/03 01:46
stepcutlem-add m .m refl = refl25/03 01:47
vixeyI saw some basic parenthesis matching thing, and also a actual library for writing parsers..25/03 16:43
vixeybut what about proving correctness wrt. specifications?25/03 16:43
liyangoh. hai.25/03 17:07
vixeyhi!25/03 17:07
liyangOur own channel to talk in. Away from those detractors and non-believers. Awesome.25/03 17:08
vixeyhehe25/03 17:08
liyangNow I have nothing to say. D:25/03 17:09
vixeythese are scary http://wiki.portal.chalmers.se/agda/uploads/Libraries.Sequent/LKNat.agda25/03 17:09
liyangThe 漢字?25/03 17:11
vixeythe whole thing, they even proved some PA theorems in PA in Agda25/03 17:11
liyanger... ^^; I don't think I'm going to read through that right now.25/03 17:12
liyang(actually, it doesn't look that scary...)25/03 18:01
stepcutI feel like the proofs in agda are a bit too automatic at times25/03 22:32
stepcutlem-1 : {a : Nat} -> suc a == a + one25/03 22:32
stepcutlem-1 = refl25/03 22:32
vixeynow what is your definition of +?25/03 22:34
stepcut_+_ :  Nat -> Nat -> Nat25/03 22:35
stepcuta + zero = a25/03 22:35
stepcuta + suc b = suc (a + b)25/03 22:35
vixeytry this one:25/03 22:35
vixeylem-2 : {a : Nat} -> suc a == one + a25/03 22:35
vixeylem-2 = refl25/03 22:35
vixeyit can't work25/03 22:35
stepcutvixey: I was following the proof on this page, http://en.wikipedia.org/wiki/Addition_of_natural_numbers/Proofs25/03 22:36
stepcutvixey: (right at the top). Which is a bit more verbose25/03 22:36
--- Day changed Thu Mar 26 2009
stepcuthrm, according to the tutorial, this proof should be 'relatively easy', but I am dumbfounded :)26/03 00:17
liyangYou'll want to pattern match on the hidden argument {a : Nat}26/03 00:21
stepcutliyang: I am working on a different proof now, lem-!-tab : forall {A n} -> (f : Fin n -> A) -> (i : Fin n) -> (tabulate f ! i) == f i26/03 00:35
liyangtabulate?26/03 00:40
liyang(hpaste it?)26/03 00:40
stepcutliyang: http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=2887#a288726/03 00:41
stepcutliyang: tabulate takes a function that productions values from indices and creates a Vec using it26/03 00:44
stepcutoops, forgot to include _==_ , I added that in another paste26/03 00:48
liyangWhat was wrong if you just did case on i?26/03 01:00
liyang(Want me to paste?)26/03 01:00
stepcutliyang: yes, I am just completely lost :)26/03 01:00
liyanglem-!-tab : forall {A n} -> (f : Fin n -> A) -> (i : Fin n) -> (tabulate f ! i) == f i26/03 01:00
liyanglem-!-tab f fzero = refl26/03 01:00
liyanglem-!-tab f (fsuc i) = lem-!-tab (f o fsuc) i26/03 01:00
stepcutthis is as far as I got:26/03 01:00
stepcutlem-!-tab f fzero = refl26/03 01:00
stepcutlem-!-tab f (fsuc i) with26/03 01:00
liyangI'm guessing you tried lem-!tab f (fsuc i) in the second case?26/03 01:01
stepcutliyang: yeah, but not because I expected it to actually work, I just couldn't think of anything else to do26/03 01:01
stepcutalso, I don't really understand why the fzero case works anyway :-/26/03 01:01
stepcutso I am going to try to understand the base case first I think26/03 01:02
liyangwell, in the fzero case, the LHS  =defn=  tabulate f ! fzero  =beta=  (f fzero :: tabulate (f o fsuc)) ! fzero  =beta=  f fzero  =defn=  RHS26/03 01:05
liyang(Have you looked at the standard library?)26/03 01:06
stepcutno26/03 01:06
liyang(It's full of Unicode, I know. But lots of standard stuff is already defined there, and I always find it useful to look through them for `inspiration'. :)26/03 01:07
stepcutyeah, I looked there for some other things, just not anything related to this problem26/03 01:07
stepcutanyway, thanks. I'll poke at it until I understand what is going on.26/03 01:07
liyangand in the fsuc case,  LHS  =defn=  tabulate f ! fsuc i  =beta=  f fzero :: tabulate (f o fsuc) ! fsuc i  =beta=  tabulate (f o fsuc) ! i  ={ lem-!-tab (f o fsuc) i }=  (f o fsuc) i  =beta=  f (fsuc i)26/03 01:11
liyang=defn=  RHS. :)26/03 01:11
liyanghttp://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=2887#a288926/03 01:22
liyanghpaste doesn't like my Unicode. D:26/03 01:23
stepcutthe unicode looks ok to me, aside from the choice of colors :)26/03 01:23
stepcuthpaste needs an agda highlight mode26/03 01:24
stepcutanyway, I need to eat, thanks!26/03 01:26
liyangMore detailed step-by-step proof: http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=2887#a289026/03 01:34
liyang(where byDef = refl, essentially.)26/03 01:36
stepcutcool!26/03 01:43
stepcutI was wondering how to do more detailed proofs26/03 01:43
lady_6thofAufor some reason i can't re-install agda26/03 10:53
lady_6thofAuthe error is:26/03 10:53
lady_6thofAuCould not find module `System.IO.UTF8':26/03 10:53
lady_6thofAuand then:26/03 10:53
lady_6thofAucabal: Error: some packages failed to install:26/03 10:53
lady_6thofAuAgda-2.2.1 failed during the building phase. The exception was:26/03 10:53
lady_6thofAuexit: ExitFailure 126/03 10:53
lady_6thofAui have no idea what else i need to install26/03 10:53
lady_6thofAuany help?26/03 10:53
swiertlady_6thofAu: what command did you give to build agda?26/03 10:55
swiertif you cd into the agda directory and just "cabal install --user" it should fetch the dependencies for you...26/03 10:55
lady_6thofAui downloaded agda using darcs, then i changed into the directory "Agda" and there i did "cabal install"26/03 10:55
swiertHmm.26/03 10:56
lady_6thofAuit doesn't it gives me this error26/03 10:56
swiertCan you check if you have "utf8-prelude" installed?26/03 10:58
swiertI'm surprised cabal didn't fetch it for you - let me have a look.26/03 10:58
swiertSorry - that should be "utf8-string"26/03 10:59
lady_6thofAui don't think it is installed26/03 11:00
lady_6thofAui can't find it anywhere26/03 11:00
swiertThat's strange. Cabal install should fetch it for you when you build agda.26/03 11:05
swiertDoes it show up when you run "ghc-pkg list"26/03 11:07
swiert?26/03 11:07
lady_6thofAusorry, did u see my previous message?26/03 11:30
swiertyes - but I don't understand why cabal doesn't download utf-string.26/03 11:32
swiertit is listed as a dependency in Agda.cabal26/03 11:32
lady_6thofAuhmm... tried again26/03 11:37
lady_6thofAunothing :S26/03 11:39
swiertlady_6thofAu: and no warning when you configure?26/03 11:39
lady_6thofAuno, nothing26/03 11:52
lady_6thofAubrb26/03 12:08
-!- iago is now known as iago_26/03 13:48
vixeyhey26/03 16:24
vixeyhow do you all do syntax with binding in Agda?26/03 16:24
vixeyI use de bruijn in haskell mostly (with name annotations sometimes)26/03 16:24
vixeyin Coq then it's mostly the same, I don't like HOAS for you need ext. axiom .. but I guess we have this in Agda26/03 16:25
liyangIs anyone logging this channel?26/03 17:13
Laneyyessir26/03 17:14
liyangHm. Why can't I change the topic? Seems a bit boring.26/03 17:14
liyangLaney: HTTP accessible?26/03 17:14
Laneynope, just irssi logs26/03 17:15
Laneywant it?26/03 17:15
liyangNisse was asking about it.26/03 17:15
liyangIf it's more convenient, I'll log it live on Sneezy and put it up on my webspace.26/03 17:16
vixeyI don't think so.. I am not sure though26/03 17:16
liyangWho owns the channel? :-/26/03 17:16
Laney26/03 17:16:41 -ChanServ(ChanServ@services.)- Information on #agda:26/03 17:16:41 -ChanServ(ChanServ@services.)- Founder    : jfredett26/03 17:16
vixeyjfredett26/03 17:16
liyang*pokes jfredett*26/03 17:17
liyangmake it -t plzkthx...26/03 17:17
* Laney tests something26/03 17:19
vixeythis is interesting, http://rafb.net/p/pYco2N43.html26/03 17:21
vixeyin B the Type takes an implicit parameter, and that seems to let agda invent new abstractions26/03 17:22
vixeyHow can it know where to put them ?26/03 17:22
vixeyI suppose it's the result of some massive conglomeration of ruby goldberg constraint solvers26/03 17:24
vixeyhow do you do anything without type-in-type :(26/03 17:30
stepcutvixey: that's what happens when you write agda code that is 'too smart'26/03 17:30
vixeywhat does?26/03 17:30
stepcutyou get code that you can't figure out how to use?26/03 17:31
vixeydon't know what you mean26/03 17:32
stepcutvixey: nevermind.26/03 17:32
stepcutvixey: it was just a reference to a thread on haskell-cafe26/03 17:33
vixeyoh I don't read haskell-cafe26/03 17:33
stepcutvixey: ah26/03 17:34
vixeyisn't that weird about inferring an abstraction though?26/03 17:35
* vixey wonders if they programmed it to do that or it just does somehow :p26/03 17:36
stepcutright now everything that agda does is weird to me26/03 17:36
* vixey (something else weird is how the user manual doesn't seem to say anything about how to enable type-in-type or turn off positivity check or ..)26/03 17:37
vixeyutterly bizzare26/03 17:44
vixeyf  is a type error26/03 17:44
vixey(\x -> f x) typechecks26/03 17:44
* vixey . o ( Too much magic )26/03 17:45
jfredettwhats happening?26/03 19:00
jfredetti'm confused...26/03 19:00
jfredettwhat am I making the topic?26/03 19:01
vixeyjust set -t then anyone could change it26/03 19:01
jfredetterm..26/03 19:01
vixeyI think liyang would add a link to logs26/03 19:01
jfredettsuresrue26/03 19:01
jfredettlet me figure out how to do that... it's been a while. :/26/03 19:02
vixey/msg chanserv op #agda jfredett26/03 19:02
vixeyI think this is the incantation26/03 19:02
-!- mode/#agda [+o jfredett] by ChanServ26/03 19:02
@jfredettooh26/03 19:02
@jfredettshiny.26/03 19:02
-!- jfredett changed the topic of #agda to: Agda Channel!26/03 19:03
@jfredettokay, that works, now I just need to set the flag thingy.26/03 19:03
@jfredettwe should probably get /bot in here at some point...26/03 19:03
vixeymm26/03 19:04
vixey/mode -t #agda26/03 19:04
vixeyor26/03 19:04
vixey/mode #agda -t26/03 19:04
vixeyor something like this.. I don't know exactly26/03 19:04
-!- mode/#agda [-t] by jfredett26/03 19:04
-!- mode/#agda [+t] by ChanServ26/03 19:04
vixeyhah26/03 19:04
stepcutjfredett: a bot written in agda, right ?26/03 19:04
vixeyChanServ is rebellious26/03 19:04
@jfredettstepcut: well, \bot for now, agdabot someday in the future26/03 19:04
vixeystepcut: eep.. well not so bad if you use a IRC lib from Haskell26/03 19:05
stepcutvixey: yeah26/03 19:05
vixeywhy do you want lambdabot?26/03 19:05
@jfredettI'm no good at the agda stuff yet-26/03 19:05
vixeyit is a bit annoying with all the join/parts26/03 19:05
@jfredetti dunno, I just think channels are naked without bots... :/26/03 19:05
@jfredettI should probably make some people who are in here more often ops... I have a habit of not paying attention alot...26/03 19:06
Laneyhttp://agda.orangesquash.org.uk/2009/March.log.html can has logs26/03 19:55
Laneyliyang: ^26/03 19:55
vixeygrump26/03 19:57
vixey/topic Agda Channel! - http://agda.orangesquash.org.uk/2009/March.log.html26/03 19:57
vixey * #agda :You need to be a channel operator to do that26/03 19:57
vixey/msg chanserv set topiclock OFF26/03 19:58
vixey/msg chanserv set #agda topiclock OFF26/03 19:58
jfredetthrm26/03 20:28
-!- mode/#agda [+o jfredett] by ChanServ26/03 20:29
-!- mode/#agda [+o vixey] by jfredett26/03 20:29
@vixeyeep26/03 20:29
-!- vixey changed the topic of #agda to: Agda Channel! - http://agda.orangesquash.org.uk/2009/March.log.html26/03 20:29
@vixeyok!26/03 20:30
-!- mode/#agda [-o vixey] by vixey26/03 20:30
@jfredetthmm, how do I make it so other people can op themselves?26/03 20:30
@jfredettI should just RTFM.26/03 20:30
vixey/msg ChanServ ACCESS #foo ADD <name> OP26/03 20:30
vixeyI think26/03 20:30
@jfredett:/26/03 20:30
vixey/msg chanserv help access26/03 20:30
@jfredettoooh... *reads*26/03 20:31
@jfredettook, who wants to be an op. :P26/03 20:33
-!- mode/#agda [-o jfredett] by jfredett26/03 20:40
vixeyjfredett: I can  be26/03 20:43
jfredett... hmm, it set the stuff on fax, even though I fed it your nick.26/03 20:46
jfredettthat seems wrong..26/03 20:47
jfredettnope- chanserv says it's all good.26/03 20:48
jfredettyou should be able to op yourself.26/03 20:48
-!- mode/#agda [+o vixey] by ChanServ26/03 20:48
-!- mode/#agda [-o vixey] by vixey26/03 20:48
jfredettawesome.26/03 20:48
vixeycool26/03 20:48
jfredettanyone else? i suppose 2 is enough...26/03 20:49
-!- pumpkin is now known as othello26/03 22:38
liyangI wouldn't mind ops kthx. :326/03 23:46
--- Day changed Fri Mar 27 2009
-!- iago is now known as iago_27/03 10:09
lady_6thofAuwhenever i try c-c c-l in emacs i get: "Symbol's function definition is void: delete-dups"27/03 10:58
lady_6thofAuand nothing else27/03 10:58
lady_6thofAuwhat can i do?27/03 10:58
liyangum er? never seen that before. hpaste/pastebin?27/03 11:48
liyangjfredett: I can haz ops kthxbai?27/03 11:53
lady_6thofAusolved... just upgrading emacs :)27/03 11:57
liyangoh wait. Now I look at it it's rather telling that it was an Emacs error. :327/03 12:01
Jaakcabal installed Agda is supposed to support emacs mode, right?27/03 13:51
Jaakexceptionally active channel ^^27/03 14:00
* vixey doesn't know anything about this cabal thing27/03 14:00
LaneyJaak: You need to add something to your .emacs27/03 14:01
JaakI'm aware of that27/03 14:03
Jaakthe stuff in README didn't work27/03 14:03
JaakI think I managed to get it working now, tho'27/03 14:03
Laneythe shell-command-to-string stuff?27/03 14:04
Laneythis changed recently27/03 14:04
JaakAh, then the hackage version is out of date (I was reading the darcs versions readme)27/03 14:06
* Laney doesn't know about the hackage stuff27/03 14:07
* vixey thinks it's a really bad idea27/03 14:07
Jaakbeats installing things manually27/03 14:08
vixeydoes it ? :p27/03 14:08
Laneygetting it from darcs is fairly automatic27/03 14:08
Laneydarcs pull && cabal install27/03 14:08
Jaakand cabal also pulls the required dependencies automatically?27/03 14:10
Jaaks/pulls/installs27/03 14:10
Laneythat's the idea27/03 14:11
Jaakwell, I just did cabal install Agda (and executable)27/03 14:13
Jaakthe other way is nicer, but I didn't know about this until now27/03 14:13
Jaakty guys, managed to install and set up the darcs version nicely27/03 15:18
jfredettliyang: if you can prove you can speak in complete sentences, and someone who I know vouches for you, sure. :)27/03 17:15
liyangjfredett: Yes. Laney's in the office down from me, and I have Nils Anders Danielsson as my personal Agda documentation.27/03 17:19
jfredettfair enough.27/03 17:20
liyangjfredett: I thought everyone found lolcats funny.27/03 17:20
vixeylolcats ???27/03 17:20
jfredetteveryone does, but people who can only speak like them are just silly.27/03 17:20
liyang(I'm also Graham Hutton's student.)27/03 17:20
stepcutlolrats.com ?27/03 17:20
liyangHope that's enough name-dropping. =)27/03 17:21
vixeyI think liyang is one of the few people actually using agda :p27/03 17:21
jfredettI was being honest, I know lots of people who can't speak english anymore cause of all that silly texting these kids do these days...27/03 17:21
liyangLolcats, not lolrats: http://icanhascheezburger.com/27/03 17:21
vixeyI like cats if they are lol or non-lol27/03 17:22
liyangvixey: 日本語をわかりますか?27/03 17:22
jfredettliyang: all set, you should be able to op yourself27/03 17:23
jfredettahh! unicode...27/03 17:23
liyangHurrah. Heading home now...27/03 17:23
jfredettstill haven't got that worked out... coLinux/XMing is a bitch...27/03 17:23
liyangYes. If you're using Agda you'd better be able to deal with Unicode. :327/03 17:23
vixeyliyang nope :(27/03 17:24
vixeyI want to learn to write it though27/03 17:24
jfredettliyang: as of right now, I'm just reading about agda- I'm not clever enough to write it yet...27/03 17:24
vixeyyeah27/03 17:24
liyangIf you're familiar with LaTeX...27/03 17:24
vixeymy emacs mode doesn't display unicode ;/27/03 17:24
vixeyI should fix that nowa27/03 17:24
liyangjfredett: Unicode -- http://wiki.portal.chalmers.se/agda/uploads/Libraries.Sequent/LKNat.agda27/03 17:24
vixeyjfredett: What do you want to use agda for ?27/03 17:25
stepcutwhen I ssh into my laptop (where agda is installed) from OS X and run emacs, I get pretty dodgey unicode support. The japanese came through ok, but lots of symbols that agda uses are just boxes :(27/03 17:26
jfredettvixey: dunno yet...27/03 17:26
stepcutwhat does !=< mean ?27/03 17:26
jfredettjust very interested in learning a new language27/03 17:26
liyangstepcut: I run Aquamacs on OS X natively.27/03 17:26
jfredettI have some experience w/ Coq, but only minimal, dependant type-fu is still a little above me...27/03 17:27
liyangIn fact, it's the only Emacs I've spent any time using.27/03 17:27
jfredettalso, I hate emacs. so I'm procrastinating having to learn it.27/03 17:27
stepcutliyang: I use aquamacs as well, but only when editting documents that live on the OS X machine27/03 17:27
vixeyjfredett me too! I want to learn assembly today27/03 17:27
liyangstepcut: sshfs.app? (FUSE)27/03 17:28
jfredettsince agda (as well as most dep. type languages) it seems, use that.27/03 17:28
vixeyto use emacs you only need to know 3 commands, like  open a file  save a file  ..27/03 17:28
jfredettvixey: it makes me want to die though...27/03 17:28
stepcutliyang: meh. Everything is already installed on the linux box. If unicode worked I would have no issues :)27/03 17:28
jfredettthe whole system, configuration and all27/03 17:28
liyangjfredett: Coq is more of a proof assistant, as opposed to a programming language (discounting the PROGRAM extension); I find its proof scripts terribly opaque and hard to understand, unless you're running through the script live.27/03 17:29
jfredettliyang: I usually run through them live, but I agree, Coq = horrible syntax27/03 17:29
liyangjfredett: I'm a Vim user. :-/ But am picking up on Emacs keybindings.27/03 17:29
* vixey misuse of the = symbol27/03 17:29
jfredettliyang: but... it makes me want to _die_27/03 17:30
liyangjfredett: point is, I can run Agda code in my head. I can't run Coq scripts. :327/03 17:30
jfredettI hate it so much. :P27/03 17:30
jfredettliyang: yeh, thats one reason I started learning about agda27/03 17:30
* vixey has done a lot more in Coq than Agda27/03 17:30
jfredettthat and epigram seems silly... two-dimensional syntax and whatever...27/03 17:31
liyangjfredett: oh come now. Richard Stallman writes fabulous operating systems.27/03 17:31
jfredettliyang: If only he could write an editor worth a damn27/03 17:31
liyangjfredett: Epigram 2 is supposed to have a linear syntax. :327/03 17:31
jfredettAlso- screen is stupid, it can't vertically split windows.27/03 17:32
* stepcut wonders which will come first, Epigram 2 or emacs 2327/03 17:32
liyangjfredett: and even then, with Epigram 1, the 2D syntax is controlled by the Emacs mode.27/03 17:32
vixeynobody is hacking on Epigram 2 afaict27/03 17:32
liyangstepcut: I'm betting on Emacs 23.27/03 17:32
* vixey Epigram stalker - watches the darcs repo27/03 17:32
liyangConor still is, I'm sure...27/03 17:32
jfredettliyang: yeh- I figure though- if I had to pick an emacs based language...27/03 17:33
liyangJames Chappers recently finished his thesis on some core theory of Epigram 2 that I've never bothered to delve into.27/03 17:33
vixeyooh27/03 17:33
vixeywait27/03 17:33
vixeybut he doesn't publish it ? http://cs.ioc.ee/~james/Publications.html27/03 17:34
stepcutoh duh. which will come first: the write of Epigram (aka, Epigram 2) -or- the rewrite of GNU/HURD27/03 17:34
liyangNicolas Oury spent the past two years on an Epigram 2 grant...27/03 17:34
jfredettI suppose I should try writing a IRC bot in agda...27/03 17:34
vixeyliyang, do you know if his thesis is online somewhere?27/03 17:35
liyangand the Morris is doing something with Thorsten that I don't understand. :-/27/03 17:35
vixeyjfredett: sounds cool, do you think you would write an IRC monad in haskell and then ffi it using agda?27/03 17:35
vixeyliyang: beyond the generics stuff?27/03 17:35
jfredettvixey: maybe...27/03 17:35
jfredetthmm27/03 17:35
liyangvixey: I think he might be doing his corrections.27/03 17:36
vixeygrump27/03 17:36
liyangHis viva was only in January.27/03 17:36
vixeyok I guess I have nothing new to read yet :p27/03 17:36
jfredettI've got a few projects I want to finish in haskell though. hmm27/03 17:36
liyangvixey: I'm not sure a thesis counts as light reading...27/03 17:36
-!- mode/#agda [+o liyang] by ChanServ27/03 17:41
-!- liyang changed the topic of #agda to: Agda: is it a dependently-typed programming language? Is it a proof-assistant based on intuinistic type theory? ¯\(°_0)/¯ Dunno, lol. | Logs: http://agda.orangesquash.org.uk/2009/March.log.html27/03 17:41
-!- mode/#agda [-o liyang] by liyang27/03 17:41
vixey:S27/03 17:41
liyangintuinistic? Learn to spell, n00b.27/03 17:41
-!- mode/#agda [+o liyang] by ChanServ27/03 17:42
vixeyintunasashimi27/03 17:42
-!- liyang changed the topic of #agda to: Agda: is it a dependently-typed programming language? Is it a proof-assistant based on intuitionistic type theory? ¯\(°_0)/¯ Dunno, lol. | Logs: http://agda.orangesquash.org.uk/2009/March.log.html27/03 17:42
-!- mode/#agda [-o liyang] by liyang27/03 17:42
vixeyI like this guy  ¯\(°_0)/¯27/03 17:44
-!- mode/#agda [+o liyang] by ChanServ27/03 18:05
-!- liyang changed the topic of #agda to: Agda: is it a dependently-typed programming language? Is it a proof-assistant based on intuitionistic type theory? ¯\(°_0)/¯ Dunno, lol. | Wiki: http://wiki.portal.chalmers.se/agda/ | Logs: http://agda.orangesquash.org.uk/27/03 18:06
-!- mode/#agda [-o liyang] by liyang27/03 18:06
liyangAdditional material welcomed: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Community27/03 18:06
--- Day changed Sat Mar 28 2009
vixeyoo hi edwinb28/03 12:25
vixeyI think I saw some of your Idris stuff, about resource aware languages? .. very interesting28/03 12:26
edwinbhello28/03 12:26
edwinbI just saw this channel mentioned on the mailing list ;)28/03 12:27
vixeywe've been here for ages but liyang just set the ball rolling28/03 12:27
* stepcut just saw the mailing list mentioned on this channel :)28/03 13:08
vixeylol28/03 13:11
-!- iago is now known as iago_28/03 16:05
-!- byorgey_ is now known as byorgey28/03 22:33
-!- iago is now known as iago_28/03 22:52
--- Day changed Sun Mar 29 2009
-!- iago is now known as iago_29/03 11:41
vixeyhi jmcarthur29/03 17:35
jmcarthurhello29/03 17:35
jmcarthuri rarely come in here. never think to. finally added to my autoconnects29/03 17:36
liyangDamn. I saw activity in the channel and was hoping someone had asked a question. D:29/03 17:41
vixeywell I am still curious about my question,29/03 17:43
vixeyI don't know what ways that agda people generally represent syntax with binding29/03 17:44
liyangDe Bruijn?29/03 17:44
vixeyyeah29/03 17:45
vixeywith pattern matching DeBruijn via Fins works a lot nicer in Agda than Coq29/03 17:45
vixeymaybe I should try that,  hoas is screwy29/03 17:45
vixeyI had to use impredicative set (which agda doesn't have.., which means type-in-type)29/03 17:46
liyangThere's a lot of existing machinery already in the standard library.29/03 17:46
liyangI don't claim to understand impredicativity, but agda does have a --type-in-type flag.29/03 17:47
jmcarthursomebody care to explain a bit what is meant by impredicativity and type-in-type?29/03 17:49
liyang--type-in-type ignores the Set : Set1 : Set2 ... stratification. You just have Set : Set.29/03 17:49
jmcarthurstill new to type theory29/03 17:49
jmcarthuroh, but it's not the same as universe polymorphism?29/03 17:50
vixeySet : Set is paradoxical for similar reasons like having an ordinal of all ordinals (it's bigger than itsself)29/03 17:50
jmcarthurjust... losing the type information, i guess?29/03 17:50
liyangAnd this is all I can say about http://en.wikipedia.org/wiki/Impredicativity29/03 17:50
jmcarthurokay thanks29/03 17:50
vixeypolymorhism is that you write Set and it can bump that up a few levels if needed29/03 17:50
vixeyif you wanted to say something like29/03 17:51
vixey(prf1 prf2 : a == b) -> prf1 == prf229/03 17:51
vixeyyou would need polymorphism29/03 17:51
vixeyanother thing agda doesn't have (afaict..) is cumulativity, so that Set_i < Set_j lets you have Set_i : Set_j29/03 17:52
jmcarthuryou mean Set : Set1 and Set1 : Set2, but not Set : Set2?29/03 17:53
vixeycumulativity would allow Set : Set229/03 17:53
vixey(and the obvious extensions to arrow types and so on)29/03 17:53
vixeypolymorphism can be a bit dodgy wrt. multiple files though. I don't think it's solved in the same sense as HM29/03 17:56
-!- byorgey_ is now known as byorgey29/03 23:52
--- Day changed Mon Mar 30 2009
--- Day changed Tue Mar 31 2009
liyangwell, this is lively.31/03 02:01
vixeyhi byorgey31/03 13:50
byorgeyhi vixey31/03 13:50
vixeywhat's kickin !31/03 13:53
* vixey found http://www.cs.cmu.edu/~rwh/papers.htm#unibind31/03 14:00
byorgeyvixey: what's that?31/03 14:12
byorgeyargh, so many things to read and so little time =(31/03 14:13
vixeyit's about syntax with binding in agda which I was asking about a couple days ago31/03 14:13
byorgeyoh, cool31/03 14:13
liyangisn't a universe construction overkill for just doing syntax with binding?31/03 14:54
vixeyI am all for overkill31/03 14:54
liyang:331/03 14:56
vixey∑:331/03 14:56
liyangtouché31/03 14:58
liyang(Cursory glance... an appendix on Agda?)31/03 14:59
liyangIsn't that kind of like saying to the reader: if you can't read Agda, screw you! (and your mother too.)31/03 15:00
liyangI'm sure at least half of the audience of ICFP haven't heard about Agda, let alone know any DTP.31/03 15:01
vixeywell some of the code is pretty tricky31/03 15:02
liyangGuess the reader is screwed in any case then. Σ:331/03 15:03
vixey:p31/03 15:03
liyang(Entering Greek letters by spelling it out using the Japanese input method. Didn't realise that was possible. :D)31/03 15:05
vixeyI don't know any DTP :(31/03 15:20
liyangYou know more than you think you do. Σ:331/03 16:35
liyang(Am I just over-using that now?)31/03 16:35
vixeyimpossibl131/03 16:41
stepcutDTP?31/03 16:52
liyangdependently-typed programming?31/03 18:06
* Laney wibbles at liyang 31/03 18:07
liyangas opposed to desk-top publishing, or distributed transaction processing31/03 18:07
liyangLaney: hullo. Crunch time.31/03 18:07
Laneycaramel crunch?31/03 18:07
liyangno, Sainsbury's own brand.31/03 18:08
Laneya poor substitute31/03 18:08
liyangyou'd think so, but this is not just any caramel crunch. This is Sainsbury's Taste the Difference caramel crunch.31/03 18:10
Laneywe have a different definition of "own brand"31/03 18:13
Laneyanywho, I was going to ask you to darcs the agda packaging up somewhere if you'd be so kind31/03 18:13
Laneyjust the various debian/31/03 18:14
liyangAck. It used to be on Carwash but Carwash is dead. It's on my laptop and tonight is really a bad time. (Crunch time, as I said earlier.) Tomorrow?31/03 18:15
Laneyyes31/03 18:16
Laney(it's you that has carwash! I was talking to Morris about it the other day)31/03 18:16
liyang?31/03 18:16
Laneyhe was thinking up names for his new laptop31/03 18:17
liyangIt used to belong to Joel.31/03 18:17
Laneyand then I tried to remember who had carwash31/03 18:17

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