/home/laney/.irssi/irclogs/Freenode/2010/#agda/February.log

--- Log opened Mon Feb 01 00:00:10 2010
-!- EnglishGent is now known as EnglishGent^afk01/02 19:57
--- Day changed Tue Feb 02 2010
-!- RichardO_ is now known as RichardO02/02 05:13
-!- RichardO_ is now known as RichardO02/02 05:33
-!- mikael is now known as kmb02/02 12:38
-!- RichardO_ is now known as RichardO02/02 18:29
-!- RichardO_ is now known as RichardO02/02 19:00
-!- opdolio is now known as dolio02/02 21:53
stevanso quiet here lately :-/02/02 23:14
MissPiggysshhh! I'm trying to concentrate02/02 23:15
MissPiggyI just about had it too02/02 23:15
stevan:-)02/02 23:15
MissPiggyto be honest, ever since I found that progapedia page on agda -- the mystery is gone02/02 23:15
MissPiggyhave you not write anything new in Agda??02/02 23:16
MissPiggywe should have more epigram parties02/02 23:17
MissPiggywhere people figure out all the syntax...02/02 23:17
stevani'm doing some reflection stuff now as part of a project02/02 23:18
MissPiggyoh cool I love that reflection02/02 23:18
MissPiggytell me about it?02/02 23:18
stevanhttp://wiki.portal.chalmers.se/cse/pmwiki.php/CS/QuantifierEliminationAndFunctionalProgramming02/02 23:19
MissPiggywow02/02 23:19
MissPiggybut isn't quantifier elimination infeasible?02/02 23:20
MissPiggylike it takes a billion years to run it02/02 23:20
stevani don't know02/02 23:20
MissPiggyI'm thinking geometry or something02/02 23:21
MissPiggythat sounds really cool though, I hope you show of here every so often :P02/02 23:21
stevanwe are focusing on dense linear orders first and if that works out it would be cool to do presburger02/02 23:22
stevanthat's partly why i'm here, i recall pumpkin talking about someone working on extending data.rational... i was wondering if he or somebody else knew more how that is going...02/02 23:23
MissPiggy:( dense linear orders02/02 23:24
MissPiggyit's the first ex. in my model theory book and I can't do it!!!02/02 23:24
MissPiggyI spent months on that02/02 23:24
stevanin agda or?02/02 23:25
MissPiggyno02/02 23:27
stevani don't get the quant elim stuff yet, i plan to spend the rest of the week trying to understand it... i got some code. if you want, we could discuss it later...02/02 23:34
stevanhave you been coding anything yourself?02/02 23:36
MissPiggynot really no, let me think well I tried to do some comp. linguistics in Coq02/02 23:37
MissPiggybut it's been so long that I seem to have run out of that fuel that makes everything you type live02/02 23:37
stevan:-/02/02 23:39
stevanhow's that epigram2 thing going? you played around with it, yes?02/02 23:44
MissPiggyyeah it's pretty cool & confusing02/02 23:44
MissPiggygoing to keep an eye on it there's a lot of stuff I want to try out02/02 23:45
MissPiggybut right now I don't understand the syntax well enough02/02 23:45
stevani keep reading these blog posts which promise more info, but they all raise more questions than they answer for me... :-/02/02 23:47
MissPiggyI think that's the point! isn't it?02/02 23:48
stevan:-) perhaps. i gotta sleep; good night.02/02 23:56
--- Day changed Wed Feb 03 2010
--- Day changed Thu Feb 04 2010
glguyHello :)04/02 08:03
copumpkinohai2u!04/02 08:03
glguyDo you agda much?04/02 08:03
copumpkinhaven't recently, but I love it when I have time04/02 08:04
copumpkinI'm not very good at it but I get addicted to it periodically04/02 08:05
glguyDoes what I pasted look remotely reasonable?04/02 08:06
copumpkinyeah04/02 08:09
copumpkinthe first parameter in the heap is the max value?04/02 08:09
glguycorrect04/02 08:12
copumpkinsleep-deprived me thinks it looks pretty decent :)04/02 08:12
copumpkinplanning on adding more?04/02 08:12
glguyyeah, I have to do the deleteMin yet04/02 08:13
copumpkincool04/02 08:13
glguyand I'll write a wrapper for the heap time that hides all the messy indexes04/02 08:13
glguyif you just wanted to use it to get elements out of and put them in04/02 08:13
copumpkinthen all you need is a foreign export haskellcall :P04/02 08:13
copumpkinand we'll have us a verified heap04/02 08:13
glguyI feel like there is probably a better approach than my less-than-eq max/min lemma pile04/02 08:14
glguywith the wrapper I can do: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=17075#a1707704/02 08:18
copumpkinit needs the inj1 inj2 breakdown?04/02 08:19
copumpkinI guess I've seen it needing that kind of thing before04/02 08:19
copumpkinoh I guess there's no way around it is there04/02 08:19
glguyI'm not sure what you're asking04/02 08:20
copumpkinit was stupid, sorry :)04/02 08:20
glguyI guess in this case the operator approach is still clear: insert a (H h) = [ H , H ]′ (insertHeap a h)04/02 08:21
copumpkinah, that operator exists? :)04/02 08:27
copumpkinI haven't used \u+ enough I guess04/02 08:28
copumpkinafter this you should prove the disjoint set union-find thing :P04/02 08:29
copumpkinspecifically the amortized time complexity :P04/02 08:29
--- Day changed Fri Feb 05 2010
glguy_Can someone tell me if I am approaching this proof correctly? http://codepad.org/HSzBCYUB I'm trying to show that my balanced tree insert function preserves the balanced tree property (or returns a full tree)05/02 07:01
glguy_I've done the algorithm where the proof was embedded in the data type, but I wanted to try where the proof was an external object05/02 07:02
dolioI think you could do without X05/02 07:14
dolioOr at least, not make it a datatype.05/02 07:15
dolioThe proofs look right, eyeballing it.05/02 07:16
glguy_I only created that X datatype because I wasn't sure how to deal with that last proof otherwise05/02 07:17
glguy_suggestion for what its type would be?05/02 07:17
glguy_(without the X)05/02 07:17
dolioWell, I mean you could write 'X : (A : Set) (n : N) -> Tree A -> Set ; X A n t = BalancedTree A n t \uplus FullTree A n T', I think.05/02 07:19
dolioI think that's the same.05/02 07:19
glguy_one thing I wanted to capture was that all of the inj1's were balanced and all of the inj2's were fulls05/02 07:21
dolioOh, right, insertTree returns a sum...05/02 07:22
dolioI guess X isn't a bad idea, then.05/02 07:23
glguy_I've been able to prove my property on trees of fixed depth05/02 07:25
glguy_but I didn't know how to prove it in the general case05/02 07:25
dolioYou mean you proved it for, like, 5?05/02 07:26
glguy_Do I have it right then when I get: Goal: X (suc (suc .n))05/02 07:26
glguy_      (insertTree (Branch F₁ t₁ t₂) | insertTree t₁)05/02 07:26
glguy_yeah, well, 0..205/02 07:26
glguy_the | insertTree   part means that I need to case on that expression to look at the left side of the bar, right?05/02 07:27
dolioProbably. Your proof is likely to have similar structure to the function you're proving about.05/02 07:28
dolioAlthough since in that case it's a with on the recursive call, it might be that you should do a with on the inductive case in your proof.05/02 07:31
dolioWhich will tell you what the recursive call was, since your proofs are indexed by the result.05/02 07:32
glguy_this is one of those functions that blows up agda's case expander05/02 07:37
stevanhi all. glguy: i saw you were playing with trees; you might want to have a look at Data.AVL in the stdlib and http://web.student.chalmers.se/groups/datx02-dtp/ (especially ulf's 2-3 trees and the revised LLRB trees).05/02 10:15
stevancopumpkin: i recalled you talked about someone working on extending the support for rationals in the stdlib, you don't happen to know how that is going?05/02 10:20
copumpkinstevan: I don't know, but NAD does. I mentioned that I'd done a little bit of work on it and he mentioned that someone else had done a lot more and that the additional work was going to get merged in soon05/02 13:18
stevancopumpkin: thanks, this "soon" was a while ago, yes?05/02 13:50
copumpkinyeah, a couple of months now05/02 13:50
glguyis --universe-polymorphism what turns "Set" into a function of some sort?05/02 18:01
npouillardglguy: yes05/02 18:02
glguyWhat type does it have, exactly?05/02 18:02
npouillardSet can still be used as Set zero, but the general form is Set ℓ where ℓ of type Level05/02 18:03
npouillardMerely something like Set : ∀ (ℓ : Level) → Set (suc ℓ)05/02 18:04
glguySet : Level -> ?05/02 18:05
npouillardSet ℓ : Set (suc ℓ)05/02 18:06
glguyah, right05/02 18:06
copumpkinglguy: you can still use it with no parameters though... it's a bit of a hack05/02 18:07
copumpkinoh npouillard already said that05/02 18:07
glguyI think he was talking about "Set zero"05/02 18:07
copumpkinso yeah, writing Set is equivalent to Set zero, and you can't always eta reduce on it :P05/02 18:08
MissPiggyEpigram has <= !!!05/02 18:13
npouillardMissPiggy: what you mean?05/02 18:18
MissPiggythey have implemented the <= view from the left gadget05/02 18:19
MissPiggy> help <=05/02 18:20
MissPiggy<= [<comma>] <eliminator> - eliminates with a motive.05/02 18:20
dolioI'm pretty sure that was already in there.05/02 19:07
dolioJust with a different name.05/02 19:08
MissPiggywell I just did darcs pull for the first time in weeks05/02 19:09
MissPiggytoday05/02 19:09
MissPiggyso it could have been in there for a while05/02 19:10
dolioThey've been writing lots of patches.05/02 19:10
dolioAnyhow, I haven't recompiled since that first day. But I'm pretty sure there was an "elim" tactic described as "eliminates with a motive".05/02 19:10
dolioI don't have the executable anymore, though.05/02 19:11
dolio"Added Buddy Holly states for holes (crying, waiting, hoping)"05/02 19:12
glguyis there a way to do my last definition "insert-full-fails" without so much refl juggling? http://codepad.org/0jodzfpl05/02 21:51
glguyI feel like I'm making this harder than it has to be my not understanding some common idiom somewhere05/02 21:51
Saizanmh, maybe it could improve with EquationalReasoning05/02 22:37
glguyhttp://codepad.org/F7p4VLdN   I didn't work out how to use equational reasoning for it, yet, but I did simplify05/02 23:30
--- Day changed Sat Feb 06 2010
opdolioEquational reasoning is a nice notation for strings of uses of transitivity.06/02 00:33
opdolioOops, he's not here anymore.06/02 00:33
SmerdyakovIs anyone interested in helping me test a platform for hosting web applications written in Ur/Web, my programming language which supports type-level computation?06/02 13:36
--- Day changed Sun Feb 07 2010
alisecabal: cannot configure Agda-2.2.6. It requires base ==4.2.* && ==4.2.* For the dependency on base ==4.2.* && ==4.2.* there are these packages: base-4.2.0.0. However none of them are available. base-4.2.0.0 was excluded because of the top level dependency base -any07/02 01:30
alisehalp.07/02 01:30
dolio#haskell!07/02 01:31
dolio:)07/02 01:31
MissPiggybut I just came from haskell07/02 01:31
alisedolio: i am _not_ going to let this diverge07/02 01:31
alisei am a total IRCer07/02 01:31
aliseyou fail at typing. plz go directly to stderr :D07/02 01:32
* alise suspects copumpkin and dolio of being the same person... SECRETLY.07/02 01:32
copumpkinwe actually have the same first name, too07/02 01:32
copumpkinso maybe it's true07/02 01:32
copumpkinbut I don't think so07/02 01:32
aliseCopumpkin "Dolio" Agda07/02 01:32
dolioI'm not sure I've ever used an Agda from hackage.07/02 01:34
MissPiggythose AIM meets must be pretty fun07/02 01:35
MissPiggythey're going to japan next07/02 01:36
aliseIs Agda.TypeChecking.Serialise meant to freeze my entire system when I compile it?07/02 04:10
dolioAgda does seem to take a lot of memory to compile for some reason.07/02 04:12
dolioHow much do you have?07/02 04:12
aliseThis box, a measly one gig. 23% used...07/02 04:12
aliseBut it freezes my entire system; can't even Ctrl-C the compile.07/02 04:13
aliseThat seems excessive if it's just some serialisation thing.07/02 04:13
dolioThat's odd.07/02 04:13
aliseIt has compiled 123 out of 191 modules by that point without problems, after all.07/02 04:13
aliseThe Glorious Glasgow Haskell Compilation System, version 6.10.4, installing with `cabal install agda`, Ubuntu 9.04, blah blah blah boring07/02 04:13
aliseSo, anyone have any clue what would cause compilation to freeze my ststem on Agda.TypeChecking.Serialise? Does it contain some evil magic code that interacts with optimisation or something?07/02 15:32
npouillardalise: which version of GHC do you have and have you a 64 bits?07/02 15:33
alise6.10.4; aye07/02 15:34
npouillardhave you tried to clean and recompile07/02 15:34
npouillardwhich OS ?07/02 15:34
aliseI did "cabal install agda", hard-rebooted my system and tried again; the exact same result.07/02 15:35
aliseUbuntu 9.04.07/02 15:35
npouillardWhich version cabal was trying to install 2.2.6 ?07/02 15:36
aliseYes.07/02 15:36
npouillarddid previous versions works better ?07/02 15:37
aliseI haven't tried; first time on this system.07/02 15:38
alise{-# LANGUAGE OverlappingInstances,              TypeSynonymInstances,              IncoherentInstances,              ExistentialQuantification,              ScopedTypeVariables,              CPP              #-} {-# OPTIONS_GHC -O2 #-}07/02 15:38
alise-O2 plus hideously scary type synonym extensions?07/02 15:38
aliseI bet that's the culprit.07/02 15:38
aliseI wonder if it's possible to force -O1.07/02 15:39
npouillardI don't think so07/02 15:39
npouillardthese extensions are indeed scray07/02 15:39
npouillard*scary07/02 15:39
npouillardcabal install agda-executable-2.2.407/02 15:40
aliseRight, and -O2 is known to do things like this iirc.07/02 15:40
aliseThat's why cabal does -O1 by default now...07/02 15:40
alisenpouillard: is there anything in 2.2.6 i'd miss?07/02 15:40
aliseor any backwards-compat breaking changes?07/02 15:40
npouillardyes some changes like universe-polymorphism and that the latest version of the stdlib depends on it07/02 15:41
aliseMaybe I'll instead try and get 2.2.6 working, then. 2.2.4 might do the same thing to my system again...07/02 15:42
npouillardalise: yes07/02 15:42
--- Day changed Mon Feb 08 2010
Saizanwhat type would you use for sets over some type T?08/02 21:25
npouillardSaizan: Finite sets or abritrary sets. For the latter I would simply suggest "T → Set"08/02 21:28
Saizanmh, arbitrary ones in theory, it's yo define an entailment relation _|-_ : (T -> Set) ->  T -> Set could work08/02 21:31
Saizanit's hard to make it decidable with that type though, right?08/02 21:32
npouillardright08/02 21:32
Saizani could use T -> Bool i guess08/02 21:33
npouillardSaizan: to be precise it depends on what you have to decide this08/02 21:33
npouillard∈-dec S = ∀ t → Dec (S t)08/02 21:36
dolioWhat's "sets over a type" mean? Types that contain some subset of the elements?08/02 21:36
* npouillard thinks that an agdabot would help08/02 21:36
Saizandolio: the type of the values that represent some subset of the elements08/02 21:39
dolioAh, then it's Σ T P, where P should be prop-valued so to speak.08/02 21:41
dolioIn that P t should have 0 or 1 elements.08/02 21:41
Saizanno, that's some subset of T08/02 21:42
Saizani want the type for what you'd denote 2^T in classical mathematics08/02 21:42
npouillardSaizan: literally T → Bool ?08/02 21:43
Saizanhence why T -> Bool might fit08/02 21:43
dolioOh. Then T -> Bool or T -> Prop, or something like that.08/02 21:43
dolioT -> Bool would be decidable subsets of T, I think.08/02 21:43
Saizani guess i've to pick one and see if i get into some problems08/02 21:44
Saizanit's all about denotational semantics for concurrent constraint programming, if you're curious :)08/02 21:44
doliohttp://math.andrej.com/2005/05/16/how-many-is-two/08/02 21:45
dolioThat might be useful.08/02 21:45
Saizanthanks08/02 21:45
dolioOr perhaps just confusing. I'm not sure I really grok it myself.08/02 21:45
dolioAgda doesn't really have anything analogous to Ω anymore, though. Only Set, which isn't really the same.08/02 21:46
dolio(If it ever really did.)08/02 21:47
Saizanehm, what would you use for finite subsets? :)08/02 23:46
MissPiggyFin n ?08/02 23:46
MissPiggyandrej is so awesome08/02 23:47
dolioFin n -> T would probably work.08/02 23:53
dolioAlthough that doesn't rule out duplicates.08/02 23:53
SaizanFinite : (D -> Set) -> Set08/02 23:58
SaizanFinite u = ∃ λ n -> ∃ λ (f : Fin n -> D) -> ∀ P -> P ∈ u -> ∃ λ i -> f i ≡ P08/02 23:58
Saizan..so that i can use it as a restriction on (D -> Set)08/02 23:58
MissPiggywhat is this for??08/02 23:59
MissPiggywhy not just Fin n?08/02 23:59
dolioFin n isn't a finite subset of some other type.08/02 23:59
MissPiggywhy does that matter08/02 23:59
--- Day changed Tue Feb 09 2010
dolioOr, it isn't the type of finite subsets of some other type.09/02 00:00
Saizanit matters because i'm working with a relation on this other type D09/02 00:01
dolioOn the Strength of Proof Irrelevant Type Theories has a questionable typing rule.09/02 00:02
MissPiggythe whole thing is questionable :P09/02 00:04
dolioIt has strong impredicative sums.09/02 00:05
MissPiggythe other issue is that benjamin is INCREDIBLY smart09/02 00:05
dolioWhich let you encode something similar to Prop : Prop.09/02 00:05
MissPiggyso I was never sure if it was just that I didn't get it09/02 00:05
--- Day changed Wed Feb 10 2010
dolioAt long last, my proof that A × (B × C) ≅ (A × B) × C is complete.10/02 02:42
dolioAnd checking the module only take 75% of my memory.10/02 02:43
Saizanis there an idiom to write down an isomorphism more compactly? http://code.haskell.org/~Saizan/Agda/NatCat.html10/02 19:02
npouillardAFAIK not that much10/02 19:08
npouillardData.Sum.map is also known as [_,_] and there the 'id' function in (Data.)?Function10/02 19:10
HairyDudeTheory question: does Martin-Löf typeability imply strong normalisation? or is the termination check not an "essential" part of type checking?10/02 19:13
HairyDudespecifically, does M-L justify Markov's principle by proving that unbounded search terminates?10/02 19:15
Saizanmap f g = [ inj₁ ∘ f , inj₂ ∘ g ] , actually, but ok :)10/02 19:29
stevanhello. is there a way around the following problem: when i got a goal which depends on some (mixfix) functions from a parametrized module then the goal because very unreadable because it includes the module name, module parameters and written in prefix style...10/02 19:42
stevans/because/becomes/10/02 19:42
Saizani'd like to know that too10/02 19:51
stevani wish there was some way to toggle between the current way it works and less noisy goals which simple ignore printing module names and module parameters...10/02 19:55
stevansimilar to how you can toggle between showing hidden args in goals or not10/02 19:56
dolioSaizan: I've been using a record: http://code.haskell.org/~dolio/agda-share/categorica/html/Category.html#222610/02 20:14
dolioThat html is out of date, but it's still similar.10/02 20:14
copumpkinI wonder if all your memory usage is from the serialization phase10/02 20:15
copumpkinlike the mailing list message10/02 20:15
dolioQuite possibly. When I have a type error, it catches it relatively quickly.10/02 20:45
dolioI can tell when I don't, even though it spends an additional minute or two thinking before it accepts.10/02 20:46
Saizanwe need to put typechecking agda on the shootout and get dons to optimize it10/02 21:59
npouillard:)10/02 21:59
MissPiggySaizan genius :D10/02 22:01
dolioHairyDude: Formal type theories don't need "termination checks", because they deal in terms such that well-typing implies strong normalization.10/02 22:02
HairyDudedolio: right. so M-L typeability is undecidable?10/02 22:03
dolioAgda's termination checker is necessary because it lets you write direct recursive functions, and uses syntactic checks to try and be sure it could be translated to such a set of core terms.10/02 22:03
HairyDudeSaizan: hehe, nice idea10/02 22:04
MissPiggyM-L typeability is undecidable??10/02 22:04
HairyDudedolio: oh, right. you get explicit recursion operators for each data type then?10/02 22:05
HairyDude(when you get to the point of adding data, anyway)10/02 22:05
MissPiggyif something passes the agda termination checker, then in theory, you could replace that with explicit recursion operators10/02 22:05
MissPiggy(eliminating dependent pattern matching goes into some more detail on this construction)10/02 22:06
MissPiggyagda doesn't do that though, the 'in theory' bit is good enough10/02 22:06
MissPiggywhat was that about M-L though ?10/02 22:06
HairyDudeMissPiggy: well I was thinking, if a term has to be strongly normalising to be typeable, that implies some sort of termination check, which is undecidable. but that's only if you make it possible to define unrestricted recursion, like agda does10/02 22:08
dolioI guess the extensional version of his type theory might have undecidable type checking, as is often reported of extensional type theories.10/02 22:08
MissPiggy"if a term has to be strongly normalising to be typeable" -- no10/02 22:08
HairyDudeextensional type theory is a weird concept10/02 22:09
MissPiggy"termination check, which is undecidable" -- no10/02 22:09
HairyDudeMissPiggy: yes, I already know I was wrong :)10/02 22:09
dolioWell typed terms are strongly normalizing, but not all strongly normalizing terms are well-typed.10/02 22:09
--- Day changed Thu Feb 11 2010
stevanhi. what's this: http://www.e-pig.org/darcsweb?r=Pig09;a=headblob;f=models/IMDesc.agda ?11/02 10:19
npouillardstevan: looks like some unfinished work about playing with universes11/02 10:22
stevanwhat does it do in the epigram2 repository tho?11/02 10:23
dolioThey're experiments with modeling the behavior of epigram2 in agda.11/02 10:25
stevanok, interesting.11/02 10:26
SmerdyakovCan I recruit anyone to help me test a platform for developing & hosting web applications written in Ur/Web, my programming language which supports type-level computation?11/02 14:53
MissPiggythis is kind of scary11/02 17:09
MissPiggyum and offtopic11/02 17:10
MissPiggyaanyway Recently a team of mathematicians have been trying to republish the famous series of papers called “SGA”, or “Séminaire de Géométrie Algébrique”.  This was largely the work of Alexander Grothendieck, who had refused to let Springer Verlag republish the original version.11/02 17:10
MissPiggyhttp://golem.ph.utexas.edu/category/2010/02/grothendieck_said_stop.html11/02 17:10
MissPiggyhttp://sbseminar.wordpress.com/2010/02/09/grothendiecks-letter/11/02 17:18
glguyHow do I avoid lots of these lemmas? lemma3 : ∀ {a b c} → b ≡ c → a ⊔ b ≡ a ⊔ c    \n     lemma3 refl = refl11/02 20:16
npouillardglguy: try the "rewrite" feature11/02 20:17
glguyDo you know of any examples of this feature?11/02 20:18
glguyI've not seen it yet11/02 20:18
npouillardfoo a b c b≡c rewrite b≡c = ...11/02 20:18
npouillardthey are some in the tests11/02 20:18
npouillardgrep for rewrite11/02 20:18
glguyOK, Data.List.Any.Properties uses it11/02 20:18
npouillardglguy: a simpler thing is to simply pattern match over refl but rewrite is handy anyway11/02 20:19
glguynpouillard, my refl is on an expression11/02 20:20
glguyso I can't pattern match11/02 20:20
glguyhttp://codepad.org/xKPqBWN211/02 20:20
glguyheight a == height b, for example11/02 20:20
glguynpouillard, rewrite is /exactly/ what I needed11/02 20:26
glguythank you11/02 20:26
npouillardglguy: do you know inspect and _with-≡_ from module on prop eq?11/02 21:09
glguyI know of them11/02 21:31
glguybut they don't help me resolve cases where I have some assumption:   this thing | some case11/02 21:31
glguywhich is what I was running into11/02 21:31
glguyor...11/02 21:32
glguyshould I be rewriting with the resulting equality?11/02 21:32
glguyr with-== eq rewrite eq = ?11/02 21:32
glguynpouillard, are you still there (I was away to lunch , sorry about slow response)11/02 21:34
dolio'rewrite a==b ...' is equivalent, I believe, to: with a | a==b \n ... | .b | refl ...11/02 21:34
glguyhttp://codepad.org/SXTSnC1411/02 21:36
glguyusing rewrite I was able to refine my last definition a lot11/02 21:36
glguydolio, ah, that would make sense11/02 21:37
glguyI think that I wasn't using inspect properly, it might have done what I wanted11/02 21:37
dolioI rarely use inspect.11/02 21:38
dolioBut maybe I just don't understand its uses that well.11/02 21:38
dolioThe thing with refining things with matching on refl, is that if you have (complex-expr-1)==(complex-expr-2), you need to give one of the expressions a name, so that it can be refined into the other one when matching on refl.11/02 21:39
dolioRewrite makes that a little easier.11/02 21:39
glguyneeding to give them a name is how I was ending up using lots of little lemmas11/02 21:40
dolioYeah, you can use with, as well, but that leads to long (vertically) functions.11/02 21:41
MissPiggyConor told me to STFU11/02 22:55
copumpkin:o11/02 22:58
copumpkinwhere11/02 22:58
MissPiggyhttp://www.reddit.com/r/dependent_types/comments/b0vb7/agda_vs_coq_by_wouter_swierstra_with_some_input/c0kepog?context=311/02 22:58
MissPiggyah there's an EDIT: now11/02 22:59
stevanbtw, epigram2 has/will have tactics, yes? are/ will be they written in epigram2?11/02 23:03
MissPiggythere's a tactic system in the haskell implementation, which I think works a bit like HOL light -- at least in a vauge sense11/02 23:05
MissPiggysome examples already like elimination with a motive and propositional simplification in the Pig09 repo11/02 23:05
stevani'm not familiar with HOL light; aren't HOL light's tactics written in ocaml?11/02 23:07
MissPiggyyeah11/02 23:07
stevanso you mean epigram2's tactics are written in haskell?11/02 23:07
MissPiggywell the whole thing is implemented in haskell (although there's some agda files too),  there is a monad (called ProofState) which has basic machinary for tactics and they implement higher level stuff in terms of that11/02 23:11
stevanbut as i understand it, one still programs in the "core" of epigram2 atm... eventually there will be more syntax etc and then one won't have direct access to the haskell implementation? will there be an epigram2 interface to the tactic machinary then or will it still be done in haskell?11/02 23:15
MissPiggyno there is an interface right now that has nothing to do with haskell except being implemented in it11/02 23:17
MissPiggysorry what I said about HOL ocaml was sort of wrong and confusing11/02 23:18
stevanso epigram2 tactics are written in epigram2? :-)11/02 23:19
MissPiggy:[11/02 23:19
MissPiggyright now it is all implemented in haskell11/02 23:19
MissPiggyI am sure that lots of reflective tactics will be done in epigram later -- but wel, it's just my best guess, someone that's actually on the project would kno11/02 23:20
MissPiggyI'm talking about Pig0911/02 23:21
MissPiggythere's also Epi 1 from ages ago, and who knows what else is going on11/02 23:21
edwinbSome form of reflection will definitely be useful11/02 23:21
edwinbI think the way it's designed all of these things are possible, just needs someone to do it ;)11/02 23:21
stevanyeah, Pig09 is what i call epigram2. what is the official name anyways?11/02 23:22
edwinbEpigram :)11/02 23:22
* MissPiggy still doesn't really understand the syntax of Pig09/Cochon.. so it's hard to do stuff with it :/11/02 23:22
edwinbThe syntax is a moving target at the minute. It'll only get easier.11/02 23:22
stevaneverybody talks about reflection replacing tactics, but are there any good examples of this happening? i only know of the ringsolver?11/02 23:24
* MissPiggy doesn't have a clue abot reflection /replacing/ tactics11/02 23:27
MissPiggyyou know how to prove that sin(1 + x^2) is continuous?11/02 23:27
MissPiggyin school they tell you11/02 23:28
MissPiggy let epsilon > 0, ....11/02 23:28
MissPiggyand it takes an hour each time11/02 23:28
MissPiggyin CoRN, they do it like in real math  -- it's the composition of continuous functions so reflection proves it automatically11/02 23:28
--- Day changed Fri Feb 12 2010
stevani asked the same question on reddit12/02 00:15
MissPiggylink?12/02 00:15
MissPiggyeh I will find it12/02 00:16
stevansame thread as before12/02 00:16
glguyIs this an "abuse" of Relation.Unary.\sub= ?  insert-balanced : {A : Set} (a : A) → Balanced ⊆ (Balanced ∘ insert a)12/02 01:37
yinhello!12/02 02:24
* glguy finally finishes the independent proof that the non-dependently typed algorithm for inserting and deleting from balanced trees maintains the balanced property12/02 09:35
dolioPer your previous question, Balanced ⊆ (Balanced ∘ insert a) is probably a little werid.12/02 09:36
dolioWeird, even.12/02 09:36
dolioIf you ask me, at least.12/02 09:38
glguyi wouldn't have asked if i didn't suspect :)12/02 09:38
dolioMaybe it's worth it to get higher-order points, though.12/02 09:44
glguyThis code is certainly not polished, but it might be interesting to someone else going through the same learning process as me12/02 09:49
glguyhttp://github.com/glguy/agda-balanced-tree-example12/02 09:49
dolioAre these AVL-ish?12/02 09:53
glguyno12/02 09:53
glguythey always insert at the left-most position at the lowest level12/02 09:54
dolioOkay.12/02 09:54
dolioDid you say you'd already done a version where the trees were correct by construction?12/02 09:54
glguyMy intention is to write a heap next12/02 09:54
glguyI did a Haskell version where they were12/02 09:55
glguyusing GADTs12/02 09:55
dolioWas that easier? It seems like it might be.12/02 09:55
glguymuch easier, I've been working on this in agda for a while12/02 09:55
glguyI just typed it up in haskell12/02 09:56
glguybut I don't know much agda12/02 09:56
glguybut12/02 09:56
dolioI suspect it'd be similarly easier in Agda.12/02 09:56
glguyI wanted to prove that the heap property was preserved12/02 09:56
glguyand not just the balanced property12/02 09:56
glguymy primary motivation for doing this in agda is to have something more interesting to prove than tautologies in agda as an exercise :)12/02 09:59
MissPiggyanyone tried making SPTs in Epigram?12/02 13:23
npouillardSPTs ?12/02 13:24
MissPiggythis stuff http://www.cs.nott.ac.uk/~pwm/12/02 13:24
npouillardMissPiggy: hum, ok12/02 13:25
MissPiggync12/02 13:45
MissPiggyoops sorry12/02 13:45
MissPiggycan't install agda :/12/02 13:48
MissPiggydoes anyone know about this?12/02 13:49
MissPiggycabal: cannot configure QuickCheck-2.1.0.3. It requires ghc -any12/02 13:49
MissPiggyThere is no available version of ghc that satisfies -any12/02 13:49
npouillardMissPiggy: hum... which version of GHC do you have, and how did you installed it12/02 13:52
MissPiggy6.12.1,12/02 13:52
MissPiggyI must have installed it from the binary on haskell.org12/02 13:52
MissPiggywhat's funny is this is probably the 20th time I've installed agda and I still don't have a clue how to stop it from going wrong :/12/02 13:52
npouillardI just switched to 6.12 yesterday and simply done a "cabal install" in the agda darcs repository12/02 13:53
MissPiggyokay I will try and get 6.12, thanks for the idea12/02 13:54
npouillardhuh, you just said you have a 6.12.1. By 6.12 I meant 6.12.*12/02 13:55
MissPiggyoh12/02 13:55
npouillardI have a 6.12.1 as well actually12/02 13:56
npouillardinstalled with ArchLinux12/02 13:56
* MissPiggy spent the whole of the last two weeks trying to install Arch.. 12/02 13:56
MissPiggy(and failed)12/02 13:56
npouillardYou where not confortable with linux previously or did you had specific issues?12/02 13:58
MissPiggyoh I just have terrible luck12/02 13:58
npouillardOK, that's a bit sad, I never had problems with it.12/02 13:59
MissPiggyalso I can't darcs get http://code.haskell.org/Agda/  :/12/02 14:00
MissPiggyit is a valid HTML page but darcs says it's not a valid repo12/02 14:00
MissPiggythis seems to work though: http://code.haskell.org/Agda/repository-before-conversion-to-darcs-2-format/12/02 14:01
Saizanah, you've an old darcs then12/02 14:01
SaizanMissPiggy: what does cabal --version says, btw?12/02 14:01
MissPiggycabal-install version 0.8.012/02 14:02
MissPiggyusing version 1.8.0.2 of the Cabal library12/02 14:02
Saizanok, that should be fine, but the error above is weird12/02 14:02
MissPiggyit's kind of funny because I would have thought -any would be lie a wildcard that always holds12/02 14:03
Saizanyeah12/02 14:03
* MissPiggy downloads TWO THOUSAND PATCHES12/02 14:03
MissPiggyone by one12/02 14:04
MissPiggyohh12/02 14:04
MissPiggymaybe I should cabal install darcs12/02 14:05
MissPiggythen use it to get the newer agda12/02 14:05
MissPiggy(that didn't work)12/02 14:05
Saizani think the two repos are just one a mirror of of the other12/02 14:06
SaizanMissPiggy: oh, i think i've understood the error you got above, it's about the ghc haskell library, which comes with ghc the compiler, your installation got broken somehow12/02 14:09
MissPiggyahh12/02 14:10
SaizanMissPiggy: if you paste ghc-pkg list we might be able to repair it12/02 14:10
MissPiggymmm12/02 14:10
MissPiggymy pkg-list is colorful12/02 14:10
MissPiggythere are some things in red such as ghc-6.12.1 & bin-package-db-0.0.0.012/02 14:11
Saizana common situation is when you've the same version of some package in both the global and user databases12/02 14:11
Saizanwhich confuses ghc-pkg and cabal12/02 14:11
Saizanyeah, the red ones are the broken ones12/02 14:11
MissPiggyhttp://www.pasteit4me.com/11202312/02 14:12
MissPiggypretty confusing but cabal seems to be at the bottom of it12/02 14:12
Saizanyeah12/02 14:12
Saizanit seems you've reinstalled Cabal-1.8.0.2 globally12/02 14:12
Saizanreplacing the one shipped with ghc12/02 14:13
MissPiggy;_;12/02 14:13
Saizanbut the ghc package was built against the old one, and so now it's broken12/02 14:13
Saizanthe somewhat good thing, is that you can keep your current cabal-install and resintall only ghc12/02 14:14
MissPiggyhey I think that is working now!12/02 14:16
MissPiggyoh no12/02 14:16
MissPiggyAgda-2.2.6 depends on haskell-src-1.0.1.3 which failed to install.12/02 14:16
MissPiggya bit closer anyway12/02 14:16
MissPiggythis is dodgy12/02 14:17
MissPiggyConfiguring binary-0.5.0.2...12/02 14:17
MissPiggyWarning: This package indirectly depends on multiple versions of the same12/02 14:17
MissPiggypackage. This is highly likely to cause a compile failure.12/02 14:17
MissPiggypackage binary-0.5.0.2 requires array-0.3.0.012/02 14:17
MissPiggypackage containers-0.3.0.0 requires array-0.3.0.012/02 14:17
MissPiggyafaict array-0.3.0.0 = array-0.3.0.012/02 14:17
MissPiggyso I dont know what's its talking about conflict for12/02 14:17
MissPiggyshould I build a new ghc myself, uninstall the old one: Then install my new one?12/02 14:18
Saizanyou've two array-0.3.0.0 packages installed12/02 14:18
Saizanthat's a problem12/02 14:18
MissPiggyoh I see12/02 14:19
MissPiggywhat do yuo do in that situation?12/02 14:19
Saizanyou could try ignoring the warning, anyhow12/02 14:19
MissPiggywell it is right in its prediction -- the stuff doesn't build12/02 14:19
Saizani'd ghc-pkg unregister --user array-0.3.0.012/02 14:19
Saizanthat will break some packages, that you'd need to reinstall12/02 14:20
MissPiggyand I can find the broken ones in ghc-pkg list?12/02 14:20
Saizanhowever, i'd probably unistall ghc and install one from scratch, using a prebuilt binary12/02 14:20
MissPiggy(there are no reds in there right now)12/02 14:20
MissPiggyby that worked!!12/02 14:21
Saizanheh :)12/02 14:21
MissPiggythe way*12/02 14:21
Saizanyeah, you'll see the broken ones in ghc-pkg list or check, if there are any12/02 14:21
MissPiggyyay12/02 14:22
Saizangot Agda installed?:)12/02 14:25
MissPiggyyes12/02 14:25
Saizannice12/02 14:25
MissPiggythank you!!12/02 14:25
Saizanno problem :)12/02 14:26
MissPiggylol I love quail mode or whatever it's called for inputting unicode12/02 14:29
MissPiggy<List A > = <Mu <1> <+> (vs A <×> vz) >12/02 14:45
MissPiggynil : forall (A : SPT z) -> El z ε <List A >12/02 14:45
MissPiggynil _ = <in <inl <void> > >12/02 14:45
MissPiggycons : forall (A : SPT z) -> El z ε A -> El z ε <List A > -> El z ε <List A >12/02 14:45
MissPiggycons _ x xs = <in <inr <pair <pop x > , <top xs > > > >12/02 14:45
MissPiggythat's from the paper about SPTs12/02 14:45
Saizanwhat is El?12/02 14:58
MissPiggythat's the interpretation, it gives values of a type12/02 15:06
MissPiggyhttp://www.pasteit4me.com/11202412/02 15:07
Saizanah, i see12/02 15:10
MissPiggyhow do you turn on universe polymorphism? :|12/02 15:19
Saizan{-# OPTIONS --universe-polymorphism #-}12/02 15:20
MissPiggy:(((12/02 15:20
MissPiggyI don't think I have a new enough version of agda?12/02 15:20
MissPiggyit just thinks Level is not in scope12/02 15:20
Saizanyou've to import it12/02 15:21
Saizanopen import Level12/02 15:22
Saizanassuming you've setup the searchpath for the standard library12/02 15:22
MissPiggyhaha oh man this sucks12/02 15:22
MissPiggyI will have to get that standard library12/02 15:22
MissPiggythanks12/02 15:22
MissPiggyah I can just paste that file into mine12/02 15:23
Saizani guess that works too :)12/02 15:24
stevanwhy don't you like the std lib?12/02 15:24
MissPiggybecause I don't know how to install it12/02 15:24
guerrillaMissPiggy: i usually just untar into the directory of the project im working on then set up the search path accordingly12/02 15:25
stevanso you got a copy of the std lib for each project you work on?12/02 15:26
guerrillastevan: yeah, which is not many since i'm still learning :)12/02 15:27
stevanone way to deal with backwards compat i guess :-)12/02 15:27
guerrillayep, i guess that's the other reason - seems like the stdlib isn't a stable API yet12/02 15:28
stevanMissPiggy: (custom-set-variables '(agda2-include-dirs (quote ("." "<your-path>/lib/src/")))12/02 15:29
--- Day changed Sun Feb 14 2010
guerrillais identifier definition and resolution formalized in any of the LC or TT?14/02 20:01
MissPiggyhuh14/02 20:11
MissPiggyyou mean like  x := foo14/02 20:11
MissPiggythen x x --> foo foo14/02 20:11
MissPiggy?14/02 20:11
guerrillayeah or lisp's (define...)14/02 20:11
guerrillait seems to me that as soon as you introduce such a construct, you introduce general recursion unless you have rules to explicitely disallow self-reference14/02 20:12
MissPiggyI don't really know any good treatmment of that but you do have to be careful about it (or you can break subject reduction, for example)14/02 20:12
MissPiggyjust make x := x a scope error14/02 20:12
guerrillai think i will14/02 20:13
guerrilla:)14/02 20:13
guerrillajust thought that one of the calculi might actually include := or define or something in its syntax and semantics for it14/02 20:14
guerrillaoh well14/02 20:14
guerrillabtw, sorry, what is "subject reduction" - i haven't read that term before14/02 20:14
MissPiggyif t : T and t --> t' then we should hope that t' : T, if NOT t' : T then we have broken subject reduction14/02 20:15
MissPiggylike 3 + 3 : Int reducing to "six" : String would not be good14/02 20:15
guerrillaright right, i've read that, but didn't recall the name14/02 20:17
guerrillathanks14/02 20:17
kmcguerrilla, many small languages that are studied formally have an expression like «let x = a in b» for x variable, a,b expressions, which can be defined to be non-recursive (x is in scope for b but not a)14/02 22:41
guerrillakmc: right, that makes sense - builds a heirarchy of scope. hadn't occured to me that that'd be different than the lisp-style macros or agda's =. makes sense though. thanks for the input14/02 22:48
--- Day changed Mon Feb 15 2010
guerrillaif anyone asks a question similar to mine about name binding, i'd recommend http://www.cs.cmu.edu/~drl/pubs/lzh08focbind/lzh08focbind-tr.pdf15/02 17:09
guerrillaFocusing on Binding and Computation -- Daniel R. Licata, Noam Zeilberger, Robert Harper15/02 17:10
guerrillaindirectly linked to by agda wiki: http://www.cs.cmu.edu/~drl/pubs.html15/02 17:10
lpjhjdhso I'm just learning agda and am trying to show that all terms in a language of numbers and addition are well typed15/02 17:15
lpjhjdhnot sure how to phrase it as a type, I tried: allwell : forall e -> isTrue (welltyped e) where isTrue is like the one from the agda tutorials15/02 17:15
lpjhjdhso both my terms will produce true, and I can just fill it in with True's inhabitant15/02 17:17
Saizanthat's one way15/02 17:22
Saizanotherwise you could define welltyped as a gadt, rather than a function Term -> Bool15/02 17:22
lpjhjdhand that would only construct terms from well-typed constituents?15/02 17:22
Saizanallwell would construct a value of that gadt for each term15/02 17:23
lpjhjdhah15/02 17:23
lpjhjdhI can't actually seem to get my initial attempt to work, I'm using the definition of True as a record with no fields15/02 17:24
Saizanso you've record True where; data False where; isTrue : Bool -> Set; isTrue true = True; isTrue false = False; ?15/02 17:25
lpjhjdhyeah15/02 17:26
lpjhjdhwhen I use _ it colors it yellow (can't determine type?) and when I use record{} I get "Expected record type, found isTrue when checking that the expression record{} has type isTrue (cata (const true |+| uncurry _∧_) (inn (inr ⟨ n0 , n1 ⟩)))"15/02 17:26
lpjhjdhobviously cata (const true |+| uncurry _∧_) will always be true since it turns numbers into trues and then pluses just and their subterms together15/02 17:26
lpjhjdh|+| is [_,_]15/02 17:27
Saizanwell that error means that it can't reduce (cata (const true |+| uncurry _∧_) (inn (inr ⟨ n0 , n1  ⟩)))15/02 17:27
Saizanto true15/02 17:27
Saizanin that scope15/02 17:27
lpjhjdhah, what would cause that to occur?15/02 17:28
Saizanwell, if some of those functions pattern match on their arguments, and their arguments happen to be a variable15/02 17:29
Saizanso you've to do case analysis to such a variable to make that application reduce15/02 17:29
Saizans/to such/on such/15/02 17:30
lpjhjdhokay15/02 17:30
lpjhjdhthanks15/02 17:30
Saizanor you might do case analysis on the result of that application15/02 17:30
lpjhjdhso to do it the other way, would it be something like: okPlus : {t0 t1 : μ NatPlusF} → Welltyped t0 → Welltyped t1 → Welltyped (inn (inr ⟨ t0 , t1 ⟩))15/02 17:32
lpjhjdhokNum : {n : ℕ} → Welltyped (inn (inl n))15/02 17:33
lpjhjdhdata Welltyped : μ NatPlusF → Set where15/02 17:33
lpjhjdhsorry, did it backwards15/02 17:33
lpjhjdhhpaste seems to be dead15/02 17:33
Saizani'm not sure i understand that snippet15/02 17:34
lpjhjdhto use a gadt, something like?  data Welltyped : NatPlus -> Set where okNat : {n : Nat} -> Welltyped (nat n); okPlus : {t0 t1 : NatPlus} -> Welltyped t0 -> Welltyped t1 -> Welltyped (t0 + t1)15/02 17:36
lpjhjdhand then: allwell : (e : NatPlus) -> Welltyped e15/02 17:36
Saizanyeah15/02 17:39
Saizanassuming data NatPlus : Set where nat : Nat -> NatPlus; _+_ : Nat -> Nat -> NatPlus15/02 17:40
lpjhjdhawesome, thanks!  That is much more attractive than using isTrue15/02 17:40
Saizanyeah, it's quite nicer to work with15/02 17:42
MissPiggyit's not really a GADT though more like an inductive-family right?15/02 17:44
Saizanoh, i were using the two terms as synonyms15/02 17:45
Saizanwhat is the difference? that the gadt is indexed over types rather than values?15/02 17:46
Saizans/the gadt is/GADTs are/15/02 17:46
lpjhjdhso if I want to make an operation semantics with plus reducing only when it's arguments are values, do I need to make a notion of value or normal and then construct such a step from two normal subterms?15/02 17:50
MissPiggywell I just think of GADT in haskell15/02 17:50
lpjhjdhlike: Plus : forall {n m} -> Normal n -> Normal m -> n + m --> (the value of n) mathematical+ (the value of m)15/02 17:51
Saizanlpjhjdh: you mean writing an interpreter for potentially open terms?15/02 17:51
lpjhjdhwhat does potentially open mean?15/02 17:52
Saizanthat they could have free variables in them15/02 17:53
MissPiggyare you writing a type checker?15/02 17:53
Saizanah, no, i see what you're asking15/02 17:54
lpjhjdhI have no notion of variables, working with something as simple as your NatPlus above.15/02 17:54
Saizanyou want to write the one-step reduction for _+_ ?15/02 17:54
lpjhjdhMissPiggy: eventually, first I need to get the hang of how to express stuff as types, I'm used to working with isabelle15/02 17:54
MissPiggyoh15/02 17:54
MissPiggyso right now you are making  (1) untyped syntax   (2) well typed syntax  ?15/02 17:54
lpjhjdhso I have left and right reduction like: PlusL : ∀{n m} → n ⟶ n' → n +a m ⟶ n' +a m15/02 17:54
MissPiggytype checker would be a function (1) -> (2) + error15/02 17:55
lpjhjdhfor a step relation: data _⟶_ : μ NatPlusF → μ NatPlusF → Set where15/02 17:55
MissPiggyahh you are doing semantics in that very general way that also covers general recursive programs15/02 17:55
MissPiggyif you have a simple language like nat you can take the easy (cheating) route :P15/02 17:55
MissPiggybut maybe you don't want to15/02 17:55
lpjhjdhMissPiggy: yeah, I'm actually only focusing on preservation right now, so not even full type safety.  In the context of interpreters as coproducts of algebras15/02 17:57
lpjhjdherr, languages rather15/02 17:57
MissPiggyyou can get preservation and all that stuff for free if you have a simple language like that15/02 17:57
Saizanmaybe what you want is "Plus : forall {n m} -> Normal n -> Normal m -> Normal (n + m)"15/02 17:58
lpjhjdhSaizan: I'd really like to say that n + m can then step to something normal15/02 17:59
lpjhjdhSaizan: maybe "Plus : forall {n m} -> Normal n -> Normal m -> PlusTerm n m --> Normal (n + m)"?15/02 18:00
MissPiggywait a second15/02 18:00
MissPiggyhave you defined untyped syntax15/02 18:00
MissPiggyi.e. something like15/02 18:01
MissPiggydata Syntax : Set where15/02 18:01
MissPiggy Constant : Nat -> Syntax15/02 18:01
Saizanlpjhjdh: ... -> (n + m) ⟶ o \x Normal o ?15/02 18:01
MissPiggy _+_ : Syntax -> Syntax -> Syntax15/02 18:01
MissPiggy _*_ : Syntax -> Syntax -> Syntax15/02 18:01
MissPiggy etc15/02 18:01
MissPiggy?15/02 18:01
Saizanlpjhjdh: where \x is the pair type constructor15/02 18:01
MissPiggy tt : Syntax15/02 18:01
MissPiggy ff : Syntax15/02 18:01
MissPiggy if_then_else_ : Syntax -> Syntax -> Syntax -> Syntax15/02 18:01
lpjhjdhis that to say that n + m reduces to o and that, that reduction is normal?15/02 18:02
lpjhjdhMissPiggy: yeah, it's basically NatPlus that Saizan defined above15/02 18:02
Saizanthat o is normal, yeah15/02 18:02
lpjhjdhokay, thanks, I'll try that15/02 18:02
MissPiggyokay so why not define a typed syntax next15/02 18:02
Saizanlpjhjdh: here Plus would be a function, not a constructor15/02 18:03
MissPiggyyou can either:  Define evaluation on untyped syntax (as a relation that can potentially get stuck)15/02 18:03
MissPiggyor you can define typed syntax, and a total function that evals it15/02 18:03
Saizanthe untyped syntax produces only welltyped terms here though15/02 18:03
lpjhjdhMissPiggy: I need to have potentially untyped terms because I want to do it for arbitrary coproducts15/02 18:03
lpjhjdheventually15/02 18:03
MissPiggywhat15/02 18:03
lpjhjdhSaizan: hmm, I'm not sure how to get the value part of n and m since I'm saying they are terms15/02 18:06
Saizanvalue part?15/02 18:06
Saizanwhat they reduce to, you mean?15/02 18:07
lpjhjdhto do (n + m)15/02 18:07
lpjhjdhyeah15/02 18:07
Saizani thought that would be stored inside Normal m and Normal n15/02 18:07
lpjhjdhoh, I was thinking normal meant it couldn't step, that's a good idea15/02 18:08
Saizanwell, not having variables if you can't step you should have a value, afaiu15/02 18:09
lpjhjdhif I were to have variables would I then just need a context from variables to numbers or something?15/02 18:10
Saizanor maybe Normal (n + m) would accept a term made of _+_ applied to variables?15/02 18:11
lpjhjdhI see.  I need to play around with some definitions I think.  Thanks for taking the time to help me out15/02 18:13
Saizannp15/02 18:13
Saizani'm not an expert in the field either, so take everything i say with caution :)15/02 18:13
Saizans/either//15/02 18:14
lpjhjdhhaha, all the suggestions seem to work out perfectly so far15/02 18:14
SaizanMissPiggy: do you remember where that STLC typechecker+interpreter featured on the FP lunch blog lives?15/02 18:19
MissPiggyyeah there's also one in the epigram paper View from the Left15/02 18:19
MissPiggyhttp://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=29115/02 18:20
Saizanyeah, i recall a repo with the code of that one, but not the actual URL15/02 18:20
jlouis915/02 19:02
--- Day changed Tue Feb 16 2010
Saizansince i've been working with decidable predicates i've almost stopped thinking and just used the types to fit things together, not sure if that's good though16/02 02:36
kmci don't even see the code anymore16/02 04:10
guerrillaWas the book "Programming in Martin-Löf's Type Theory" (out of print) replaced by something else?16/02 10:18
* guerrilla doesn't understand why such a good book would go out of print otherwise16/02 10:18
--- Day changed Wed Feb 17 2010
glguyIs there something I can read that will help me understand how to use Induction.WellFounded?17/02 00:27
Saizanthe idea is that if you can build an Acc x for your x, then you can structurally recurse over it to keep the termination checker happy, which gives you more freedom than structural recursion over x, generally17/02 00:35
Saizani don't know of a tutorial though17/02 00:36
glguywould I be able to construct such an Acc for a pair of lists showing that the sum of their sizes gets smaller?17/02 00:37
glguySupposing I wanted to write a merge function over two sorted lists17/02 00:37
Saizani think so, your _<_ would compare the sum the sizes17/02 00:38
glguyyeah17/02 00:38
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=21167#a21167 <- the standard natural example17/02 00:43
glguyhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=21167#a2117317/02 00:51
glguystep 1 (operating on single lists by length)17/02 00:52
dolioI have a file where I used well-founded induction to prove the soundness of propositional logic.17/02 01:25
doliohttp://code.haskell.org/~dolio/agda-share/logic/html/Propositional.html17/02 01:25
dolioI just wrote it down as a single recursion combinator, though. It's not all modular like Induction.WellFounded is.17/02 01:25
dolioIt's a slightly more exciting example than natural numbers with <, though.17/02 01:26
Enriquegda17/02 05:56
copumpkin:o17/02 05:56
* glguy boggles as agda simply /accepts/ the obvious merge implementation17/02 18:00
glguyOK, I was wrong that the termination checker understood my merge, BUT I was able to write it using Induction.Lexicographic17/02 19:05
glguyand it actually doesn't look too bad17/02 19:05
glguyhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=21444#a2144417/02 19:28
copumpkinglguy: now do it for colists!17/02 19:54
glguyAgda: is it a dependently-typed programming language? Is it a Turing-tarpit? ¯\(°_0)/¯17/02 22:51
Saizangetting slowed down by termination proofs?17/02 22:53
glguyby the desire to prove all sorts of properties :)17/02 22:54
dolioIt's not a Turing tarpit.17/02 22:54
dolioMaybe a total tarpit.17/02 22:54
glguy:)17/02 22:54
Saizanhehe :)17/02 22:59
* glguy has the horrifying realization that the structure of any proof of a property of the function defined using the lexicographic induction module will likely need to use lexicographic induction17/02 23:34
--- Day changed Thu Feb 18 2010
* Saizan found a "bug" in the epitome18/02 03:32
copumpkin?18/02 03:32
Saizanthe description of the computational behaviour of "branches" looks ill-typed and doesn't seem match the implementation, though i might be reading this wrong18/02 03:34
rla_why does emacs editor from agda on windows open files as read only?18/02 11:34
rla_only sane way to write agda programs is to use emacs?18/02 13:10
guerrillarla_: i use vim and makefiles...18/02 13:16
guerrillaso, im curious - how much of Ana Bove's thesis is incorperated into agda? i just started reading it... seems related to what glguy has been going through recently18/02 13:52
Saizanhah, i was wondering where i should've reported or sent a patch for the epitome thing, but it seems this channel works :)18/02 14:11
copumpkinI can understand many of the calls for papers that go on the agda mailing list18/02 14:40
copumpkinbut a conference on education??18/02 14:40
guerrillamathematics education? teaching constructive mathematics?18/02 14:44
guerrillaseems appropriate18/02 14:44
copumpkinhttp://snapplr.com/c17z18/02 14:45
copumpkinas appropriate as a conference on "stuff"18/02 14:46
copumpkinI dunno, if it's relevant to agda people it seems like the very very edge of relevance :)18/02 14:46
copumpkinI get the impression that someone showing up to that conference and giving a talk on the use of a theorem prover to teach math wouldn't be very understood18/02 14:47
guerrillareally?18/02 14:47
guerrillai could see it..18/02 14:47
guerrillathere were lots of courses in teaching alg/ds w/ scheme and lisp back in the day18/02 14:48
guerrillaor pascal for that matter18/02 14:48
guerrillagranted, thats in cs and not math..18/02 14:48
guerrilla*shrug*18/02 14:48
copumpkinI just think the adult learning, business learning, etc. might consider "math education" to mean "teach me algebra! what? I'm talking about x + y, not groups and rings! what the hell are those? nobody uses those in the real world"18/02 14:49
copumpkinbut maybe I'm just projecting :P18/02 14:49
guerrillaprobably18/02 14:50
* copumpkin erases his prejudices and starts from scratch18/02 14:50
guerrillaive heard calculus is more and mroe taught via proofs these days18/02 14:50
copumpkincan't comment on that :)18/02 14:50
copumpkinah well, time for class18/02 14:52
guerrillalater18/02 14:52
copumpkinciao :)18/02 14:52
--- Day changed Sun Feb 21 2010
cadshey, are there any basic agda tutorials that can show me how agda works by proving a simple theorem from algebra, say?21/02 01:40
cadsSome basic induction would be nice, like  \sum_{k = 0}^{n} k = n (n +1) / 2.21/02 01:45
Saizanhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials <- the first one has some proofs by induction over naturals not so far in it21/02 01:59
Saizanor you could look at the code from the standard library21/02 02:00
aliseIn the stdlib, things like monoids are modelled as records; no type parameters or anything. So, then, how do you specify "some Monoid" in a type signature?21/02 02:00
alisei.e. the equivalent of (Foo a) => ... in Haskell.21/02 02:00
Saizan(m : Monoid) -> .. and use Carrier m in place of a21/02 02:01
cadsthanks Saizan! My brain's been hitting a wall with even starting to mess with agda.21/02 02:02
cadsIt's saying, "Am need step by step introduction for understanding"21/02 02:02
aliseSaizan: So then consider "(Foo a, Bar a) => ...".21/02 02:03
aliseDo we do:21/02 02:03
alise(a : Foo) -> (b : Bar) -> (a \equiv b) or something?21/02 02:03
aliseFurthermore, can we make these arguments implicit? If not, passing around various monoids and the like will, I expect, be a pain in the posterior.21/02 02:03
Saizanyou could parametrize your module over them21/02 02:04
Saizanrather than each function, so you don't have to pass them around so much21/02 02:04
aliseYou still have to pass a whole big bag o' them at some point, which is irritating when we have a facility like implicit arguments that would work if only it were Monoid m, no?21/02 02:05
Saizanand, you could do (Foo.Carrier a \== Bar.Carrier b) though maybe you'd prefer using IsMonoid and make the sharing work by construction21/02 02:05
Saizanno, it wouldn't work? implicit arguments are not typeclasses21/02 02:06
aliseYes, I know that.21/02 02:06
aliseBut if you consider Monoid : Set -> Set... where the result is a record type using that set, I don't see why you couldn't use implicit arguments.21/02 02:06
aliseAdmittedly I don't know how Agda does implicit arguments.21/02 02:06
Saizanwell, there's nothing preventing Monoid to be defined that way21/02 02:07
Saizanbut, whick "Monoid X" value would agda fill in for an implict argument of type Monoid X? does it just pick the nearest one around?21/02 02:08
Saizanyou could easily have monoid1 and monoid2 both fitting that type and not being equal21/02 02:09
alisewell of course implicit arguments cannot be inferred in all cases21/02 02:10
aliseThat seems blindingly obvious to me, as you can make anything an implicit argument.21/02 02:10
alise/Most/ of the time, though, there'll be only one.21/02 02:10
Saizani'm saying that it couldn't get inferred most of the time21/02 02:10
Saizanbut you can try :)21/02 02:11
aliseWhy not? Most of the time, a certain type will only have one monoid, no?21/02 02:11
Saizanimplicit arguments don't really work by guessing like that, ime21/02 02:11
Saizanthey only get filled when there's one obvious solution, e.g. for indexes of some other argument type21/02 02:12
Saizanfoo : {n : Nat} -> Fin n -> X; i : Fin 1; then foo i works because the 'n' can be read off the type of i21/02 02:14
alisewell, if there's only one Monoid a...21/02 02:14
alisebut you're right it would be an extension21/02 02:14
aliseI'm playing with solutions to the issue in my own pet (vaporware) dependent language...21/02 02:15
Saizantypeclasse do this for you because there's a guarantee there's only one matching instance and a procedure to find it21/02 02:15
aliseyeah, but typeclasses suck :)21/02 02:16
Saizanthey are pretty limited by the fact that you've to be able to find a solution, yeah :)21/02 02:17
Saizanthough explicit instantiation can be done with newtypes21/02 02:17
alisewhat we could have is a marker that a certain definition can be "filled in" for an implicit thingy of that type21/02 02:18
alisebut that feels "impure", somehow, to depend on such theoretically unnecessary markers21/02 02:18
aliseit's a non-trivial problem!21/02 02:19
alisemaybe the IsFoo kin are the best; that lets you do {IsFoo blah} -> {IsBar blah} -> ...use blah here..., right?21/02 02:19
aliseAlthough, no, wait, you need to specify the operations and the like in the IsX call.21/02 02:19
alise'tis a non-trivial problem21/02 02:19
Saizanyou could put the operations inside the record21/02 02:20
Saizaninstead of having them as parameters of it21/02 02:20
Saizan(keeping the type outside)21/02 02:20
Saizanthough that's kind of arbitrary, there's already people on #haskell that would like to index Monoid by the operation too :)21/02 02:21
aliseyeah that's what I originally said—but you can't use that as an implicit param21/02 02:22
aliseor, can you use IsX as an implicit param either? I guess not.21/02 02:22
alisePhooey. When my language is older than your language, it'll beat your language up. :P21/02 02:22
Saizanit's harder to compare functions in a satisfying why, but if you keep it intensional it's still decidable21/02 02:23
Saizan*way21/02 02:23
aliseWhy do you need to compare them?21/02 02:25
Saizanjust like you need to compare types to find the right instance21/02 02:26
aliseAh; you mean equality, not ordering.21/02 02:26
Saizanyeah21/02 02:26
Saizanbtw, i think i'd like to try such a language :)21/02 02:29
Saizanthough this filling in mechanism has to be kept really predictable, imo21/02 02:30
Saizanalise: you might want to look at Coq, i think they've implemented something typeclass-like with tactics, they might have extended it too21/02 02:32
aliseyeah a good look at Coq is on my todo list21/02 02:33
alisereally i don't need any specific mechanism21/02 02:34
aliseI know that typeclasses are the Wrong Thing and I know that specifying trivial monoid instances all the time is the Wrong Thing, but apart from that I have no clue what the Right Thing is21/02 02:35
Saizanabstacting such things at a larger scope is fairly nice when you can21/02 02:36
Saizanyou tend to need qualified names or renaming if you use multiple e.g. monoids in the same code though, which is not ideal21/02 02:37
aliseyeah is it just me or is agda's solution to lots of _+_s just to rename them on import?21/02 02:41
alisethat is so weak.21/02 02:41
alisewb.21/02 02:42
alise<alise> yeah is it just me or is agda's solution to lots of _+_s just to rename them on import? <alise> that is so weak.21/02 02:42
alisein case you didn't see21/02 02:42
alise(re: qualified names/renaming)21/02 02:42
Saizan_you see some of that21/02 02:43
Saizan_if you're using two monoids on the same type you're screwed anyway, though21/02 02:47
Saizan_there's not much difference between the effort needed to specify the operation and passing the whole record in21/02 02:50
alisemaybe what we need is to be able to import two values with the same name, but disambiguable based on type21/02 02:53
aliseand have Monoid m; if we always name it monoid, then we can just import all monoids and specify "monoid" (which we could sugar away).21/02 02:53
aliseYou have to specify if you have multiple monoids on the same type, but that's not too common to matter much. You can always name one something other than "monoid".21/02 02:53
aliseThis also lets you import multiple _+_s.21/02 02:54
aliseIt's a bit of a hack, though.21/02 02:54
aliseA kludgey hack.21/02 02:54
copumpkinbut if both monoids are over the same set, how can you disambiguate on type?21/02 02:54
copumpkinI guess you don't try21/02 02:54
Saizan_ehm, yeah, we could do that, which is basically a small bridge between records and typeclasses21/02 02:55
alisecopumpkin: exactly21/02 02:56
alisecopumpkin: which is why it's based on name21/02 02:56
alisename one monoid and the other altMonoid21/02 02:56
aliseof course, basing it on name is /really/ ugly.21/02 02:57
Saizan_maybe we just need better code editor and/or better serialization formats for code21/02 02:57
alisewhat's that got to do with this :)21/02 02:57
aliseif the resulting code is still ugly automation doesn't help21/02 02:57
Saizan_there's no abstraction or expressiveness gained here, it's just nicer to look at21/02 02:58
Saizan_so a different format could make it better, without requiring weird things in the language21/02 02:58
aliseSurely this is a problem to be solved with syntactic sucrose.21/02 02:59
Saizan_maybe limiting oursevels to static text is the problem :)21/02 02:59
aliseYeah, so say we all. I dabbled in two-dimensional syntax as recently as... well, days ago, but right now I'm content with Unicode-drunk linear syntax.21/02 03:00
aliseMostly because two-dimensional notation often just seems to be inconsistency for the sake of it.21/02 03:00
Saizan_i wasn't thinking of other dimensions21/02 03:02
Saizan_i was thinking of a format that more aware of binding and less of names21/02 03:02
aliseSeems a bit vague.21/02 03:03
Saizan_or that just wisely hides unimportant parts and help you fill them as you go, without incorporating automagic searches into the language21/02 03:04
aliseThen again, I'm one to talk.21/02 03:04
Saizan_yeah, i'm just tossing ideas around21/02 03:04
aliseMe with the grandoise progamming language/OS visions. :)21/02 03:04
--- Log closed Sun Feb 21 11:54:38 2010
--- Log opened Sun Feb 21 11:54:43 2010
-!- Irssi: #agda: Total of 22 nicks [0 ops, 0 halfops, 0 voices, 22 normal]21/02 11:54
-!- Irssi: Join to #agda was synced in 67 secs21/02 11:55
--- Day changed Mon Feb 22 2010
alisewhy is ⊤ used as the name for the unit type? that isn't what ⊤ means :P22/02 01:42
aliseat least in type theory22/02 01:42
dolioWhat does it mean in type theory?22/02 01:51
alisehttp://en.wikipedia.org/wiki/Top_type22/02 01:51
aliseThe top type in type theory, commonly abbreviated as top or by the down tack symbol (⊤) is the universal type--that type which contains every possible object in the type system of interest. The top type is sometimes called the universal supertype as all other types in any given type system are subtypes of top. It is in contrast with the bottom type, or the universal subtype, which is the type containing no members at all.22/02 01:51
alisefor any type a, ⊥ ≤ a ≤ ⊤22/02 01:52
aliseso the unit type is quite an awful lot of values away from being ⊤ :P22/02 01:52
copumpkin#1 as a type was ugly, maybe?22/02 01:53
dolioWell, Agda doesn't really have any subtyping.22/02 01:53
copumpkinand it's against the rules to use actual words as names in the standard library22/02 01:53
dolioAnyhow, the definitions of ⊥ and ⊤ come from logic.22/02 01:53
alisedolio: That doesn't mean it isn't a misuse.22/02 01:53
aliseAgda doesn't have the law of the excluded middle, either, but you don't name some random thing not-p-and-not-p :P22/02 01:54
alisedolio: For logic, yeah, it's reasonable.22/02 01:54
aliseBut it's still really confusing considering how much type theory Agda has in it.22/02 01:54
dolioWell, it has plenty of logic in it, too.22/02 01:54
aliseYeah, but this /is/ in the type system. :P22/02 01:55
dolioSo is the logic.22/02 01:55
aliseClearly the unit type should be renamed to ⊡.22/02 01:56
aliseIt is a box containing exactly one thing.22/02 01:56
dolioexists t. t is isomorphic to the unit type, anyway.22/02 01:56
aliseThen the enemies of English, and the enemies of type theory, can both be happy!22/02 01:56
alisedolio: Well, that's true.22/02 01:56
aliseActually I think you just convinced me it's okay with that.22/02 01:57
copumpkin22/02 01:57
dolioUnless you have a language where all types are empty, I suppose...22/02 01:58
dolioBut that doesn't seem like it'd be very useful.22/02 01:58
dolioBut then the unit type would also be empty... so I guess they still would be isomorphic.22/02 01:59
Saizanif you use coercions with your subtypes, then the above descriptions say that \top is final and \bot is initial, just like they are in agda22/02 02:13
Saizan(which is another way to say that they are isomorphic to exists t. t and forall t. t i guess?)22/02 02:14
guerrillaso that Ur/Web language is apparently dependently typed (http://www.impredicative.com/ur/demo/)22/02 11:28
guerrilla(the language used in that web platform mentioned on the last front-page post on LtU)22/02 11:29
--- Day changed Tue Feb 23 2010
* Guest12506 would be interested in feedback on both style and approach if anyone was interested http://www.galois.com/~emertens/revrev/revlistapp.html23/02 02:30
Saizan_pretty nice23/02 02:35
copumpkinI like it :)23/02 02:35
glguyare the extra refls overkill or educational?23/02 02:35
copumpkingeneral style-wise, I'd write what your goal is (in human) at the top :P I only figured out what you were working towards at the end23/02 02:35
glguyhmm, good point :)23/02 02:36
Saizan_a bit inconsistent to use rewrite just at the end while sticking to eq-reasoning the whole time :)23/02 02:36
glguytrue enough :)23/02 02:36
glguyI think I was just really excited to be done at that point!23/02 02:37
* copumpkin has never used rewrite :o23/02 02:37
Saizan_eheh, i guess :)23/02 02:37
Saizan_i like the refl steps23/02 02:37
copumpkindoesn't Algebra have an Involutive property?23/02 02:37
copumpkinyeah, you could write your rev-rev using it23/02 02:38
copumpkinbut that might just obscure things23/02 02:38
glguyI'm not sure I know how to pronounce that23/02 02:38
glguymuch less use it :)23/02 02:38
copumpkinreverse-app (reverse-app xs) ≡ xs23/02 02:38
copumpkinInvolutive reverse-app :P23/02 02:38
copumpkinsame thing23/02 02:38
* copumpkin doesn't know how to pronounce it either, though23/02 02:39
copumpkininVOLutive?23/02 02:39
copumpkininvolUtive?23/02 02:39
copumpkinI quite like your naming of parameters in types23/02 02:40
copumpkinI might start doing that too23/02 02:40
copumpkinin the past I've only done it if I need them later in the type23/02 02:41
glguyI haven't decided which way I like more23/02 02:41
Saizan_what do you mean?23/02 02:41
copumpkinrev : {A : Set} (xs ys : List A) → List A23/02 02:42
copumpkinI'd have written rev : {A : Set} -> List A -> List A -> List A23/02 02:42
Saizan_ah, i see23/02 02:42
Saizan_i'd probably have written \all {A} (xs ys : List A) -> List A , or abstracted A at the module level23/02 02:43
copumpkinyeah, good point23/02 02:43
glguy\all {A} is ambiguous23/02 02:43
glguyList is good for any level of set23/02 02:44
copumpkinah, that's annoying23/02 02:44
copumpkinbut you can still factor it out into a module parameter23/02 02:44
glguysure23/02 02:44
copumpkinthen you could even have this work over any level of set23/02 02:44
copumpkinwithout too much pain23/02 02:44
Saizan_ah, true, wasn't thinking of universes23/02 02:44
glguywould I be proving the exact same properties if I parameterized the module instead of each function?23/02 02:48
* glguy wonders if there isn't some subtle difference to what has been proven23/02 02:48
Saizan_if you had module revlistapp {A : Set} where ... then for each function defined there revlistapp.foo : {A : Set} -> <rest of the type>, no?23/02 02:51
Saizan_and all your types seem to fit that form23/02 02:52
Saizan_and you don't seem to instantiate your functions to something other than A when you reuse them later23/02 02:53
Saizan_you could also "open Monoid (monoid A)" once at the module level23/02 02:54
glguyyeah, I had it that way at first23/02 02:55
glguyI was trying to be clear about where those were coming from23/02 02:55
glguymaybe with some "renaming" I can make it nice23/02 02:55
Saizan_you still need a "right-id = proj\_2 identity" though23/02 02:56
glguybah, monoid : Set -> Monoid23/02 02:59
glguywhich screws up my level polymorphic version23/02 02:59
copumpkinyeah, that's lame23/02 03:00
copumpkinit's Algebra's fault though23/02 03:00
copumpkinthe whole module is still monomorphic23/02 03:00
glguyhttp://www.galois.com/~emertens/revrev/html/revlistapp.html now with more universe polymorhpism23/02 03:08
glguymorphism* :)23/02 03:08
copumpkinyou should fix up Algebra and send in a patch! :P23/02 03:08
copumpkinmuch prettier than seeing all the {A : Set}23/02 03:12
glguyIs there is potentially theoretic level that only elements of Set can be Monoid?23/02 03:13
glguylevel/reason23/02 03:13
copumpkinI doubt it23/02 03:13
glguyWith my current knowledge level, I tend to assume that if something in the library doesn't work like I want it to that I don't want to do what I wanted :)23/02 03:14
copumpkinI'm pretty sure it's just because nobody has had time to universe-polymorphize Algebra yet23/02 03:14
copumpkinbut I may be wrong23/02 03:14
glguyI'm using released version 0.323/02 03:15
glguyit might be different in darcs23/02 03:15
copumpkinyep23/02 03:15
copumpkinrecord Monoid c ℓ : Set (suc (c ⊔ ℓ)) where23/02 03:15
glguyWhat do people do for darcs on Snow Leopard?23/02 03:56
* glguy finds the binaries on the darcs site...23/02 03:57
glguy(colloquy is such a buggy client)23/02 04:44
copumpkinyeah :)23/02 04:44
copumpkinIRC clients tend to be pretty shitty, in my experience23/02 04:44
copumpkinespecially the pretty mac ones23/02 04:45
* copumpkin closes his eyes and dreams of a UI library that makes beautiful mac GUIs, FRP-like, in an awesome future dependently typed language with magic proofs that write themselves!23/02 04:49
roconnorwhy does Peter Morris use such strange notation for Sigma types in http://www.cs.ioc.ee/~tarmo/tsem09/morris.html ?23/02 14:55
npouillardroconnor: which slide ?23/02 15:05
roconnorany slide with a Sigma on it23/02 15:06
roconnorhe writes Σ A \ a -> B23/02 15:06
npouillardha, the backslash you mean23/02 15:06
roconnora notation I have never seen23/02 15:06
npouillardlike in haskell \ can be used as a λ23/02 15:06
roconnorah23/02 15:07
npouillardbut someone should tell him23/02 15:07
npouillardthose backslashes looks ugly23/02 15:07
roconnorI was wondering if there was some advangate over Σ a:A. B23/02 15:09
roconnorI guess the advantage is that it better represents the "natural" syntax for sigma types as an inductive familiy of two arguments23/02 15:09
roconnorthough Σ A (λa. B) I would find easier to read :D23/02 15:10
npouillardin agda this is λ a → not λa.23/02 15:10
npouillardand in agda Σ is not builtin syntax23/02 15:11
roconnortoo bad.  λ a ↦  seems a bit nicer than using →.23/02 15:12
npouillardright, but since → is already reserved for function space it let ↦ free to be used in definition23/02 15:13
npouillardI often use "_,_↦_ : Map → Key → Val → Map"23/02 15:14
roconnor:)23/02 15:14
roconnorthat should be "_[_↦_] : Map → Key → Val → Map"23/02 15:15
npouillard:)23/02 15:15
npouillardwhy not23/02 15:15
npouillardI like it too23/02 15:15
roconnorcan you use that syntax?23/02 15:15
npouillardsure23/02 15:18
glguycopumpkin, Check out "prop" http://www.galois.com/~emertens/revrev/revlistapp.html#589923/02 22:51
copumpkinoh my23/02 22:52
copumpkinthat's nice23/02 22:52
copumpkincan it not infer the type of f?23/02 22:53
glguyof 'f'?23/02 22:53
glguyit can not23/02 22:53
Saizanprop?23/02 22:53
copumpkinweird23/02 22:53
glguySaizan, yeah, that one :)23/02 22:53
copumpkinseems pretty obvious to me, but then again I haven't figured out what agda can infer and can't23/02 22:53
copumpkin and when23/02 22:53
glguyI know that it covers the type in yellow23/02 22:53
glguyI think that it does not learn enough about the type until the end23/02 22:54
glguyat which point it is too late23/02 22:54
copumpkinoh, it's probably because it isn't constrained to A23/02 22:54
copumpkin(f : _ A -> _ A)23/02 22:54
copumpkin:P23/02 22:54
* copumpkin shrugs23/02 22:54
glguyI also did "++-right-identity" using the Inductive module (as the expense of conciseness :-D) http://www.galois.com/~emertens/revrev/revlistapp.html#95423/02 22:55
glguyat the expense*23/02 22:55
glguya normal foldr doesn't work (obviously) because the type of the proof changes at every step23/02 22:56
copumpkinwow, you actually used the other colon23/02 22:56
glguyI did that to help show what was going on23/02 22:57
glguyit isn't necessary23/02 22:57
copumpkinpretty cool :)23/02 22:58
copumpkincouldn't you use prop to prove rev-app?23/02 22:59
glguyit was fun when I discovered that (∀ xs ys → f (xs ++ ys) ≡ f ys ++ f xs  ) → f [] ≡ []23/02 22:59
copumpkinwith a helper23/02 22:59
glguypossibly?23/02 23:00
glguyI just did "prop" over lunch23/02 23:00
glguyI haven't considered how it affects things, yet23/02 23:00
copumpkinoh, so you can get rid of one parameter to prop?23/02 23:01
glguyWell, it originally had f [] == [] as a parameter23/02 23:02
glguybut then I did the proof deriving that from the append property23/02 23:02
copumpkinoh I see23/02 23:02
copumpkinomg it's TacticalGrace23/02 23:02
glguywithout f [ x ] == [ x ]   (const []) would be a valid implementation23/02 23:03
TacticalGracehey copumpkin23/02 23:03
copumpkinah23/02 23:04
copumpkinhi :)23/02 23:04
glguyIs there something like ⊤ (top) that exists in universes other than Set?23/02 23:11
copumpkindon't think so, and I remember bottom is just in Set too23/02 23:12
npouillardglguy: You can use Lift ⊤23/02 23:19
copumpkinoh nice23/02 23:20
copumpkinwhen did that appear?23/02 23:20
--- Day changed Wed Feb 24 2010
Saizanwe can pattern match on records now? nice.24/02 07:16
Saizanagda: Oops!  Entered absent arg ww_s8Yi9{v} [lid] tcm{tv a8XlM} [tv] Agda-2.2.7:Agda.TypeChecking.Monad.Base.TCState{tc r2Qcm} <- i'm not sure if this is an agda or a ghc bug..24/02 07:21
npouillardcopumpkin: just before the 2.2.6 release I think24/02 09:08
--- Day changed Thu Feb 25 2010
glguyThoughts on whether this agda program captures the trivial exercise from TAPL 2.2.6? http://www.galois.com/~emertens/exercise2.2.6/Tapl2.html25/02 09:31
glguy(I recognize that this is a highly trivial proof, but I'd like to see how many of these I can do with Agda and I'd like to start at the beginning)25/02 09:32
HairyDudeIs there a "decidable partial order" type in the standard library?25/02 16:08
HairyDudeactually, just realised I actually want total orders, but I'm interested in the answer anyway.25/02 16:10
* HairyDude finds his agda is out of date and upgrades it.25/02 16:20
HairyDudealso, a small request: could the standard library tarball (and the directory it contains) please be called agda-lib not just lib? seeing it in a directory listing it's not clear at a glance what it is25/02 16:30
HairyDudewiki page on universe polymorphism is out of date.25/02 16:39
kosmikusI don't think this is the right place for bug reports25/02 16:49
HairyDudepoint25/02 16:55
HairyDudehrm. does the mailing list deliver non-text attachments? gmail doesn't realise an .agda file is actually text25/02 17:22
guerrillai think i may have ased this before, but does anyone here actually dev agda?25/02 17:22
copumpkinguerrilla: in what sense?25/02 17:26
copumpkinI've written a fair amount of agda code25/02 17:26
copumpkinnot sure you'd call it development in the traditional sense though :)25/02 17:26
guerrillai meant working on agda itself25/02 17:34
copumpkinoh :)25/02 17:35
copumpkinno25/02 17:35
copumpkinnot as far as I know, anyway25/02 17:35
guerrillayeah, i didn't think so :)25/02 17:35
stevancopumpkin: btw, is the regex link still 404 for you?25/02 17:36
copumpkinstevan: nope, fixed now, thanks :)25/02 17:36
copumpkinI took a quick look at it yesterday and it looked interesting25/02 17:36
guerrillacurious, what's this about regex?25/02 17:37
guerrillasomeone doing some FL stuff in agda?25/02 17:37
stevanreddit.com/r/dependent_types/25/02 17:38
guerrillawow *brain explodes* didn't know that existed :)25/02 17:39
guerrillathis paper on regex is great.25/02 17:42
guerrillaim so happy now :)25/02 17:42
copumpkin:)25/02 17:44
copumpkinI started writing a module with the same goal25/02 17:44
copumpkinbut got bored/started shaving a yak25/02 17:44
guerrillaah25/02 17:44
guerrillayes, i'd like to keep going to CFG/PDA and then AGs25/02 17:45
guerrillai'm not good enough with Agda yet, so been messing around trying different things25/02 17:45
guerrillastill don't know how to represent disjoint sets over an arbitrary sets yet though25/02 17:46
guerrillaA \intersection B = \emptyset25/02 17:46
Saizan\all x -> A x -> \neg B x and vice versa?25/02 18:04
guerrilla1sec Saizan - phone25/02 18:13
guerrillak, sorry about that25/02 18:16
guerrillayes, i think that's basically what i mean25/02 18:16
guerrillabut i think i need it as a proof object, so that i can construct a record that contains both sets and that proof25/02 18:16
HairyDudehmm. "right hand side must be a single hole" is a rather annoying limitation.25/02 21:23
HairyDudeis there a "decidable unary relation" type?25/02 23:57
--- Day changed Fri Feb 26 2010
HairyDudethere's Data.Fin.Dec and Data.Sets but neither is quite right, I want something like DecPred : forall {A l} -> (P : Pred A l) -> (x : A) -> Dec (P x)26/02 00:02
HairyDudewell that's not quite right, but you know what I mean26/02 00:03
copumpkinwhat would be the type of _->_ in agda, if it can be written?26/02 06:15
guerrillaSet1?26/02 06:16
Saizan{A : Set i} {B : A -> Set j} -> (x : A) -> B x -> Set (max i j) ?26/02 06:19
Saizanwell, in a sort of imaginary world26/02 06:21
dolioI think that's too many arguments.26/02 06:24
dolioIt'd be {i j} (A : Set i) (B : A -> Set j) -> Set (max i j)26/02 06:25
dolioBut that uses -> to define the type of ->.26/02 06:25
copumpkin:)26/02 06:25
guerrilladolio: yeah, looks a little impredicative :)26/02 06:31
guerrillawould have to use a further relation i guess26/02 06:32
dolioWell, when you formalize these things with pure type systems, you usually have a sort of schema for giving the type of particular instances of pi types.26/02 06:33
dolioAnd it's a little less weird in Haskell because the (->) for types isn't the same as the (->) for kinds.26/02 06:34
guerrillatrue26/02 06:34
dolio(And the forall for types.)26/02 06:34
dolioIt's not all mixed together like with dependent types.26/02 06:34
guerrillahmm, OT, but haskell kinds are a subset of the arity system in M-L TT, right?26/02 06:37
guerrilla(since kinds don't apply to records, as i understand it)26/02 06:37
dolioRecords?26/02 06:38
guerrillayeah..26/02 06:38
guerrilla1sec, maybe that's not what they're called in ML TT26/02 06:38
guerrillacombinations26/02 06:39
dolioWell, I don't know ML TT really. At least not the technical terminology.26/02 06:39
guerrillai assumed those were equivalent to records26/02 06:39
guerrillaseems like it, combination <-> record instantiation and selection <-> selection26/02 06:39
Saizandolio: oh, right, i was mixing the type of _->_ with the type built with it26/02 06:41
dolioHaskell kinds are definitely a sub-system (or something) of what you get in a calculus like Agda (or, more accurately, the calculus of constructions).26/02 06:43
copumpkinwhat do people mean when they say a "calculus of X" or "X calculus"?26/02 06:43
copumpkinI've seen so many different calculi that I'm not sure what unifies them26/02 06:43
copumpkinis there a universal calculus like a universal algebra that defines them all?26/02 06:44
guerrillacopumpkin: from a thread on mathoverflow, it seems that there is no definition of a calculus26/02 06:44
dolioI don't think so. It's just a cool name.26/02 06:44
copumpkineveryone just has an intuitive feel for what people mean by it, I guess?26/02 06:44
guerrillawell, one difference i see between a calculus and an algebra is that a calculus gets you an end result at some point and an algebra is just used for rewriting26/02 06:48
* copumpkin defines a calculus as a stone and moves on26/02 06:48
guerrillahehe26/02 06:48
guerrillanice26/02 06:48
copumpkin:)26/02 06:48
copumpkinin italian, kidney stones are called that26/02 06:49
guerrillaright, i actually remember something about that26/02 06:49
guerrillacalc as in calcium? kinda makes sense26/02 06:49
copumpkinyeah, it just means stone in latin26/02 06:49
guerrillakinda morbid if they used them for counting26/02 06:49
Saizanto calculate comes from the fact that romans used stones for it26/02 06:49
copumpkinor pebble, maybe26/02 06:49
dolioWell, the thing is, it's not very obvious (to me) that "The Calculus" has anything to do with lambda calculus and pi calculus and propositional calculus...26/02 06:50
dolioAnd relational calculus.26/02 06:50
guerrillaisn't "the calculus" actually "infintesimal calculus"?26/02 06:50
Saizanso, maybe, the idea is that these systems are so simple that you can calculate with them26/02 06:51
guerrillayeah, kind of get a "results"-feeling from calculus26/02 06:51
guerrillawhere algebra is more abstract26/02 06:51
dolioWell, there's relational algebra, too.26/02 06:51
dolioThe difference being that with relational algebra, you talk about composition of operations and stuff, and relational calculus is some kind of modified predicate calculus for reasoning about relational databases.26/02 06:52
guerrilladescribing vs. calculating?26/02 06:53
guerrillamaybe...26/02 06:53
dolioI don't really see how one is more results-based.26/02 06:53
guerrillalike as in getting an end value26/02 06:56
guerrilla*shrug*26/02 06:56
Saizanare there algebras with binders?26/02 06:56
dolioYeah, I've thought about that. But the propositional calculus doesn't have binders.26/02 06:57
guerrillabinders as in some form of quantification or abstraction?26/02 06:57
dolioMaybe it should be propositional algebra?26/02 06:57
Saizanunless you go higher order.26/02 06:57
guerrilla Results 1 - 10 of about 3,610 for "lambda algebra". (0.10 seconds)26/02 06:57
guerrilla Results 1 - 10 of about 2,750 for "propositional algebra". (0.17 seconds)26/02 06:57
guerrillahehe (not too much spam either)26/02 06:57
Saizanhowever i've seen people talk about both process calculi and process algebras26/02 06:57
Saizanto mean the same thing.26/02 06:58
dolioThere's also algebraic study of logic, which with categorical logic, can account for quantifiers. :)26/02 06:58
copumpkinjust out of curiosity, what should I look for if I want to fit quantifiers in?26/02 06:59
dolioWhat?26/02 07:00
copumpkinwhat you just said about accounting for quantifiers26/02 07:01
dolioQuantifiers involve adjunctions.26/02 07:01
copumpkinooh26/02 07:01
copumpkincan't get away from 'em26/02 07:01
dolioIt goes something like...26/02 07:02
dolioYour formulas are in some way parameterized by a set (or object) of variables.26/02 07:03
dolioAnd change of that set of variables is a functor.26/02 07:03
dolioExistential quantification is left adjoint to that functor, and universal quantification is right adjoint.26/02 07:04
copumpkinooh26/02 07:05
copumpkinthat seems so elegant26/02 07:05
copumpkinI really need to read more of TTT26/02 07:05
copumpkinI assume that would cover it?26/02 07:05
dolioI haven't gotten to that yet. It might.26/02 07:05
dolioAwodey's book covers it a little.26/02 07:06
guerrillaTTT?26/02 07:06
copumpkintriples toposes and theories26/02 07:06
copumpkinin some order26/02 07:06
dolioYou've got the first two switched.26/02 07:07
copumpkindamn26/02 07:07
copumpkinI guess triples and theories should go together26/02 07:07
* guerrilla saves26/02 07:07
copumpkinhttp://code.haskell.org/~dolio/agda-share/induction/html/Transfinite.html is pretty cool26/02 07:11
copumpkinhadn't seen it before26/02 07:11
dolioOMG, Agda can do stuff infinitely many times!26/02 07:13
copumpkin:)26/02 07:13
guerrillahehe, funny: http://www.dpmms.cam.ac.uk/~ardm/inefff.dvi26/02 07:40
guerrilla    * Adrian Mathias, A Term of Length 4,523,659,424,929, Synthese 133 (2002) 75--8626/02 07:40
guerrillawhat do errors such as the following mean?26/02 11:41
guerrillaA !=< _926/02 11:41
guerrillawhen checking that the expression a has type _926/02 11:41
npouillardguerrilla: try giving A a type26/02 12:25
npouillard∀ {A : Set} → ...26/02 12:26
guerrillaah26/02 12:54
guerrillathanks26/02 12:54
--- Day changed Sat Feb 27 2010
* glguy has another trivial TAPL exercise to share http://www.galois.com/~emertens/exercise2.2.6/Tapl2.html27/02 04:00
* copumpkin doesn't really understand how the begin ... \qed stuff works27/02 04:01
glguyI understand how to use it27/02 04:01
glguythe question is if I can explain myself :)27/02 04:01
copumpkinI don't really have a good feeling of how or when to use it :) I usually just have a bunch of cong/subst/trans/syms27/02 04:02
copumpkinand am not sure which ones I could use that thing for27/02 04:02
glguyit is good for any preorder where you want to show the intermediate steps off all the cong and subst and commute and whatnot27/02 04:03
copumpkinhm27/02 04:03
glguyI used it a ton http://www.galois.com/~emertens/revrev/revlistapp.html27/02 04:03
glguyin that file27/02 04:03
glguybecause I was proving lots of x == y27/02 04:03
copumpkinyeah27/02 04:03
glguyand there were a number of steps to transform x into y27/02 04:03
copumpkinso the first thing in the list is always the x in x == y?27/02 04:03
glguyright27/02 04:03
glguyand the last is always y27/02 04:03
glguybut sometimes agda can simpify things down for you27/02 04:04
glguyso it will ask you to prove something syntactically different than your type27/02 04:04
glguyI still like to start from the literal goal27/02 04:04
glguyand use refl steps to work toward the simpified goal27/02 04:04
copumpkinhm, ok27/02 04:05
* copumpkin plays with it a bit27/02 04:05
glguyit didn't click for me at first27/02 04:05
* copumpkin pulls in Data.Nat.Properties27/02 04:08
dolioThe reasoning module is for lots of chained trans.27/02 04:22
* Saizan wants editor support to write cong's27/02 04:23
doliox \qed is another name for refl : x == x27/02 04:23
doliobegin_ is the identity function.27/02 04:24
dolioAnd the _~<_>_ is transitivity.27/02 04:24
doliox ~< x~y > y~z27/02 04:24
copumpkinI see27/02 04:27
dolioAnd that operator is... left associative?27/02 04:29
dolioI think that's right.27/02 04:29
dolioWait, maybe right associative.27/02 04:30
glguyx ~<_> (y ~<_> z \qed)27/02 04:30
glguybinds like that27/02 04:30
dolioYeah. That's right, I guess.27/02 04:30
dolio(Right as in the opposite of left.)27/02 04:31
glguya lot of time I end up with:   begin x ~< eq > ?27/02 04:31
glguyand build out27/02 04:31
dolioAh, nice. I usually just write it all out at once, but that's dangerous.27/02 04:31
glguyif I know exactly how to write it outright, I've done that27/02 04:31
glguybut I'm still learning27/02 04:32
Saizani tend to keep it like "begin x ~< eq > ? ~< ? > y \qed27/02 04:32
glguyyeah, that's what i've adopted27/02 04:32
glguyI'll do all of the values first27/02 04:32
glguyand then come back and do the reasons that the transition was ok27/02 04:33
glguyx =< ? > y =< ? > z \qed27/02 04:33
copumpkinwe need a property called irregardless: http://snapplr.com/t9rg27/02 05:15
glguyso is symmetry:   ∀ a b → a ∾ b → b ∾ a   while commutativity is  ∀ a b → a ∾ b ≡ b ∾ a  ?27/02 06:46
copumpkinsymmetry of relations, commutativity of operations, as far as I know27/02 06:48
copumpkinso yeah :)27/02 06:49
copumpkinI wouldn't use the same symbol for both27/02 06:50
glguyI'd like to be able to define functions with a subscript argument27/02 07:07
copumpkinme too27/02 07:07
glguycopumpkin: I know you were just posting a snippet earlier, but do you know how to produce HTML from an Agda file?27/02 07:16
copumpkinI think it's a parameter to agda-executable27/02 07:16
copumpkinlet me look27/02 07:16
glguyagda --html27/02 07:16
copumpkinah ok :)27/02 07:17
copumpkinoh, I was just posting a screenshot of the docs page27/02 07:17
copumpkinwait, were you suggesting or asking?27/02 07:17
glguySuggesting it as a possibility for you just in case you did a screen shot because you didn't know about html output27/02 07:17
copumpkinoh, no :) I just have a screenshotter a keybinding away27/02 07:18
copumpkinand am extremely lazy :P27/02 07:18
copumpkinthanks though27/02 07:18
guerrillaok, syntactic question - what if you need to use a type in a module parameter that is not yet imported?27/02 15:19
guerrillafor example,27/02 15:19
guerrillamodule Eq (A : Set) (_==_ : A → A → Bool) where27/02 15:19
guerrillawhere, normally, Bool would be imported right after that declaration...27/02 15:20
guerrillai guess you just put it before... hmm, i didn't realize that was valid27/02 15:20
guerrillan/m :P27/02 15:21
guerrillain Relation.Unary why is the name Pred used? predicate?27/02 21:49
MissPiggypredecessor27/02 21:50
MissPiggyno you are right27/02 21:50
guerrillaso the set level of the preceding universe? *confused*27/02 21:50
guerrillahehe27/02 21:50
guerrillai really am not following this code...27/02 21:51
guerrillai supposed it makes sense that a unary relation is a predicate (or a set) depending on how you look at it27/02 21:51
guerrillabut i'm not entirely sure why or how it is using universe polymorphism27/02 21:51
--- Day changed Sun Feb 28 2010
lpjhjdhSo I'm trying to give a progress proof for the toy language Pierce gives in TAPL and I'm having a bit of trouble with a few cases, don't think I understand with well enough28/02 20:47
lpjhjdhI've written everything up in Isar first so I have a reference of how I need to go about everything28/02 20:48
lpjhjdhanyone have a hint for me?  http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23101#a2310128/02 20:48
lpjhjdhthat currently doesn't actually work gives: "Missing with-clause for function progress"28/02 20:51
lpjhjdhIn Isar I use disjunction elimination with the IH28/02 20:56
Saizanlpjhjdh: hard to say without being able to test it, though you should have better luck with a distinct lemma in a where clause28/02 21:52
lpjhjdhwhere clause?28/02 21:55
lpjhjdhwhat's is that?28/02 21:55
lpjhjdhwhat*28/02 21:55
lpjhjdhhere's my isabelle case if that helps: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23104#a2310428/02 21:57
glguyhttp://www.galois.com/~emertens/exercise2.2.6/Tapl2.html#198728/02 21:58
glguythat function uses a where clause28/02 21:58
glguyit lets you put local definitions after your goal28/02 21:58
lpjhjdhooh, a la haskell28/02 21:59
lpjhjdhwould giving you the whole contex help?28/02 22:04
* glguy doesn't know the question28/02 22:04
glguyI'm pretty new to Agda, but I'll help you translate your proof, if it can28/02 22:05
lpjhjdhthat was at Saizan, but I'm trying to show progress for a toy language from TAPL.  I'm working on the iszero clause http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23101#a2310128/02 22:05
lpjhjdhand the link I gave above is the working piece from my Isabelle proof28/02 22:06
lpjhjdhI didn't really know what I was doing with those "with" clauses28/02 22:07
lpjhjdhI want to give proof by disjunction elimination over the result of the IH from n28/02 22:07
Saizanthat code looks like it should work28/02 22:15
Saizanbut the "with" construct is sugar, and not always perfect28/02 22:16
Saizanso, writing out an helper function that does the pattern matching might help28/02 22:17
lpjhjdhah, I'll try that, thanks28/02 22:17
Saizanso that you write progress {suc n} {suc n'} (ok-suc nty) = helper (progress {n} {n'} nty) where helper : ...; helper (inl nst) = ..; helper (inr vn) = ..28/02 22:18
lpjhjdhso I'm getting yellow highlighting on "pg {iszero n} {n", can't figure out the rest of the implicit params?28/02 22:28
lpjhjdhhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=23105#a2310528/02 22:28
lpjhjdhis that what it means?28/02 22:29
lpjhjdhI can't actually give it n' and t' because I won't know if n' exists or what t' is until I match on "progress {n} nty"28/02 22:29
lpjhjdhcause if n were a value to begin with then iszero will go to true or false, but if it can step then iszero will simply step28/02 22:29
Saizani don't undestand28/02 22:53
Saizant' is the second implicit argument to progress, so you've it28/02 22:53
lpjhjdhoh, ha, thank you, I was thinking I needed to be specific (like iszero n')28/02 22:54
lpjhjdhit's actually n' that it can't figure out, I don't have n'28/02 22:56
Saizanwell, that's a problem then28/02 22:56
lpjhjdhbecause n' won't even exist if n is a value (n = zero)28/02 22:56
lpjhjdhthen I need more case analysis I guess :(28/02 22:56
Saizanhow do you make the recursive call to progress without n'?28/02 22:56
lpjhjdhtrue, I guess I was just trying to ride off my Isabelle version which says "(∃e' . e ⟼ e') ∨ isvalue e" so the e' isn't there right away28/02 22:58
Saizanmaybe you need different types for your Agda version28/02 22:59
lpjhjdhis there a way to say: progress : ∀{t τ} → t :: τ → (∃t' . t ⟶ t') ∨ Value t28/02 22:59
Saizanyes, see Data.Product28/02 22:59
lpjhjdhthanks!28/02 22:59
Saizan(the syntax will be "progress : ∀{t τ} → t :: τ → (∃ \lambda t' -> t ⟶ t') ∨ Value t")28/02 23:01
lpjhjdhhmm, is there something I can read to learn about existentials in agda/dependent-types28/02 23:03
Saizanmh, the tutorials on the wiki should have some introduction28/02 23:05
lpjhjdhI don't know anything about dependant type theory, is that somehow related to sigma pi types?28/02 23:06
Saizanhowever in constructive logic, a proof of exists a : A. B a, is a pair of and element of type A and a proof that B holds for a28/02 23:06
Saizanthis is what's called a sigma type28/02 23:07
Saizandata Sigma (A : Set) (B : A -> Set) : Set where _,_ : (a : A) -> (B a) -> Sigma A B28/02 23:07
Saizanthen ∃ is just a synonym where the A argument is implicit28/02 23:08
Saizanthe symbol Sigma is used because the existential quantifier can be seen as a generalization of the \/ connective, also denoted +28/02 23:09
Saizaninstead of having only two possible cases, you have one for every element of A28/02 23:10
lpjhjdhand then it holds for at least one of those?28/02 23:10
lpjhjdhbecause you just have to find *some* B a to construct sigma?28/02 23:11
Saizanyeah, a value of Sigma A B is a proof that there's at least one (a : A) for which B a holds28/02 23:11
Saizanright28/02 23:12
lpjhjdhah, that's quite helpful, thanks again28/02 23:13
Saizane.g. data IsEven : Nat -> Set where evenz : IsEven zero; evenss : forall {n} -> IsEven n -> IsEven (suc (suc n)); 2isEven : Sigma Nat IsEven; 2isEven = suc (suc zero) , evenss evenz28/02 23:14
Saizanwell, 2isEven is not a great name28/02 23:15
Saizan"some-n-is-even"28/02 23:15
Saizanyou'd have "2isEven : IsEven (suc (suc zero))"28/02 23:16

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