copumpkin copumpkin glguy --- Log opened Sat May 01 00:00:15 2010 I am NOT a fan of listservs sending me my password in plaintext 01/05 04:11 including the chalmers agda one 01/05 04:11 * glguy solicits feedback on http://www.galois.com/~emertens/treerec/preorder.html 01/05 06:50 I'm trying to document this portion of the Tree stuff I've been doing so that someone else could use it as an example in the future 01/05 06:50 or at least the w.f. induction part 01/05 06:51 * Saizan didn't realize records aren't checked for positivity 01/05 06:53 glguy: I found it fairly easy to understand what was going on. The wording of "'preOrder's helper function's relationship to the specification" in the same' description seemed a little awkward to me though, had to read it a few times to figure out what was meant. In case it matters, I only have a very very basic understanding of well founded recursion and have never tried using it before. 01/05 07:16 OK, I'll have to try to clear up that language 01/05 07:18 I wanted to write "I needed this to prove the next thing" :) 01/05 07:18 I'd try swapping the word order, "we must first prove the relationship between preOrder's helper function and the specification" 01/05 07:19 better? 01/05 07:23 yep 01/05 07:24 thanks for reading through it 01/05 07:26 your welcome 01/05 07:26 * glguy learns a new operator from the stdlib: same : preOrder ≗ spec 01/05 08:42 * Saizan wants hoogle for agda 01/05 08:48 is that just (f g : A -> B) (x : A) -> f x \== g x ? 01/05 08:49 "\lambda f g -> forall x -> f x \== g x" 01/05 08:50 It is (f g : A -> B) -> Set 01/05 08:57 and equals forall t -> f t == g t 01/05 08:57 Saizan: If you're still there, check out preOrder' implemented using all of the various type synonyms used in the Induction module... http://www.galois.com/~emertens/treerec/preorder2.html#4660 01/05 09:00 look ma', no arrows 01/05 09:00 heh :) 01/05 09:01 I want to think that with enough familiarity of these operators that they actually make the meaning clearer... 01/05 09:02 "Universal Sig" doesn't feel quite right given that Sig ignores its argument 01/05 09:07 i like ⊆′ though 01/05 09:07 that makes it particularly universal! 01/05 09:08 not much of a property though :) 01/05 09:09 (and looking more at it the use of ⊆′ has the same problem, i just felt more familiar with it) 01/05 09:09 well, the argument isn't as ignored in the sub=' case 01/05 09:15 due to the <-Rec 01/05 09:15 * glguy sets out to write a proof inthat file that makes use of the argument to the predicate 01/05 09:19 Saizan: head to the bottom of that page http://www.galois.com/~emertens/treerec/preorder2.html#4660 01/05 09:32 sure the structure of the proof is basically identical 01/05 09:33 but the predicate is more interesting :) 01/05 09:33 true :) 01/05 09:36 * Saizan wonders if one could come up with a sensible name for P 01/05 09:37 Does it help to look at it like P = λ ts → ∀ xs ys → preOrder′ ts (xs ++ ys) ≡ preOrder′ ts xs ++ ys 01/05 09:37 (seems to help put ts xs and ys on the same playing field 01/05 09:38 yeah, it's quite less noisy like that 01/05 09:47 Well, I could fiddle with this all night, but I need to get some sleep 01/05 09:51 good night 01/05 09:51 --- Day changed Sun May 02 2010 I'm getting an error about not being able to instantiate a metavariable because it can't depend on something 02/05 01:18 I'm unfamiliar with the theory of dependant types so it's rather nonsensical to me 02/05 01:18 it's just what you'd imagine 02/05 01:21 there's a hidden variable somewhere that needs a value (from (type) inference) 02/05 01:21 you can use  instantiate (3 := x)  but there's usually a different way to have ti cleared 02/05 01:22 ok, I'll try splitting some stuff up maybe 02/05 01:22 I'm able to write what I expect as it's own function 02/05 01:23 fax: I've been trying to write up a subset of the preorder stuff for a blog post or something. Maybe it will help someone else (sorry if you've already seen the new commented version) http://www.galois.com/~emertens/treerec/preorder.html 02/05 01:33 If you have any ideas for how to make it easier to understand let me know 02/05 01:33 oh shit this is #agda 02/05 01:34 I thought it was #coq 02/05 01:34 lpjhjdh lol sorry just ignore what I said it's completely wrong 02/05 01:34 hah, no worries, I'm just mindlessly shuffling things around to see if I can get things more readable 02/05 01:36 lpjhjdh: How big is the code? 02/05 01:37 maybe if I post the problem that would be helpful 02/05 01:38 not large 02/05 01:38 Paste it somewhere. 02/05 01:38 now that moved things it's one line 02/05 01:38 glguy_: this is great that will be very useful for people that don'tknow how to use well founded relations 02/05 01:38 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25272#a25272 02/05 01:39 Wow. 02/05 01:40 oh yeah, and weaken : ∀{x}{φ₁ φ₂} → x ∷ φ₁ ⊆ φ₂ → φ₁ ⊆ φ₂ 02/05 01:40 What line causes the error? The 'no' line? 02/05 01:40 yeah, and it's underlining x∷φ₁⊆φ₂ 02/05 01:40 I uncluttered the error a bit 02/05 01:43 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25272#a25273 02/05 01:43 any notion of what's going? 02/05 01:46 Well, metavariables have nothing to do with dependent type theory directly. 02/05 01:47 It has to do with Agda's ability to infer things if you put down a _, or use implicit arguments. 02/05 01:47 ah 02/05 01:48 When you do that, it fills the spot with a 'metavariable', and runs a unification algorithm trying to figure out what should go in there. 02/05 01:48 So, it's unhappy with some implicit argument, but I'm not sure which one. 02/05 01:49 Is that lemma even going to be true? 02/05 01:49 How will you decide if x was in φ₂ 02/05 01:49 I was thinking any (_≟_ x) φ₂ 02/05 01:50 glguy_: x is from (and the phis hold elements from) a decidable setoid, it looks like. 02/05 01:50 yeah... I see the DecSetoid now :) 02/05 01:51 I think the only other implicit var there is from φ₁⊈φ₂ 02/05 01:53 lpjhjdh: It looks like the problem is that it somewhere thinks there's an x' happening, when you want it to be x. 02/05 01:53 ah, yeah, it's calling the implicit var in φ₁⊈φ₂ x' 02/05 01:53 If you want the two phis to have the same type you'll have to name it 02/05 01:57 unless your sub= operator isn't polymorphic in some list type 02/05 01:57 e.g. you can't have forall xs ys. where you need: (A : Set) (xs ys : List A) 02/05 01:58 hm, just use a lambda then? 02/05 01:59 what type did you expect the two phis to have? 02/05 01:59 List DecSetoid.Carrier 02/05 01:59 is sub= defined as  List Carrier -> List Carrier -> Set? 02/05 02:00 _⊆_ : List A → List A → Set with A being from D.setoid 02/05 02:01 Is the DecSetoid picked as a module parameter? 02/05 02:02 yeah 02/05 02:02 oh, then this probably shouldn't matter 02/05 02:02 but you might try explicitly giving the types instead of using the forall shortcut 02/05 02:03 ah, I'll give that a shot, thanks 02/05 02:03 hmm, still having the issue 02/05 02:05 boo :) 02/05 02:05 I was hoping to use the subset from Data.List.Any but maybe I'll try making everything explicit 02/05 02:05 that worked 02/05 02:11 so xs ⊑ ys = (x : A) → x ∈ xs → x ∈ ys works but xs ⊆ ys = {x : A} → x ∈ xs → x ∈ ys doesn't 02/05 02:12 how do you do substitution with equality from a setoid? 02/05 02:31 I think you'd need a proof that the function/predicate/whatever respects the setoid. 02/05 02:35 In which case it's trivial. 02/05 02:35 okay, I was wondering what respects was 02/05 02:36 could you help me understand this signature?  Substitutive : ∀ {a ℓ₁} {A : Set a} → Rel A ℓ₁ → (ℓ₂ : Level) → Set _ 02/05 02:42 The 'a' and the ells are for universe polymorphism. 02/05 02:46 So that you can have Substitutive that works at multiple different levels. 02/05 02:48 Instead of just working on, say, Set. 02/05 02:48 okay 02/05 02:49 can any function be made to use universe polymorphism? 02/05 03:11 More or less. Universe polymorphism in agda is accomplished by having Set be an indexed type (by Level), with ordinary pi types. 02/05 03:15 so maybe one could infer the universe? 02/05 03:16 I'm not sure what you mean by that. 02/05 03:18 If you want to make an apple pie, first you must infer the universe 02/05 03:21 Proof time! 02/05 03:30 Here's a statement: "If two rational numbers a/b and c/d differ by 1/bd, then of all the rational numbers between them, the one with the lowest denominator is (a+c)/(b+d)." 02/05 03:31 It's a reasonably well-known theorem (or maybe I made a mistake and it's false), and I feel like writing up a proof of it in Agda. 02/05 03:32 Wish me luck! 02/05 03:32 Good luck. I suspect you'll need it. 02/05 03:36 Well, I can't say this is going very well. 02/05 03:57 Upon trying to open an Agda file with Emacs, I get this: File mode specification error: (file-error "Cannot open load file" "haskell-indent") 02/05 03:57 This is on a Mac. 02/05 03:58 Did you install Haskell-mode? 02/05 04:10 Yes. 02/05 04:10 I added this to my .emacs and haven't had problems since http://fpaste.org/n9Fe/ 02/05 04:12 but if you've already done that I won't be able to help you 02/05 04:12 Hmm, /opt/local/share/emacs/site-lisp/haskell-mode-2.4 doesn't exist. 02/05 04:26 Maybe I installed it wrong somehow. 02/05 04:26 I installed it through macports 02/05 04:29 You installed Agda through MacPorts? 02/05 04:30 no, haskell-mode 02/05 04:31 You have to install haskell-mode separately 02/05 04:31 Oh, I was confusing agda-mode with haskell-mode.  I have the former but not the latter. 02/05 04:32 "sudo port install haskell-mode" tells me that that doesn't exist. 02/05 04:33 then that isn't the name of the port 02/05 04:37 Well, that's too bad. 02/05 04:37 So I have an odd question... 02/05 04:42 There are a number of things which seem obvious/nice to have, but which are actually problematic (e.g., injective constructors, surjective pairing). Is there a good listing/summary of such things somewhere? 02/05 04:42 ...or good examples of where they conflict with other dependent typing features? 02/05 04:45 Surjective pairing is eta equality of pairs? 02/05 04:56 surjective_pair : (p:A*B) -> (fst p, snd p) = p 02/05 04:56 ...or equivalent 02/05 04:57 dolio (equivalent to proof irrelevance) 02/05 04:57 (fst p, snd p) = p looks correct. 02/05 04:58 Is there something wrong with it? 02/05 04:58 It's equivalent to proof irrelevance? 02/05 04:58 I'm also curious about why eta conversion and extensional equality of functions (i.e., (forall x, f x = g x) -> f = g) are problematic (they're problematic in Coq at least, but I don't know whether that's a Coq-ism or a deeper issue) 02/05 04:58 dolio: axiom K 02/05 04:59 uorygl: The more problematic version is at the type level IIRC: (P: Sigma(x:A).B) -> Sigma(x: proj1 P).(proj2 P) = P. 02/05 04:59 Huh. 02/05 05:00 Again, I'm not entirely sure of the details, which is why I'm searching for a good overview of metatheoretic design issues for dependent types. 02/05 05:01 Where did I leave off? 02/05 05:02 nothing 02/05 05:03 Making definitional equality extensional is problematic because you lose things like decidability of type checking. 02/05 05:03 If you have x : ... f ..., and you want to know if x : ... g ... is valid, you probably need to decide f = g. 02/05 05:03 And if, to do that, you need to decide (forall x. f x = g x), well, you can't do that in general. 02/05 05:04 dolio: sure. But I'm saying that, if you can indeed prove (x:_) -> f x = g x, then why should it be problematic to derive f=g from that proof? 02/05 05:05 I'd suppose that the issue has something to do with axiom K or, equivalently, Martin-Lof vs John-Major equality 02/05 05:05 If we're talking an equality type, then the reason is that in Coq, the equality type is defined to reify the definitional equality. 02/05 05:06 So Id A x y is inhabited only when x = y is definitionally true. 02/05 05:07 OTT, by contrast, has an equality type that isn't linked to the definitional equality used in type checking. 02/05 05:08 koninkje - what is meant by 'problematic' 02/05 05:08 So you get extensional equality in the equality type, but intensional equality for type checking. 02/05 05:08 fax: introduces inconsistency to the system (e.g. injective constructors + impredicativity), etc. 02/05 05:09 koninkje: neither of these do 02/05 05:09 fax: Or, for another concrete example, makes case elimination not have the nice properties we would like 02/05 05:09 fax: Or reders type checking/inference significantly harder, etc 02/05 05:10 s/reders/renders/ 02/05 05:10 have you read simply easy? 02/05 05:10 Yeah, though it's been a while 02/05 05:11 they have revised it a couple times 02/05 05:11 Is K usually considered proof irrelevance? I know you can use proof irrelevance to get K, but Agda has K without proof irrelevance. 02/05 05:11 dolio: they're all equivalent in terms of provability -- (but we really want to have the definitional equality of course..) 02/05 05:11 If I understand correctly K is heterogeneous equality (or equivalently a stronger eliminator for [homogeneous] equality of existential types) 02/05 05:14 K states that every proof of x = x is refl. 02/05 05:14 fax: as I recall, Simply Easy is only dealing with an LF- or ITT-like system rather than CC-like (where new issues are raised) 02/05 05:16 ...though, as I said, it's been a while 02/05 05:16 oh well id on't know what the difference are 02/05 05:16 K : (A : Set) (x : A) (P : (x = x) -> Set) (eq : x = x) -> P refl -> P eq 02/05 05:17 http://github.com/larrytheliquid/Lemmachine 02/05 05:18 this is a good idea 02/05 05:18 fax: in LF you have Pi instead of arrow, and as you move towards ITT you add Sigma and the like. Overall, things are still well-behaved, just with dependency added in. Whereas in CC you get Prop 02/05 05:19 what's arrow? 02/05 05:19 The normal notation for the type of functions in non-dependent languages (e.g. simply typed, System F,...) 02/05 05:20 When you only have Pi, terms can be used to index types, but terms cannot *be* types themselves. Once you add Prop to the mix, then terms can indeed be types themselves 02/05 05:21 really?? how? 02/05 05:21 For example, the "lambda" or forall quantifier of terms in Prop reifies the Pi at the type level 02/05 05:21 But if we do the obvious thing to have an exists quantifier which reflects Sigma, then the system becomes inconsistent 02/05 05:22 I am not really understanding this 02/05 05:22 SO we have our normal lambdas right? 02/05 05:23 I think of lambda and forall as different things 02/05 05:23 The type of a lambda is a Pi:  lambda (x:A).e:B :: Pi(x:A).B 02/05 05:24 okay 02/05 05:24 And we have the type of Pi is Set (or *, or some other atomic name):  Pi(x:A).B :: Set 02/05 05:24 Now, over in the Prop side of things we have something analogous to lambda 02/05 05:25 Some people just call it "lambda" ---which leads to all sorts of confusion--- other people call it "forall" 02/05 05:25 Notably, this is not the same thing as the forall in System F 02/05 05:26 So we can ask, what is the type of forall? 02/05 05:26 what confusion does it lead to? 02/05 05:26 calling it forall is confusing me 02/05 05:26 and the wierd thing is we get: forall(x:Prop).e:Prop :: Prop 02/05 05:26 Well, a lambda constructs a function and has   Pi for a type (which is non-atomic and gives the types of the input and output of the function) 02/05 05:27 Whereas forall/lambda is a constructor of propositions and just has the atomic type Prop 02/05 05:28 urgh this does not make sense 02/05 05:28 I've never seen "forall" used as an analogue to lambda for prop. 02/05 05:28 It's usually the analogue of pi. 02/05 05:29 dolio: That's the notation used in ATTPL 02/05 05:30 I think that's the only way forall(x:Prop).e:Prop : Prop makes sense, too. 02/05 05:30 I have read ATTPL and I don't know this notation :P 02/05 05:30 Pi(x:A).B:Set : Set 02/05 05:30 Well they say "all" instead of "forall" but it's the same difference 02/05 05:30 I woulh just use Pi for everything 02/05 05:31 then you can describe it with PTS 02/05 05:31 But there is a difference between Pi as describing a class of terms (namely lambdas) vs Pi/forall as a term itself 02/05 05:31 but terms and types are in the same syntactic category 02/05 05:31 In PTS they use lambda 02/05 05:31 But they are ontologically distinct 02/05 05:32 The only reason they're in the same syntactic category is because people are lazy about distinguishing the term and type grammars 02/05 05:32 (for obvious reasons) 02/05 05:32 in the presentations of PTSs that I have seen, we have Lambda and Pi 02/05 05:32 Yes, but the constructors of propositions are written with lambda in the PTSes I've seen 02/05 05:33 it's true you could use the same token for both (like use lambda everywhere) -- but that's insane 02/05 05:33 indeed 02/05 05:33 Also, it introduces confusion in higher-order languages since type-level lambda is not the same thing as Pi 02/05 05:34 http://www.cs.ru.nl/~freek/aut/aut.pdf 02/05 05:35 "We will brieﬂy discuss the lack of popularity in the type theoretic 02/05 05:35 community of the λ-typed type theories in Section 7.2 below." 02/05 05:35 Most people also don't distinguish terms as types vs terms as terms, whereas ATTPL does by using "pf" or "prf" type constructors 02/05 05:36 I think they did that to try and make it easier for beginners to understand -- it seems needless to me 02/05 05:37 Are you talking about meta-level pi in the logical framework versus object-level forall? 02/05 05:39 Because there can be an object-level pi, as well. 02/05 05:39 dolio: type-level pi vs term-level forall, yes. The latter could be considered a term-level pi, though there are reasons to avoid that notation 02/05 05:40 I mean there can be an object-level pi in addition to the object-level forall for props, but they're both different from meta-level pi. 02/05 05:41 (namely to retain a notion of distinguishing terms from types, which is possible, though most folks have abandoned doing so) 02/05 05:41 What do you mean by object-level pi (as distinct from object-level forall)? 02/05 05:41 Let me look something up to make sure I get this right... 02/05 05:42 do you mean the standard distinction between object and meta, or are you just meaning term vs type? 02/05 05:42 Okay, in UTT, Luo specifies Prop in the logical framework like so: 02/05 05:43 (because both term and type are object-level) 02/05 05:43 * koninkje really should read some of Luo's work 02/05 05:44 Prop : Type, Prf : (Prop)Type, forall : (A : Type) ((A)Prop)Prop, /\ : (A:Type)(P:(A)Prop)((x:A)Prf(P(x)))Prf(forall(A,P)) ... 02/05 05:44 He also defines: Pi : (A:Type)((A)Type)Type, \ : (A:Type)(B:(A)Type)((x:A)B(x)) Pi(A,B) 02/05 05:45 That's Pi in the object language he's defining. Just like Prop is part of the object language being defined. 02/05 05:46 I assume (Prop)Type is his notation for Prop->Type ? 02/05 05:46 Yes. His notation for LF uses (x:A)B for pi types, and (A)B if x isn't used. 02/05 05:46 * koninkje nods 02/05 05:47 There's also eliminators for both of those, but I don't feel like typing them. 02/05 05:48 I think Agda 1 was similar to that. 02/05 05:48 Sure. So he's just distinguishing them based on Prop vs Type, and the distinction could be collapsed if sorts were introduced? 02/05 05:49 i.e. Sort={Type,Prop,...} and foo : (S:Sort)(A:S)((a:A)S)S 02/05 05:50 Though sorts may best be left as a metatheoretic device rather than actually incorporated into the object language 02/05 05:51 The object language he's defining is similar to Coq. 02/05 05:51 you know the best book is 02/05 05:52 folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf 02/05 05:52 There's a Prop universe and a Set universe (later he gets around to having a hierarchy of universes), and Prop is impredicative, but Set isn't. 02/05 05:52 dolio: sure. (Similarly, Coq's three induction/recursion functions for inductive datatypes could be collapsed into a single one if sorts were first-class) 02/05 05:53 what do you mean first-class 02/05 05:53 dolio: so it's like pCIC then? 02/05 05:53 You can actually do this kind of stuff in Agda, since it has induction-recursion, except you can't define impredicative prop, because it's a negative type. 02/05 05:54 What's the p stand for there? 02/05 05:54 fax: I mean if sorts were actually part of Coq (the object language) instead of merely in the metatheory describing Coq 02/05 05:54 koninkje: aren't they ? 02/05 05:54 I mean the sorts are {Prop,Type[0],Type[1],...} 02/05 05:55 and they all have types 02/05 05:55 Well, Prop, Type[0], Type[1] etc are all in Coq 02/05 05:55 But there's nothing which comprises all of those elements 02/05 05:55 The LF methodology is to have Prop : Sort, Type[0] : Sort, etc. 02/05 05:55 I.e. I can't quantify over {Prop,Type[0],...} 02/05 05:55 ah 02/05 05:56 you can quantify over Type though 02/05 05:56 And then you have prop : Type[0], and El prop = Prop, or something like that. 02/05 05:56 hm 02/05 05:56 That way you can meta-quantify over all universes. 02/05 05:57 All universes in the object-language. 02/05 05:57 Then how come universe polymorphism is so esoteric? 02/05 05:58 e.g. why doesn't Coq just define a single inductive/recursive principle for wach data type? 02/05 05:58 Because no one likes programming with the LF and Tarski-style universes. :) 02/05 05:58 heh :) 02/05 05:59 http://i.imgur.com/1qOPB.png here are the rules for lambda-cube 02/05 05:59 well these are the rules: http://i.imgur.com/z9NIS.png 02/05 05:59 Anyhow, if you look at some Agda 1 code, one of the things that gets done right away is defining object-level Pi. 02/05 06:01 http://www.dcs.ed.ac.uk/home/pgh/amenities.agda 02/05 06:05 universe polymorphism is marked "experiemental" and I've seen it said on the mailing list that it is subject to change 02/05 07:45 What aspects of it are unfinished and eligible for major change? 02/05 07:45 it seems pretty straight-forward from the uninformed point of view 02/05 07:46 maybe how the levels are represented? 02/05 07:48 * glguy_ switches computes 02/05 07:49 Why does Rel operate at an arbitrary level? 02/05 07:54 when would I want Set 0 -> Set 0 -> Set 10, for example? 02/05 07:55 I guess because the resulting set was already going to be based on some Set 9? 02/05 07:55 yeah 02/05 08:09 Is there a practical example where a program uses more than about Set 2? 02/05 08:25 pratical examples? in my Agda? :) 02/05 08:27 * Saizan doesn't know 02/05 08:27 Do you know where the rules for what level something is in are written down? 02/05 08:35 no, but in that thread Nils pointed to the release notes, iirc 02/05 08:36 ok 02/05 08:36 * glguy switches network interfaces 02/05 08:36 Are "inductive families" specifically the data types that use indexes?  data A B : THIS -> STUFF -> Set where ? 02/05 09:00 as opposed to only parametrization? i think so but i'm not sure 02/05 09:02 I'm trying to find the maximal element in a list so I first made a datatype MaxIn indexed by a max, a list, and a proof that it really is a max.  I was then going to rebuild an input list as a MaxIn 02/05 09:17 but it's proving kind of cumbersome, is this a bad approach? 02/05 09:17 I wrote MaxIn just find, it's the rebuilding that's goofy 02/05 09:17 fine* 02/05 09:17 how does MaxIn look like? 02/05 09:18 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25283#a25283 02/05 09:19 i don't think i'd have (∀ y → y ∈ xs → y ≤ m) as an index, maybe as a field, but i think it should be derivable from the rest 02/05 09:20 ah, that makes sense, thanks 02/05 09:21 so do you mean I could write: findMaximal : {m : Nat}{xs : List Nat} -> MaxIn m xs -> forall y -> y in xs -> y <= m 02/05 09:24 hmm, maybe I won't actually need the MaxIn, just the lemmas I wrote to give the proofs of an element's maximality 02/05 09:26 yeah, i meant that 02/05 09:28 Interesting, in the darcs version of the standard lib, \ex is the type of the dependent pair and \Sigma is just a convenient wrapper 02/05 09:32 i guess someone was tired of seeing the extra type parameter in normalized types?:) 02/05 09:34 it seems like it means that the goals are just that much less helpful 02/05 09:37 you get to guess what the first type was 02/05 09:38 suppose you have: val : A × Set \n val = ? 02/05 09:39 Goal: ∃ (λ _ → Set) 02/05 09:39 right 02/05 09:39 but you can turn on the display of implicit parameters 02/05 09:39 or you can type ? , ? 02/05 09:39 there might have been a value that had that tuple type yo ucould have used 02/05 09:40 sure 02/05 09:41 the extra type argument didn't bother me, so i'd probably prefer Sigma as the real type too, unless there's some other reason 02/05 09:43 glguy: Universe polymorphism isn't necessarily useful in practice because things need to work at very high universes. 02/05 19:30 But it isn't uncommon to want, say, List Set, and defining a List1 in addition to List isn't a great solution. 02/05 19:31 And yes, inductive families are indexed data definitions. They allow you to define a whole family of types T x at once, inductively. The family as a whole is closed, inductively, under the constructors. 02/05 19:45 * pigworker is experimenting with this IRC client. 02/05 20:58 pigworker: So, in OTT, is there any kind of distinction between propositional false and the empty set, such that the former doesn't entail arbitrary computational sets (if you take my meaning)? 02/05 21:01 IIUC you're asking whether the false Prop eliminates over Set or not; the false Prop does eliminate over Set 02/05 21:03 Yeah, I suppose that's what I'm asking. 02/05 21:03 I've been thinking off and on about the EPTS stuff, with regard to erasibility in inductives... 02/05 21:04 And it occurred to me that given the definition of Squash in Mishra-Linger's thesis, and its eliminator, I don't think you can prove Squash 0 -> 0. 02/05 21:05 Or Squash 0 -> A for arbitrary A. 02/05 21:05 Only Squash 0 -> Squash A. 02/05 21:05 So in a sense, you can't prove that Squash 0 is uninhabited, assuming you take that to mean that it entails the empty set. 02/05 21:07 no escape from Squash, huh? even stronger than double negation! 02/05 21:08 Actually, it depends. 02/05 21:09 * pigworker has just found an annoying bug/feature in Agda's implicit syntax machinery 02/05 21:09 He has a section on the elimination rule for 0, in which he mentions that you can make its type elim_0 : (P : 0 -> Set) => (z : 0) => P z, => being irrelevant pi... 02/05 21:10 If that's the elimination rule, then you can prove Squash 0 -> 0 02/05 21:11 However, there are problems with that rule. 02/05 21:11 If elim_0 : (P : 0 -> Set) => (z : 0) -> P z, then you can't escape from Squash. 02/05 21:12 (I think.) 02/05 21:13 So the idea is that irrelevant application can unpack Squash? 02/05 21:13 Squash 0. 02/05 21:15 Or, in general, yes, I suppose. 02/05 21:15 Because Squash holds something irrelevant, so you can only use it in irrelevant spots. 02/05 21:15 elim_Squash : (A : Set) => (t : Squash A) -> (P : Squash a -> Set) => ((x : A) => P (poof @A @x)) -> P t 02/05 21:17 So, specialized to 0, you have to provide: f : (z : 0) => 0, but I don't think you can write such a term. 02/05 21:18 He refers to the irrelevant 0 elimination as 'empty type target erasure', if that means anything to you. Evidently it can lead to normalization of erased terms getting stuck on elim_0. 02/05 21:23 I'd be suspicious of (x : 0) => 0 if irrelevance-erasure is performed before computing *open* terms 02/05 21:24 (x : 0) => 0 is actually equivalent in some sense to Squash 0 -> 0. 02/05 21:26 In that A => B is equivalent to Squash A -> B in the non-dependent pi case. 02/05 21:27 I suppose (x : 0) => 0 is rather obviously suspect, because it would have to erase to M : 0, plus an application of generalization. 02/05 21:31 And there should be no closed term with type 0. 02/05 21:31 But if the 0 argument to elim_0 is irrelevant, then elim_0 is just such a term, in a sense. 02/05 21:33 This is the kind of issue which makes run-time erasure mechanisms fit badly with proof erasure. 02/05 21:42 Yeah. 02/05 21:43 More precisely, in open terms, there are proofs it's ok to *identify* but not to *erase*. 02/05 21:46 * pigworker has just mailed the Agda list with some trouble. 02/05 21:48 I've been worried for some time that Agda's implicit syntax machinery is suspiciously clever. It turns out that sometimes it's also suspiciously stupid. 02/05 21:57 Heh. 02/05 21:58 I recall being in situations where I could enter things from a shed that wouldn't subsequently check. I wonder if it's related to this. 02/05 21:58 My guess is that it tries to solve (f a b) = (f a' b') by solving a=a' and b=b', even when f is defined and not necessarily injective. 02/05 21:59 I think I encountered such issues as well. But this was quite some time ago, and clearly a bug. I think your issue is somewhat more tricky. 02/05 21:59 http://code.google.com/p/agda/issues/detail?id=212 02/05 22:00 hi kosmikus 02/05 22:00 If unification makes unforced moves, it becomes dependent on the order in which constraints come up. One symptom of such a dependency is phantom refinements. 02/05 22:00 hi fax 02/05 22:01 That got merged with 118, of course, which has lots of other examples. 02/05 22:01 yes, that bug report looks familiar 02/05 22:02 dolio: That's a different problem to the one I'm raising. 02/05 22:04 Okay. 02/05 22:04 Moreover, that's not a Dybjer-Setzer IR definition. level should not be in scope when declaring type 02/05 22:05 IR definitions are least fixpoints of endofunctors on Sigma Set \ S -> D for some decoder type D (often Set). When you declare a constructor, you may decode only its recursive arguments. Agda doesn't quite see it that way. 02/05 22:08 Huh, apparently you can circumvent the positivity checker using this bug. 02/05 22:11 118, that is. 02/05 22:11 I've never proved false 02/05 22:12 :( 02/05 22:12 118 looks like definitions arriving too late to save a postponed constraint; lack of such-and-such-checking on refinement is surely a different problem. 02/05 22:15 hi guys, any suggestions on how one might go about merging the three datatypes here: http://web.student.chalmers.se/~stevan/csallp/html/Formulas.html into one? here is a failed attempt: http://patch-tag.com/r/stevan/csallp/snapshot/current/content/raw/prototype/UlfDataTypes.agda . thanks. 02/05 22:38 since you've a fixed set of labels you could use the naive encoding of row types 02/05 22:47 probably not the most idiomatic way 02/05 22:48 row types? 02/05 22:49 it's a form of subtyping 02/05 22:55 since basically NQF <: QF <: Fm there 02/05 22:56 stevan:  You can make dnf work by doing case analysis on t1 and t2, but it won't be pleasant. 02/05 22:57 At least, I think you should be able to. 02/05 22:57 yeah, that would work 02/05 22:58 * Saizan tries to remember how the row types encoding worked 02/05 22:59 At least, examining t1 and t2 should lead to contradictions of some kind when they're not nqf. 02/05 23:01 Might be hard to set up. 02/05 23:02 another option is to push constraints down rather than calculating the type of the result 02/05 23:17 hmm, how do you mean push constraints down? 02/05 23:20 so whats new 02/05 23:21 * pigworker reads logs; has gone brown; poetic justice? 02/05 23:29 stevan: well, take the index as a parameter and add some proof obligations inside the term 02/05 23:35 so that the Type index is always a variable in the definition of Expr and you won't have problems with unification 02/05 23:36 the obligations should be implicit arguments, and their types should be given by predicates that return \top or \bot , since a value of type \top can be inferred 02/05 23:37 that's my random thought anyway :) 02/05 23:37 ah ok, i think i see what you mean now 02/05 23:40 --- Day changed Mon May 03 2010 i can't find anything on row types, you don't happen to have an url or something, Saizan ? 03/05 00:04 Look for papers by Daan Leijen or Simon Peyton-Jones on extensible records. 03/05 00:55 thanks 03/05 00:59 when is agda unable to solve some constraint? 03/05 03:26 in a pattern match 03/05 03:26 agda is saying .r != r, doesn't the . mean that the term is precisely r? 03/05 05:17 .r is probably an implicit variable somewhere 03/05 05:18 it is, I see now when I try to name it, it won't admit .r 03/05 05:19 :( 03/05 05:19 That’s saying the same thing 03/05 05:20 so I've been trying to write a typechecker for the lambda calculus with essentially references using an effect system and have hit a bit of trouble while trying to extend a context and was hoping someone might be able to enlighten me 03/05 17:31 the typing rule for a lambda abstraction extends the body expression's context by mapping its introduced variable to a type and a region 03/05 17:32 but I don't have a rule for selecting regions so I can't prove they will be the same for equal expressions 03/05 17:32 or at least that is what I believe to be the issue 03/05 17:32 is there an object anyone could recommend that gives a precise rule for selecting unique names? 03/05 17:33 halp. I don't understand corecursion. :( 03/05 22:07 And hpaste doesn't seem to work. D: 03/05 22:08 See here: http://pastebin.com/EVSLxkfq 03/05 22:10 How exactly does the productivity checker work anyway? Both ∶D and D∶ are guarded as far as I can see. 03/05 22:11 id is in the way I think 03/05 22:15 that's an interesting CoNat :P 03/05 22:16 would D∶ = suc (id (♯ D∶)) pass the checker? 03/05 22:17 copumpkin: I don't understand what ‘in the way’ means here. 03/05 22:19 Saizan: I don't think so 03/05 22:20 liyang: there's some rule about there only being "constructors" around recursive calls 03/05 22:20 I don't really know the details or why it's implemented that way 03/05 22:21 Saizan: yeah, it doesn't pass 03/05 22:21 an arbitrary function could force too much of the recursive call 03/05 22:22 http://snapplr.com/xfkw 03/05 22:22 though i hope there's room for improvement in the productivity checker 03/05 22:23 maybe with some laziness analysis :) 03/05 22:23 it seems like it should be able to see through my example 03/05 22:23 Saizan: it's still the wrong colour. :( 03/05 22:23 liyang: it's really annoying sometimes... when I did a naive translation of luqui's control-monad-omega to agda, I had to write a mini "language" in an ADT in agda, along with an interpreter for it 03/05 22:25 which complicated the proof of the function so much that I was unable to complete it :P 03/05 22:25 (because I needed my recursive terms to be constructors of some type) 03/05 22:26 i wonder if you the anamorphisms pass the productivity checker, in general 03/05 22:27 s/you// 03/05 22:27 What do you mean in general? 03/05 22:27 The problem with D: is that it's not directly guarded by constructors, I believe. 03/05 22:29 Agda's checker actually admits things that the usual categorical theory wouldn't. 03/05 22:31 dolio: which D: do you mean? 03/05 22:31 i mean if for every coinductive type you define you can also define the corresponding unfold 03/05 22:31 For instance, it makes no sense, purely from a coalgebra perspective, for sticking the non-recursive ∞ around recursive arguments to turn it into a greatest-fixed point. 03/05 22:32 Saizan: You can do that, I think. 03/05 22:32 liyang: Actually, your D: works here. 03/05 22:35 Wait, I'm wrong. 03/05 22:36 I typed :D instead. 03/05 22:36 wow, dolio is using smilies! 03/05 22:37 dolio: was about to ask which version you were using… 03/05 22:37 Anyhow, consider tail : U -> U ; tail (u t) = ♭ t 03/05 22:37 Then D: = u (# tail D:) 03/05 22:38 That has the same form, but it's not going to work. 03/05 22:38 *nod* 03/05 22:38 --- Day changed Tue May 04 2010 have there been any interesting recent additions to the agda std lib? 04/05 06:51 or to agda itself for that matter 04/05 06:51 I seem to have reached some sort of mutual understanding with the productivity checker. 04/05 16:37 mutual? 04/05 16:37 Not quite. There was scope for a bad pun there which I've evidently failed to take advantage of. 04/05 16:39 :J 04/05 16:39 I am still scared to touch anything coinductive 04/05 16:40 liyang: eheh, so what did you discover?:) 04/05 16:41 Yesterday I was asking about how to get around Agda not accepting e.g. inf = suc (# (id inf)) as terminating. 04/05 16:41 (hang on, fiddling with yesterday's example.) 04/05 16:43 (By turning all those function that get ‘in the way’ to constructors of an auxiliary datatype, and interpreting them later.) 04/05 17:15 I'm not sure if my example has made it any clearer. :-/ 04/05 17:15 I wonder if that can be automated 04/05 17:18 because everyone seems to be doing it 04/05 17:18 that's pretty ugly 04/05 17:20 i'd rather have some non-termination monad and a way to project values out by proving liveness 04/05 17:21 http://pastebin.com/s8gBrGUq 04/05 17:21 (Yes, it is ugly.) 04/05 17:21 (Suggestions for improvements welcome. As are comments that would help me understand exactly what it is I'm doing here.) 04/05 17:33 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14829 <- another example from copumpkin 04/05 17:34 well, the idea is sort of like implementing a lazy eval interpreter 04/05 17:36 there should be a paper on this technique 04/05 17:39 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=562 04/05 17:39 there is a lazy monad with fixed points 04/05 17:40 http://www.cs.st-andrews.ac.uk/~eb/partial.php 04/05 17:41 SK Combinator in coq 04/05 17:41 slides describing it http://www.comlab.ox.ac.uk/ralf.hinze/WG2.8/22/slides/tarmo.pdf 04/05 17:42 Computation by Prophecy  http://www.cs.nott.ac.uk/~vxc/publications/Prophecy_TLCA2007.pdf 04/05 17:43 http://www.cs.nott.ac.uk/~vxc/publications/rec_coind.v 04/05 17:44 that's the code from General Recursion via Coinductive Types http://www.cs.nott.ac.uk/~vxc/publications/Recursion_Coinductive_LMCS_2005.pdf 04/05 17:44 and https://lists.chalmers.se/pipermail/agda/2008/000667.html factorial in agda 04/05 17:45 mh, i guess "the evolution of an agda programmer" would be very weird :) 04/05 17:49 :D 04/05 17:53 Thanks, all of that's going to take me a while to digest… 04/05 17:55 So, after all that head-banging last night, and it turns out Nisse already wrote a paper about it: http://cs.nott.ac.uk/~nad/publications/danielsson-productivity.html 04/05 20:23 yeah that's where the eval stuff came form IIRC 04/05 20:24 there's also that one about an ad-hoc monolithic productivity checker 04/05 20:24 I haven't been keeping up with the literature lately. :-/ 04/05 20:26 (/That/ one?) 04/05 20:26 * fax neither 04/05 20:34 I'm not sure what you're referring to with that ad-hoc monolithic productivity checker. :( 04/05 21:00 http://www.cs.nott.ac.uk/~nad/publications/danielsson-aim9-talk.pdf 04/05 21:01 http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=109 04/05 21:01 roll/unroll and fold/unfold are the same concept when talking about \mu abstraction, right? 04/05 21:46 no I don't think so 04/05 21:46 really? ok. i'll have to look closer 04/05 21:46 i don't recall having seen fold/unfold used before until i started looking at "Termination Checking with Types" by Abel 04/05 21:47 great paper on implementing recursion btw 04/05 21:48 --- Day changed Wed May 05 2010 :( trying to "load" a file containing the McCarthy 91 function causes Agda to go off into neverland 05/05 01:17 Test case failed, I guess. 05/05 01:18 How did you define the function? 05/05 01:21 I'll paste in a moment 05/05 01:52 I tried letting it run since I said that earlier 05/05 01:52 and came back to all my memory paged out 05/05 01:52 http://fpaste.org/hxkQ/ 05/05 01:55 * glguy → Home 05/05 02:02 http://www.galois.com/~emertens/rlistrec/Induction.List.html is there a simpler way to define rlistrec ? 05/05 04:36 http://www.galois.com/~emertens/rlistrec/Induction.List.html I think that this version is simpler and rlist-view will be more reusable 05/05 08:54 oh... "rlist-view" is already implemented as "Data.List.initLast" 05/05 09:31 i'm never going to be able to prove ConvergeNow (1 ∷ .Factorial.♯-0 (fibs-aux g) tt xs) (1 ∷ .Factorial.♯-2) 05/05 17:48 am i? 05/05 17:48 why not?? 05/05 17:48 data ConvergeNow {a : Set} (x : a) : a -> Set where 05/05 17:48 converge-now : ConvergeNow x x 05/05 17:48 well, because i've no clue on how to handle those .Factorial.#-n 05/05 17:49 are they convertible to something i can refer to? 05/05 17:49 i can give you more of the definitions if that helps 05/05 17:50 well I like to look at stuff but you should know I have never done anything with codata and I have no idea about it 05/05 17:51 so I am not very likely to have an idea to fix it 05/05 17:51 or finish 05/05 17:51 Saizan: I guess you should bisimulation instead of equality 05/05 17:52 if they are Data.Stream's I sugest Data.Stream._≈_ 05/05 17:53 instead of your ConvergeNow which look the same as Relation.Binary.PropositionalEquality._≡_ 05/05 17:54 http://github.com/Saizan/partial/blob/master/Factorial.agda <- the goal is the first one in fix-fibs-ind 05/05 17:55 npouillard: oh, right 05/05 17:55 * Saizan tries to abstract the equality used from the Convergence module 05/05 17:57 Saizan: I don't think you need both \infty and codata in the definiton of D 05/05 18:00 ah, i must have missed that when i converted dolio's code to \infty 05/05 18:02 I sugest to use \infty instead of using codata 05/05 18:04 yeah, fixed that, thanks :) 05/05 18:05 * glguy doesn't understand when Agda uses the things that it learns from casing 05/05 18:19 i don't understand that completely either 05/05 18:20 why do I need to "rewrite eq" in this code to get the type of 'p' to use what was learned when casing on initLast xs?  http://www.galois.com/~emertens/rlistrec/Induction.List.html 05/05 18:21 i.e. just matching with refl won't work? 05/05 18:22 nope, the type of the refl isn't simple enough 05/05 18:22 if you were to case on the eq you'd end up with:   .(initLast xs) with-== refl 05/05 18:23 * Saizan waits for ghc to load the modules 05/05 18:27 The Induction.WellFounded.Inverse-image module is from the darcs version of the stdlib 05/05 18:27 yup, pulled that 05/05 18:32 ig euss the problem is that the need to scrutinize (initLast (ys ++ y ∷ [])) appears only after you've seen that xs is not [] 05/05 18:33 so what you'd like to be rewritten is not in the context yet when the rewriting (i.e. the matching) happens 05/05 18:34 the question is if it's feasible to keep this information around and apply it to the new context 05/05 18:35 this assuming the question was something like "why doesn't it work by just matching on (initLast xs)?" 05/05 18:37 So is what I have there the "simplest" you can write that case of body? 05/05 18:44 Oh, I think it works if I case on them the other order 05/05 18:47 OK, check out that link again 05/05 18:48 so in  "with a | b" the things we learned from casing on 'a' are used to rewrite the types of b 05/05 18:49 * glguy was just referred to Data.List.Reverse 05/05 18:53 pigworker: hi 05/05 19:06 I was trying SHE today and while the cabal install worked fine, I got trouble with the darcs repo 05/05 19:07 hi 05/05 19:07 about some missing patches... 05/05 19:07 weird; let me try a build from scratch 05/05 19:07 it was the darcs get 05/05 19:08 ... a darcs problem, more than a SHE one 05/05 19:08 maybe a call to darcs repair in the public repo 05/05 19:09 darcs get; cabal install just worked for me 05/05 19:10 oh 05/05 19:10 http://personal.cis.strath.ac.uk/~conor/pub/she <== is this the right URL 05/05 19:10 it tells that  http://personal.cis.strath.ac.uk/~conor/pub/she/_darcs/patches/20090906150800-4d78e-028efb8f8ab10771d5a6a241e44d035633bdd5a1.gz is missing 05/05 19:11 good point; I just did a pull over ssh, not http; will try again; (darcs repair sees no trouble) 05/05 19:11 I just managed to get "darcs get http://personal.cis.strath.ac.uk/~conor/pub/she" to work ok. 05/05 19:13 thanks for the clue; not sure how to chase it 05/05 19:14 * npouillard tried from another machine (with a better internet connection) and it worked 05/05 19:15 good: I just checked the public repo and that patch is present, with the same permissions as the others 05/05 19:17 So what is Nils' nick? I keep getting email answers to my questions that I ask on IRC? Is he reading logs, perhaps? 05/05 19:18 (one two many ?s) 05/05 19:18 ha, damn: too* 05/05 19:18 (and I love the email, I'm just curious) 05/05 19:19 Does Agda phone home when I make a type error, perhaps? 05/05 19:20 haha 05/05 19:20 pigworker: Is there differences between the darcs version and the one on hackage? 05/05 19:22 http://personal.cis.strath.ac.uk/~conor/pub/she/_darcs/patches/20090721161456-4d78e-cb10bcea05ecee5aed80ec015a644d0ba1bcda37.gz: HTTP response code said error) 05/05 19:22 but wget works on it 05/05 19:23 yes, the darcs one is different and much more recent 05/05 19:23 how odd: I can't see what's different about that patch 05/05 19:25 very strange maybe a darcs bug... 05/05 19:25 I don't know enough about darcs, but I do know that the public repo lives under darcs version 1. Maybe I should request an upgrade, but I prefer to avoid making work for sysadmins. 05/05 19:27 I should update the hackage version, but I've forgotten how. 05/05 19:28 Not implemented: type checking of with application 05/05 22:57 when checking that the expression :( 05/05 22:57 join #proglangtheory 05/05 23:05 A coinductive monad for prop-bounded recursion 05/05 23:07 http://www.plpv.org/plpv07/plpv07-megacz.pdf 05/05 23:07 Associat0r please _DO NOT_ do that 05/05 23:13 --- Day changed Thu May 06 2010 * glguy_ prospose a new implementation of Data.List.Reverse 06/05 07:31 http://www.galois.com/~emertens/rlist/Data.List.Reverse.html 06/05 07:31 current version: http://www.cs.nott.ac.uk/~nad/repos/lib/src/Data/List/Reverse.agda 06/05 07:31 new one was easier to reason about (for me) and is possibly easier to follow on inspection 06/05 07:32 (but that might be cause I wrote it and am more familiar) 06/05 07:32 and by reason about I mean use when proving 06/05 07:34 Saizan: you alive? 06/05 08:05 glguy_: yup 06/05 08:06 since no one else is and you just joined I'll repost http://fpaste.org/PagH/ 06/05 08:07 You don't even hvae to respond if you don't want to 06/05 08:07 At some point I'm going to have to extend the Induction.* modules to be more universe polymorphic... 06/05 08:09 * Saizan looks at the code 06/05 08:09 It has implications like the elements and relations that related them of a well-founded relation being stuck in the same level 06/05 08:10 having rev defined in a let makes it hard(impossible?) to prove reverseView-[], reverseView-∷ʳ i guess? 06/05 08:16 s/let/where/ 06/05 08:16 the [] one is there for symmetry 06/05 08:17 the ::r one isn't hard to prove but it would be tedious to have to do the "rewrites" all the time 06/05 08:18 and a bit less resiliant if the implementation ever changed 06/05 08:18 the old version was pretty opaque, for me at least 06/05 08:19 i couldn't figure out how to write the equation forms 06/05 08:20 mh, i haven't had my tea yet, they both look quite opaque to me, but i appreciate that you've splitted up in smaller lemmas 06/05 08:22 I mean "opaque" as in I could figure out how to coax out any values 06/05 08:24 couldn't 06/05 08:26 (taking care of the baby is destroying my spelling tonight... too much rushing about) 06/05 08:26 i guess i'd have to try proving something with both of those to tell 06/05 08:28 You'd just have to try to prove reverseView-∷ʳ on the old implementation 06/05 08:36 Hmm... Type checking HOAS with dependent types is tricky. 06/05 09:00 Or at least, it's looking like it's not any easier than various other methods. 06/05 09:01 glguy_: is it even possible? 06/05 09:11 Saizan: I'm not comfortable saying that it isn't possible 06/05 09:12 I wasn't able to 06/05 09:12 ah, ok, this is what i was referring to with "Saizan : having rev defined in a let makes it hard(impossible?) to prove reverseView-[], reverseView-∷ʳ i guess?" 06/05 09:13 is there a cong for Setoid's or do i have to require additional properties? 06/05 09:43 considering that you can make the rationals as a setoid over pairs i guess i do 06/05 09:44 glguy_: btw, this style of abstracting from the implementation by exposing equations feels like doing twelf in reverse 06/05 09:49 Is that good or bad or indifferent? 06/05 09:49 it's a sign that perhaps a functional logic hybrid language would be better 06/05 09:51 NAD commented the he prefers "correct by construction" to deconstructing the implementation 06/05 09:53 mh, i'm not sure i understand what that means here 06/05 09:57 rather than providing the equations that describe the program I think he liked programs that carried their properties in their results 06/05 09:57 He pointed me to Data.Nat.DivMod as an example 06/05 09:58 Whether or not his comment was actually relevant here that was the module he referred to 06/05 09:58 ok, but Reverse is already something like DivMod 06/05 10:00 extensionally there is only one way to build a value of type Reverse xs, the problem is that intensionally there are many and that gets in the way 06/05 10:01 though i guess we could make a datatype that talks about the ways you can build a Reverse xs 06/05 10:02 yikes 06/05 10:03 Does this concept have a name: (A : Set) (P : Pred A _) (i : A) (x y : P i) → x ≡ y 06/05 10:05 ? 06/05 10:05 errr 06/05 10:05 oh, right, that's what I meant. for example: A = List .B and P = Reverse 06/05 10:06 it's a well-known one, but i'm not sure if it has a name by itself, uniqueness of proof? it's related to proof irrelevance 06/05 10:08 btw, do you have an example where you need reverseView-∷ʳ ? 06/05 10:08 I've since deleted it 06/05 10:10 the module I was using it in is in flux atm 06/05 10:10 I'm playing with a predicate for lists are that "descending" wrt some _<_ 06/05 10:11 and I was using it to do:  Descending (xs ::r x) -> Descending xs 06/05 10:12 oh, ok, since it's a bit surprising that you need it 06/05 10:13 so maybe you could've done without 06/05 10:14 maybe, but in general I'm not happy with functions that I can't prove seemingly obvious things about 06/05 10:14 * Saizan tries to prove the lemma by going though (A : Set) (P : Pred A _) (i : A) (x y : P i) → x ≡ y 06/05 10:16 I have to go to bed now ,but I'll check the channel log later to hear if it worked 06/05 10:18 unique : ∀ {A : Set} {xs : List A} (x y : Reverse xs) → x ≡ y 06/05 11:23 reverseView-∷ʳ : ∀ {A : Set} xs (x : A) → reverseView (xs ∷ʳ x) ≡ xs ∶ reverseView xs ∶ʳ x 06/05 11:23 reverseView-∷ʳ xs x = unique _ _ 06/05 11:23 in retrospect it's fairly obvious 06/05 11:23 now i've to finish writing unique 06/05 11:24 glguy_: http://gist.github.com/392000 <- here it is 06/05 11:41 since i got disconnected the moment i linked it, here it is again: http://gist.github.com/392000 <- proof of the lemma for glguy_ 06/05 11:44 (i guess what i said above about extensionality/intensionality is quite bogus) 06/05 11:49 Saizan: well done 06/05 17:01 I'm going to have to learn more about heterogeneous == now 06/05 17:02 what's to know?? 06/05 17:03 how to make use of it 06/05 17:03 I haven't opened the module before today 06/05 17:04 a definition of Reverse which doesn't use ::r in the index would make the whole thing much simpler i suspect 06/05 17:05 * glguy_ heads to work 06/05 17:13 Saizan, http://www.galois.com/~emertens/rlist/Data.List.Reverse.html#2836 (yeah, same thing you did, but with more pattern matching :) ) 06/05 18:53 * glguy wanted to work through it as an exercise in using ≅ 06/05 18:56 glguy: hah, looks less painful to write :) 06/05 19:29 I didn't know about ∷ʳ-injective in Data.List.Properties before reading your code 06/05 19:30 I got pretty far reimplementing that function before I looked closely enough to see what that was 06/05 19:31 --- Day changed Fri May 07 2010 I can't find any documentation on the "constructor" syntax I've been observing in the standard library 07/05 01:56 can anyone point me to some? 07/05 01:56 That's a somewhat recently added feature for records. 07/05 01:57 It lets you specify a name for an automatically generated constructor. Previously you'd have to write a function yourself using the record { ... } syntax. 07/05 01:58 That's all it does, though. It doesn't let you pattern match with that constructor. 07/05 01:58 (At least, as far as I know.) 07/05 01:59 Thanks. 07/05 02:01 rntz, dolio: with a recent enough Agda you can pattern match too 07/05 08:40 Really? Sweet. 07/05 08:55 Saizan: By the way, you fooled around with PHOAS a while back, right? 07/05 08:58 dolio: yeah 07/05 08:59 Did you do any type checking? Or just stuff in the style of the paper, where the types are enforced by construction? 07/05 08:59 the latter 07/05 09:00 Saizan: I would be interested to look at some PHOAS code in agda too 07/05 09:01 I've been fooling with switching an interpreter I wrote to PHOAS internally (because something is wrong with the current string-variables and alpha renaming code, and I have no idea what it is)... 07/05 09:03 But type checking is proving difficult. 07/05 09:03 npouillard: http://code.haskell.org/~Saizan/SystemFpred.agda <- cast can be avoided by postulating extensional equality for functions iirc 07/05 09:04 Primarily (I think) because it uses multiple operations that each internally use different instantiations of the PHOAS. 07/05 09:05 So the operations are well defined on Term c, but the internal operations don't work on the same Term' c v. 07/05 09:05 And working with Term c directly isn't great, because it's opaque. 07/05 09:06 tried working with the different instantiations in parallel? 07/05 09:06 though Agda won't know that they agree on the structure.. 07/05 09:07 Well, I'm writing in Haskell, so that doesn't matter so much. 07/05 09:07 It's worth a shot. 07/05 09:08 Saizan: what is inj? 07/05 09:09 npouillard: it's how i inject monotypes into polytypes 07/05 09:10 Why do you need it? 07/05 09:11 to keep the type system predicative 07/05 09:11 _[_]_ : ∀ {t1 : tvar -> ty} → term (Π t1) → (t2 : type tvar ) {m : T (isMono tvar t2)} → {t1' : ty} → t1 $t2 ≡ t1' → term t1' <- here i require that t2 which is used for type instantiation is a monotype 07/05 09:13 do you plan to add a tower of universe? 07/05 09:15 inj is mostly useful to hold the proof so i can do "⌊ inj m {p} ⌋p = ↑ ⌊ m , p ⌋m" i guess. 07/05 09:17 it's been a while since i've touched this code, the ugliness of Subst scared me off i think :) 07/05 09:18 Saizan: sure, but here you are more restrictive than predicative 07/05 09:18 npouillard: ah, do you have an example? 07/05 09:19 id₁ : ∀(α : 1) α → α 07/05 09:26 id₁ = Λ(α : 1) λ(x : α) x 07/05 09:28 id₀ : ∀(α : 0) α → α 07/05 09:28 id₀ = Λ(α : 0) λ(x : α) x 07/05 09:28 id₁ [∀(α : 0) α → α] id₀ 07/05 09:29 . 07/05 09:29 ah, i see 07/05 09:29 i guess mine is predicative restricted to just one level 07/05 09:30 yes 07/05 09:31 dolio: i guess the best way is to instantiate to the product 07/05 11:38 a datatype introduces a module? 07/05 13:37 no I don't think so, a record does, though 07/05 13:37 --- Day changed Sat May 08 2010 http://www.galois.com/~emertens/doubleneg/doubleneg.html 08/05 11:44 I thought this was kind of a fun use of the PreorderReasoning module 08/05 11:44 where my relation is λ A B → A → B 08/05 11:44 cool :) 08/05 11:54 but what have you proved there? 08/05 11:56 that the first line -> the last one 08/05 11:57 that isn't necessarily interesting 08/05 11:57 I just wanted to use curry 08/05 11:57 and that notation 08/05 11:57 I'm sure that there is something interesting to be done with that notation 08/05 11:57 oh, ok then 08/05 11:59 I just hadn't though to use it for -> before 08/05 11:59 thought* 08/05 11:59 it gives a very old-school logic feeling, too bad that i can't seem to find a way to see the corresponding lambda term from that 08/05 12:02 let A (m : Nat) : Nat -> Nat ; 08/05 18:14 <= Nat.Ind m ; 08/05 18:14 = Nat.suc ; 08/05 18:14 = Iter (A xf^1) ; 08/05 18:14 root ; 08/05 18:14 from Ackermann.pig 08/05 18:14 do you understand the tactic language? 08/05 18:16 no 08/05 18:17 * Saizan neither 08/05 18:17 I think if you just try random stuff it does the right thing sometimes 08/05 18:17 I am waiting until there are enough examples that I don't have to actually figure anything out 08/05 18:18 I can just paste things together 08/05 18:18 heh 08/05 18:18 oh 08/05 18:19 and universes 08/05 18:19 UnorderedPairs.pig is realy nice too 08/05 18:20 xf^1 is the inductive hypothesis i guess 08/05 18:21 fax, Saizan, I'm told that nobody does 08/05 18:38 the xf^1 kind of names are names automatically generated by Pig, so they are ugly 08/05 18:39 automatically generated names? oh no!! 08/05 18:39 yeah... 08/05 18:39 this is a bane for back compatability in Coq 08/05 18:39 but there will be a fix, Adam is working on that 08/05 18:39 you have to sometimes go through pages of proof scripts changing everything from x to y 08/05 18:39 that's a cheap hack for us, right now. But it won't stay long 08/05 18:41 some discussions about a "high-level" language have started. So, we should be able to define functions by pattern-matching one day. 08/05 18:42 fax, List.pig is probably easier to understand. Fibo, Ackermann & co have been implemented to stress-test the unification machinery. I find myself stressed when I look at them. 08/05 18:48 hehehe 08/05 18:48 it is really exciting to see this happening! 08/05 18:49 well, thanks for your interest :-) 08/05 18:56 pedagand: btw, is there a way to dump a proof script to a file after you've completed a definition? 08/05 19:06 the elaborated term is even worse to read :) 08/05 19:06 *completed a definition interactively 08/05 19:07 you can dump the development (that is, a roughly pretty printed representation of the proof tree) but there is nothing to store the proof script 08/05 19:07 I personally use rlwrap, which stores things in an history file 08/05 19:07 I think Adam uses the emacs buffer 08/05 19:07 ah, right 08/05 19:08 the real solution would be either this high-level language or a ProofGeneral interface 08/05 19:09 I don't think we will spend our energy on connecting to ProofGeneral, as the high-level language should come soon 08/05 19:10 makes sense 08/05 19:11 xf : (m : Nat) -> < plus^1 m xf : Nat > <- this binding is a bit puzzling instead 08/05 19:12 http://pastebin.com/cyY77t4z <- in this context 08/05 19:12 i guess the xf in the type really refers to xf^1 above 08/05 19:13 s/really/actually/ 08/05 19:13 bleh, indeed, that's strange 08/05 19:14 I guess, that's a candidate for a bug report :-) 08/05 19:16 btw, I think you should Nat.ind on m, rather than n 08/05 19:22 true 08/05 19:22 or do "<= [n] Nat.Ind n", where [n] specify that anything in context before n are "parameters" (global context) 08/05 19:23 the [n] trick should disappear, super-Adam was working on computing parameters automatically on Friday 08/05 19:23 ah, i was wondering what [..] did 08/05 19:23 infer xf gets the type right 08/05 19:23 so i guess it's a pretty printing problem 08/05 19:24 it's a cheap hack, once again: to determine where the global context stops, local context starts 08/05 19:24 yes, I suspected that too 08/05 19:24 is there a name for those lambdas that get listed? to use it in the issue title 08/05 19:24 I call that the context 08/05 19:25 k 08/05 19:25 has anyone thought about hwo to do category theory in epigram 08/05 19:41 fax, according to the OTT paper, we are supposed to have it easy 08/05 19:47 I thought about trying some things but lack of time, etc. 08/05 19:47 hem, when I say "easy", I mean "easier" than before, right. Don't misread me :-) 08/05 19:48 any news on the equality for coinductives?:) 08/05 19:50 sorry, what's the story about that, again? 08/05 19:51 that equality should move towards something more like bisimulation, while currently it's just the structural one you get by default 08/05 19:53 ha, ok. That sounds like a question for the Boss :-) me, poor peon, have not been aware on any move on that side 08/05 19:55 hehe, i should send a mail to the list :) 08/05 19:55 I'm told that there will be a pigweek sometime soon, so you should definitely manifest your interest(s) 08/05 19:56 those are in-person events, right? 08/05 19:57 yep 08/05 19:58 btw, I've a naive Agda question (being on #agda, I'm trying to be on-topic :-)) 08/05 19:59 Saizan, I reckon that you've looked at models/Desc.agda 08/05 20:00 you might have noticed the "reflFun" postulate 08/05 20:00 I feel bad about it for some weeks now. Is there a way to achieve the same thing, without introducing a postulate? 08/05 20:00 reflFun is (rougly): (f : (a : A) -> B a)(g : (a : A) -> B a)-> ((a : A) -> f a == g a) -> f == g 08/05 20:01 this is not derivable in agda 08/05 20:02 it does have eta but that is stronger than eta 08/05 20:02 yeah, I suspected that because it's the motivating example for OTT. Out of curiosity, when you need something like that in a proof, how do you work around it? 08/05 20:04 do you rephrase your theorem? Or you introduce this kind of postulate? 08/05 20:04 you could make it a module argument but that wouldn't change much, or we could look at where it's used an try to see if something weaker fits 08/05 20:04 * fax tends to give up.. maybe other people have better methods 08/05 20:04 fax, :-) 08/05 20:04 you can use a differen equivalence relation than Identity 08/05 20:05 like one that has extensionality built in for function types 08/05 20:05 but then you have to prove everything is a morphism if you want to rewrite 08/05 20:05 it gets a unweildy fast 08/05 20:05 pedagand: i got the same problem when writing down Conor's correctness proof for unification, the solution was to carry around additional properties for the functions involved, it was a pain :\ 08/05 20:06 Saizan, it is used in IDesc.agda, to prove that the hosted and embedded Desc are equivalent. But don't waste your time with that, that was curiosity 08/05 20:06 fax, ha ok, I wasn't aware of that machinery. Thanks 08/05 20:06 is it some kind of "setoid" way of doing? 08/05 20:07 yeah 08/05 20:07 it's pretty awful 08/05 20:07 that is one reason why epigram is so exciting 08/05 20:07 but Epigram is awful for other reasons: syntax, UI, etc. :-D 08/05 20:08 thanks for your answers, I'll find back my sleep, that's great 08/05 20:09 i wonder if you can still prove cong and trans if you add reflFun as a constructor of _==_ 08/05 20:10 I wonder if I want to know the answer :-) 08/05 20:10 wow that is an interesting idea! 08/05 20:10 you need to make the type an index rather than a parameter though.. 08/05 20:12 naivety again: would "_==_" still be an inductive type? 08/05 20:12 hum, judging by the silence, that was a stupid question :-) 08/05 20:15 * fax is trying something 08/05 20:16 I didn't see the original question to answer :) 08/05 20:16 it should still be inductive 08/05 20:17 at least, agda accepts it :) 08/05 20:17 subst : forall {A : Set} (P : A -> Set) (a : A) -> P a -> forall b -> a == b -> P b 08/05 20:18 I don't know how to prove this for it though 08/05 20:18 I mean the predicate P probably needs to be respecting the equivalence 08/05 20:18 which means it's basically setoid again 08/05 20:18 pedagand: I think the 'real' solution is to use setoids. 08/05 20:19 http://pastie.org/951702.txt 08/05 20:19 But they're quite tedious. 08/05 20:19 yeah, and cong is the same 08/05 20:20 dolio, ok, thanks 08/05 20:20 I usually just postulate extensionality. :) 08/05 20:21 dolio, when you say "postulate extensionality", is it a postulate similar to reflFun? Or something even more powerful? 08/05 20:32 reflFun is extensionality. 08/05 20:33 For functions, at least. 08/05 20:33 but without definitional equality collapsing with propositional equality, isn't it? 08/05 20:34 well, you can pattern match against "reflFun f g p" to get f to be definitionally equal to g in the current context 08/05 20:36 I recall asking Conor, he told that this wasn't really extensionality, just an annoying stuck term. But I can be misinterpreting his saying. 08/05 20:36 and right, it won't reduce to refl 08/05 20:37 that's the frustratong things about adding axioms (other than inductive types) 08/05 20:37 Yeah, it will stick if it ever has to reduce reflFun. I'm not sure I've ever been in a situation where it has to do that, though. 08/05 20:38 you cannot add anything new to the convertion rule 08/05 20:38 I think plastic (which is irritatingly closed source) lets you do this 08/05 20:38 ha ok, I think I get your (and Conor's) point now 08/05 20:39 thanks 08/05 20:39 pedagand: You can postulate 'lem : (P : Set) -> P \/ Not P' and do classical reasoning if you want, too. 08/05 20:40 you could probably by pass the problem of no reduction by using a reflective blah blah this is way too complicated for anyone to actually try in practice 08/05 20:41 But, any results you get from that might get stuck. 08/05 20:42 yeah, I see: in a sense, you can act "as if" your system was extensional / classic, but when you need to compute over these things, it tells you to go away. Did I got it? 08/05 20:42 Which makes it non-constructive, I guess. :) 08/05 20:42 pedagand: yeah 08/05 20:44 Yeah, 'lem P' won't reduce any further. But elimination of P \/ Not P relies on elements of that type being either inl p or inr np. 08/05 20:45 So you've added an extra element 'lem P' that you can't compute over. 08/05 20:45 Good, thanks. 08/05 20:46 are there interesting datatypes of the form "data T : .. -> Set .. where con : .. -> (t : T ..) -> .. something involving t .." ? 08/05 20:47 self indexed types? 08/05 20:48 They'd have to be inductive-recursive, I expect. 08/05 20:48 well, not necessarily, i meant that t might be used in a later field too 08/05 20:49 Oh, or mutually inductive in that case. 08/05 20:49 Saizan: Inductive-recursive universes are easily of that form. 08/05 20:51 data U : Set where pi : (s : U) (f : T s -> U) -> U ; T : U -> Set ; T (pi s f) = (S : T s) -> T (f S) 08/05 20:51 oh, right, i had it under my nose :) 08/05 20:53 without IR the only way is to make it an argument of some polymorphic function i guess 08/05 20:53 --- Day changed Sun May 09 2010 * dolio thinks he may have finally figured out what's blowing up in his interpreter. 09/05 02:04 So what are the implications of ∃ becoming a record? 09/05 05:20 How is it different now than when it was a data? 09/05 05:21 It get eta expanded during normalization. 09/05 05:21 So you get p = (fst p, snd p) definitionally. 09/05 05:22 ah 09/05 05:22 I've actually had to define that lemma before 09/05 05:22 Is eta-expansion different than eta-conversion? 09/05 05:24 the opposite of eta-conversion? 09/05 05:24 eta conversion refers to treating it as an equation, I think. 09/05 05:25 Expansion is when you use it as a rewrite rule from p to (fst p, snd p). Reduction is the opposite. 09/05 05:25 Is there a case when you have a inductive type (but not an inductive family) where you might want a single constructor data type now? 09/05 05:27 Using eta reduction as a rule in your normalization tends to cause problems with confluence, though 09/05 05:28 Probably not, since I've been told that you can match on constructors defined for records now. 09/05 05:29 previously it was a syntactical reason and not a theoretical reason? 09/05 05:29 Previously you had to choose between pattern matching and eta equality. 09/05 05:29 Do we not have to choose now because of new research or new implementation? 09/05 05:30 Well, I don't think there was ever any doubt that pattern matching on records could be implemented. It just hadn't been. 09/05 05:30 Isn't there some doubt that dependently-typed pattern matching should be implemented? 09/05 05:31 Something about axiom K and some other stuff I didn't know about 09/05 05:31 I don't think K is that controversial. 09/05 05:32 Unless you're into homotopy lambda calculus or something. 09/05 05:32 * glguy goes back to wikipedia again :) 09/05 05:33 While I work out the consequences of axiom K my son is working out the consequences of rolling over onto his back 09/05 05:34 he works so hard to flip over and then is very unhappy when he succeeds 09/05 05:34 Heh. 09/05 05:35 homotopy is bringing up lots of people talking about how coffee mugs are like toruses 09/05 05:35 Yeah, I don't think there's much out there on homotopy lambda calculus. It's, like, one guy's research project. 09/05 05:36 But I've seen it stated that there's more than one proof of x = x in it, which contradicts K. 09/05 05:37 Homotopy has to do with topology, of course. 09/05 05:37 http://www.math.ias.edu/~vladimir/Site3/home.html 09/05 05:38 http://www.andrew.cmu.edu/user/awodey/preprints/homotopy.pdf 09/05 05:38 I'm not 100% sure the second one is relevant, but it sounds like it is. 09/05 05:38 Does "refl" ever carry any information? After type checking wouldn't it be safe to erase? 09/05 05:39 I think so. But you can only erase it at runtime, if I understand correctly. 09/05 05:39 erase at runtime? 09/05 05:40 If you erase equality proofs when you're checking open terms (like during type checking), then you'd be potentially erasing false hypotheses. 09/05 05:41 Like \(eq : x = (x -> x) -> 09/05 05:41 but that function would never be called 09/05 05:42 anyway 09/05 05:42 since you never had an eq to call it with when you compiled 09/05 05:42 You could require it to be normalized during type checking. 09/05 05:43 Like, if it's called f, and you try to type check "refl : f = g", then to decide f = g, it has to normalize f and g. 09/05 05:44 But f will loop on normalization. 09/05 05:44 Anyhow, the point is, you can erase it (probably) when you're emitting code, but not before you type check. 09/05 05:45 right, i was thinking after type-checking 09/05 05:46 I know. Just wanted to spell it out. Because there are other schemes where you can do some level of erasure during checking. But that won't work for equality. 09/05 05:48 --- Day changed Mon May 10 2010 what does an empty pair of parenthesis mean in agda? as in: evalφ t (prim f s) () 10/05 02:00 absurd pattern 10/05 02:26 no value of that type exists so you don't need to provide an implementation 10/05 02:26 example : 1 ≡ 0 → ℕ 10/05 02:27 example () 10/05 02:27 ok, thats what I thought. thanks 10/05 02:27 code.haskell.org seems to be dead, anyone have a link to the agda source? 10/05 02:32 nm, the haskell guys restarted it 10/05 02:43 does anybody know the "pedantic" name for projection of pairs? Like beta for lambda, iota for inductive types, and so on 10/05 14:44 I think I heard (maybe even wrote) \pi-rule once, but I come to doubt about it... 10/05 14:45 i've often seen \pi_1 and \pi_2 to refer to those 10/05 14:48 i don't remember a name for both at once though 10/05 14:49 ok, good. Thanks 10/05 14:49 well, I guess, it's really two rules, but two rather boring and similar rules :-) 10/05 14:50 Chapter 2 of Zhaohui's book calls them \sigma http://books.google.com/books?id=z3uicYzJR1MC&pg=PA21&lpg=PA21&dq=Luo+ECC&source=bl&ots=grlf2h9WfY&sig=vjVNDMzibE7m9gMNBEP3X2-j9zE&hl=en&ei=3Q_oS93POMqrsAbgw8GOBA&sa=X&oi=book_result&ct=result&resnum=4&ved=0CCAQ6AEwAw#v=onepage&q=Luo%20ECC&f=false 10/05 14:55 ha, so I shall abide by the Luo (hem, sorry about that pitiful joke). Thanks 10/05 15:07 so you should (so you should be) 10/05 15:17 --- Day changed Tue May 11 2010 * dolio now understands the true horror of using string variables and alpha renaming. 11/05 00:56 alpha conversion and fresh variables: the single biggest source of compiler bugs? 11/05 01:10 I thought, "I'm not generating induction principles and stuff, so I don't need fancy locally nameless stuff like pigworker suggests." But, I was wrong. 11/05 01:12 yeah, free and bound variables are just different beasts 11/05 01:14 --- Log closed Tue May 11 04:05:12 2010 --- Log opened Tue May 11 04:05:17 2010 -!- Irssi: #agda: Total of 26 nicks [0 ops, 0 halfops, 0 voices, 26 normal] 11/05 04:05 -!- Irssi: Join to #agda was synced in 80 secs 11/05 04:06 --- Day changed Wed May 12 2010 pigworker: Ping. 12/05 00:42 dolio: not long for awake 12/05 00:42 I'll make it short, then. Have you considered adding a 'let ... in' sugar for applicatives to SHE? 12/05 00:42 let x <- fx ; y <- fy ; ... in e ==> pure (\x y ... -> e) <*> fx <*> fy <*> ... 12/05 00:43 Yes, I have, but not with those semantics. 12/05 00:44 If you do it that way, you have to be clear that x is not in scope for fy, which is odd for that sugar. 12/05 00:45 Is there a way where it can be in scope? 12/05 00:46 Or do you mean 'let ... in' isn't appropriate syntax? 12/05 00:46 My thinking is just that inside idiom brackets, let should desugar to do. Moggi-style 12/05 00:47 I mean, if you use the result of one computation to determine the next computation, that's yer actual monad. 12/05 00:47 Right. 12/05 00:47 I was actually thinking of situations where I wanted to use it with applicatives. 12/05 00:48 "let" is the original Moggi syntax for monadic bind and that's exactly as it should be 12/05 00:48 But writing (\x y z ... -> ...) <$> ... is awkward. 12/05 00:48 or (| (\x y z ... -> ...) ... |) 12/05 00:49 For reordering or duplicating values? 12/05 00:49 The thing I was doing recently that made me think of it was pretty printing inside a fresh name generator. 12/05 00:50 do px <- pp x ; py <- pp y ... ; return (px <> py <> ...) 12/05 00:50 But that doesn't require the full power of a monad. 12/05 00:51 (| pp x <> (| pp y <> ... |) |) ? 12/05 00:51 my not-really-a-parser isn't any good at operator precedence, so the flat version isn't available just now 12/05 00:53 That'll desugar into something like (<>) <$> pp x <*> ((<>) <$> pp y <*> ...)? 12/05 00:55 yes 12/05 00:55 That works, then, I guess. 12/05 00:55 Anyhow, what I was doing reminded me that I'd seen a suggestion that do-alike sugar for applicatives would be a series of non-recursive, independent bindings, followed by a pure expression involving those bindings, which was exactly what I was doing. 12/05 00:57 I don't know whether it comes up enough to warrant sugar, though. 12/05 00:57 At the time, it was suggested that this was rather like let in Lisp, but I suppose that's actually more like do. 12/05 00:58 It could be tidier with better parsing, but you get pure-functions-effectful-arguments with the usual syntax. I agree that naming helps when things are more tangled up. 12/05 00:58 such as when you're pattern matching 12/05 01:00 Saizan: I'm not sure what you mean 12/05 01:01 "pure (\p1 p2 ... -> e) <*> fx <*> fy <*> ..." is quite akward since the patterns are far from what they refer to, and you can't massage it into an expression with no new bindings like with <> above 12/05 01:02 unless you use a named function instead of the lambda 12/05 01:03 where pN is a pattern more complex than a variable 12/05 01:04 I see. pN had better be irrefutable 12/05 01:04 yeah 12/05 01:05 Tupling is a nasty way out of the problem. 12/05 01:07 I don't think "let" has the right associations, but I do take the point that some way to name the values near the computations would be good. 12/05 01:11 Yeah, I'm not married to 'let' by any means. 12/05 01:12 Something like (|p <- c in f blah... |) yields (| (\ ~p -> f) c blah... |) 12/05 01:18 It would, of course, be possible to decide how to desugar idiomatic "let" on the basis of a dependency check, but that seems flaky to me. 12/05 01:21 That sounds like it'd be more work than having two different syntaxes. 12/05 01:24 Yes, especially without a real parser. 12/05 01:24 G'night! 12/05 01:37 --- Day changed Thu May 13 2010 http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=385 <- anyone tried reflection yet? 13/05 23:15 --- Day changed Fri May 14 2010 Saizan: I thought about writing a propositional solver like this, but never really followed through. 14/05 00:03 Oh, I didn't know about the quoting stuff, though. 14/05 00:04 yeah, i should have specified i was referring to the new stuff :) 14/05 00:08 i'm just passing the description of \lambda2 (CoC) in Barendgret's "Lambda Calculi with Types".. and I'm wondering why is the dependent sum type often not introduced? I've seen a few other calculi recently that introduce \Pi without any mention of \Sigma at all. is it because it can be derived or is it just to simplify the descriptions? 14/05 21:36 \lambdaP2 i meant. 14/05 21:37 just curious :) 14/05 21:38 afaiu, \Sigma can be derived if you add something like \== 14/05 21:44 yeah. i also figured, if Bool is built-in to a dep.type system.. (true, ..) and (false, ..) may suffice 14/05 21:58 bbiab. 14/05 22:01 --- Day changed Sat May 15 2010 guerrilla: The calculus of constructions doesn't have sigma, and you can't encode it. You can encode all inductive types, but not with their strong induction principles. 15/05 03:22 so you can't have sigma in coq? 15/05 03:23 Coq is the calculus of inductive constructions. 15/05 03:23 The calculus of constructions is just a dependently typed lambda calculus. Adding strong inductive types is an extension beyond that. 15/05 03:24 ah 15/05 03:25 But, it's in the same family as stuff like System F and F_omega, which don't have separate inductive types, either, although in those, you couldn't have strong elimination principles anyway. 15/05 03:26 So System F is in a sense just as good as it would be if it were extended with some notion of inductive declaration. 15/05 03:27 Except possibly from an efficiency perspective. 15/05 03:28 Inductive types might be redundant if you have access to parametricity in the language, though. 15/05 03:31 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24938 15/05 03:33 How does the unicode lexing work? It seems Lexer.x defines identchar only as [ $digit$alpha $op ], where$alpha = [ A-Z a-z _ ] and so on 15/05 06:36 is Agda/src/full/Agda/Syntax/Parser/Lexer.x the actual lexer? 15/05 06:48 is it possible to separate cases into separate functions? 15/05 12:36 i have a function definition with lots of cases and it makes code so unreadable 15/05 12:37 it would be nice if i could split it up 15/05 12:37 i think the only pratical way is to redefine your datatype 15/05 12:53 i.e. instead of "data A where B C D E : A;" you could use "data BC where B C : BC; data DE where D E : DE; data A where bc : BC -> A; de : DE -> A" 15/05 12:55 ow 15/05 13:07 another way would be to define an ad-hoc induction principle i guess.. 15/05 13:12 something like : (P : A -> Set) -> ((x : A) -> isBC x -> P x) -> ((x : A) -> isDE x -> P x) -> (x : A) -> P x 15/05 13:13 where e.g. isBC B = \top; isBC C = \top; isBC _ = \bot 15/05 13:14 hm, i'm going to try to split case result instead 15/05 13:15 i can't split datatype 15/05 13:15 and i better avoid clever tricks i do not understand 15/05 13:15 you could keep both the A and the splitted up A and define a conversion function i guess 15/05 13:16 hm, another question 15/05 13:29 what are variables with dot (.) prepended? 15/05 13:30 dot patterns are those whose value is inferred from other patterns 15/05 13:35 though i think i've seen .x in the types of the goal simply to indicate that such x is an implicit parameter that you didn't explicitly bind 15/05 13:36 It's not really inference, when pattern matching is what you're talking about. 15/05 13:40 It's that the value of (part of) some argument is determined by the value of some other pattern. 15/05 13:40 sorry, i used the verb in a non-technical sense 15/05 13:40 hm, i'm starting to realize what it is 15/05 13:44 what would be the best way to return multiple values from a function? 15/05 13:48 are you using the standard library? if so there's Data.Product 15/05 13:49 but if i want to avoid it, i should create my own data type? 15/05 13:50 yeah 15/05 13:50 * Gammu Discounts!! Our Special Limited Time Offers Up To May,22!!!New BranD!! Notebooks,Plasma and LCD TV's.Buy your electronic needs at our unique prices. Laptop Sony VAIO® VGN-FW590FFD-575,57$!!!Apple MacBook® Air MC234LL/A-695,27$!!! http://www.elplace.com/ 15/05 23:00 --- Day changed Sun May 16 2010 maybe I should buy my electronics at elplace.com 16/05 00:25 can't argue with unique prices 16/05 00:25 uniqueness of prices requires an extra axiom 16/05 00:29 sorry 16/05 00:30 can I get linear prices instead of unique ones? 16/05 00:30 No. They've been used up already. 16/05 00:31 do you need something or just want to buy :) 16/05 00:32 * Saizan wonders why one has to provide the context separately when quoting a term 16/05 00:34 s/term/goal/ 16/05 00:34 it feels like working in a language without first-class functions :) 16/05 00:34 :O 16/05 00:36 http://patch-tag.com/r/gallais/agda/snapshot/current/content/raw/src/prop_logic/Examples.agda <- like at the bottom here 16/05 00:38 I need to look up this quoting stuff 16/05 00:42 whole agda looks still like deep magic for me 16/05 00:43 http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=385 <- i started from here, though [1] and the above patch-tag repo are most illuminating 16/05 00:44 Hello! 16/05 20:56 env2con : ∀{Γ} → Env Γ → Con -- Is there a way to declare this function inline as a lambda expression? 16/05 20:57 env2con {Γ} γ = Γ 16/05 20:57 \ {Γ} (γ : Env Γ) -> Γ 16/05 21:09 that works? 16/05 21:09 we need an agdabot! :P 16/05 21:09 hehe 16/05 21:10 \{Γ : Con} (γ : Env Γ) -> Γ -- this worked 16/05 21:21 thanks! 16/05 21:21 cool 16/05 21:21 wow, I can even put lambda expressions inside type signatures 16/05 21:22 even let .. in .. expressions! 16/05 21:45 --- Day changed Tue May 18 2010 Hi, if anybody could take a look at http://paste2.org/p/836142 and perhaps help me, or point me in the right direction on how to complete the last of the functions, I would be very grateful, thanks 18/05 18:36 I'm trying to prove that a function (Nat -> Nat) that always output a even value is not surjective 18/05 18:38 pattern match on x? 18/05 18:42 hmm yes, however - if I do so, the goal reads '?0 : (toEven zero | even zero) \== 1 → \bot" 18/05 18:48 well zero should be fairly trivial 18/05 18:48 you can probably get away with a () in the pattern 18/05 18:48 hm, yeah, \lambda () works 18/05 18:49 yeah, or that 18/05 18:49 but of course not for the (suc x) case 18/05 18:49 yeah :P 18/05 18:49 anyway, I need to run 18/05 18:49 will bbl 18/05 18:49 good luck :) 18/05 18:49 ok, thanks! 18/05 18:49 codolio: hey, what happend to http://code.haskell.org/~dolio/agda-share/categorica/ ? :-/ 18/05 19:10 stevan: I had to restart my repository because storing the agda-generated html in it destroyed it. 18/05 19:11 And I haven't gotten around to adding the category stuff back. 18/05 19:11 ok 18/05 19:12 Don't store agda-generated html in a darcs repository, by the way. :) 18/05 19:14 i usually have a www: entry in a Makefile nearby which does agda --html and scp:ies the output to the webserver. :-) 18/05 19:17 I think something I wrote triggered lots of re-generation of standard library html. 18/05 19:17 And the generated html seems to have lots of random numbers in it. 18/05 19:18 So I ended up with like 25,000 changes to process. 18/05 19:18 :-/ 18/05 19:20 And, of course, I would have just accepted them all, but darcs doesn't seem equipped to handle that many changes at once. 18/05 19:20 It just hung for as long as I cared to wait. 18/05 19:20 --- Day changed Thu May 20 2010 does anyone know of any nice set of proof exercises? 20/05 01:42 for some reason I feel guilty when I use Bool in agda 20/05 08:06 copumpkin: that it is not always a bad idea, you can have a property on the side ∀ x → (f x ≡ true) ⇔ P x 20/05 08:08 yeah, I know there are a few good times to have it and I think this is a good one 20/05 08:09 but I still feel a little dirty using it 20/05 08:09 maybe I'll think of something better later :P 20/05 08:09 I really want a graph datastructure where nodes can express properties about their neighbors 20/05 09:03 the std lib graph doesn't allow that easily 20/05 09:03 omg kmc 20/05 09:08 omg (?) 20/05 09:12 yep 20/05 09:15 hi 20/05 11:31 My Professor just mentioned AGDA 20/05 11:31 How difficult a language is this to learn? 20/05 11:31 That might depend on your background. 20/05 11:33 KK 20/05 11:55 --- Day changed Fri May 21 2010 does anyone have any ideas about my question yesterday about creating a graph data structure that allows you to specify properties about a vertex's neigborhood? I can do it in an ugly manner but I was wondering if anyone had thought about building a datastructure to support this directly 21/05 01:52 this property would holds for all the vertexes? 21/05 02:28 Saizan: possibly. If I had that I could probably encode per-vertex properties too 21/05 03:21 that was a deep discussion with Panarchy last night 21/05 03:22 oh, i missed that 21/05 03:23 http://snapplr.com/rrwq 21/05 03:23 ah, i didn't catch the sarcasm :) 21/05 03:25 any ideas about the graph? 21/05 03:37 did that kaoos guy with the toEven function ever succeed in his proof? 21/05 06:04 I'm not sure. Using booleans is a recipe for failure, though. 21/05 06:09 yeah, I'm just trying his thing now cause I'm bored 21/05 06:09 well, that was easy 21/05 06:12 very ugly proof though 21/05 06:12 dolio: how would you rewrite it without bools? 21/05 06:14 http://paste2.org/p/836142 was his original code 21/05 06:16 * copumpkin still doesn't really understand how to eliminate absurd patterns from negation proofs 21/05 06:21 copumpkin: do you mean with things like:  \ () 21/05 06:21 the absurd lambda? 21/05 06:22 or \bot-elim? 21/05 06:22 yeah, or just putting () in a pattern 21/05 06:22 I can prove things fine using those, but I wouldn't know how to prove the same thing without them 21/05 06:22 not sure if that makes sense 21/05 06:23 for example, in the proof of the above I wrote a helper forall n -> suc (suc n) == 1 -> \bot 21/05 06:23 its implementation is an absurd pattern with no body 21/05 06:23 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25607#a25607 21/05 06:27 oh 21/05 06:27 that seems pretty obvious now :) 21/05 06:27 much nicer 21/05 06:27 I'm not sure I understand the horner encoding of variable identity in the agda ring solver 21/05 07:07 I should reread the paper 21/05 07:11 coq is rather ugly 21/05 07:20 even just the naming schemes people use in it, from what I've seen 21/05 07:20 if a pure type system is strongly normalising then type checking in it is decidable, right? 21/05 12:20 guerrilla: That might depend on how much you think you can add before it's no longer a pure type system. 21/05 13:24 If it's just a lambda calculus parameterized by rules for sorts and whatnot, then yes. 21/05 13:25 If adding an extensional identity type is allowed, then no. 21/05 13:26 dolio: thanks. yes, i meant the former case, literally a PTS as defined by Barengredt 21/05 13:32 the paper "Pure Type Systems with Denitions" by Severi and Poll adds both global and local definitions while preserving strong normalisation 21/05 13:34 i thought it might be fun to implement but was just curious if it type checking in it would still be decidable 21/05 13:34 it doesn't explicitely state whether it is or not, only that it's strongly normalising, so i though that decidability might have been an obvious consequence of that or something 21/05 13:35 but when i was reading about another extended PTS (I think with GADTs built-in or something like that), it said the reason it was not decidable was because of beta-reduction (which is used in the beta-conversion rule of any PTS) 21/05 13:43 s/rule/typing rule 21/05 13:43 Hmm 21/05 13:44 Well, regular PTS have checking methods that would seem to reliably terminate if you have strong normalization. 21/05 13:45 definitely 21/05 13:45 as long as the number of sorts is finite 21/05 13:45 Well, even with infinite sorts, you just need them to have decidable equality. 21/05 13:46 yeah, i thought so too. i think it may have been stated differently than how i just said it 21/05 13:47 if it has finite sorts it is decidable, if not, it may not be 21/05 13:47 but CoC with infinite sorts is not decidable. that was explicitely proven somewhere.. 21/05 13:48 It was? 21/05 13:48 yeah, 1sec. let me find where that came from 21/05 13:48 i thought it was "Pure Type Systems for Functional Programming" by Roorda.. but apparently not 21/05 13:52 Well, I have a program that does check CoC with infinite sorts. I'd be surprised to learn that it loops somewhere. 21/05 13:52 i think to get it to happen, you have to do something really convoluted 21/05 13:53 coquand '87 21/05 13:53 err '86 21/05 13:53 section 11 21/05 13:53 blah, no sorry again wrong. 21/05 13:53 nevermind this, i can't find it and it's irrelevant anyway :P 21/05 13:54 I mean, it checks lots of other things too. All pure type systems. 21/05 13:55 The sorts are just a parameter, and it just requires Eq in Haskell. 21/05 13:55 yep 21/05 13:55 thinking about it, it seems like it should. but i don't trust myself on that 21/05 13:56 I guess it requires the rules, too. But that's just Sort -> Sort -> Sort. 21/05 13:56 yep 21/05 13:56 And in the case of infinite CoC, it's 'rule _ 0 = 0 ; rule i j = max i j'. 21/05 13:56 yeah, i'm going to use an axiom and rule table though, just to be pedantic 21/05 13:57 Roorda already did this, http://www.cs.chalmers.se/~jwr/pure/ 21/05 13:58 just making sure i can (and making it a little bit prettier, hehe) 21/05 13:58 his thing also adds a totally diferent formalism for definitions.. and also adds gadts. 21/05 13:59 and i think either and both additions makes it undecidable 21/05 14:00 I suppose given the axiom of choice, you might be able to define a set of rules that is uncomputable. 21/05 14:00 (described in his master's thesis) 21/05 14:00 i guess so.. s1 -> s2, s2 -> s1 21/05 14:00 hehe 21/05 14:00 or maybe that'd reject all with pi abstractions 21/05 14:01 *shrug* 21/05 14:01 Incidentally, saying that CoC with infinite universes is undecidable is tantamount to saying that Coq does not have decidable type checking (since Coq is actually extended beyond that). 21/05 14:03 Which would also surprise me. 21/05 14:03 i'm aware of that :) but it could be possible. i also really doubt it though 21/05 14:05 Well, in this paper, they have case expressions. 21/05 14:05 I can believe that checking case expressions with GADTs can't be done well. 21/05 14:06 i agree 21/05 14:06 GHC makes you annotate them manually, I think. 21/05 14:06 yeah, i'm also not convinced it's necessary. the question of whether something is a term or a type constructor seems pretty subjective to me and should remain an artifact of a nice abstraction layer 21/05 14:07 data constructor i meant 21/05 14:07 i may retract that later though :P 21/05 14:09 Oh, one issue with CoC, I suppose, is cumulativity. 21/05 14:11 My checker doesn't do anything like that. 21/05 14:11 That would make CoC with infinite universes fail to be injective by this paper's definition. 21/05 14:12 ok 21/05 14:12 Because (i,j,k) is a rule for all k >= max i j. 21/05 14:12 yeah.. i see 21/05 14:13 btw, anyone know a good latex package to write seq.calc/typing rules in? 21/05 14:16 http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/nd.html 21/05 14:17 I haven't used those much, but they seemed all right. 21/05 14:17 perfect 21/05 14:17 copumpkin, dolio: the surjectiv thing: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25582#a25582 21/05 17:01 guerrilla: So, I think I understand what the problem is now. 21/05 18:08 guerrilla: If you have infinite sorts, and an infinite number of axioms/rules like '(i,j) j > i' and so on, then the only general PTS checking algorithm you could use is, when you need to use an axiom/rule for a given input, try them all, using a search of some kind. 21/05 18:11 But, that will only work if the term you're checking is well-typed (and your search is good enough to find the solution). If it isn't well typed, you'll never finish rejecting all the possibilities, so you can't decide when a term is ill-typed. 21/05 18:12 Or, may not be able to. 21/05 18:12 However, that doesn't mean there aren't better algorithms for particular type systems. For instance, I think Luo's ECC has decidable checking, despite having an infinite cumulative hierarchy, because instead of having a bunch of rules, he has a subtyping relation between sorts (and pi types), and an algorithm for inferring the least type by that relation. 21/05 18:15 stevan: Yeah, when I actually worked through it, using booleans didn't seem like much of a handicap. However, in general, when you're working in a dependent type theory, I think it's advisable to split your predicates into something Set/Prop valued that you can use as proofs, and a decider that returns a proof if the predicate is in fact decidable. 21/05 18:20 dolio: yes, ECC seems to be decidable, i just read that a few minutes ago. 21/05 23:13 dolio: check this out, ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/tlca95.ps.gz 21/05 23:14 "Extensions of Pure Type Systems" by Barthe 21/05 23:14 (same guy that created the elmt(.|.) etc. stuff) 21/05 23:15 going back to the gadt thing, now i'm thinking.. adding non-dependent sum types would preserve SN 21/05 23:20 --- Day changed Sat May 22 2010 guerrilla: I don't really understand the point of the K-rules. 22/05 01:33 Isn't K equivalent to (\x y -> x)? 22/05 01:33 I suppose it is interesting that adding K is equivalent to adding definitions and the other stuff, since K looks so trivial. 22/05 01:36 dolio: yeh, it seems K = id. but built into the TT 22/05 02:33 think it was just to make a point of.. given an addition, show what effects (if any) this has 22/05 02:34 I suppose none of those extensions could really be said to add much power to the type theory. 22/05 02:39 I added definitions to my PTS interpreter without even thinking about it. 22/05 02:39 But K appears to be a useless addition, despite being equivalent from a proving strong normalization perspective. 22/05 02:41 yeah, you just have to be careful to not have definitions introduce recursion on accident 22/05 02:42 i think its nice to have it part of the theory though 22/05 02:42 just.. aesthetics though 22/05 02:42 I find it a bit more surprising that subsets and quotients are equivalent to the other two. 22/05 02:43 Although those two don't really add anything that you couldn't do by hand, I guess. 22/05 02:44 At least in that setting. 22/05 02:45 yeah, the more i look into this 22/05 02:45 it seems that a PTS like CoC can pretty much express everything we want. everything else seems to be sugar 22/05 02:45 and having just started learning stratego/xt, this is a convenient conclusion 22/05 02:47 Well, CoC can't do strong induction principles. That's a genuine addition. 22/05 02:49 yeah, good point 22/05 02:49 was thinking of trying to generalise \lambda\mu to extend a PTS to do that 22/05 02:50 "Termination Checking with Types" by Abel for example 22/05 02:51 Setoids aren't much fun to work with in my experience, either. So quotient types and the like are handy, if not genuinely offering more power. 22/05 02:51 yeah, i agree with the former, but haven't worked with quotient types much 22/05 02:52 s/much/at all 22/05 02:52 do you know ECC? 22/05 02:55 I've read a fair amount of Luo's book. 22/05 02:56 yeah, i just found it 22/05 02:57 question then.. 22/05 02:57 he adds dep.sum types, but is that restricted to Prop? 22/05 02:58 (i'll read it tmrw, but it's near 4am now) 22/05 02:58 Dependent sums are specifically left out of Prop, as I recall. 22/05 02:59 ok 22/05 02:59 that would make more sense 22/05 02:59 my follow-up then would be why to even have them :P 22/05 02:59 You can make a sum with a Prop in it, but to do so you have to promote the Prop to a Type_i. 22/05 02:59 ah 22/05 03:00 Because they're useful for regular types, too? 22/05 03:00 Like, typing algebraic structures. 22/05 03:01 no i meant, if they were restricted to only prop, that doesnt sound terribly useful 22/05 03:01 Oh, okay. 22/05 03:02 Yeah, that would probably make less sense. 22/05 03:02 Especially since if they lived in Prop, I think the only way to maintain strong normalization is to only allow the rule (Prop, Prop, Prop). 22/05 03:03 Since he mentions that strong impredicative sums allow you to essentially have Prop : Prop. 22/05 03:04 ick 22/05 03:07 --- Day changed Mon May 24 2010 I wish Agda would infer types for helper functions by Miller unification. 24/05 12:53 if that would reduce the need to annotate functions defined via pattern matching in where clauses i'd like it too :) 24/05 14:33 That's one of the few things I miss of the inference in Haskell. 24/05 14:55 Generally, I reckon it should be ok to write f blah = mutter (g x y) where  g pat = exp ... inferring type g (x : X)(y : Y) -> T, where T is the type pushed into the application. We'd need to ensure that T does not depend on any vars whose types depend on x and y, but otherwise, it should work. 24/05 15:24 --- Log closed Mon May 24 16:43:11 2010 --- Log opened Mon May 24 16:55:57 2010 -!- Irssi: #agda: Total of 27 nicks [0 ops, 0 halfops, 0 voices, 27 normal] 24/05 16:55 -!- Irssi: Join to #agda was synced in 76 secs 24/05 16:57 --- Log closed Mon May 24 17:12:08 2010 --- Log opened Mon May 24 17:12:38 2010 -!- Irssi: #agda: Total of 27 nicks [0 ops, 0 halfops, 0 voices, 27 normal] 24/05 17:12 -!- Irssi: Join to #agda was synced in 70 secs 24/05 17:13 what about a proo assistant based on category theory? 24/05 21:24 rather than type theory? 24/05 21:24 proof 24/05 21:24 how can I make it 24/05 21:25 I tried to immerese category theory in type theory but it sinks 24/05 21:25 is that code available somewhere? :-) 24/05 21:28 someone ought to have tried to make a proof assistant based on CT? i can't seem to find anything with google tho... 24/05 21:42 the reason I want this is so I can do the book Computation Category Theory 24/05 21:42 based on what aspect of CT? 24/05 21:44 If you want to make a proof assistant/language out of category theory, presumably you can't just look at the definitions of categories in general and such. 24/05 21:46 Rather, you have to look at foundational theories, like the Category of Categories as a Foundation. 24/05 21:47 the notion of computation in CT isn't clear to me... 24/05 21:47 Because those are the sort of theories that have existence claims, rather than just deducing things from definitions. 24/05 21:48 Similarly, type theory is foundational. "Pi types exist. Sigma types exists. Inductive types exist...." 24/05 21:48 I don't know if that'll give you an easy proof environment, though. 24/05 21:51 Type theory works nicely for that because it's essentially a fancy higher-order logic. 24/05 21:51 But viewing logics as a category gets you something that doesn't immediately resemble logic. 24/05 21:52 * pigworker has just blogged about Ornaments (with links to code). Knackered now. 24/05 22:40 I wonder how to compute the proposition asserted by a categorical diagram. 24/05 22:48 Wow. 24/05 23:07 * Saizan tries to replay the List -> Vec passage at home 24/05 23:27 --- Day changed Tue May 25 2010 hi 25/05 14:35 I have a question about using 'with' views to prove equivalence 25/05 14:35 basically, if I have foo with (bar x)  foo | y, how can I prove bar x == y on the right-hand side? 25/05 14:36 there's the inspect idiom 25/05 14:37 from Relation.Binary.PropositionalEquality 25/05 14:37 thanks, I'll check that 25/05 14:38 ah 25/05 14:41 now I see :) 25/05 14:41 Here's a lemma, there's a lemma and another little lemma. Fuzzy lemma, funny lemma, lemma lemma, shed. http://is.gd/coLk4 #agda 25/05 17:35 hi 25/05 21:10 is there a way to do efficient arithmetics with Agda? unary's just not cutting it for me... 25/05 21:10 and writing an e.g. decimal representation library would be way over my league 25/05 21:11 you could make yourself a binary natural type 25/05 21:11 oh 25/05 21:11 If you declare your naturals BUILTIN, it will use the underlying Haskell Integer implementation. 25/05 21:11 oh 25/05 21:11 really? 25/05 21:11 Yes. 25/05 21:11 for what operations? 25/05 21:11 + and * 25/05 21:11 let me check if this is enough to speed up _|?_ 25/05 21:12 I remember when I was doing the rational arithmetic though 25/05 21:12 that's true only for evaluation, right? 25/05 21:12 i mean, not typechecking 25/05 21:12 even with the builtin naturals, it was really really slow at normalizing terms 25/05 21:12 yeah :/ 25/05 21:12 I'm not sure why it would use different methods for type checking than for C-c C-n, but perhaps. 25/05 21:13 Actually, I suppose I do know. 25/05 21:14 Type checking can occur on open terms. 25/05 21:14 yeah, maybe it's actually checking which kind of terms the arguments are 25/05 21:15 am I right in seeing that _divMod_ is written in such a way that native + and * will not speed it up? 25/05 21:15 C-c C-n has the same problem if you add postulates, though. 25/05 21:16 You can declare subtraction builtin, too. 25/05 21:17 That will help divMod a little. 25/05 21:17 * _Cactus_ looks for documentation on BUILTINs 25/05 21:21 I see that there are some BUILTIN declarations in the std library's Data.Nat 25/05 21:25 should that be enough? 25/05 21:25 yes 25/05 21:25 hmm 25/05 22:06 I'm using Data.Nat, and it doesn't seem to use native ints for anything 25/05 22:06 what did you try? 25/05 22:13 I may have screwed that up :) 25/05 22:16 is there an equivalent of haskell's "seq" for agda? or is everything strict by default? 25/05 22:16 Neither. 25/05 22:18 so const (1 + 2) "Foo" doesn't evaluate 1+2, right? 25/05 22:18 Probably not. 25/05 22:18 ooookay. so how do I test if bignum + bignum' is calculated "fast", if I can't show it from main? (since show is horribly slow for large numbers) 25/05 22:19 C-c C-n 25/05 22:19 Ask the emacs mode to normalize something large. 25/05 22:19 Like 20! or something. 25/05 22:19 and that doesn't use show? 25/05 22:20 If the built-in is working right, it will show like a base-10 numeral. 25/05 22:21 thanks, that seems to work 25/05 22:22 sooo.. I see now that I've had machine-native + and * all along... now back to the beginning, is there a way to speed up _|?_? 25/05 22:22 _Cactus_: get a faster computer 25/05 22:23 :) 25/05 22:23 I mean asymptomatically :) 25/05 22:24 unary numbers are optimal 25/05 22:24 _Cactus_: I honestly have no clue :) 25/05 22:24 I thought e-ary numbers were optimal :) 25/05 22:24 Okay, BUILTIN doesn't optimize equality checking in types, at least. 25/05 22:26 what are you using _|?_ for? do you need the proofs it creates? 25/05 22:28 doesn't Rational use it all the time everywhere? 25/05 22:29 oh maybe not 25/05 22:30 stevan: yes, because I'd like to use _|_ in the specification 25/05 22:43 is it typechecking or running your stuff that takes long time? 25/05 22:46 running 25/05 22:46 tried compiling it? :-) not sure if that helps tho. 25/05 22:50 yes 25/05 22:52 as an added bonus, I don't know how I'll display the results in the compiled program, because Data.Nat.Show is so slow:) 25/05 22:52 ok :-), hmm... i'm running out of ideas. perhaps use the ffi to haskell to call it's show somehow? 25/05 23:00 why do you wanna run programs on big instances anyways?! you have a proof of it working? isn't that enough? :-p 25/05 23:01 well what if the proof is of the existance of some object but I need the actual value? 25/05 23:04 I thought that's the whole point of a proven program... that I prove that it will find the right answer, then run it to actually get the answer 25/05 23:07 ok, yes 25/05 23:08 but anyway, I have to leave now 25/05 23:08 I'll come by again with the same problem :) 25/05 23:08 sure, see you 25/05 23:09 --- Day changed Wed May 26 2010 FWIW, http://personal.cis.strath.ac.uk/~conor/fooling/Bin.agda is a stab at binary numbers. 26/05 00:21 anyone used sized types here? 26/05 19:24 I've begun before, but got quickly distracted. 26/05 19:31 dolio: do you have some code using them? 26/05 19:38 I doubt it. 26/05 19:47 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25726#a25726 <- they let you write fold the right way! 26/05 19:55 it seems the implementation in Agda is incomplete, e.g. there's no subtyping 26/05 22:25 ? 26/05 22:30 oh, the sized types 26/05 22:30 yup 26/05 22:31 --- Day changed Thu May 27 2010 * copumpkin is trying a kind of proof he hasn't tried before 27/05 01:06 :o 27/05 01:06 :O 27/05 01:07 this is tricky! 27/05 01:13 but I'm avoiding telling y'all what it is cause I'm sure you'll get it in one minute 27/05 01:13 copumpkin: the rest of the folks here might, I won't. 27/05 01:14 brain is already fried for the day. 27/05 01:14 not even sure it can be proved 27/05 01:30 seems like it should though 27/05 01:30 * Saizan is curious 27/05 01:31 * copumpkin tickles Saizan 27/05 01:31 I want to try a little longer, then I'll show you :P 27/05 01:31 * Saizan makes a tea then and reads some more on sized types 27/05 01:33 gah, this should be easy 27/05 01:47 Saizan: I'm trying to prove that the keep function Yitz sent to -cafe is impossible 27/05 01:47 but the types are all forcing each other 27/05 01:47 proving something like fix is impossible is pretty easy 27/05 01:48 how is the thread called? 27/05 01:50 currying combinators 27/05 01:50 the first proposed type, right? 27/05 01:52 keep :: ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b 27/05 01:52 yeah 27/05 01:52 I've almost convinced myself that the proof is impossible 27/05 01:53 but I'm also convinced that the function can't exist 27/05 01:53 completeness of Djinn? 27/05 02:00 :) 27/05 02:00 I mean, I trust djinn 27/05 02:00 but I'd still like to prove it in agda 27/05 02:00 Djinn is complete for intuitionistic propositional formulae 27/05 02:01 copumpkin: seen on #haskell the proof of Not (Not (((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b)) ? 27/05 02:01 oh I got it 27/05 02:01 maybe not 27/05 02:02 hmm, I'm kind of bothered now 27/05 02:05 I have a Set-level hole that I can't seem to fill 27/05 02:07 but the value-level stuff typechecked fine 27/05 02:07 I guess when agda can't figure out something's a function type and you put a ? in as a parameter, it doesn't make it into a hole 27/05 02:10 copumpkin: I wouldn't necessarily expect to be able to prove that that type is uninhabited easily. 27/05 02:12 maybe not, but it seems impossible to do? 27/05 02:13 And if it's classically valid, then you won't be able to prove that at all. 27/05 02:13 unless I'm missing something 27/05 02:13 can I prove that I can't prove it? :P 27/05 02:13 I can make an argument for it 27/05 02:14 Yes. 27/05 02:14 I guess that's what @djinn just did in #haskell 27/05 02:14 * copumpkin sighs 27/05 02:14 If Foo is a (propositional) classical theorem, then Not (Not Foo) is an intuitionistic theorem. 27/05 02:15 yeah 27/05 02:15 but not vice versa? 27/05 02:15 Which means that you can't prove Not Foo. 27/05 02:15 Unless your logic is inconsistent. 27/05 02:15 yeah 27/05 02:15 I guess I just confused agda enough to typecheck, minus a Set hole that couldn't be filled 27/05 02:16 you should be able to prove the unprovability of Foo, but only by formalising provability 27/05 02:16 Right. 27/05 02:16 You'd have to write djinn in agda, more or less. 27/05 02:16 in other words, prove the completeness of djinn 27/05 02:16 isn't showing Not (Not Foo) enough to show that Not Foo can't be proven? 27/05 02:17 I thought about doing that once, but then I looked at djinn, and it was way more complicated than I expected. 27/05 02:17 i.e., if you give me a proof of Not Foo, I'll give you absurdity? 27/05 02:17 oh I see 27/05 02:17 I misread what pigworker said :) 27/05 02:17 djinn has an amusing termination proof (plug PAR 2010 gig) 27/05 02:18 copumpkin: what i made djinn prove in #haskell is quite irrelevant 27/05 02:20 i made it prove ∀ {t b u t1} -> Not (Not (((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b)), but we'd need Not (Not ((∀ {t b u t1 : Set} -> ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b))) 27/05 02:21 and afaiu those two are not equivalent 27/05 02:21 oh 27/05 02:22 well I still have my informal argument that it's not possible, but it may be flawed :) 27/05 02:22 how about forall hmm . ((thingy -> hmm) -> hmm) ? 27/05 02:23 we'd still have to put the quantifiers inside thingy i think, and djinn doesn't allow that 27/05 02:24 What was copumpkin trying to prove? "forall ... Not ..." or "Not (forall ...)"? 27/05 02:25 not (forall ...) 27/05 02:26 is that wrong? 27/05 02:26 No. But it'd be an anti-classical result. 27/05 02:26 Kind of like the one with injective type constructors, or impredicative set. 27/05 02:27 ah 27/05 02:27 the informal statement was "there's no total function of type ..." so the most appropriate interpretation should be not (forall ..) right? 27/05 02:27 not and forall are not readily exchangeable, but this is notnot 27/05 02:27 (Which lets you prove Not (forall P. P \/ Not P)) 27/05 02:27 Saizan: that's what I thought 27/05 02:27 In other words, I don't think you'd be able to prove it unless you found something that would get a new flag for Agda. 27/05 02:29 Or used one of the existing ones. 27/05 02:30 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25737#a25737 is my informal argument 27/05 02:30 in pseudo-haskell/agda without the explicit foralls on type variables 27/05 02:31 If you turn on injective type constructors, you can get 'Not (forall P -> P \/ Not P)', which probably lets you prove the Not (forall ...) version. 27/05 02:31 hmm 27/05 02:31 Since that gives you LEM, and thus classical logic inside the Not. 27/05 02:32 And LEM gives you double-negation elimination, and that should let you go from 'forall ... Not (Not P)' to 'forall ... P'. 27/05 02:34 So you can use djinn's proof of Not (Not P). 27/05 02:34 exactly: negative statements behave classically 27/05 02:35 hm, interesting 27/05 02:36 negative statements have not computational content, so their classical content is as constructive as possible 27/05 02:37 I see 27/05 02:38 does "∀ {F : Set -> Set} -> (∀ x -> Not (Not (F x))) -> Not1 (Not1 (∀ x -> F x))" hold classically? i can't seem to be able to prove it (with vanilla agda at least), Not1 is Not for Set1 27/05 02:39 Classically, yes. 27/05 02:41 Eliminate the Not Not, introduce the Not1 Not1? 27/05 02:41 oh, right. 27/05 02:42 You could permute the Nots with the foralls (turning it into exists in between), but that's probably harder. 27/05 02:42 Boy, the function djinn found sure is large. 27/05 02:46 I wonder if that's really necessary. 27/05 02:46 is it possible to write _|_ -> a without using an absurd pattern? 27/05 02:55 you just did 27/05 02:56 s/write/write a function of type/ :P 27/05 02:57 ultimately, no 27/05 02:57 AFAIK, that's the only primitive falsity elimination 27/05 02:58 You can if you define _|_ = forall a. a. 27/05 02:58 But that won't work so nice. 27/05 02:59 well, so much for my fun proof I guess 27/05 03:03 * copumpkin finds something else "bite-sized" to prove 27/05 03:04 at least I proved that fix is impossible to write :) 27/05 03:04 (unfortunately, it was the world's simplest proof) 27/05 03:14 * copumpkin is still looking for a good way to make a graph type where nodes can express properties about their neighborhoods 27/05 03:17 Oh, I had my thinking backwards. 27/05 03:17 oh the suspense! 27/05 03:19 dolio: how was your thinking backwards? 27/05 03:22 (Not1 (Not1 (∀ {a : Set} ->(Not (Not a) -> a))) <- i can't find a way to prove this) 27/05 03:22 I was thinking you could use Not LEM to prove Not type-of-keep, because LEM implies type-of-keep. 27/05 03:22 heh, no 27/05 03:23 Saizan: It may not be possible. Not (Not classical-prop) is only necessarily intuitionistically valid for propositional statements, not statements in first-order logic or higher. 27/05 03:26 Saizan: In fact, if you could prove that, then the anti-classical proof from injective type constructors would have resulted in a proof of false. 27/05 03:29 i suspected something like that 27/05 03:30 Same with impredicative set in coq. 27/05 03:30 But there's still an option for that, so presumably it's not outright contradictory. 27/05 03:30 As far as anyone knows. 27/05 03:30 so there's no embedding that handles quantifiers? 27/05 03:31 I don't know if there's no embedding, but not that one. 27/05 03:32 "record types not allowed in mutual blocks" :( 27/05 03:32 that seems like a strange limitation 27/05 03:33 http://plato.stanford.edu/entries/logic-intuitionistic/#BasProThe <- hah, that's DNS 27/05 03:34 well, not that, the thing above :) 27/05 03:34 I don't suppose there's a way to get the visibility in types to go backwards? 27/05 03:39 like T x -> (x : Nat) -> ... 27/05 03:40 No. 27/05 03:40 damn, this is going to force my "list" cons type to be backwards :P 27/05 03:41 ah well, worse things have happened 27/05 03:41 "Record types are absolutely not allowed to be recursive so allowing them in mutual blocks would mean some extra (non trivial?) checks to make sure everything is safe." 27/05 03:43 how are (agda) records more powerful than regular data types? 27/05 03:43 They have eta. 27/05 03:43 eta? 27/05 03:45 Normalization of records involves eta expansion. 27/05 03:46 t = record { x = t.x ; y = t.y ; ... } 27/05 03:46 Agda lets me make recursive records, though, so that quote is out of date. 27/05 03:48 Or there's a bug. 27/05 03:48 yeah, a later comment changed it 27/05 03:48 was just curious 27/05 03:48 but the records still can't live in mutual blocks 27/05 03:48 I'm not sure how they accomplished it. It seems like you could eta expand (some) recursive records indefinitely. 27/05 03:50 yeah, they say it can hang the typechecker if you do that 27/05 03:50 records don't have any positivity check 27/05 03:52 Really? 27/05 03:52 yeah, you can't recurse over them anyway 27/05 03:53 That's not true. 27/05 03:58 pff who needs records anyway 27/05 04:02 ... i just proved false. 27/05 04:03 yay! 27/05 04:03 I love it when that happens 27/05 04:03 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25741#a25741 27/05 04:04 i guess the termination checker wasn't that informed some constructors are fake. 27/05 04:05 Yes, I just did that. 27/05 04:05 Submitting a report. 27/05 04:05 :) 27/05 04:05 * copumpkin hopes that one day he too will be able to prove false 27/05 04:06 You can construct non-terminating elements of U without using the constructor, too. 27/05 04:06 yeah, but you can't use them to inhabit \bot 27/05 04:07 Actually, you can. 27/05 04:10 * Saizan wants to see this 27/05 04:13 You have to use a different type. 27/05 04:15 U = U -> A 27/05 04:15 oh, sure, you can just blatantly write fix. 27/05 04:18 ugh, my graph type is not strictly positive 27/05 04:25 maybe this is doomed to failure 27/05 04:25 copumpkin: Coq allows some degree of switching the order of visibility with its notation. 27/05 04:27 But that'd require fancier parsing/syntax than Agda's current mixfix stuff. 27/05 04:27 ah :/ 27/05 04:27 That's how they get nice stuff like { x : A | P x } ==> Sig A (\x -> P x), too. 27/05 04:28 ah :/ 27/05 04:29 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25742#a25742 27/05 04:31 can anyone see a way of making that work? it seems inherently non-positive, but I still want it :P 27/05 04:34 Not off hand. 27/05 04:35 not even sure how usable it would be if I succeeded 27/05 04:36 but it seems like something one might want 27/05 04:36 you could make up an universe for things of type "Graph Node Edge n → Set" :) 27/05 04:39 :O 27/05 04:39 * copumpkin has not the power to create universes of his own 27/05 04:39 maybe I should just settle for separate proofs about graphs 27/05 04:41 so going back to the proof that keep has an impossible type 27/05 04:59 it's possible to prove that some types are impossible, and impossible for others 27/05 05:00 is there a way to determine ahead of time which will be which? 27/05 05:00 or some way of describing features of a type that make it impossible to prove impossible? 27/05 05:01 (in constructive logic, at least) 27/05 05:01 If it's just a propositional statement, and it's classically valid, then you can't prove that it's uninhabited. 27/05 05:03 Because Not (Not P) is intuitionistically valid, meaning you can't prove Not P. 27/05 05:03 That's with all the quantification on the outside in each case. 27/05 05:04 It's not that forall .... P being a classical theorem implies that Not (Not (forall .... P)) is an intuitionistic theorem. 27/05 05:05 * pigworker just bashed out this STLC beta-eta-long-normalizer http://personal.cis.strath.ac.uk/~conor/fooling/Nobby.agda 27/05 13:40 the Nat's are supposed to be de-brujin indexes right? 27/05 14:24 believe it or not, they're just names 27/05 14:25 oh, good, "... | inl y = unq (su y) T (var y)" makes more sense then :) 27/05 14:26 how'd you define _<_ for Brouwer's Ordinals? i.e. data Ord : Set where z : Ord; s : Ord -> Ord; limit : (Nat -> Ord) -> Ord 27/05 16:19 x < z is empty; x < s y = x <= y; x < limit f = Sigma Nat \ n -> x <= f n; x <= y if x is y or x < y 27/05 16:36 thanks 27/05 16:46 oh for that graph structure I wanted, I can just turn off the positivity checker 27/05 22:10 which is evil, but ah well :P 27/05 22:10 You could prove false, and say that it's a graph. 27/05 22:55 dolio: yeah 27/05 23:33 how much can you do with agda's reflection? would it be possible to serialize arbitrary terms? 27/05 23:36 there is a "unknown" term in the agda syntax in agda, so i'd guess it doesn't work for arbitrary terms atm atleast? 27/05 23:47 i translated pigworker Noddy into something easier (on the eyes): http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25776#a25776 27/05 23:49 --- Day changed Fri May 28 2010 copumpkin: you mean serialize to disk? 28/05 00:08 well, get full access to the entire structure, so it could eventually be serialized if someone wrote a Binary-like module for agda 28/05 00:08 you can only get a term that represent the current goal though 28/05 00:10 oh 28/05 00:10 hmm 28/05 00:10 it's something more TH-like than Java-reflection-like 28/05 00:10 stevan: Heh, I thought you meant that you got rid of the 2-letter type names and such. But you meant that you added unicode. 28/05 00:29 :-) 28/05 00:30 * Saizan still needs to work out how the Nats work 28/05 00:31 Even if you can only get the current goal quoted, it's conceivable that you could get it to quote arbitrary terms. 28/05 00:34 By making a combinator that turns an arbitrary term into a goal by wrapping it thinly. 28/05 00:35 Perhaps the type of quoteGoal avoids that, though. 28/05 00:36 isn't there a quote keyword which takes a string and quotes it to an agda term also? 28/05 00:36 there's "quote " which gives you the corresponding QName 28/05 00:38 and quoteGoal doesn't really have a type.. 28/05 00:39 new constructor patterns for records appear to be strict 28/05 00:44 They appear to behave exactly like constructors for inductive data. 28/05 00:46 You can even define recursive records, and write structurally recursive functions by pattern matching. 28/05 00:46 That fails to respect the definitional equality: they should be lazy. 28/05 00:46 And they pass the termination checker. 28/05 00:46 Also, records aren't positivity checked. 28/05 00:49 I filed a report about that last part, but you might want to mention the laziness. 28/05 00:52 will do 28/05 00:57 By the way, Nobby was just the warmup for http://personal.cis.strath.ac.uk/~conor/fooling/DepNobby.agda 28/05 01:12 Good ol' dependent composition. Such a friendly type. 28/05 01:31 you actually using the dependent-ness of it? 28/05 01:33 I don't know. It's hard to see anywhere in DepNobby. 28/05 01:33 I guess it must be used somewhere. 28/05 01:34 Why not be fully general, if you can, though? 28/05 01:34 oh, I have no problem with it 28/05 01:35 was just curious :) I hadn't looked at DepNobby yet 28/05 01:36 sometimes the extra implicit parameters get in the way 28/05 01:37 could (in theory) agda's inference be any better than it is now, by the way? 28/05 01:38 Yes, unless Agda is smarter than I think it is, it's hard to imagine that it specializes to the non-dependent case. 28/05 01:39 Since it needs to figure out that we mean \ {_} -> g when g is written. 28/05 01:39 Or something like that; I didn't go look at the type. 28/05 01:40 yeah, i was referring to something like that 28/05 01:40 copumpkin: i imagine so, pigworker mentioned a possible improvement the other day using Miller unification(?) 28/05 01:41 oh yeah 28/05 01:41 Dependent composition usually specialises to simpler variants by Miller unification (which Agda does, a bit). 28/05 08:16 is there a way to get something like GHC's type families (with pattern matching on type constructors) in agda? 28/05 08:54 it seems like with agda's flexibility you could break parametricity that way 28/05 08:54 There's no pattern matching for Set. But you can make a universe and pattern match on its codes (as I did in DepNobby). 28/05 09:00 ah yeah 28/05 09:02 l. 28/05 10:03 sorry 28/05 10:03 * Saizan wonders if you can have an inductive datatype of transfinite sequences 28/05 15:14 --- Day changed Sat May 29 2010 i seem to be able to define via well-founded recursion (see nats, merge, ham) things that appear to behave like infinite streams (see take): 29/05 00:13 http://code.haskell.org/~Saizan/coord/Ord.html 29/05 00:13 the two things don't quite fit together to me, comments?:) 29/05 00:14 can you prove false with it? 29/05 00:17 i don't think so 29/05 00:21 * Saizan removed the useless postulates 29/05 00:25 does that still work if you remove the ∞ from Stream? (it looks like it should but I'm not sure) 29/05 00:28 yes, but then you need to use well-founded recursion even to define map 29/05 00:29 no, wait 29/05 00:29 the induction principle for Stream should give you map f (y' j; lem with exp; ... | pat = body; ... | pat2 = body2 29/05 01:54 It's a pain to manually copy large intermediate types as a lemma so I can do pattern matching under a lambda 29/05 01:56 * Saizan agrees 29/05 01:58 is there something special about inference for holes that would prevent translating a case as I suggested above? 29/05 01:59 i don't know, but sometimes you have metavariables in the type of the hole, in those cases it probably wouldn't work 29/05 02:00 if you ask on the mailing list you'd probably get some more authoritative answer :) 29/05 02:01 do you know anything about extensional equality, or how to avoid it? 29/05 02:01 I 29/05 02:01 I've been using hypothesis of Extensionality, which then leads to working under lambda and problems with lemmas 29/05 02:02 Saizan: you may have noticed but ... your Stream-like things don't appear to behave quite like streams. http://codepad.org/lRHrNX9F 29/05 02:02 eeeeek 29/05 02:02 napping why do you use extensionality? 29/05 02:02 for now I'm just messing around trying to prove monad laws 29/05 02:03 TheOnionKnight: :O 29/05 02:03 TheOnionKnight: hah, evil :) 29/05 02:03 so some sort of looser equivalence than \== is probably what I want eventually 29/05 02:03 but I haven't stumbled across anything like that in the standard library 29/05 02:04 napping: there's some recent experimental work on using this thing called observational equality in Epigram 2, though that's not really usable yet 29/05 02:04 I wish epigram 2 was ready! 29/05 02:05 Is there some sort of pointwise equality setoid somewhere in the standard library? 29/05 02:06 TheOnionKnight: i guess i'd need some sort of parametricity condition :) 29/05 02:07 it shouldn't be hard to define i think? though i'm not sure if a setoid would be more comfortable, rather than less 29/05 02:08 It might need a universe of types 29/05 02:09 copumpkin: btw, do you have that thing you wanted to prove about streams up somewhere? 29/05 02:09 One odd thing with extensionality or maybe the emacs mode is that refining (ext _) clears all the highlighting, but then retypechecking complains at the _ 29/05 02:12 Saizan: hmm, do you remember more specifically what it was? 29/05 02:13 (sorry chinese food arrived and disconnected me!) 29/05 02:13 copumpkin: about the Omega monad i think 29/05 02:13 oh 29/05 02:13 that was about colists 29/05 02:13 dolio eventually proved it quite elegantly :) 29/05 02:14 I probably have the shitty code lying around though if you still want it 29/05 02:14 napping: ah, i've heard other cases where refining and typechecking didn't quite agree 29/05 02:14 copumpkin: if it's easy to find :) 29/05 02:14 Saizan: http://pastie.org/982656 :P 29/05 02:18 feeling masochistic? 29/05 02:18 copumpkin: thanks :) 29/05 02:18 what are you going to do with it? :o 29/05 02:19 cry? :P 29/05 02:19 http://code.haskell.org/~Saizan/coord/Ord.html <- i seem to have found a way to mix well-founded recursion and coinductive types, i want to see how far it goes 29/05 02:20 oh cool 29/05 02:20 let me see if I can find Colist.NonEmpty 29/05 02:20 since I made that and then deleted it 29/05 02:20 oh, I lost it 29/05 02:21 but it's pretty mechanical 29/05 02:21 i see 29/05 02:24 a bit of a pain, sorry :) 29/05 02:24 well, that's half the point :) 29/05 02:26 not the right kind of pain though :P 29/05 02:26 copumpkin: :O 29/05 02:55 :O :O 29/05 02:56 will agda ever get any sort of type erasure? 29/05 02:58 of course, usually when i ask a question about agda features it's already been done or it's theoretically impossible 29/05 02:59 there's a fair amount of published and implemented research on erasing types and proofs from languages like agda 29/05 03:04 it seems like agda's compiler side isn't getting much love 29/05 03:04 which is fine by me, but it'd be nice to see it become more general-purpose 29/05 03:04 that's my impression too 29/05 03:05 copumpkin: http://code.haskell.org/~Saizan/coord/DiagonalOrd.html <- i got stripe defined, the proof will have to wait :P 29/05 03:59 oh nice, without the custom DSL 29/05 04:00 yeah, just some juggling with sizes 29/05 04:01 Saizan ace 29/05 04:01 I have no idea how this wokrs 29/05 04:01 so sizes are hints to the termination checker that you're getting closer to the goal, even though it can't see it? 29/05 04:01 You're sure that you can't prove false with this? 29/05 04:02 because that was my problem when I translated luqui's code directly 29/05 04:02 it translated into fairly pretty agda but was horribly pink 29/05 04:02 which is why I had to jump through all those horrible hoops to make the special language 29/05 04:02 soupdragon: i've not postulated anything, but i'd have to prove the consistency of Agda to be sure of that 29/05 04:02 yeah I mean specifically this 29/05 04:03 not agda in general 29/05 04:03 copumpkin: i use well-founded recursion on the Acc argument when the productivity checker doesn't like what i write 29/05 04:04 * copumpkin doesn't even know what well-founded means :) 29/05 04:04 * copumpkin looks it up 29/05 04:04 well, it's well-founded on the ordinal i, which gets transformed into structural recursion on Acc, to be more precise, i guess 29/05 04:05 ah, I see 29/05 04:05 soupdragon: how'd you go about checking if we can prove false with this? 29/05 04:06 just like if you can see a way 29/05 04:07 copumpkin: however i'm not so sure what these things actually are.. 29/05 04:07 i could easily prove false if there was an ordinal o such that o < o or equivalently o = suc o, but that's hopefully impossible 29/05 04:09 yay 29/05 06:36 another convert to the Church of Agda 29/05 06:36 Hey, I only read the brochure so far. 29/05 06:36 I'm also picking up C# to join a friend on a project, so my conversion will take a while more. 29/05 06:37 * BMeph counts the seconds before copumpkin starts handing out tambourines... 29/05 06:37 So, what is the nicest way to work with Agda on windows? 29/05 06:47 (no emacs) 29/05 06:47 with emacs 29/05 06:51 :P 29/05 06:51 Bah, I don't want to grow a neckbeard. 29/05 06:52 So is there an ide? or should I just roll with Notepad++ like a gangsta? 29/05 06:59 emacs is the ide 29/05 07:00 many have resisted emacs in the past for agda 29/05 07:00 all have succumbed 29/05 07:00 le sigh. 29/05 07:01 Fine I'll do it, only because I already have emacs installed. I just lost interest within 5 words in the manual. 29/05 07:01 Curious: What does the name agda mean? 29/05 07:01 wow, nad was harsh on my feature request :P 29/05 08:54 I figured out a way around my non-positive type for that weird graph I wanted to build 29/05 08:58 I just give each node access to its neighbors instead of the whole graph 29/05 08:59 not ideal, but it'll work I think 29/05 08:59 filed bug report, based on strict record constructor matching: SR fails! http://personal.cis.strath.ac.uk/~conor/fooling/RecConBug.agda 29/05 11:35 breaks SR in the sense that both goo and goo' normalize to the same term but they don't get the same type? 29/05 14:21 danharaj: the name comes from a swedish song, http://youtube.com/watch?v=oKUscEWPVAM 29/05 14:46 Saizan: yes; goo' is defined to be the normal form of goo. 29/05 15:20 --- Day changed Sun May 30 2010 you're in a maze of twisty little Any datatypes, all alike.. 30/05 01:40 hello 30/05 12:23 hi 30/05 12:46 Saizan: hehe 30/05 12:47 was curious about some Agda, reading tutorial, installing 30/05 12:47 good 30/05 12:47 Saizan: your thoughts 30/05 12:52 on the Haskell / Agda relationship ? 30/05 12:52 well, in agda a lot of what you'd want to do with GADTs and type hackery in haskell is much simpler and saner and i like the ability to prove properties of my code. though i've some occasional fights with the termination checker. 30/05 13:10 oh, and i tend to miss typeclasses :) 30/05 13:11 greetings everyone 30/05 21:09 i'm trying to compile http://www.cs.cmu.edu/~drl/pubs/ml09sectyp/ml09sectyp.tgz 30/05 21:10 and there are dozens of name clashes using the darcs version of agda 30/05 21:10 as in 30/05 21:10 The modules Nat.Nat and Nat clash. 30/05 21:11 when scope checking the declaration open Nat.NatOP public 30/05 21:11 i'm now renaming the modules like Nat to Natm which is ugly 30/05 21:11 has anzone thought of good naming conventions for those cases? 30/05 21:12 hi 30/05 23:25 what does agda wstand for? 30/05 23:26 I'm not sure anyone here is going to know the answer to that. 30/05 23:27 The Agda people here use is Agda 2, which presumably got the name from Agda 1. But I think the implementors aren't even the same. 30/05 23:27 --- Day changed Mon May 31 2010 hello 31/05 01:20 What is the best way to install and set up agda on 64-bit windows? the wiki says that the prebuilt packages are not for 64-bit 31/05 04:10 tried "cabal install Agda"? 31/05 04:11 ah, that could work. 31/05 04:11 Is agda really that closely allied with Haskell? 31/05 04:12 what do you mean?:) 31/05 04:13 Using the same package infrastructure, being able to import haskell functions... what else is there :p 31/05 04:13 Can you derive haskell code in agda? 31/05 04:14 ah, well, it's just that Agda is implemented as an haskell library :) 31/05 04:15 o rly 31/05 04:15 i don't think there's any easy to use code extraction facility, but i didn't look for it 31/05 04:15 though the compiler probably emits haskell 31/05 04:16 When I tried to cabal install agda, I got an error about a file not having a newline at the end. 31/05 04:31 So I downloaded the cabal tarball and fixed it, it looks like it built correctly, but who should I notify about this error? 31/05 04:31 http://hackage.haskell.org/package/Agda <- the mantainer, or maybe directly on the bug tracker 31/05 04:37 i guess it's something windows specific 31/05 04:37 I guess I have to learn emacs now :| 31/05 04:42 I have to say, Agda does not invite me into its home with cookies and milk. 31/05 04:42 It's worth it. 31/05 04:42 You'll miss the features when you go back to write Haskell or whatever. 31/05 04:43 For a second I wasn't sure if you meant emacs or agda :p 31/05 04:43 The features of the emacs mode. 31/05 04:43 Things like "tell me what type of thing I need to put in this hole in my code." 31/05 04:44 that's a feature I did not care for in visual studio. 31/05 04:45 I imagine it's a little less interesting there. 31/05 04:46 yes I suppose agda types are decidedly richer that C++ types. 31/05 04:46 Well, that's not necessarily true if you want to look at things a certain way, but I doubt the visual studio tool would extend in the same way. 31/05 04:48 alright, so are there any tutorials that simultaneously teach agda and emacs? Because I am new to both. 31/05 04:49 Not that I know of. Truth be told, I don't use all that much emacs fanciness (I think). 31/05 04:50 C-n and C-p go down and up. C-f and C-b go right and left. C-e and C-a go to the end/beginning of the line. C-d deletes a character. 31/05 04:52 you really use those to move the cursor? 31/05 04:53 Yes. 31/05 04:53 * Saizan is amazed 31/05 04:53 C-space sets a mark. C-w cuts the stuff between your cursor and the mark. C-y pastes. C-k cuts the rest of the line. C-s starts a forward search, C-r a backwards search... 31/05 04:54 i guess the advantage is that you don't have to move the right hand from its usual position 31/05 04:54 C-x C-s saves C-x C-c quits. And the rest you can probably learn by looking at the agda menu, and the right-click menu for a shed. 31/05 04:55 I'm on a dvorak layout, so f p b n are kind of in awkard positions for moving like that. 31/05 04:55 so  how does agda mode work? What does that even do? 31/05 04:55 you can use the arrow keys too 31/05 04:55 a and e are perfect :p 31/05 04:56 M-a M-e 31/05 04:56 Anyhow, in agda mode, you can type stuff like 'foo x y z = ?' and load the file, and it will type check everything, and if successful you'll get something that looks like 'foo x y z = { }0', where that last part acts sort of like 'undefined' in Haskell, in that it will take on any type, but you'll be able to enter commands to manipulate the definition in various ways. 31/05 05:00 Like, there's a command for 'expand the definition to do case analysis on x'. 31/05 05:00 Or, 'tell me what type the hole needs to be'. 31/05 05:00 Or 'see if this term is the right type, and fill it in if so.' 31/05 05:01 And other stuff I use less, like 'try to figure out what the term should be by yourself.' 31/05 05:01 so how do I turn on agda-mode? 31/05 05:07 http://wiki.portal.chalmers.se/agda/agda.php?n=Main.README-2-2-6 31/05 05:09 I think that should say. 31/05 05:09 Evidently you run "agda-mode setup". 31/05 05:10 I did that in the command line. Now how do I invoke the agda-mode commands in emacs? Are they now always available? 31/05 05:11 How did you start emacs? 31/05 05:11 'emacs' in the command line 31/05 05:12 It'll probably auto-load it if you start it with 'emacs Foo.agda'. 31/05 05:12 ah 31/05 05:12 and how would I load it otherwise? 31/05 05:12 I think you can do meta-x and type in agda-mode. 31/05 05:13 ah yes, I think you're right. 31/05 05:13 I think I need haskell-mode too, as it says it cannot load haskell-indent 31/05 05:13 yup 31/05 05:13 what does ~ stand for in paths? Specifically for windows, would that be the toplevel directory of the drive? e.g. C:\ or F:\? 31/05 05:22 ~ is your home directory. 31/05 05:24 I'm not sure what it means on windows. Probably something inside Documents and Settings. 31/05 05:24 huh, alright everything seems to be in order. Thanks guys. 31/05 05:31 That's enough wrestling tonight X_X 31/05 05:31