stevan MissPiggy MissPiggy --- Log opened Mon Feb 01 00:00:10 2010 -!- EnglishGent is now known as EnglishGent^afk 01/02 19:57 --- Day changed Tue Feb 02 2010 -!- RichardO_ is now known as RichardO 02/02 05:13 -!- RichardO_ is now known as RichardO 02/02 05:33 -!- mikael is now known as kmb 02/02 12:38 -!- RichardO_ is now known as RichardO 02/02 18:29 -!- RichardO_ is now known as RichardO 02/02 19:00 -!- opdolio is now known as dolio 02/02 21:53 so quiet here lately :-/ 02/02 23:14 sshhh! I'm trying to concentrate 02/02 23:15 I just about had it too 02/02 23:15 :-) 02/02 23:15 to be honest, ever since I found that progapedia page on agda -- the mystery is gone 02/02 23:15 have you not write anything new in Agda?? 02/02 23:16 we should have more epigram parties 02/02 23:17 where people figure out all the syntax... 02/02 23:17 i'm doing some reflection stuff now as part of a project 02/02 23:18 oh cool I love that reflection 02/02 23:18 tell me about it? 02/02 23:18 http://wiki.portal.chalmers.se/cse/pmwiki.php/CS/QuantifierEliminationAndFunctionalProgramming 02/02 23:19 wow 02/02 23:19 but isn't quantifier elimination infeasible? 02/02 23:20 like it takes a billion years to run it 02/02 23:20 i don't know 02/02 23:20 I'm thinking geometry or something 02/02 23:21 that sounds really cool though, I hope you show of here every so often :P 02/02 23:21 we are focusing on dense linear orders first and if that works out it would be cool to do presburger 02/02 23:22 that's partly why i'm here, i recall pumpkin talking about someone working on extending data.rational... i was wondering if he or somebody else knew more how that is going... 02/02 23:23 :( dense linear orders 02/02 23:24 it's the first ex. in my model theory book and I can't do it!!! 02/02 23:24 I spent months on that 02/02 23:24 in agda or? 02/02 23:25 no 02/02 23:27 i don't get the quant elim stuff yet, i plan to spend the rest of the week trying to understand it... i got some code. if you want, we could discuss it later... 02/02 23:34 have you been coding anything yourself? 02/02 23:36 not really no, let me think well I tried to do some comp. linguistics in Coq 02/02 23:37 but it's been so long that I seem to have run out of that fuel that makes everything you type live 02/02 23:37 :-/ 02/02 23:39 how's that epigram2 thing going? you played around with it, yes? 02/02 23:44 yeah it's pretty cool & confusing 02/02 23:44 going to keep an eye on it there's a lot of stuff I want to try out 02/02 23:45 but right now I don't understand the syntax well enough 02/02 23:45 i keep reading these blog posts which promise more info, but they all raise more questions than they answer for me... :-/ 02/02 23:47 I think that's the point! isn't it? 02/02 23:48 :-) perhaps. i gotta sleep; good night. 02/02 23:56 --- Day changed Wed Feb 03 2010 --- Day changed Thu Feb 04 2010 Hello :) 04/02 08:03 ohai2u! 04/02 08:03 Do you agda much? 04/02 08:03 haven't recently, but I love it when I have time 04/02 08:04 I'm not very good at it but I get addicted to it periodically 04/02 08:05 Does what I pasted look remotely reasonable? 04/02 08:06 yeah 04/02 08:09 the first parameter in the heap is the max value? 04/02 08:09 correct 04/02 08:12 sleep-deprived me thinks it looks pretty decent :) 04/02 08:12 planning on adding more? 04/02 08:12 yeah, I have to do the deleteMin yet 04/02 08:13 cool 04/02 08:13 and I'll write a wrapper for the heap time that hides all the messy indexes 04/02 08:13 if you just wanted to use it to get elements out of and put them in 04/02 08:13 then all you need is a foreign export haskellcall :P 04/02 08:13 and we'll have us a verified heap 04/02 08:13 I feel like there is probably a better approach than my less-than-eq max/min lemma pile 04/02 08:14 with the wrapper I can do: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=17075#a17077 04/02 08:18 it needs the inj1 inj2 breakdown? 04/02 08:19 I guess I've seen it needing that kind of thing before 04/02 08:19 oh I guess there's no way around it is there 04/02 08:19 I'm not sure what you're asking 04/02 08:20 it was stupid, sorry :) 04/02 08:20 I guess in this case the operator approach is still clear: insert a (H h) = [ H , H ]′ (insertHeap a h) 04/02 08:21 ah, that operator exists? :) 04/02 08:27 I haven't used \u+ enough I guess 04/02 08:28 after this you should prove the disjoint set union-find thing :P 04/02 08:29 specifically the amortized time complexity :P 04/02 08:29 --- Day changed Fri Feb 05 2010 Can someone tell me if I am approaching this proof correctly? http://codepad.org/HSzBCYUB I'm trying to show that my balanced tree insert function preserves the balanced tree property (or returns a full tree) 05/02 07:01 I've done the algorithm where the proof was embedded in the data type, but I wanted to try where the proof was an external object 05/02 07:02 I think you could do without X 05/02 07:14 Or at least, not make it a datatype. 05/02 07:15 The proofs look right, eyeballing it. 05/02 07:16 I only created that X datatype because I wasn't sure how to deal with that last proof otherwise 05/02 07:17 suggestion for what its type would be? 05/02 07:17 (without the X) 05/02 07:17 Well, I mean you could write 'X : (A : Set) (n : N) -> Tree A -> Set ; X A n t = BalancedTree A n t \uplus FullTree A n T', I think. 05/02 07:19 I think that's the same. 05/02 07:19 one thing I wanted to capture was that all of the inj1's were balanced and all of the inj2's were fulls 05/02 07:21 Oh, right, insertTree returns a sum... 05/02 07:22 I guess X isn't a bad idea, then. 05/02 07:23 I've been able to prove my property on trees of fixed depth 05/02 07:25 but I didn't know how to prove it in the general case 05/02 07:25 You mean you proved it for, like, 5? 05/02 07:26 Do I have it right then when I get: Goal: X (suc (suc .n)) 05/02 07:26 (insertTree (Branch F₁ t₁ t₂) | insertTree t₁) 05/02 07:26 yeah, well, 0..2 05/02 07:26 the | insertTree   part means that I need to case on that expression to look at the left side of the bar, right? 05/02 07:27 Probably. Your proof is likely to have similar structure to the function you're proving about. 05/02 07:28 Although since in that case it's a with on the recursive call, it might be that you should do a with on the inductive case in your proof. 05/02 07:31 Which will tell you what the recursive call was, since your proofs are indexed by the result. 05/02 07:32 this is one of those functions that blows up agda's case expander 05/02 07:37 hi all. glguy: i saw you were playing with trees; you might want to have a look at Data.AVL in the stdlib and http://web.student.chalmers.se/groups/datx02-dtp/ (especially ulf's 2-3 trees and the revised LLRB trees). 05/02 10:15 copumpkin: i recalled you talked about someone working on extending the support for rationals in the stdlib, you don't happen to know how that is going? 05/02 10:20 stevan: I don't know, but NAD does. I mentioned that I'd done a little bit of work on it and he mentioned that someone else had done a lot more and that the additional work was going to get merged in soon 05/02 13:18 copumpkin: thanks, this "soon" was a while ago, yes? 05/02 13:50 yeah, a couple of months now 05/02 13:50 is --universe-polymorphism what turns "Set" into a function of some sort? 05/02 18:01 glguy: yes 05/02 18:02 What type does it have, exactly? 05/02 18:02 Set can still be used as Set zero, but the general form is Set ℓ where ℓ of type Level 05/02 18:03 Merely something like Set : ∀ (ℓ : Level) → Set (suc ℓ) 05/02 18:04 Set : Level -> ? 05/02 18:05 Set ℓ : Set (suc ℓ) 05/02 18:06 ah, right 05/02 18:06 glguy: you can still use it with no parameters though... it's a bit of a hack 05/02 18:07 oh npouillard already said that 05/02 18:07 I think he was talking about "Set zero" 05/02 18:07 so yeah, writing Set is equivalent to Set zero, and you can't always eta reduce on it :P 05/02 18:08 Epigram has <= !!! 05/02 18:13 MissPiggy: what you mean? 05/02 18:18 they have implemented the <= view from the left gadget 05/02 18:19 > help <= 05/02 18:20 <= [] - eliminates with a motive. 05/02 18:20 I'm pretty sure that was already in there. 05/02 19:07 Just with a different name. 05/02 19:08 well I just did darcs pull for the first time in weeks 05/02 19:09 today 05/02 19:09 so it could have been in there for a while 05/02 19:10 They've been writing lots of patches. 05/02 19:10 Anyhow, I haven't recompiled since that first day. But I'm pretty sure there was an "elim" tactic described as "eliminates with a motive". 05/02 19:10 I don't have the executable anymore, though. 05/02 19:11 "Added Buddy Holly states for holes (crying, waiting, hoping)" 05/02 19:12 is there a way to do my last definition "insert-full-fails" without so much refl juggling? http://codepad.org/0jodzfpl 05/02 21:51 I feel like I'm making this harder than it has to be my not understanding some common idiom somewhere 05/02 21:51 mh, maybe it could improve with EquationalReasoning 05/02 22:37 http://codepad.org/F7p4VLdN   I didn't work out how to use equational reasoning for it, yet, but I did simplify 05/02 23:30 --- Day changed Sat Feb 06 2010 Equational reasoning is a nice notation for strings of uses of transitivity. 06/02 00:33 Oops, he's not here anymore. 06/02 00:33 Is anyone interested in helping me test a platform for hosting web applications written in Ur/Web, my programming language which supports type-level computation? 06/02 13:36 --- Day changed Sun Feb 07 2010 cabal: cannot configure Agda-2.2.6. It requires base ==4.2.* && ==4.2.* For the dependency on base ==4.2.* && ==4.2.* there are these packages: base-4.2.0.0. However none of them are available. base-4.2.0.0 was excluded because of the top level dependency base -any 07/02 01:30 halp. 07/02 01:30 #haskell! 07/02 01:31 :) 07/02 01:31 but I just came from haskell 07/02 01:31 dolio: i am _not_ going to let this diverge 07/02 01:31 i am a total IRCer 07/02 01:31 you fail at typing. plz go directly to stderr :D 07/02 01:32 * alise suspects copumpkin and dolio of being the same person... SECRETLY. 07/02 01:32 we actually have the same first name, too 07/02 01:32 so maybe it's true 07/02 01:32 but I don't think so 07/02 01:32 Copumpkin "Dolio" Agda 07/02 01:32 I'm not sure I've ever used an Agda from hackage. 07/02 01:34 those AIM meets must be pretty fun 07/02 01:35 they're going to japan next 07/02 01:36 Is Agda.TypeChecking.Serialise meant to freeze my entire system when I compile it? 07/02 04:10 Agda does seem to take a lot of memory to compile for some reason. 07/02 04:12 How much do you have? 07/02 04:12 This box, a measly one gig. 23% used... 07/02 04:12 But it freezes my entire system; can't even Ctrl-C the compile. 07/02 04:13 That seems excessive if it's just some serialisation thing. 07/02 04:13 That's odd. 07/02 04:13 It has compiled 123 out of 191 modules by that point without problems, after all. 07/02 04:13 The Glorious Glasgow Haskell Compilation System, version 6.10.4, installing with cabal install agda, Ubuntu 9.04, blah blah blah boring 07/02 04:13 So, anyone have any clue what would cause compilation to freeze my ststem on Agda.TypeChecking.Serialise? Does it contain some evil magic code that interacts with optimisation or something? 07/02 15:32 alise: which version of GHC do you have and have you a 64 bits? 07/02 15:33 6.10.4; aye 07/02 15:34 have you tried to clean and recompile 07/02 15:34 which OS ? 07/02 15:34 I did "cabal install agda", hard-rebooted my system and tried again; the exact same result. 07/02 15:35 Ubuntu 9.04. 07/02 15:35 Which version cabal was trying to install 2.2.6 ? 07/02 15:36 Yes. 07/02 15:36 did previous versions works better ? 07/02 15:37 I haven't tried; first time on this system. 07/02 15:38 {-# LANGUAGE OverlappingInstances,              TypeSynonymInstances,              IncoherentInstances,              ExistentialQuantification,              ScopedTypeVariables,              CPP              #-} {-# OPTIONS_GHC -O2 #-} 07/02 15:38 -O2 plus hideously scary type synonym extensions? 07/02 15:38 I bet that's the culprit. 07/02 15:38 I wonder if it's possible to force -O1. 07/02 15:39 I don't think so 07/02 15:39 these extensions are indeed scray 07/02 15:39 *scary 07/02 15:39 cabal install agda-executable-2.2.4 07/02 15:40 Right, and -O2 is known to do things like this iirc. 07/02 15:40 That's why cabal does -O1 by default now... 07/02 15:40 npouillard: is there anything in 2.2.6 i'd miss? 07/02 15:40 or any backwards-compat breaking changes? 07/02 15:40 yes some changes like universe-polymorphism and that the latest version of the stdlib depends on it 07/02 15:41 Maybe I'll instead try and get 2.2.6 working, then. 2.2.4 might do the same thing to my system again... 07/02 15:42 alise: yes 07/02 15:42 --- Day changed Mon Feb 08 2010 what type would you use for sets over some type T? 08/02 21:25 Saizan: Finite sets or abritrary sets. For the latter I would simply suggest "T → Set" 08/02 21:28 mh, arbitrary ones in theory, it's yo define an entailment relation _|-_ : (T -> Set) ->  T -> Set could work 08/02 21:31 it's hard to make it decidable with that type though, right? 08/02 21:32 right 08/02 21:32 i could use T -> Bool i guess 08/02 21:33 Saizan: to be precise it depends on what you have to decide this 08/02 21:33 ∈-dec S = ∀ t → Dec (S t) 08/02 21:36 What's "sets over a type" mean? Types that contain some subset of the elements? 08/02 21:36 * npouillard thinks that an agdabot would help 08/02 21:36 dolio: the type of the values that represent some subset of the elements 08/02 21:39 Ah, then it's Σ T P, where P should be prop-valued so to speak. 08/02 21:41 In that P t should have 0 or 1 elements. 08/02 21:41 no, that's some subset of T 08/02 21:42 i want the type for what you'd denote 2^T in classical mathematics 08/02 21:42 Saizan: literally T → Bool ? 08/02 21:43 hence why T -> Bool might fit 08/02 21:43 Oh. Then T -> Bool or T -> Prop, or something like that. 08/02 21:43 T -> Bool would be decidable subsets of T, I think. 08/02 21:43 i guess i've to pick one and see if i get into some problems 08/02 21:44 it's all about denotational semantics for concurrent constraint programming, if you're curious :) 08/02 21:44 http://math.andrej.com/2005/05/16/how-many-is-two/ 08/02 21:45 That might be useful. 08/02 21:45 thanks 08/02 21:45 Or perhaps just confusing. I'm not sure I really grok it myself. 08/02 21:45 Agda doesn't really have anything analogous to Ω anymore, though. Only Set, which isn't really the same. 08/02 21:46 (If it ever really did.) 08/02 21:47 ehm, what would you use for finite subsets? :) 08/02 23:46 Fin n ? 08/02 23:46 andrej is so awesome 08/02 23:47 Fin n -> T would probably work. 08/02 23:53 Although that doesn't rule out duplicates. 08/02 23:53 Finite : (D -> Set) -> Set 08/02 23:58 Finite u = ∃ λ n -> ∃ λ (f : Fin n -> D) -> ∀ P -> P ∈ u -> ∃ λ i -> f i ≡ P 08/02 23:58 ..so that i can use it as a restriction on (D -> Set) 08/02 23:58 what is this for?? 08/02 23:59 why not just Fin n? 08/02 23:59 Fin n isn't a finite subset of some other type. 08/02 23:59 why does that matter 08/02 23:59 --- Day changed Tue Feb 09 2010 Or, it isn't the type of finite subsets of some other type. 09/02 00:00 it matters because i'm working with a relation on this other type D 09/02 00:01 On the Strength of Proof Irrelevant Type Theories has a questionable typing rule. 09/02 00:02 the whole thing is questionable :P 09/02 00:04 It has strong impredicative sums. 09/02 00:05 the other issue is that benjamin is INCREDIBLY smart 09/02 00:05 Which let you encode something similar to Prop : Prop. 09/02 00:05 so I was never sure if it was just that I didn't get it 09/02 00:05 --- Day changed Wed Feb 10 2010 At long last, my proof that A × (B × C) ≅ (A × B) × C is complete. 10/02 02:42 And checking the module only take 75% of my memory. 10/02 02:43 is there an idiom to write down an isomorphism more compactly? http://code.haskell.org/~Saizan/Agda/NatCat.html 10/02 19:02 AFAIK not that much 10/02 19:08 Data.Sum.map is also known as [_,_] and there the 'id' function in (Data.)?Function 10/02 19:10 Theory question: does Martin-Löf typeability imply strong normalisation? or is the termination check not an "essential" part of type checking? 10/02 19:13 specifically, does M-L justify Markov's principle by proving that unbounded search terminates? 10/02 19:15 map f g = [ inj₁ ∘ f , inj₂ ∘ g ] , actually, but ok :) 10/02 19:29 hello. is there a way around the following problem: when i got a goal which depends on some (mixfix) functions from a parametrized module then the goal because very unreadable because it includes the module name, module parameters and written in prefix style... 10/02 19:42 s/because/becomes/ 10/02 19:42 i'd like to know that too 10/02 19:51 i wish there was some way to toggle between the current way it works and less noisy goals which simple ignore printing module names and module parameters... 10/02 19:55 similar to how you can toggle between showing hidden args in goals or not 10/02 19:56 Saizan: I've been using a record: http://code.haskell.org/~dolio/agda-share/categorica/html/Category.html#2226 10/02 20:14 That html is out of date, but it's still similar. 10/02 20:14 I wonder if all your memory usage is from the serialization phase 10/02 20:15 like the mailing list message 10/02 20:15 Quite possibly. When I have a type error, it catches it relatively quickly. 10/02 20:45 I can tell when I don't, even though it spends an additional minute or two thinking before it accepts. 10/02 20:46 we need to put typechecking agda on the shootout and get dons to optimize it 10/02 21:59 :) 10/02 21:59 Saizan genius :D 10/02 22:01 HairyDude: Formal type theories don't need "termination checks", because they deal in terms such that well-typing implies strong normalization. 10/02 22:02 dolio: right. so M-L typeability is undecidable? 10/02 22:03 Agda's termination checker is necessary because it lets you write direct recursive functions, and uses syntactic checks to try and be sure it could be translated to such a set of core terms. 10/02 22:03 Saizan: hehe, nice idea 10/02 22:04 M-L typeability is undecidable?? 10/02 22:04 dolio: oh, right. you get explicit recursion operators for each data type then? 10/02 22:05 (when you get to the point of adding data, anyway) 10/02 22:05 if something passes the agda termination checker, then in theory, you could replace that with explicit recursion operators 10/02 22:05 (eliminating dependent pattern matching goes into some more detail on this construction) 10/02 22:06 agda doesn't do that though, the 'in theory' bit is good enough 10/02 22:06 what was that about M-L though ? 10/02 22:06 MissPiggy: well I was thinking, if a term has to be strongly normalising to be typeable, that implies some sort of termination check, which is undecidable. but that's only if you make it possible to define unrestricted recursion, like agda does 10/02 22:08 I guess the extensional version of his type theory might have undecidable type checking, as is often reported of extensional type theories. 10/02 22:08 "if a term has to be strongly normalising to be typeable" -- no 10/02 22:08 extensional type theory is a weird concept 10/02 22:09 "termination check, which is undecidable" -- no 10/02 22:09 MissPiggy: yes, I already know I was wrong :) 10/02 22:09 Well typed terms are strongly normalizing, but not all strongly normalizing terms are well-typed. 10/02 22:09 --- Day changed Thu Feb 11 2010 hi. what's this: http://www.e-pig.org/darcsweb?r=Pig09;a=headblob;f=models/IMDesc.agda ? 11/02 10:19 stevan: looks like some unfinished work about playing with universes 11/02 10:22 what does it do in the epigram2 repository tho? 11/02 10:23 They're experiments with modeling the behavior of epigram2 in agda. 11/02 10:25 ok, interesting. 11/02 10:26 Can I recruit anyone to help me test a platform for developing & hosting web applications written in Ur/Web, my programming language which supports type-level computation? 11/02 14:53 this is kind of scary 11/02 17:09 um and offtopic 11/02 17:10 aanyway Recently a team of mathematicians have been trying to republish the famous series of papers called “SGA”, or “Séminaire de Géométrie Algébrique”.  This was largely the work of Alexander Grothendieck, who had refused to let Springer Verlag republish the original version. 11/02 17:10 http://golem.ph.utexas.edu/category/2010/02/grothendieck_said_stop.html 11/02 17:10 http://sbseminar.wordpress.com/2010/02/09/grothendiecks-letter/ 11/02 17:18 How do I avoid lots of these lemmas? lemma3 : ∀ {a b c} → b ≡ c → a ⊔ b ≡ a ⊔ c    \n     lemma3 refl = refl 11/02 20:16 glguy: try the "rewrite" feature 11/02 20:17 Do you know of any examples of this feature? 11/02 20:18 I've not seen it yet 11/02 20:18 foo a b c b≡c rewrite b≡c = ... 11/02 20:18 they are some in the tests 11/02 20:18 grep for rewrite 11/02 20:18 OK, Data.List.Any.Properties uses it 11/02 20:18 glguy: a simpler thing is to simply pattern match over refl but rewrite is handy anyway 11/02 20:19 npouillard, my refl is on an expression 11/02 20:20 so I can't pattern match 11/02 20:20 http://codepad.org/xKPqBWN2 11/02 20:20 height a == height b, for example 11/02 20:20 npouillard, rewrite is /exactly/ what I needed 11/02 20:26 thank you 11/02 20:26 glguy: do you know inspect and _with-≡_ from module on prop eq? 11/02 21:09 I know of them 11/02 21:31 but they don't help me resolve cases where I have some assumption:   this thing | some case 11/02 21:31 which is what I was running into 11/02 21:31 or... 11/02 21:32 should I be rewriting with the resulting equality? 11/02 21:32 r with-== eq rewrite eq = ? 11/02 21:32 npouillard, are you still there (I was away to lunch , sorry about slow response) 11/02 21:34 'rewrite a==b ...' is equivalent, I believe, to: with a | a==b \n ... | .b | refl ... 11/02 21:34 http://codepad.org/SXTSnC14 11/02 21:36 using rewrite I was able to refine my last definition a lot 11/02 21:36 dolio, ah, that would make sense 11/02 21:37 I think that I wasn't using inspect properly, it might have done what I wanted 11/02 21:37 I rarely use inspect. 11/02 21:38 But maybe I just don't understand its uses that well. 11/02 21:38 The thing with refining things with matching on refl, is that if you have (complex-expr-1)==(complex-expr-2), you need to give one of the expressions a name, so that it can be refined into the other one when matching on refl. 11/02 21:39 Rewrite makes that a little easier. 11/02 21:39 needing to give them a name is how I was ending up using lots of little lemmas 11/02 21:40 Yeah, you can use with, as well, but that leads to long (vertically) functions. 11/02 21:41 Conor told me to STFU 11/02 22:55 :o 11/02 22:58 where 11/02 22:58 http://www.reddit.com/r/dependent_types/comments/b0vb7/agda_vs_coq_by_wouter_swierstra_with_some_input/c0kepog?context=3 11/02 22:58 ah there's an EDIT: now 11/02 22:59 btw, epigram2 has/will have tactics, yes? are/ will be they written in epigram2? 11/02 23:03 there's a tactic system in the haskell implementation, which I think works a bit like HOL light -- at least in a vauge sense 11/02 23:05 some examples already like elimination with a motive and propositional simplification in the Pig09 repo 11/02 23:05 i'm not familiar with HOL light; aren't HOL light's tactics written in ocaml? 11/02 23:07 yeah 11/02 23:07 so you mean epigram2's tactics are written in haskell? 11/02 23:07 well the whole thing is implemented in haskell (although there's some agda files too),  there is a monad (called ProofState) which has basic machinary for tactics and they implement higher level stuff in terms of that 11/02 23:11 but as i understand it, one still programs in the "core" of epigram2 atm... eventually there will be more syntax etc and then one won't have direct access to the haskell implementation? will there be an epigram2 interface to the tactic machinary then or will it still be done in haskell? 11/02 23:15 no there is an interface right now that has nothing to do with haskell except being implemented in it 11/02 23:17 sorry what I said about HOL ocaml was sort of wrong and confusing 11/02 23:18 so epigram2 tactics are written in epigram2? :-) 11/02 23:19 :[ 11/02 23:19 right now it is all implemented in haskell 11/02 23:19 I am sure that lots of reflective tactics will be done in epigram later -- but wel, it's just my best guess, someone that's actually on the project would kno 11/02 23:20 I'm talking about Pig09 11/02 23:21 there's also Epi 1 from ages ago, and who knows what else is going on 11/02 23:21 Some form of reflection will definitely be useful 11/02 23:21 I think the way it's designed all of these things are possible, just needs someone to do it ;) 11/02 23:21 yeah, Pig09 is what i call epigram2. what is the official name anyways? 11/02 23:22 Epigram :) 11/02 23:22 * MissPiggy still doesn't really understand the syntax of Pig09/Cochon.. so it's hard to do stuff with it :/ 11/02 23:22 The syntax is a moving target at the minute. It'll only get easier. 11/02 23:22 everybody talks about reflection replacing tactics, but are there any good examples of this happening? i only know of the ringsolver? 11/02 23:24 * MissPiggy doesn't have a clue abot reflection /replacing/ tactics 11/02 23:27 you know how to prove that sin(1 + x^2) is continuous? 11/02 23:27 in school they tell you 11/02 23:28 let epsilon > 0, .... 11/02 23:28 and it takes an hour each time 11/02 23:28 in CoRN, they do it like in real math  -- it's the composition of continuous functions so reflection proves it automatically 11/02 23:28 --- Day changed Fri Feb 12 2010 i asked the same question on reddit 12/02 00:15 link? 12/02 00:15 eh I will find it 12/02 00:16 same thread as before 12/02 00:16 Is this an "abuse" of Relation.Unary.\sub= ?  insert-balanced : {A : Set} (a : A) → Balanced ⊆ (Balanced ∘ insert a) 12/02 01:37 hello! 12/02 02:24 * glguy finally finishes the independent proof that the non-dependently typed algorithm for inserting and deleting from balanced trees maintains the balanced property 12/02 09:35 Per your previous question, Balanced ⊆ (Balanced ∘ insert a) is probably a little werid. 12/02 09:36 Weird, even. 12/02 09:36 If you ask me, at least. 12/02 09:38 i wouldn't have asked if i didn't suspect :) 12/02 09:38 Maybe it's worth it to get higher-order points, though. 12/02 09:44 This code is certainly not polished, but it might be interesting to someone else going through the same learning process as me 12/02 09:49 http://github.com/glguy/agda-balanced-tree-example 12/02 09:49 Are these AVL-ish? 12/02 09:53 no 12/02 09:53 they always insert at the left-most position at the lowest level 12/02 09:54 Okay. 12/02 09:54 Did you say you'd already done a version where the trees were correct by construction? 12/02 09:54 My intention is to write a heap next 12/02 09:54 I did a Haskell version where they were 12/02 09:55 using GADTs 12/02 09:55 Was that easier? It seems like it might be. 12/02 09:55 much easier, I've been working on this in agda for a while 12/02 09:55 I just typed it up in haskell 12/02 09:56 but I don't know much agda 12/02 09:56 but 12/02 09:56 I suspect it'd be similarly easier in Agda. 12/02 09:56 I wanted to prove that the heap property was preserved 12/02 09:56 and not just the balanced property 12/02 09:56 my primary motivation for doing this in agda is to have something more interesting to prove than tautologies in agda as an exercise :) 12/02 09:59 anyone tried making SPTs in Epigram? 12/02 13:23 SPTs ? 12/02 13:24 this stuff http://www.cs.nott.ac.uk/~pwm/ 12/02 13:24 MissPiggy: hum, ok 12/02 13:25 nc 12/02 13:45 oops sorry 12/02 13:45 can't install agda :/ 12/02 13:48 does anyone know about this? 12/02 13:49 cabal: cannot configure QuickCheck-2.1.0.3. It requires ghc -any 12/02 13:49 There is no available version of ghc that satisfies -any 12/02 13:49 MissPiggy: hum... which version of GHC do you have, and how did you installed it 12/02 13:52 6.12.1, 12/02 13:52 I must have installed it from the binary on haskell.org 12/02 13:52 what's funny is this is probably the 20th time I've installed agda and I still don't have a clue how to stop it from going wrong :/ 12/02 13:52 I just switched to 6.12 yesterday and simply done a "cabal install" in the agda darcs repository 12/02 13:53 okay I will try and get 6.12, thanks for the idea 12/02 13:54 huh, you just said you have a 6.12.1. By 6.12 I meant 6.12.* 12/02 13:55 oh 12/02 13:55 I have a 6.12.1 as well actually 12/02 13:56 installed with ArchLinux 12/02 13:56 * MissPiggy spent the whole of the last two weeks trying to install Arch.. 12/02 13:56 (and failed) 12/02 13:56 You where not confortable with linux previously or did you had specific issues? 12/02 13:58 oh I just have terrible luck 12/02 13:58 OK, that's a bit sad, I never had problems with it. 12/02 13:59 also I can't darcs get http://code.haskell.org/Agda/  :/ 12/02 14:00 it is a valid HTML page but darcs says it's not a valid repo 12/02 14:00 this seems to work though: http://code.haskell.org/Agda/repository-before-conversion-to-darcs-2-format/ 12/02 14:01 ah, you've an old darcs then 12/02 14:01 MissPiggy: what does cabal --version says, btw? 12/02 14:01 cabal-install version 0.8.0 12/02 14:02 using version 1.8.0.2 of the Cabal library 12/02 14:02 ok, that should be fine, but the error above is weird 12/02 14:02 it's kind of funny because I would have thought -any would be lie a wildcard that always holds 12/02 14:03 yeah 12/02 14:03 * MissPiggy downloads TWO THOUSAND PATCHES 12/02 14:03 one by one 12/02 14:04 ohh 12/02 14:04 maybe I should cabal install darcs 12/02 14:05 then use it to get the newer agda 12/02 14:05 (that didn't work) 12/02 14:05 i think the two repos are just one a mirror of of the other 12/02 14:06 MissPiggy: oh, i think i've understood the error you got above, it's about the ghc haskell library, which comes with ghc the compiler, your installation got broken somehow 12/02 14:09 ahh 12/02 14:10 MissPiggy: if you paste ghc-pkg list we might be able to repair it 12/02 14:10 mmm 12/02 14:10 my pkg-list is colorful 12/02 14:10 there are some things in red such as ghc-6.12.1 & bin-package-db-0.0.0.0 12/02 14:11 a common situation is when you've the same version of some package in both the global and user databases 12/02 14:11 which confuses ghc-pkg and cabal 12/02 14:11 yeah, the red ones are the broken ones 12/02 14:11 http://www.pasteit4me.com/112023 12/02 14:12 pretty confusing but cabal seems to be at the bottom of it 12/02 14:12 yeah 12/02 14:12 it seems you've reinstalled Cabal-1.8.0.2 globally 12/02 14:12 replacing the one shipped with ghc 12/02 14:13 ;_; 12/02 14:13 but the ghc package was built against the old one, and so now it's broken 12/02 14:13 the somewhat good thing, is that you can keep your current cabal-install and resintall only ghc 12/02 14:14 hey I think that is working now! 12/02 14:16 oh no 12/02 14:16 Agda-2.2.6 depends on haskell-src-1.0.1.3 which failed to install. 12/02 14:16 a bit closer anyway 12/02 14:16 this is dodgy 12/02 14:17 Configuring binary-0.5.0.2... 12/02 14:17 Warning: This package indirectly depends on multiple versions of the same 12/02 14:17 package. This is highly likely to cause a compile failure. 12/02 14:17 package binary-0.5.0.2 requires array-0.3.0.0 12/02 14:17 package containers-0.3.0.0 requires array-0.3.0.0 12/02 14:17 afaict array-0.3.0.0 = array-0.3.0.0 12/02 14:17 so I dont know what's its talking about conflict for 12/02 14:17 should I build a new ghc myself, uninstall the old one: Then install my new one? 12/02 14:18 you've two array-0.3.0.0 packages installed 12/02 14:18 that's a problem 12/02 14:18 oh I see 12/02 14:19 what do yuo do in that situation? 12/02 14:19 you could try ignoring the warning, anyhow 12/02 14:19 well it is right in its prediction -- the stuff doesn't build 12/02 14:19 i'd ghc-pkg unregister --user array-0.3.0.0 12/02 14:19 that will break some packages, that you'd need to reinstall 12/02 14:20 and I can find the broken ones in ghc-pkg list? 12/02 14:20 however, i'd probably unistall ghc and install one from scratch, using a prebuilt binary 12/02 14:20 (there are no reds in there right now) 12/02 14:20 by that worked!! 12/02 14:21 heh :) 12/02 14:21 the way* 12/02 14:21 yeah, you'll see the broken ones in ghc-pkg list or check, if there are any 12/02 14:21 yay 12/02 14:22 got Agda installed?:) 12/02 14:25 yes 12/02 14:25 nice 12/02 14:25 thank you!! 12/02 14:25 no problem :) 12/02 14:26 lol I love quail mode or whatever it's called for inputting unicode 12/02 14:29 = <+> (vs A <×> vz) > 12/02 14:45 nil : forall (A : SPT z) -> El z ε 12/02 14:45 nil _ = > > 12/02 14:45 cons : forall (A : SPT z) -> El z ε A -> El z ε -> El z ε 12/02 14:45 cons _ x xs = , > > > 12/02 14:45 that's from the paper about SPTs 12/02 14:45 what is El? 12/02 14:58 that's the interpretation, it gives values of a type 12/02 15:06 http://www.pasteit4me.com/112024 12/02 15:07 ah, i see 12/02 15:10 how do you turn on universe polymorphism? :| 12/02 15:19 {-# OPTIONS --universe-polymorphism #-} 12/02 15:20 :((( 12/02 15:20 I don't think I have a new enough version of agda? 12/02 15:20 it just thinks Level is not in scope 12/02 15:20 you've to import it 12/02 15:21 open import Level 12/02 15:22 assuming you've setup the searchpath for the standard library 12/02 15:22 haha oh man this sucks 12/02 15:22 I will have to get that standard library 12/02 15:22 thanks 12/02 15:22 ah I can just paste that file into mine 12/02 15:23 i guess that works too :) 12/02 15:24 why don't you like the std lib? 12/02 15:24 because I don't know how to install it 12/02 15:24 MissPiggy: i usually just untar into the directory of the project im working on then set up the search path accordingly 12/02 15:25 so you got a copy of the std lib for each project you work on? 12/02 15:26 stevan: yeah, which is not many since i'm still learning :) 12/02 15:27 one way to deal with backwards compat i guess :-) 12/02 15:27 yep, i guess that's the other reason - seems like the stdlib isn't a stable API yet 12/02 15:28 MissPiggy: (custom-set-variables '(agda2-include-dirs (quote ("." "/lib/src/"))) 12/02 15:29 --- Day changed Sun Feb 14 2010 is identifier definition and resolution formalized in any of the LC or TT? 14/02 20:01 huh 14/02 20:11 you mean like  x := foo 14/02 20:11 then x x --> foo foo 14/02 20:11 ? 14/02 20:11 yeah or lisp's (define...) 14/02 20:11 it seems to me that as soon as you introduce such a construct, you introduce general recursion unless you have rules to explicitely disallow self-reference 14/02 20:12 I don't really know any good treatmment of that but you do have to be careful about it (or you can break subject reduction, for example) 14/02 20:12 just make x := x a scope error 14/02 20:12 i think i will 14/02 20:13 :) 14/02 20:13 just thought that one of the calculi might actually include := or define or something in its syntax and semantics for it 14/02 20:14 oh well 14/02 20:14 btw, sorry, what is "subject reduction" - i haven't read that term before 14/02 20:14 if t : T and t --> t' then we should hope that t' : T, if NOT t' : T then we have broken subject reduction 14/02 20:15 like 3 + 3 : Int reducing to "six" : String would not be good 14/02 20:15 right right, i've read that, but didn't recall the name 14/02 20:17 thanks 14/02 20:17 guerrilla, many small languages that are studied formally have an expression like «let x = a in b» for x variable, a,b expressions, which can be defined to be non-recursive (x is in scope for b but not a) 14/02 22:41 kmc: right, that makes sense - builds a heirarchy of scope. hadn't occured to me that that'd be different than the lisp-style macros or agda's =. makes sense though. thanks for the input 14/02 22:48 --- Day changed Mon Feb 15 2010 if anyone asks a question similar to mine about name binding, i'd recommend http://www.cs.cmu.edu/~drl/pubs/lzh08focbind/lzh08focbind-tr.pdf 15/02 17:09 Focusing on Binding and Computation -- Daniel R. Licata, Noam Zeilberger, Robert Harper 15/02 17:10 indirectly linked to by agda wiki: http://www.cs.cmu.edu/~drl/pubs.html 15/02 17:10 so I'm just learning agda and am trying to show that all terms in a language of numbers and addition are well typed 15/02 17:15 not sure how to phrase it as a type, I tried: allwell : forall e -> isTrue (welltyped e) where isTrue is like the one from the agda tutorials 15/02 17:15 so both my terms will produce true, and I can just fill it in with True's inhabitant 15/02 17:17 that's one way 15/02 17:22 otherwise you could define welltyped as a gadt, rather than a function Term -> Bool 15/02 17:22 and that would only construct terms from well-typed constituents? 15/02 17:22 allwell would construct a value of that gadt for each term 15/02 17:23 ah 15/02 17:23 I can't actually seem to get my initial attempt to work, I'm using the definition of True as a record with no fields 15/02 17:24 so you've record True where; data False where; isTrue : Bool -> Set; isTrue true = True; isTrue false = False; ? 15/02 17:25 yeah 15/02 17:26 when I use _ it colors it yellow (can't determine type?) and when I use record{} I get "Expected record type, found isTrue when checking that the expression record{} has type isTrue (cata (const true |+| uncurry _∧_) (inn (inr ⟨ n0 , n1 ⟩)))" 15/02 17:26 obviously cata (const true |+| uncurry _∧_) will always be true since it turns numbers into trues and then pluses just and their subterms together 15/02 17:26 |+| is [_,_] 15/02 17:27 well that error means that it can't reduce (cata (const true |+| uncurry _∧_) (inn (inr ⟨ n0 , n1  ⟩))) 15/02 17:27 to true 15/02 17:27 in that scope 15/02 17:27 ah, what would cause that to occur? 15/02 17:28 well, if some of those functions pattern match on their arguments, and their arguments happen to be a variable 15/02 17:29 so you've to do case analysis to such a variable to make that application reduce 15/02 17:29 s/to such/on such/ 15/02 17:30 okay 15/02 17:30 thanks 15/02 17:30 or you might do case analysis on the result of that application 15/02 17:30 so to do it the other way, would it be something like: okPlus : {t0 t1 : μ NatPlusF} → Welltyped t0 → Welltyped t1 → Welltyped (inn (inr ⟨ t0 , t1 ⟩)) 15/02 17:32 okNum : {n : ℕ} → Welltyped (inn (inl n)) 15/02 17:33 data Welltyped : μ NatPlusF → Set where 15/02 17:33 sorry, did it backwards 15/02 17:33 hpaste seems to be dead 15/02 17:33 i'm not sure i understand that snippet 15/02 17:34 to use a gadt, something like?  data Welltyped : NatPlus -> Set where okNat : {n : Nat} -> Welltyped (nat n); okPlus : {t0 t1 : NatPlus} -> Welltyped t0 -> Welltyped t1 -> Welltyped (t0 + t1) 15/02 17:36 and then: allwell : (e : NatPlus) -> Welltyped e 15/02 17:36 yeah 15/02 17:39 assuming data NatPlus : Set where nat : Nat -> NatPlus; _+_ : Nat -> Nat -> NatPlus 15/02 17:40 awesome, thanks!  That is much more attractive than using isTrue 15/02 17:40 yeah, it's quite nicer to work with 15/02 17:42 it's not really a GADT though more like an inductive-family right? 15/02 17:44 oh, i were using the two terms as synonyms 15/02 17:45 what is the difference? that the gadt is indexed over types rather than values? 15/02 17:46 s/the gadt is/GADTs are/ 15/02 17:46 so if I want to make an operation semantics with plus reducing only when it's arguments are values, do I need to make a notion of value or normal and then construct such a step from two normal subterms? 15/02 17:50 well I just think of GADT in haskell 15/02 17:50 like: Plus : forall {n m} -> Normal n -> Normal m -> n + m --> (the value of n) mathematical+ (the value of m) 15/02 17:51 lpjhjdh: you mean writing an interpreter for potentially open terms? 15/02 17:51 what does potentially open mean? 15/02 17:52 that they could have free variables in them 15/02 17:53 are you writing a type checker? 15/02 17:53 ah, no, i see what you're asking 15/02 17:54 I have no notion of variables, working with something as simple as your NatPlus above. 15/02 17:54 you want to write the one-step reduction for _+_ ? 15/02 17:54 MissPiggy: eventually, first I need to get the hang of how to express stuff as types, I'm used to working with isabelle 15/02 17:54 oh 15/02 17:54 so right now you are making  (1) untyped syntax   (2) well typed syntax  ? 15/02 17:54 so I have left and right reduction like: PlusL : ∀{n m} → n ⟶ n' → n +a m ⟶ n' +a m 15/02 17:54 type checker would be a function (1) -> (2) + error 15/02 17:55 for a step relation: data _⟶_ : μ NatPlusF → μ NatPlusF → Set where 15/02 17:55 ahh you are doing semantics in that very general way that also covers general recursive programs 15/02 17:55 if you have a simple language like nat you can take the easy (cheating) route :P 15/02 17:55 but maybe you don't want to 15/02 17:55 MissPiggy: yeah, I'm actually only focusing on preservation right now, so not even full type safety.  In the context of interpreters as coproducts of algebras 15/02 17:57 err, languages rather 15/02 17:57 you can get preservation and all that stuff for free if you have a simple language like that 15/02 17:57 maybe what you want is "Plus : forall {n m} -> Normal n -> Normal m -> Normal (n + m)" 15/02 17:58 Saizan: I'd really like to say that n + m can then step to something normal 15/02 17:59 Saizan: maybe "Plus : forall {n m} -> Normal n -> Normal m -> PlusTerm n m --> Normal (n + m)"? 15/02 18:00 wait a second 15/02 18:00 have you defined untyped syntax 15/02 18:00 i.e. something like 15/02 18:01 data Syntax : Set where 15/02 18:01 Constant : Nat -> Syntax 15/02 18:01 lpjhjdh: ... -> (n + m) ⟶ o \x Normal o ? 15/02 18:01 _+_ : Syntax -> Syntax -> Syntax 15/02 18:01 _*_ : Syntax -> Syntax -> Syntax 15/02 18:01 etc 15/02 18:01 ? 15/02 18:01 lpjhjdh: where \x is the pair type constructor 15/02 18:01 tt : Syntax 15/02 18:01 ff : Syntax 15/02 18:01 if_then_else_ : Syntax -> Syntax -> Syntax -> Syntax 15/02 18:01 is that to say that n + m reduces to o and that, that reduction is normal? 15/02 18:02 MissPiggy: yeah, it's basically NatPlus that Saizan defined above 15/02 18:02 that o is normal, yeah 15/02 18:02 okay, thanks, I'll try that 15/02 18:02 okay so why not define a typed syntax next 15/02 18:02 lpjhjdh: here Plus would be a function, not a constructor 15/02 18:03 you can either:  Define evaluation on untyped syntax (as a relation that can potentially get stuck) 15/02 18:03 or you can define typed syntax, and a total function that evals it 15/02 18:03 the untyped syntax produces only welltyped terms here though 15/02 18:03 MissPiggy: I need to have potentially untyped terms because I want to do it for arbitrary coproducts 15/02 18:03 eventually 15/02 18:03 what 15/02 18:03 Saizan: hmm, I'm not sure how to get the value part of n and m since I'm saying they are terms 15/02 18:06 value part? 15/02 18:06 what they reduce to, you mean? 15/02 18:07 to do (n + m) 15/02 18:07 yeah 15/02 18:07 i thought that would be stored inside Normal m and Normal n 15/02 18:07 oh, I was thinking normal meant it couldn't step, that's a good idea 15/02 18:08 well, not having variables if you can't step you should have a value, afaiu 15/02 18:09 if I were to have variables would I then just need a context from variables to numbers or something? 15/02 18:10 or maybe Normal (n + m) would accept a term made of _+_ applied to variables? 15/02 18:11 I see.  I need to play around with some definitions I think.  Thanks for taking the time to help me out 15/02 18:13 np 15/02 18:13 i'm not an expert in the field either, so take everything i say with caution :) 15/02 18:13 s/either// 15/02 18:14 haha, all the suggestions seem to work out perfectly so far 15/02 18:14 MissPiggy: do you remember where that STLC typechecker+interpreter featured on the FP lunch blog lives? 15/02 18:19 yeah there's also one in the epigram paper View from the Left 15/02 18:19 http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=291 15/02 18:20 yeah, i recall a repo with the code of that one, but not the actual URL 15/02 18:20 9 15/02 19:02 --- Day changed Tue Feb 16 2010 since i've been working with decidable predicates i've almost stopped thinking and just used the types to fit things together, not sure if that's good though 16/02 02:36 i don't even see the code anymore 16/02 04:10 Was the book "Programming in Martin-Löf's Type Theory" (out of print) replaced by something else? 16/02 10:18 * guerrilla doesn't understand why such a good book would go out of print otherwise 16/02 10:18 --- Day changed Wed Feb 17 2010 Is there something I can read that will help me understand how to use Induction.WellFounded? 17/02 00:27 the idea is that if you can build an Acc x for your x, then you can structurally recurse over it to keep the termination checker happy, which gives you more freedom than structural recursion over x, generally 17/02 00:35 i don't know of a tutorial though 17/02 00:36 would I be able to construct such an Acc for a pair of lists showing that the sum of their sizes gets smaller? 17/02 00:37 Supposing I wanted to write a merge function over two sorted lists 17/02 00:37 i think so, your _<_ would compare the sum the sizes 17/02 00:38 yeah 17/02 00:38 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=21167#a21167 <- the standard natural example 17/02 00:43 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=21167#a21173 17/02 00:51 step 1 (operating on single lists by length) 17/02 00:52 I have a file where I used well-founded induction to prove the soundness of propositional logic. 17/02 01:25 http://code.haskell.org/~dolio/agda-share/logic/html/Propositional.html 17/02 01:25 I just wrote it down as a single recursion combinator, though. It's not all modular like Induction.WellFounded is. 17/02 01:25 It's a slightly more exciting example than natural numbers with <, though. 17/02 01:26 gda 17/02 05:56 :o 17/02 05:56 * glguy boggles as agda simply /accepts/ the obvious merge implementation 17/02 18:00 OK, I was wrong that the termination checker understood my merge, BUT I was able to write it using Induction.Lexicographic 17/02 19:05 and it actually doesn't look too bad 17/02 19:05 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=21444#a21444 17/02 19:28 glguy: now do it for colists! 17/02 19:54 Agda: is it a dependently-typed programming language? Is it a Turing-tarpit? ¯\(°_0)/¯ 17/02 22:51 getting slowed down by termination proofs? 17/02 22:53 by the desire to prove all sorts of properties :) 17/02 22:54 It's not a Turing tarpit. 17/02 22:54 Maybe a total tarpit. 17/02 22:54 :) 17/02 22:54 hehe :) 17/02 22:59 * glguy has the horrifying realization that the structure of any proof of a property of the function defined using the lexicographic induction module will likely need to use lexicographic induction 17/02 23:34 --- Day changed Thu Feb 18 2010 * Saizan found a "bug" in the epitome 18/02 03:32 ? 18/02 03:32 the description of the computational behaviour of "branches" looks ill-typed and doesn't seem match the implementation, though i might be reading this wrong 18/02 03:34 why does emacs editor from agda on windows open files as read only? 18/02 11:34 only sane way to write agda programs is to use emacs? 18/02 13:10 rla_: i use vim and makefiles... 18/02 13:16 so, im curious - how much of Ana Bove's thesis is incorperated into agda? i just started reading it... seems related to what glguy has been going through recently 18/02 13:52 hah, i was wondering where i should've reported or sent a patch for the epitome thing, but it seems this channel works :) 18/02 14:11 I can understand many of the calls for papers that go on the agda mailing list 18/02 14:40 but a conference on education?? 18/02 14:40 mathematics education? teaching constructive mathematics? 18/02 14:44 seems appropriate 18/02 14:44 http://snapplr.com/c17z 18/02 14:45 as appropriate as a conference on "stuff" 18/02 14:46 I dunno, if it's relevant to agda people it seems like the very very edge of relevance :) 18/02 14:46 I get the impression that someone showing up to that conference and giving a talk on the use of a theorem prover to teach math wouldn't be very understood 18/02 14:47 really? 18/02 14:47 i could see it.. 18/02 14:47 there were lots of courses in teaching alg/ds w/ scheme and lisp back in the day 18/02 14:48 or pascal for that matter 18/02 14:48 granted, thats in cs and not math.. 18/02 14:48 *shrug* 18/02 14:48 I just think the adult learning, business learning, etc. might consider "math education" to mean "teach me algebra! what? I'm talking about x + y, not groups and rings! what the hell are those? nobody uses those in the real world" 18/02 14:49 but maybe I'm just projecting :P 18/02 14:49 probably 18/02 14:50 * copumpkin erases his prejudices and starts from scratch 18/02 14:50 ive heard calculus is more and mroe taught via proofs these days 18/02 14:50 can't comment on that :) 18/02 14:50 ah well, time for class 18/02 14:52 later 18/02 14:52 ciao :) 18/02 14:52 --- Day changed Sun Feb 21 2010 hey, are there any basic agda tutorials that can show me how agda works by proving a simple theorem from algebra, say? 21/02 01:40 Some basic induction would be nice, like  \sum_{k = 0}^{n} k = n (n +1) / 2. 21/02 01:45 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials <- the first one has some proofs by induction over naturals not so far in it 21/02 01:59 or you could look at the code from the standard library 21/02 02:00 In the stdlib, things like monoids are modelled as records; no type parameters or anything. So, then, how do you specify "some Monoid" in a type signature? 21/02 02:00 i.e. the equivalent of (Foo a) => ... in Haskell. 21/02 02:00 (m : Monoid) -> .. and use Carrier m in place of a 21/02 02:01 thanks Saizan! My brain's been hitting a wall with even starting to mess with agda. 21/02 02:02 It's saying, "Am need step by step introduction for understanding" 21/02 02:02 Saizan: So then consider "(Foo a, Bar a) => ...". 21/02 02:03 Do we do: 21/02 02:03 (a : Foo) -> (b : Bar) -> (a \equiv b) or something? 21/02 02:03 Furthermore, can we make these arguments implicit? If not, passing around various monoids and the like will, I expect, be a pain in the posterior. 21/02 02:03 you could parametrize your module over them 21/02 02:04 rather than each function, so you don't have to pass them around so much 21/02 02:04 You still have to pass a whole big bag o' them at some point, which is irritating when we have a facility like implicit arguments that would work if only it were Monoid m, no? 21/02 02:05 and, you could do (Foo.Carrier a \== Bar.Carrier b) though maybe you'd prefer using IsMonoid and make the sharing work by construction 21/02 02:05 no, it wouldn't work? implicit arguments are not typeclasses 21/02 02:06 Yes, I know that. 21/02 02:06 But if you consider Monoid : Set -> Set... where the result is a record type using that set, I don't see why you couldn't use implicit arguments. 21/02 02:06 Admittedly I don't know how Agda does implicit arguments. 21/02 02:06 well, there's nothing preventing Monoid to be defined that way 21/02 02:07 but, whick "Monoid X" value would agda fill in for an implict argument of type Monoid X? does it just pick the nearest one around? 21/02 02:08 you could easily have monoid1 and monoid2 both fitting that type and not being equal 21/02 02:09 well of course implicit arguments cannot be inferred in all cases 21/02 02:10 That seems blindingly obvious to me, as you can make anything an implicit argument. 21/02 02:10 /Most/ of the time, though, there'll be only one. 21/02 02:10 i'm saying that it couldn't get inferred most of the time 21/02 02:10 but you can try :) 21/02 02:11 Why not? Most of the time, a certain type will only have one monoid, no? 21/02 02:11 implicit arguments don't really work by guessing like that, ime 21/02 02:11 they only get filled when there's one obvious solution, e.g. for indexes of some other argument type 21/02 02:12 foo : {n : Nat} -> Fin n -> X; i : Fin 1; then foo i works because the 'n' can be read off the type of i 21/02 02:14 well, if there's only one Monoid a... 21/02 02:14 but you're right it would be an extension 21/02 02:14 I'm playing with solutions to the issue in my own pet (vaporware) dependent language... 21/02 02:15 typeclasse do this for you because there's a guarantee there's only one matching instance and a procedure to find it 21/02 02:15 yeah, but typeclasses suck :) 21/02 02:16 they are pretty limited by the fact that you've to be able to find a solution, yeah :) 21/02 02:17 though explicit instantiation can be done with newtypes 21/02 02:17 what we could have is a marker that a certain definition can be "filled in" for an implicit thingy of that type 21/02 02:18 but that feels "impure", somehow, to depend on such theoretically unnecessary markers 21/02 02:18 it's a non-trivial problem! 21/02 02:19 maybe the IsFoo kin are the best; that lets you do {IsFoo blah} -> {IsBar blah} -> ...use blah here..., right? 21/02 02:19 Although, no, wait, you need to specify the operations and the like in the IsX call. 21/02 02:19 'tis a non-trivial problem 21/02 02:19 you could put the operations inside the record 21/02 02:20 instead of having them as parameters of it 21/02 02:20 (keeping the type outside) 21/02 02:20 though that's kind of arbitrary, there's already people on #haskell that would like to index Monoid by the operation too :) 21/02 02:21 yeah that's what I originally said—but you can't use that as an implicit param 21/02 02:22 or, can you use IsX as an implicit param either? I guess not. 21/02 02:22 Phooey. When my language is older than your language, it'll beat your language up. :P 21/02 02:22 it's harder to compare functions in a satisfying why, but if you keep it intensional it's still decidable 21/02 02:23 *way 21/02 02:23 Why do you need to compare them? 21/02 02:25 just like you need to compare types to find the right instance 21/02 02:26 Ah; you mean equality, not ordering. 21/02 02:26 yeah 21/02 02:26 btw, i think i'd like to try such a language :) 21/02 02:29 though this filling in mechanism has to be kept really predictable, imo 21/02 02:30 alise: you might want to look at Coq, i think they've implemented something typeclass-like with tactics, they might have extended it too 21/02 02:32 yeah a good look at Coq is on my todo list 21/02 02:33 really i don't need any specific mechanism 21/02 02:34 I know that typeclasses are the Wrong Thing and I know that specifying trivial monoid instances all the time is the Wrong Thing, but apart from that I have no clue what the Right Thing is 21/02 02:35 abstacting such things at a larger scope is fairly nice when you can 21/02 02:36 you tend to need qualified names or renaming if you use multiple e.g. monoids in the same code though, which is not ideal 21/02 02:37 yeah is it just me or is agda's solution to lots of _+_s just to rename them on import? 21/02 02:41 that is so weak. 21/02 02:41 wb. 21/02 02:42 yeah is it just me or is agda's solution to lots of _+_s just to rename them on import? that is so weak. 21/02 02:42 in case you didn't see 21/02 02:42 (re: qualified names/renaming) 21/02 02:42 you see some of that 21/02 02:43 if you're using two monoids on the same type you're screwed anyway, though 21/02 02:47 there's not much difference between the effort needed to specify the operation and passing the whole record in 21/02 02:50 maybe what we need is to be able to import two values with the same name, but disambiguable based on type 21/02 02:53 and have Monoid m; if we always name it monoid, then we can just import all monoids and specify "monoid" (which we could sugar away). 21/02 02:53 You have to specify if you have multiple monoids on the same type, but that's not too common to matter much. You can always name one something other than "monoid". 21/02 02:53 This also lets you import multiple _+_s. 21/02 02:54 It's a bit of a hack, though. 21/02 02:54 A kludgey hack. 21/02 02:54 but if both monoids are over the same set, how can you disambiguate on type? 21/02 02:54 I guess you don't try 21/02 02:54 ehm, yeah, we could do that, which is basically a small bridge between records and typeclasses 21/02 02:55 copumpkin: exactly 21/02 02:56 copumpkin: which is why it's based on name 21/02 02:56 name one monoid and the other altMonoid 21/02 02:56 of course, basing it on name is /really/ ugly. 21/02 02:57 maybe we just need better code editor and/or better serialization formats for code 21/02 02:57 what's that got to do with this :) 21/02 02:57 if the resulting code is still ugly automation doesn't help 21/02 02:57 there's no abstraction or expressiveness gained here, it's just nicer to look at 21/02 02:58 so a different format could make it better, without requiring weird things in the language 21/02 02:58 Surely this is a problem to be solved with syntactic sucrose. 21/02 02:59 maybe limiting oursevels to static text is the problem :) 21/02 02:59 Yeah, so say we all. I dabbled in two-dimensional syntax as recently as... well, days ago, but right now I'm content with Unicode-drunk linear syntax. 21/02 03:00 Mostly because two-dimensional notation often just seems to be inconsistency for the sake of it. 21/02 03:00 i wasn't thinking of other dimensions 21/02 03:02 i was thinking of a format that more aware of binding and less of names 21/02 03:02 Seems a bit vague. 21/02 03:03 or that just wisely hides unimportant parts and help you fill them as you go, without incorporating automagic searches into the language 21/02 03:04 Then again, I'm one to talk. 21/02 03:04 yeah, i'm just tossing ideas around 21/02 03:04 Me with the grandoise progamming language/OS visions. :) 21/02 03:04 --- Log closed Sun Feb 21 11:54:38 2010 --- Log opened Sun Feb 21 11:54:43 2010 -!- Irssi: #agda: Total of 22 nicks [0 ops, 0 halfops, 0 voices, 22 normal] 21/02 11:54 -!- Irssi: Join to #agda was synced in 67 secs 21/02 11:55 --- Day changed Mon Feb 22 2010 why is ⊤ used as the name for the unit type? that isn't what ⊤ means :P 22/02 01:42 at least in type theory 22/02 01:42 What does it mean in type theory? 22/02 01:51 http://en.wikipedia.org/wiki/Top_type 22/02 01:51 The top type in type theory, commonly abbreviated as top or by the down tack symbol (⊤) is the universal type--that type which contains every possible object in the type system of interest. The top type is sometimes called the universal supertype as all other types in any given type system are subtypes of top. It is in contrast with the bottom type, or the universal subtype, which is the type containing no members at all. 22/02 01:51 for any type a, ⊥ ≤ a ≤ ⊤ 22/02 01:52 so the unit type is quite an awful lot of values away from being ⊤ :P 22/02 01:52 #1 as a type was ugly, maybe? 22/02 01:53 Well, Agda doesn't really have any subtyping. 22/02 01:53 and it's against the rules to use actual words as names in the standard library 22/02 01:53 Anyhow, the definitions of ⊥ and ⊤ come from logic. 22/02 01:53 dolio: That doesn't mean it isn't a misuse. 22/02 01:53 Agda doesn't have the law of the excluded middle, either, but you don't name some random thing not-p-and-not-p :P 22/02 01:54 dolio: For logic, yeah, it's reasonable. 22/02 01:54 But it's still really confusing considering how much type theory Agda has in it. 22/02 01:54 Well, it has plenty of logic in it, too. 22/02 01:54 Yeah, but this /is/ in the type system. :P 22/02 01:55 So is the logic. 22/02 01:55 Clearly the unit type should be renamed to ⊡. 22/02 01:56 It is a box containing exactly one thing. 22/02 01:56 exists t. t is isomorphic to the unit type, anyway. 22/02 01:56 Then the enemies of English, and the enemies of type theory, can both be happy! 22/02 01:56 dolio: Well, that's true. 22/02 01:56 Actually I think you just convinced me it's okay with that. 22/02 01:57 回 22/02 01:57 Unless you have a language where all types are empty, I suppose... 22/02 01:58 But that doesn't seem like it'd be very useful. 22/02 01:58 But then the unit type would also be empty... so I guess they still would be isomorphic. 22/02 01:59 if you use coercions with your subtypes, then the above descriptions say that \top is final and \bot is initial, just like they are in agda 22/02 02:13 (which is another way to say that they are isomorphic to exists t. t and forall t. t i guess?) 22/02 02:14 so that Ur/Web language is apparently dependently typed (http://www.impredicative.com/ur/demo/) 22/02 11:28 (the language used in that web platform mentioned on the last front-page post on LtU) 22/02 11:29 --- Day changed Tue Feb 23 2010 * Guest12506 would be interested in feedback on both style and approach if anyone was interested http://www.galois.com/~emertens/revrev/revlistapp.html 23/02 02:30 pretty nice 23/02 02:35 I like it :) 23/02 02:35 are the extra refls overkill or educational? 23/02 02:35 general style-wise, I'd write what your goal is (in human) at the top :P I only figured out what you were working towards at the end 23/02 02:35 hmm, good point :) 23/02 02:36 a bit inconsistent to use rewrite just at the end while sticking to eq-reasoning the whole time :) 23/02 02:36 true enough :) 23/02 02:36 I think I was just really excited to be done at that point! 23/02 02:37 * copumpkin has never used rewrite :o 23/02 02:37 eheh, i guess :) 23/02 02:37 i like the refl steps 23/02 02:37 doesn't Algebra have an Involutive property? 23/02 02:37 yeah, you could write your rev-rev using it 23/02 02:38 but that might just obscure things 23/02 02:38 I'm not sure I know how to pronounce that 23/02 02:38 much less use it :) 23/02 02:38 reverse-app (reverse-app xs) ≡ xs 23/02 02:38 Involutive reverse-app :P 23/02 02:38 same thing 23/02 02:38 * copumpkin doesn't know how to pronounce it either, though 23/02 02:39 inVOLutive? 23/02 02:39 involUtive? 23/02 02:39 I quite like your naming of parameters in types 23/02 02:40 I might start doing that too 23/02 02:40 in the past I've only done it if I need them later in the type 23/02 02:41 I haven't decided which way I like more 23/02 02:41 what do you mean? 23/02 02:41 rev : {A : Set} (xs ys : List A) → List A 23/02 02:42 I'd have written rev : {A : Set} -> List A -> List A -> List A 23/02 02:42 ah, i see 23/02 02:42 i'd probably have written \all {A} (xs ys : List A) -> List A , or abstracted A at the module level 23/02 02:43 yeah, good point 23/02 02:43 \all {A} is ambiguous 23/02 02:43 List is good for any level of set 23/02 02:44 ah, that's annoying 23/02 02:44 but you can still factor it out into a module parameter 23/02 02:44 sure 23/02 02:44 then you could even have this work over any level of set 23/02 02:44 without too much pain 23/02 02:44 ah, true, wasn't thinking of universes 23/02 02:44 would I be proving the exact same properties if I parameterized the module instead of each function? 23/02 02:48 * glguy wonders if there isn't some subtle difference to what has been proven 23/02 02:48 if you had module revlistapp {A : Set} where ... then for each function defined there revlistapp.foo : {A : Set} -> , no? 23/02 02:51 and all your types seem to fit that form 23/02 02:52 and you don't seem to instantiate your functions to something other than A when you reuse them later 23/02 02:53 you could also "open Monoid (monoid A)" once at the module level 23/02 02:54 yeah, I had it that way at first 23/02 02:55 I was trying to be clear about where those were coming from 23/02 02:55 maybe with some "renaming" I can make it nice 23/02 02:55 you still need a "right-id = proj\_2 identity" though 23/02 02:56 bah, monoid : Set -> Monoid 23/02 02:59 which screws up my level polymorphic version 23/02 02:59 yeah, that's lame 23/02 03:00 it's Algebra's fault though 23/02 03:00 the whole module is still monomorphic 23/02 03:00 http://www.galois.com/~emertens/revrev/html/revlistapp.html now with more universe polymorhpism 23/02 03:08 morphism* :) 23/02 03:08 you should fix up Algebra and send in a patch! :P 23/02 03:08 much prettier than seeing all the {A : Set} 23/02 03:12 Is there is potentially theoretic level that only elements of Set can be Monoid? 23/02 03:13 level/reason 23/02 03:13 I doubt it 23/02 03:13 With my current knowledge level, I tend to assume that if something in the library doesn't work like I want it to that I don't want to do what I wanted :) 23/02 03:14 I'm pretty sure it's just because nobody has had time to universe-polymorphize Algebra yet 23/02 03:14 but I may be wrong 23/02 03:14 I'm using released version 0.3 23/02 03:15 it might be different in darcs 23/02 03:15 yep 23/02 03:15 record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where 23/02 03:15 What do people do for darcs on Snow Leopard? 23/02 03:56 * glguy finds the binaries on the darcs site... 23/02 03:57 (colloquy is such a buggy client) 23/02 04:44 yeah :) 23/02 04:44 IRC clients tend to be pretty shitty, in my experience 23/02 04:44 especially the pretty mac ones 23/02 04:45 * copumpkin closes his eyes and dreams of a UI library that makes beautiful mac GUIs, FRP-like, in an awesome future dependently typed language with magic proofs that write themselves! 23/02 04:49 why does Peter Morris use such strange notation for Sigma types in http://www.cs.ioc.ee/~tarmo/tsem09/morris.html ? 23/02 14:55 roconnor: which slide ? 23/02 15:05 any slide with a Sigma on it 23/02 15:06 he writes Σ A \ a -> B 23/02 15:06 ha, the backslash you mean 23/02 15:06 a notation I have never seen 23/02 15:06 like in haskell \ can be used as a λ 23/02 15:06 ah 23/02 15:07 but someone should tell him 23/02 15:07 those backslashes looks ugly 23/02 15:07 I was wondering if there was some advangate over Σ a:A. B 23/02 15:09 I guess the advantage is that it better represents the "natural" syntax for sigma types as an inductive familiy of two arguments 23/02 15:09 though Σ A (λa. B) I would find easier to read :D 23/02 15:10 in agda this is λ a → not λa. 23/02 15:10 and in agda Σ is not builtin syntax 23/02 15:11 too bad.  λ a ↦  seems a bit nicer than using →. 23/02 15:12 right, but since → is already reserved for function space it let ↦ free to be used in definition 23/02 15:13 I often use "_,_↦_ : Map → Key → Val → Map" 23/02 15:14 :) 23/02 15:14 that should be "_[_↦_] : Map → Key → Val → Map" 23/02 15:15 :) 23/02 15:15 why not 23/02 15:15 I like it too 23/02 15:15 can you use that syntax? 23/02 15:15 sure 23/02 15:18 copumpkin, Check out "prop" http://www.galois.com/~emertens/revrev/revlistapp.html#5899 23/02 22:51 oh my 23/02 22:52 that's nice 23/02 22:52 can it not infer the type of f? 23/02 22:53 of 'f'? 23/02 22:53 it can not 23/02 22:53 prop? 23/02 22:53 weird 23/02 22:53 Saizan, yeah, that one :) 23/02 22:53 seems pretty obvious to me, but then again I haven't figured out what agda can infer and can't 23/02 22:53 and when 23/02 22:53 I know that it covers the type in yellow 23/02 22:53 I think that it does not learn enough about the type until the end 23/02 22:54 at which point it is too late 23/02 22:54 oh, it's probably because it isn't constrained to A 23/02 22:54 (f : _ A -> _ A) 23/02 22:54 :P 23/02 22:54 * copumpkin shrugs 23/02 22:54 I also did "++-right-identity" using the Inductive module (as the expense of conciseness :-D) http://www.galois.com/~emertens/revrev/revlistapp.html#954 23/02 22:55 at the expense* 23/02 22:55 a normal foldr doesn't work (obviously) because the type of the proof changes at every step 23/02 22:56 wow, you actually used the other colon 23/02 22:56 I did that to help show what was going on 23/02 22:57 it isn't necessary 23/02 22:57 pretty cool :) 23/02 22:58 couldn't you use prop to prove rev-app? 23/02 22:59 it was fun when I discovered that (∀ xs ys → f (xs ++ ys) ≡ f ys ++ f xs  ) → f [] ≡ [] 23/02 22:59 with a helper 23/02 22:59 possibly? 23/02 23:00 I just did "prop" over lunch 23/02 23:00 I haven't considered how it affects things, yet 23/02 23:00 oh, so you can get rid of one parameter to prop? 23/02 23:01 Well, it originally had f [] == [] as a parameter 23/02 23:02 but then I did the proof deriving that from the append property 23/02 23:02 oh I see 23/02 23:02 omg it's TacticalGrace 23/02 23:02 without f [ x ] == [ x ]   (const []) would be a valid implementation 23/02 23:03 hey copumpkin 23/02 23:03 ah 23/02 23:04 hi :) 23/02 23:04 Is there something like ⊤ (top) that exists in universes other than Set? 23/02 23:11 don't think so, and I remember bottom is just in Set too 23/02 23:12 glguy: You can use Lift ⊤ 23/02 23:19 oh nice 23/02 23:20 when did that appear? 23/02 23:20 --- Day changed Wed Feb 24 2010 we can pattern match on records now? nice. 24/02 07:16 agda: Oops!  Entered absent arg ww_s8Yi9{v} [lid] tcm{tv a8XlM} [tv] Agda-2.2.7:Agda.TypeChecking.Monad.Base.TCState{tc r2Qcm} <- i'm not sure if this is an agda or a ghc bug.. 24/02 07:21 copumpkin: just before the 2.2.6 release I think 24/02 09:08 --- Day changed Thu Feb 25 2010 Thoughts on whether this agda program captures the trivial exercise from TAPL 2.2.6? http://www.galois.com/~emertens/exercise2.2.6/Tapl2.html 25/02 09:31 (I recognize that this is a highly trivial proof, but I'd like to see how many of these I can do with Agda and I'd like to start at the beginning) 25/02 09:32 Is there a "decidable partial order" type in the standard library? 25/02 16:08 actually, just realised I actually want total orders, but I'm interested in the answer anyway. 25/02 16:10 * HairyDude finds his agda is out of date and upgrades it. 25/02 16:20 also, a small request: could the standard library tarball (and the directory it contains) please be called agda-lib not just lib? seeing it in a directory listing it's not clear at a glance what it is 25/02 16:30 wiki page on universe polymorphism is out of date. 25/02 16:39 I don't think this is the right place for bug reports 25/02 16:49 point 25/02 16:55 hrm. does the mailing list deliver non-text attachments? gmail doesn't realise an .agda file is actually text 25/02 17:22 i think i may have ased this before, but does anyone here actually dev agda? 25/02 17:22 guerrilla: in what sense? 25/02 17:26 I've written a fair amount of agda code 25/02 17:26 not sure you'd call it development in the traditional sense though :) 25/02 17:26 i meant working on agda itself 25/02 17:34 oh :) 25/02 17:35 no 25/02 17:35 not as far as I know, anyway 25/02 17:35 yeah, i didn't think so :) 25/02 17:35 copumpkin: btw, is the regex link still 404 for you? 25/02 17:36 stevan: nope, fixed now, thanks :) 25/02 17:36 I took a quick look at it yesterday and it looked interesting 25/02 17:36 curious, what's this about regex? 25/02 17:37 someone doing some FL stuff in agda? 25/02 17:37 reddit.com/r/dependent_types/ 25/02 17:38 wow *brain explodes* didn't know that existed :) 25/02 17:39 this paper on regex is great. 25/02 17:42 im so happy now :) 25/02 17:42 :) 25/02 17:44 I started writing a module with the same goal 25/02 17:44 but got bored/started shaving a yak 25/02 17:44 ah 25/02 17:44 yes, i'd like to keep going to CFG/PDA and then AGs 25/02 17:45 i'm not good enough with Agda yet, so been messing around trying different things 25/02 17:45 still don't know how to represent disjoint sets over an arbitrary sets yet though 25/02 17:46 A \intersection B = \emptyset 25/02 17:46 \all x -> A x -> \neg B x and vice versa? 25/02 18:04 1sec Saizan - phone 25/02 18:13 k, sorry about that 25/02 18:16 yes, i think that's basically what i mean 25/02 18:16 but i think i need it as a proof object, so that i can construct a record that contains both sets and that proof 25/02 18:16 hmm. "right hand side must be a single hole" is a rather annoying limitation. 25/02 21:23 is there a "decidable unary relation" type? 25/02 23:57 --- Day changed Fri Feb 26 2010 there's Data.Fin.Dec and Data.Sets but neither is quite right, I want something like DecPred : forall {A l} -> (P : Pred A l) -> (x : A) -> Dec (P x) 26/02 00:02 well that's not quite right, but you know what I mean 26/02 00:03 what would be the type of _->_ in agda, if it can be written? 26/02 06:15 Set1? 26/02 06:16 {A : Set i} {B : A -> Set j} -> (x : A) -> B x -> Set (max i j) ? 26/02 06:19 well, in a sort of imaginary world 26/02 06:21 I think that's too many arguments. 26/02 06:24 It'd be {i j} (A : Set i) (B : A -> Set j) -> Set (max i j) 26/02 06:25 But that uses -> to define the type of ->. 26/02 06:25 :) 26/02 06:25 dolio: yeah, looks a little impredicative :) 26/02 06:31 would have to use a further relation i guess 26/02 06:32 Well, when you formalize these things with pure type systems, you usually have a sort of schema for giving the type of particular instances of pi types. 26/02 06:33 And it's a little less weird in Haskell because the (->) for types isn't the same as the (->) for kinds. 26/02 06:34 true 26/02 06:34 (And the forall for types.) 26/02 06:34 It's not all mixed together like with dependent types. 26/02 06:34 hmm, OT, but haskell kinds are a subset of the arity system in M-L TT, right? 26/02 06:37 (since kinds don't apply to records, as i understand it) 26/02 06:37 Records? 26/02 06:38 yeah.. 26/02 06:38 1sec, maybe that's not what they're called in ML TT 26/02 06:38 combinations 26/02 06:39 Well, I don't know ML TT really. At least not the technical terminology. 26/02 06:39 i assumed those were equivalent to records 26/02 06:39 seems like it, combination <-> record instantiation and selection <-> selection 26/02 06:39 dolio: oh, right, i was mixing the type of _->_ with the type built with it 26/02 06:41 Haskell kinds are definitely a sub-system (or something) of what you get in a calculus like Agda (or, more accurately, the calculus of constructions). 26/02 06:43 what do people mean when they say a "calculus of X" or "X calculus"? 26/02 06:43 I've seen so many different calculi that I'm not sure what unifies them 26/02 06:43 is there a universal calculus like a universal algebra that defines them all? 26/02 06:44 copumpkin: from a thread on mathoverflow, it seems that there is no definition of a calculus 26/02 06:44 I don't think so. It's just a cool name. 26/02 06:44 everyone just has an intuitive feel for what people mean by it, I guess? 26/02 06:44 well, one difference i see between a calculus and an algebra is that a calculus gets you an end result at some point and an algebra is just used for rewriting 26/02 06:48 * copumpkin defines a calculus as a stone and moves on 26/02 06:48 hehe 26/02 06:48 nice 26/02 06:48 :) 26/02 06:48 in italian, kidney stones are called that 26/02 06:49 right, i actually remember something about that 26/02 06:49 calc as in calcium? kinda makes sense 26/02 06:49 yeah, it just means stone in latin 26/02 06:49 kinda morbid if they used them for counting 26/02 06:49 to calculate comes from the fact that romans used stones for it 26/02 06:49 or pebble, maybe 26/02 06:49 Well, the thing is, it's not very obvious (to me) that "The Calculus" has anything to do with lambda calculus and pi calculus and propositional calculus... 26/02 06:50 And relational calculus. 26/02 06:50 isn't "the calculus" actually "infintesimal calculus"? 26/02 06:50 so, maybe, the idea is that these systems are so simple that you can calculate with them 26/02 06:51 yeah, kind of get a "results"-feeling from calculus 26/02 06:51 where algebra is more abstract 26/02 06:51 Well, there's relational algebra, too. 26/02 06:51 The difference being that with relational algebra, you talk about composition of operations and stuff, and relational calculus is some kind of modified predicate calculus for reasoning about relational databases. 26/02 06:52 describing vs. calculating? 26/02 06:53 maybe... 26/02 06:53 I don't really see how one is more results-based. 26/02 06:53 like as in getting an end value 26/02 06:56 *shrug* 26/02 06:56 are there algebras with binders? 26/02 06:56 Yeah, I've thought about that. But the propositional calculus doesn't have binders. 26/02 06:57 binders as in some form of quantification or abstraction? 26/02 06:57 Maybe it should be propositional algebra? 26/02 06:57 unless you go higher order. 26/02 06:57 Results 1 - 10 of about 3,610 for "lambda algebra". (0.10 seconds) 26/02 06:57 Results 1 - 10 of about 2,750 for "propositional algebra". (0.17 seconds) 26/02 06:57 hehe (not too much spam either) 26/02 06:57 however i've seen people talk about both process calculi and process algebras 26/02 06:57 to mean the same thing. 26/02 06:58 There's also algebraic study of logic, which with categorical logic, can account for quantifiers. :) 26/02 06:58 just out of curiosity, what should I look for if I want to fit quantifiers in? 26/02 06:59 What? 26/02 07:00 what you just said about accounting for quantifiers 26/02 07:01 Quantifiers involve adjunctions. 26/02 07:01 ooh 26/02 07:01 can't get away from 'em 26/02 07:01 It goes something like... 26/02 07:02 Your formulas are in some way parameterized by a set (or object) of variables. 26/02 07:03 And change of that set of variables is a functor. 26/02 07:03 Existential quantification is left adjoint to that functor, and universal quantification is right adjoint. 26/02 07:04 ooh 26/02 07:05 that seems so elegant 26/02 07:05 I really need to read more of TTT 26/02 07:05 I assume that would cover it? 26/02 07:05 I haven't gotten to that yet. It might. 26/02 07:05 Awodey's book covers it a little. 26/02 07:06 TTT? 26/02 07:06 triples toposes and theories 26/02 07:06 in some order 26/02 07:06 You've got the first two switched. 26/02 07:07 damn 26/02 07:07 I guess triples and theories should go together 26/02 07:07 * guerrilla saves 26/02 07:07 http://code.haskell.org/~dolio/agda-share/induction/html/Transfinite.html is pretty cool 26/02 07:11 hadn't seen it before 26/02 07:11 OMG, Agda can do stuff infinitely many times! 26/02 07:13 :) 26/02 07:13 hehe, funny: http://www.dpmms.cam.ac.uk/~ardm/inefff.dvi 26/02 07:40 * Adrian Mathias, A Term of Length 4,523,659,424,929, Synthese 133 (2002) 75--86 26/02 07:40 what do errors such as the following mean? 26/02 11:41 A !=< _9 26/02 11:41 when checking that the expression a has type _9 26/02 11:41 guerrilla: try giving A a type 26/02 12:25 ∀ {A : Set} → ... 26/02 12:26 ah 26/02 12:54 thanks 26/02 12:54 --- Day changed Sat Feb 27 2010 * glguy has another trivial TAPL exercise to share http://www.galois.com/~emertens/exercise2.2.6/Tapl2.html 27/02 04:00 * copumpkin doesn't really understand how the begin ... \qed stuff works 27/02 04:01 I understand how to use it 27/02 04:01 the question is if I can explain myself :) 27/02 04:01 I don't really have a good feeling of how or when to use it :) I usually just have a bunch of cong/subst/trans/syms 27/02 04:02 and am not sure which ones I could use that thing for 27/02 04:02 it is good for any preorder where you want to show the intermediate steps off all the cong and subst and commute and whatnot 27/02 04:03 hm 27/02 04:03 I used it a ton http://www.galois.com/~emertens/revrev/revlistapp.html 27/02 04:03 in that file 27/02 04:03 because I was proving lots of x == y 27/02 04:03 yeah 27/02 04:03 and there were a number of steps to transform x into y 27/02 04:03 so the first thing in the list is always the x in x == y? 27/02 04:03 right 27/02 04:03 and the last is always y 27/02 04:03 but sometimes agda can simpify things down for you 27/02 04:04 so it will ask you to prove something syntactically different than your type 27/02 04:04 I still like to start from the literal goal 27/02 04:04 and use refl steps to work toward the simpified goal 27/02 04:04 hm, ok 27/02 04:05 * copumpkin plays with it a bit 27/02 04:05 it didn't click for me at first 27/02 04:05 * copumpkin pulls in Data.Nat.Properties 27/02 04:08 The reasoning module is for lots of chained trans. 27/02 04:22 * Saizan wants editor support to write cong's 27/02 04:23 x \qed is another name for refl : x == x 27/02 04:23 begin_ is the identity function. 27/02 04:24 And the _~<_>_ is transitivity. 27/02 04:24 x ~< x~y > y~z 27/02 04:24 I see 27/02 04:27 And that operator is... left associative? 27/02 04:29 I think that's right. 27/02 04:29 Wait, maybe right associative. 27/02 04:30 x ~<_> (y ~<_> z \qed) 27/02 04:30 binds like that 27/02 04:30 Yeah. That's right, I guess. 27/02 04:30 (Right as in the opposite of left.) 27/02 04:31 a lot of time I end up with:   begin x ~< eq > ? 27/02 04:31 and build out 27/02 04:31 Ah, nice. I usually just write it all out at once, but that's dangerous. 27/02 04:31 if I know exactly how to write it outright, I've done that 27/02 04:31 but I'm still learning 27/02 04:32 i tend to keep it like "begin x ~< eq > ? ~< ? > y \qed 27/02 04:32 yeah, that's what i've adopted 27/02 04:32 I'll do all of the values first 27/02 04:32 and then come back and do the reasons that the transition was ok 27/02 04:33 x =< ? > y =< ? > z \qed 27/02 04:33 we need a property called irregardless: http://snapplr.com/t9rg 27/02 05:15 so is symmetry:   ∀ a b → a ∾ b → b ∾ a   while commutativity is  ∀ a b → a ∾ b ≡ b ∾ a  ? 27/02 06:46 symmetry of relations, commutativity of operations, as far as I know 27/02 06:48 so yeah :) 27/02 06:49 I wouldn't use the same symbol for both 27/02 06:50 I'd like to be able to define functions with a subscript argument 27/02 07:07 me too 27/02 07:07 copumpkin: I know you were just posting a snippet earlier, but do you know how to produce HTML from an Agda file? 27/02 07:16 I think it's a parameter to agda-executable 27/02 07:16 let me look 27/02 07:16 agda --html 27/02 07:16 ah ok :) 27/02 07:17 oh, I was just posting a screenshot of the docs page 27/02 07:17 wait, were you suggesting or asking? 27/02 07:17 Suggesting it as a possibility for you just in case you did a screen shot because you didn't know about html output 27/02 07:17 oh, no :) I just have a screenshotter a keybinding away 27/02 07:18 and am extremely lazy :P 27/02 07:18 thanks though 27/02 07:18 ok, syntactic question - what if you need to use a type in a module parameter that is not yet imported? 27/02 15:19 for example, 27/02 15:19 module Eq (A : Set) (_==_ : A → A → Bool) where 27/02 15:19 where, normally, Bool would be imported right after that declaration... 27/02 15:20 i guess you just put it before... hmm, i didn't realize that was valid 27/02 15:20 n/m :P 27/02 15:21 in Relation.Unary why is the name Pred used? predicate? 27/02 21:49 predecessor 27/02 21:50 no you are right 27/02 21:50 so the set level of the preceding universe? *confused* 27/02 21:50 hehe 27/02 21:50 i really am not following this code... 27/02 21:51 i supposed it makes sense that a unary relation is a predicate (or a set) depending on how you look at it 27/02 21:51 but i'm not entirely sure why or how it is using universe polymorphism 27/02 21:51 --- Day changed Sun Feb 28 2010 So I'm trying to give a progress proof for the toy language Pierce gives in TAPL and I'm having a bit of trouble with a few cases, don't think I understand with well enough 28/02 20:47 I've written everything up in Isar first so I have a reference of how I need to go about everything 28/02 20:48 anyone have a hint for me?  http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23101#a23101 28/02 20:48 that currently doesn't actually work gives: "Missing with-clause for function progress" 28/02 20:51 In Isar I use disjunction elimination with the IH 28/02 20:56 lpjhjdh: hard to say without being able to test it, though you should have better luck with a distinct lemma in a where clause 28/02 21:52 where clause? 28/02 21:55 what's is that? 28/02 21:55 what* 28/02 21:55 here's my isabelle case if that helps: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23104#a23104 28/02 21:57 http://www.galois.com/~emertens/exercise2.2.6/Tapl2.html#1987 28/02 21:58 that function uses a where clause 28/02 21:58 it lets you put local definitions after your goal 28/02 21:58 ooh, a la haskell 28/02 21:59 would giving you the whole contex help? 28/02 22:04 * glguy doesn't know the question 28/02 22:04 I'm pretty new to Agda, but I'll help you translate your proof, if it can 28/02 22:05 that was at Saizan, but I'm trying to show progress for a toy language from TAPL.  I'm working on the iszero clause http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23101#a23101 28/02 22:05 and the link I gave above is the working piece from my Isabelle proof 28/02 22:06 I didn't really know what I was doing with those "with" clauses 28/02 22:07 I want to give proof by disjunction elimination over the result of the IH from n 28/02 22:07 that code looks like it should work 28/02 22:15 but the "with" construct is sugar, and not always perfect 28/02 22:16 so, writing out an helper function that does the pattern matching might help 28/02 22:17 ah, I'll try that, thanks 28/02 22:17 so that you write progress {suc n} {suc n'} (ok-suc nty) = helper (progress {n} {n'} nty) where helper : ...; helper (inl nst) = ..; helper (inr vn) = .. 28/02 22:18 so I'm getting yellow highlighting on "pg {iszero n} {n", can't figure out the rest of the implicit params? 28/02 22:28 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23105#a23105 28/02 22:28 is that what it means? 28/02 22:29 I can't actually give it n' and t' because I won't know if n' exists or what t' is until I match on "progress {n} nty" 28/02 22:29 cause if n were a value to begin with then iszero will go to true or false, but if it can step then iszero will simply step 28/02 22:29 i don't undestand 28/02 22:53 t' is the second implicit argument to progress, so you've it 28/02 22:53 oh, ha, thank you, I was thinking I needed to be specific (like iszero n') 28/02 22:54 it's actually n' that it can't figure out, I don't have n' 28/02 22:56 well, that's a problem then 28/02 22:56 because n' won't even exist if n is a value (n = zero) 28/02 22:56 then I need more case analysis I guess :( 28/02 22:56 how do you make the recursive call to progress without n'? 28/02 22:56 true, I guess I was just trying to ride off my Isabelle version which says "(∃e' . e ⟼ e') ∨ isvalue e" so the e' isn't there right away 28/02 22:58 maybe you need different types for your Agda version 28/02 22:59 is there a way to say: progress : ∀{t τ} → t :: τ → (∃t' . t ⟶ t') ∨ Value t 28/02 22:59 yes, see Data.Product 28/02 22:59 thanks! 28/02 22:59 (the syntax will be "progress : ∀{t τ} → t :: τ → (∃ \lambda t' -> t ⟶ t') ∨ Value t") 28/02 23:01 hmm, is there something I can read to learn about existentials in agda/dependent-types 28/02 23:03 mh, the tutorials on the wiki should have some introduction 28/02 23:05 I don't know anything about dependant type theory, is that somehow related to sigma pi types? 28/02 23:06 however in constructive logic, a proof of exists a : A. B a, is a pair of and element of type A and a proof that B holds for a 28/02 23:06 this is what's called a sigma type 28/02 23:07 data Sigma (A : Set) (B : A -> Set) : Set where _,_ : (a : A) -> (B a) -> Sigma A B 28/02 23:07 then ∃ is just a synonym where the A argument is implicit 28/02 23:08 the symbol Sigma is used because the existential quantifier can be seen as a generalization of the \/ connective, also denoted + 28/02 23:09 instead of having only two possible cases, you have one for every element of A 28/02 23:10 and then it holds for at least one of those? 28/02 23:10 because you just have to find *some* B a to construct sigma? 28/02 23:11 yeah, a value of Sigma A B is a proof that there's at least one (a : A) for which B a holds 28/02 23:11 right 28/02 23:12 ah, that's quite helpful, thanks again 28/02 23:13 e.g. data IsEven : Nat -> Set where evenz : IsEven zero; evenss : forall {n} -> IsEven n -> IsEven (suc (suc n)); 2isEven : Sigma Nat IsEven; 2isEven = suc (suc zero) , evenss evenz 28/02 23:14 well, 2isEven is not a great name 28/02 23:15 "some-n-is-even" 28/02 23:15 you'd have "2isEven : IsEven (suc (suc zero))" 28/02 23:16