--- Log opened Sat May 01 00:00:15 2010
copumpkinI am NOT a fan of listservs sending me my password in plaintext01/05 04:11
copumpkinincluding the chalmers agda one01/05 04:11
* glguy solicits feedback on http://www.galois.com/~emertens/treerec/preorder.html01/05 06:50
glguyI'm trying to document this portion of the Tree stuff I've been doing so that someone else could use it as an example in the future01/05 06:50
glguyor at least the w.f. induction part01/05 06:51
* Saizan didn't realize records aren't checked for positivity01/05 06:53
TheOnionKnightglguy: I found it fairly easy to understand what was going on. The wording of "'preOrder's helper function's relationship to the specification" in the same' description seemed a little awkward to me though, had to read it a few times to figure out what was meant. In case it matters, I only have a very very basic understanding of well founded recursion and have never tried using it before.01/05 07:16
glguyOK, I'll have to try to clear up that language01/05 07:18
glguyI wanted to write "I needed this to prove the next thing" :)01/05 07:18
TheOnionKnightI'd try swapping the word order, "we must first prove the relationship between preOrder's helper function and the specification"01/05 07:19
glguybetter?01/05 07:23
TheOnionKnightyep01/05 07:24
glguythanks for reading through it01/05 07:26
TheOnionKnightyour welcome01/05 07:26
* glguy learns a new operator from the stdlib: same : preOrder ≗ spec01/05 08:42
* Saizan wants hoogle for agda01/05 08:48
Saizanis that just (f g : A -> B) (x : A) -> f x \== g x ?01/05 08:49
Saizan"\lambda f g -> forall x -> f x \== g x"01/05 08:50
glguyIt is (f g : A -> B) -> Set01/05 08:57
glguyand equals forall t -> f t == g t01/05 08:57
glguySaizan: If you're still there, check out preOrder' implemented using all of the various type synonyms used in the Induction module... http://www.galois.com/~emertens/treerec/preorder2.html#466001/05 09:00
glguylook ma', no arrows01/05 09:00
Saizanheh :)01/05 09:01
glguyI want to think that with enough familiarity of these operators that they actually make the meaning clearer...01/05 09:02
Saizan"Universal Sig" doesn't feel quite right given that Sig ignores its argument01/05 09:07
Saizani like ⊆′ though01/05 09:07
glguythat makes it particularly universal!01/05 09:08
Saizannot much of a property though :)01/05 09:09
Saizan(and looking more at it the use of ⊆′ has the same problem, i just felt more familiar with it)01/05 09:09
glguywell, the argument isn't as ignored in the sub=' case01/05 09:15
glguydue to the <-Rec01/05 09:15
* glguy sets out to write a proof inthat file that makes use of the argument to the predicate01/05 09:19
glguySaizan: head to the bottom of that page http://www.galois.com/~emertens/treerec/preorder2.html#466001/05 09:32
glguysure the structure of the proof is basically identical01/05 09:33
glguybut the predicate is more interesting :)01/05 09:33
Saizantrue :)01/05 09:36
* Saizan wonders if one could come up with a sensible name for P01/05 09:37
glguyDoes it help to look at it like P = λ ts → ∀ xs ys → preOrder′ ts (xs ++ ys) ≡ preOrder′ ts xs ++ ys01/05 09:37
glguy(seems to help put ts xs and ys on the same playing field01/05 09:38
Saizanyeah, it's quite less noisy like that01/05 09:47
glguyWell, I could fiddle with this all night, but I need to get some sleep01/05 09:51
glguygood night01/05 09:51
--- Day changed Sun May 02 2010
lpjhjdhI'm getting an error about not being able to instantiate a metavariable because it can't depend on something02/05 01:18
lpjhjdhI'm unfamiliar with the theory of dependant types so it's rather nonsensical to me02/05 01:18
faxit's just what you'd imagine02/05 01:21
faxthere's a hidden variable somewhere that needs a value (from (type) inference)02/05 01:21
faxyou can use  instantiate (3 := x)  but there's usually a different way to have ti cleared02/05 01:22
lpjhjdhok, I'll try splitting some stuff up maybe02/05 01:22
lpjhjdhI'm able to write what I expect as it's own function02/05 01:23
glguy_fax: I've been trying to write up a subset of the preorder stuff for a blog post or something. Maybe it will help someone else (sorry if you've already seen the new commented version) http://www.galois.com/~emertens/treerec/preorder.html02/05 01:33
glguy_If you have any ideas for how to make it easier to understand let me know02/05 01:33
faxoh shit this is #agda02/05 01:34
faxI thought it was #coq02/05 01:34
faxlpjhjdh lol sorry just ignore what I said it's completely wrong02/05 01:34
lpjhjdhhah, no worries, I'm just mindlessly shuffling things around to see if I can get things more readable02/05 01:36
doliolpjhjdh: How big is the code?02/05 01:37
lpjhjdhmaybe if I post the problem that would be helpful02/05 01:38
lpjhjdhnot large02/05 01:38
dolioPaste it somewhere.02/05 01:38
lpjhjdhnow that moved things it's one line02/05 01:38
faxglguy_: this is great that will be very useful for people that don'tknow how to use well founded relations02/05 01:38
lpjhjdhhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=25272#a2527202/05 01:39
dolioWow.02/05 01:40
lpjhjdhoh yeah, and weaken : ∀{x}{φ₁ φ₂} → x ∷ φ₁ ⊆ φ₂ → φ₁ ⊆ φ₂02/05 01:40
dolioWhat line causes the error? The 'no' line?02/05 01:40
lpjhjdhyeah, and it's underlining x∷φ₁⊆φ₂02/05 01:40
lpjhjdhI uncluttered the error a bit02/05 01:43
lpjhjdhhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=25272#a2527302/05 01:43
lpjhjdhany notion of what's going?02/05 01:46
dolioWell, metavariables have nothing to do with dependent type theory directly.02/05 01:47
dolioIt has to do with Agda's ability to infer things if you put down a _, or use implicit arguments.02/05 01:47
lpjhjdhah02/05 01:48
dolioWhen you do that, it fills the spot with a 'metavariable', and runs a unification algorithm trying to figure out what should go in there.02/05 01:48
dolioSo, it's unhappy with some implicit argument, but I'm not sure which one.02/05 01:49
glguy_Is that lemma even going to be true?02/05 01:49
glguy_How will you decide if x was in φ₂02/05 01:49
lpjhjdhI was thinking any (_≟_ x) φ₂02/05 01:50
dolioglguy_: x is from (and the phis hold elements from) a decidable setoid, it looks like.02/05 01:50
glguy_yeah... I see the DecSetoid now :)02/05 01:51
lpjhjdhI think the only other implicit var there is from φ₁⊈φ₂02/05 01:53
doliolpjhjdh: It looks like the problem is that it somewhere thinks there's an x' happening, when you want it to be x.02/05 01:53
lpjhjdhah, yeah, it's calling the implicit var in φ₁⊈φ₂ x'02/05 01:53
glguy_If you want the two phis to have the same type you'll have to name it02/05 01:57
glguy_unless your sub= operator isn't polymorphic in some list type02/05 01:57
glguy_e.g. you can't have forall xs ys. where you need: (A : Set) (xs ys : List A)02/05 01:58
lpjhjdhhm, just use a lambda then?02/05 01:59
glguy_what type did you expect the two phis to have?02/05 01:59
lpjhjdhList DecSetoid.Carrier02/05 01:59
glguy_is sub= defined as  List Carrier -> List Carrier -> Set?02/05 02:00
lpjhjdh_⊆_ : List A → List A → Set with A being from D.setoid02/05 02:01
glguy_Is the DecSetoid picked as a module parameter?02/05 02:02
lpjhjdhyeah02/05 02:02
glguy_oh, then this probably shouldn't matter02/05 02:02
glguy_but you might try explicitly giving the types instead of using the forall shortcut02/05 02:03
lpjhjdhah, I'll give that a shot, thanks02/05 02:03
lpjhjdhhmm, still having the issue02/05 02:05
glguy_boo :)02/05 02:05
lpjhjdhI was hoping to use the subset from Data.List.Any but maybe I'll try making everything explicit02/05 02:05
lpjhjdhthat worked02/05 02:11
lpjhjdhso xs ⊑ ys = (x : A) → x ∈ xs → x ∈ ys works but xs ⊆ ys = {x : A} → x ∈ xs → x ∈ ys doesn't02/05 02:12
lpjhjdhhow do you do substitution with equality from a setoid?02/05 02:31
dolioI think you'd need a proof that the function/predicate/whatever respects the setoid.02/05 02:35
dolioIn which case it's trivial.02/05 02:35
lpjhjdhokay, I was wondering what respects was02/05 02:36
lpjhjdhcould you help me understand this signature?  Substitutive : ∀ {a ℓ₁} {A : Set a} → Rel A ℓ₁ → (ℓ₂ : Level) → Set _02/05 02:42
dolioThe 'a' and the ells are for universe polymorphism.02/05 02:46
dolioSo that you can have Substitutive that works at multiple different levels.02/05 02:48
dolioInstead of just working on, say, Set.02/05 02:48
lpjhjdhokay02/05 02:49
Mathnerd314can any function be made to use universe polymorphism?02/05 03:11
dolioMore or less. Universe polymorphism in agda is accomplished by having Set be an indexed type (by Level), with ordinary pi types.02/05 03:15
Mathnerd314so maybe one could infer the universe?02/05 03:16
dolioI'm not sure what you mean by that.02/05 03:18
faxIf you want to make an apple pie, first you must infer the universe02/05 03:21
uoryglProof time!02/05 03:30
uoryglHere's a statement: "If two rational numbers a/b and c/d differ by 1/bd, then of all the rational numbers between them, the one with the lowest denominator is (a+c)/(b+d)."02/05 03:31
uoryglIt's a reasonably well-known theorem (or maybe I made a mistake and it's false), and I feel like writing up a proof of it in Agda.02/05 03:32
uoryglWish me luck!02/05 03:32
dolioGood luck. I suspect you'll need it.02/05 03:36
uoryglWell, I can't say this is going very well.02/05 03:57
uoryglUpon trying to open an Agda file with Emacs, I get this: File mode specification error: (file-error "Cannot open load file" "haskell-indent")02/05 03:57
uoryglThis is on a Mac.02/05 03:58
glguy_Did you install Haskell-mode?02/05 04:10
uoryglYes.02/05 04:10
glguy_I added this to my .emacs and haven't had problems since http://fpaste.org/n9Fe/02/05 04:12
glguy_but if you've already done that I won't be able to help you02/05 04:12
uoryglHmm, /opt/local/share/emacs/site-lisp/haskell-mode-2.4 doesn't exist.02/05 04:26
uoryglMaybe I installed it wrong somehow.02/05 04:26
glguy_I installed it through macports02/05 04:29
uoryglYou installed Agda through MacPorts?02/05 04:30
glguy_no, haskell-mode02/05 04:31
glguy_You have to install haskell-mode separately02/05 04:31
uoryglOh, I was confusing agda-mode with haskell-mode.  I have the former but not the latter.02/05 04:32
uorygl"sudo port install haskell-mode" tells me that that doesn't exist.02/05 04:33
glguy_then that isn't the name of the port02/05 04:37
uoryglWell, that's too bad.02/05 04:37
koninkjeSo I have an odd question...02/05 04:42
koninkjeThere are a number of things which seem obvious/nice to have, but which are actually problematic (e.g., injective constructors, surjective pairing). Is there a good listing/summary of such things somewhere?02/05 04:42
koninkje...or good examples of where they conflict with other dependent typing features?02/05 04:45
dolioSurjective pairing is eta equality of pairs?02/05 04:56
koninkjesurjective_pair : (p:A*B) -> (fst p, snd p) = p02/05 04:56
koninkje...or equivalent02/05 04:57
faxdolio (equivalent to proof irrelevance)02/05 04:57
uorygl(fst p, snd p) = p looks correct.02/05 04:58
uoryglIs there something wrong with it?02/05 04:58
dolioIt's equivalent to proof irrelevance?02/05 04:58
koninkjeI'm also curious about why eta conversion and extensional equality of functions (i.e., (forall x, f x = g x) -> f = g) are problematic (they're problematic in Coq at least, but I don't know whether that's a Coq-ism or a deeper issue)02/05 04:58
faxdolio: axiom K02/05 04:59
koninkjeuorygl: The more problematic version is at the type level IIRC: (P: Sigma(x:A).B) -> Sigma(x: proj1 P).(proj2 P) = P.02/05 04:59
uoryglHuh.02/05 05:00
koninkjeAgain, I'm not entirely sure of the details, which is why I'm searching for a good overview of metatheoretic design issues for dependent types.02/05 05:01
dolioWhere did I leave off?02/05 05:02
faxnothing02/05 05:03
dolioMaking definitional equality extensional is problematic because you lose things like decidability of type checking.02/05 05:03
dolioIf you have x : ... f ..., and you want to know if x : ... g ... is valid, you probably need to decide f = g.02/05 05:03
dolioAnd if, to do that, you need to decide (forall x. f x = g x), well, you can't do that in general.02/05 05:04
koninkjedolio: sure. But I'm saying that, if you can indeed prove (x:_) -> f x = g x, then why should it be problematic to derive f=g from that proof?02/05 05:05
koninkjeI'd suppose that the issue has something to do with axiom K or, equivalently, Martin-Lof vs John-Major equality02/05 05:05
dolioIf we're talking an equality type, then the reason is that in Coq, the equality type is defined to reify the definitional equality.02/05 05:06
dolioSo Id A x y is inhabited only when x = y is definitionally true.02/05 05:07
dolioOTT, by contrast, has an equality type that isn't linked to the definitional equality used in type checking.02/05 05:08
faxkoninkje - what is meant by 'problematic'02/05 05:08
dolioSo you get extensional equality in the equality type, but intensional equality for type checking.02/05 05:08
koninkjefax: introduces inconsistency to the system (e.g. injective constructors + impredicativity), etc.02/05 05:09
faxkoninkje: neither of these do02/05 05:09
koninkjefax: Or, for another concrete example, makes case elimination not have the nice properties we would like02/05 05:09
koninkjefax: Or reders type checking/inference significantly harder, etc02/05 05:10
koninkjes/reders/renders/02/05 05:10
faxhave you read simply easy?02/05 05:10
koninkjeYeah, though it's been a while02/05 05:11
faxthey have revised it a couple times02/05 05:11
dolioIs K usually considered proof irrelevance? I know you can use proof irrelevance to get K, but Agda has K without proof irrelevance.02/05 05:11
faxdolio: they're all equivalent in terms of provability -- (but we really want to have the definitional equality of course..)02/05 05:11
TheOnionKnightIf I understand correctly K is heterogeneous equality (or equivalently a stronger eliminator for [homogeneous] equality of existential types)02/05 05:14
dolioK states that every proof of x = x is refl.02/05 05:14
koninkjefax: as I recall, Simply Easy is only dealing with an LF- or ITT-like system rather than CC-like (where new issues are raised)02/05 05:16
koninkje...though, as I said, it's been a while02/05 05:16
faxoh well id on't know what the difference are02/05 05:16
dolioK : (A : Set) (x : A) (P : (x = x) -> Set) (eq : x = x) -> P refl -> P eq02/05 05:17
faxhttp://github.com/larrytheliquid/Lemmachine02/05 05:18
faxthis is a good idea02/05 05:18
koninkjefax: in LF you have Pi instead of arrow, and as you move towards ITT you add Sigma and the like. Overall, things are still well-behaved, just with dependency added in. Whereas in CC you get Prop02/05 05:19
faxwhat's arrow?02/05 05:19
koninkjeThe normal notation for the type of functions in non-dependent languages (e.g. simply typed, System F,...)02/05 05:20
koninkjeWhen you only have Pi, terms can be used to index types, but terms cannot *be* types themselves. Once you add Prop to the mix, then terms can indeed be types themselves02/05 05:21
faxreally?? how?02/05 05:21
koninkjeFor example, the "lambda" or forall quantifier of terms in Prop reifies the Pi at the type level02/05 05:21
koninkjeBut if we do the obvious thing to have an exists quantifier which reflects Sigma, then the system becomes inconsistent02/05 05:22
faxI am not really understanding this02/05 05:22
koninkjeSO we have our normal lambdas right?02/05 05:23
faxI think of lambda and forall as different things02/05 05:23
koninkjeThe type of a lambda is a Pi:  lambda (x:A).e:B :: Pi(x:A).B02/05 05:24
faxokay02/05 05:24
koninkjeAnd we have the type of Pi is Set (or *, or some other atomic name):  Pi(x:A).B :: Set02/05 05:24
koninkjeNow, over in the Prop side of things we have something analogous to lambda02/05 05:25
koninkjeSome people just call it "lambda" ---which leads to all sorts of confusion--- other people call it "forall"02/05 05:25
koninkjeNotably, this is not the same thing as the forall in System F02/05 05:26
koninkjeSo we can ask, what is the type of forall?02/05 05:26
faxwhat confusion does it lead to?02/05 05:26
faxcalling it forall is confusing me02/05 05:26
koninkjeand the wierd thing is we get: forall(x:Prop).e:Prop :: Prop02/05 05:26
koninkjeWell, a lambda constructs a function and has   Pi for a type (which is non-atomic and gives the types of the input and output of the function)02/05 05:27
koninkjeWhereas forall/lambda is a constructor of propositions and just has the atomic type Prop02/05 05:28
faxurgh this does not make sense02/05 05:28
dolioI've never seen "forall" used as an analogue to lambda for prop.02/05 05:28
dolioIt's usually the analogue of pi.02/05 05:29
koninkjedolio: That's the notation used in ATTPL02/05 05:30
dolioI think that's the only way forall(x:Prop).e:Prop : Prop makes sense, too.02/05 05:30
faxI have read ATTPL and I don't know this notation :P02/05 05:30
dolioPi(x:A).B:Set : Set02/05 05:30
koninkjeWell they say "all" instead of "forall" but it's the same difference02/05 05:30
faxI woulh just use Pi for everything02/05 05:31
faxthen you can describe it with PTS02/05 05:31
koninkjeBut there is a difference between Pi as describing a class of terms (namely lambdas) vs Pi/forall as a term itself02/05 05:31
faxbut terms and types are in the same syntactic category02/05 05:31
koninkjeIn PTS they use lambda02/05 05:31
koninkjeBut they are ontologically distinct02/05 05:32
koninkjeThe only reason they're in the same syntactic category is because people are lazy about distinguishing the term and type grammars02/05 05:32
koninkje(for obvious reasons)02/05 05:32
faxin the presentations of PTSs that I have seen, we have Lambda and Pi02/05 05:32
koninkjeYes, but the constructors of propositions are written with lambda in the PTSes I've seen02/05 05:33
faxit's true you could use the same token for both (like use lambda everywhere) -- but that's insane02/05 05:33
koninkjeindeed02/05 05:33
koninkjeAlso, it introduces confusion in higher-order languages since type-level lambda is not the same thing as Pi02/05 05:34
faxhttp://www.cs.ru.nl/~freek/aut/aut.pdf02/05 05:35
fax"We will briefly discuss the lack of popularity in the type theoretic02/05 05:35
faxcommunity of the λ-typed type theories in Section 7.2 below."02/05 05:35
koninkjeMost people also don't distinguish terms as types vs terms as terms, whereas ATTPL does by using "pf" or "prf" type constructors02/05 05:36
faxI think they did that to try and make it easier for beginners to understand -- it seems needless to me02/05 05:37
dolioAre you talking about meta-level pi in the logical framework versus object-level forall?02/05 05:39
dolioBecause there can be an object-level pi, as well.02/05 05:39
koninkjedolio: type-level pi vs term-level forall, yes. The latter could be considered a term-level pi, though there are reasons to avoid that notation02/05 05:40
dolioI mean there can be an object-level pi in addition to the object-level forall for props, but they're both different from meta-level pi.02/05 05:41
koninkje(namely to retain a notion of distinguishing terms from types, which is possible, though most folks have abandoned doing so)02/05 05:41
koninkjeWhat do you mean by object-level pi (as distinct from object-level forall)?02/05 05:41
dolioLet me look something up to make sure I get this right...02/05 05:42
koninkjedo you mean the standard distinction between object and meta, or are you just meaning term vs type?02/05 05:42
dolioOkay, in UTT, Luo specifies Prop in the logical framework like so:02/05 05:43
koninkje(because both term and type are object-level)02/05 05:43
* koninkje really should read some of Luo's work02/05 05:44
dolioProp : Type, Prf : (Prop)Type, forall : (A : Type) ((A)Prop)Prop, /\ : (A:Type)(P:(A)Prop)((x:A)Prf(P(x)))Prf(forall(A,P)) ...02/05 05:44
dolioHe also defines: Pi : (A:Type)((A)Type)Type, \ : (A:Type)(B:(A)Type)((x:A)B(x)) Pi(A,B)02/05 05:45
dolioThat's Pi in the object language he's defining. Just like Prop is part of the object language being defined.02/05 05:46
koninkjeI assume (Prop)Type is his notation for Prop->Type ?02/05 05:46
dolioYes. His notation for LF uses (x:A)B for pi types, and (A)B if x isn't used.02/05 05:46
* koninkje nods02/05 05:47
dolioThere's also eliminators for both of those, but I don't feel like typing them.02/05 05:48
dolioI think Agda 1 was similar to that.02/05 05:48
koninkjeSure. So he's just distinguishing them based on Prop vs Type, and the distinction could be collapsed if sorts were introduced?02/05 05:49
koninkjei.e. Sort={Type,Prop,...} and foo : (S:Sort)(A:S)((a:A)S)S02/05 05:50
koninkjeThough sorts may best be left as a metatheoretic device rather than actually incorporated into the object language02/05 05:51
dolioThe object language he's defining is similar to Coq.02/05 05:51
faxyou know the best book is02/05 05:52
faxfolli.loria.fr/cds/1999/library/pdf/curry-howard.pdf02/05 05:52
dolioThere's a Prop universe and a Set universe (later he gets around to having a hierarchy of universes), and Prop is impredicative, but Set isn't.02/05 05:52
koninkjedolio: sure. (Similarly, Coq's three induction/recursion functions for inductive datatypes could be collapsed into a single one if sorts were first-class)02/05 05:53
faxwhat do you mean first-class02/05 05:53
koninkjedolio: so it's like pCIC then?02/05 05:53
dolioYou can actually do this kind of stuff in Agda, since it has induction-recursion, except you can't define impredicative prop, because it's a negative type.02/05 05:54
dolioWhat's the p stand for there?02/05 05:54
koninkjefax: I mean if sorts were actually part of Coq (the object language) instead of merely in the metatheory describing Coq02/05 05:54
faxkoninkje: aren't they ?02/05 05:54
faxI mean the sorts are {Prop,Type[0],Type[1],...}02/05 05:55
faxand they all have types02/05 05:55
koninkjeWell, Prop, Type[0], Type[1] etc are all in Coq02/05 05:55
koninkjeBut there's nothing which comprises all of those elements02/05 05:55
dolioThe LF methodology is to have Prop : Sort, Type[0] : Sort, etc.02/05 05:55
koninkjeI.e. I can't quantify over {Prop,Type[0],...}02/05 05:55
faxah02/05 05:56
faxyou can quantify over Type though02/05 05:56
dolioAnd then you have prop : Type[0], and El prop = Prop, or something like that.02/05 05:56
faxhm02/05 05:56
dolioThat way you can meta-quantify over all universes.02/05 05:57
dolioAll universes in the object-language.02/05 05:57
koninkjeThen how come universe polymorphism is so esoteric?02/05 05:58
koninkjee.g. why doesn't Coq just define a single inductive/recursive principle for wach data type?02/05 05:58
dolioBecause no one likes programming with the LF and Tarski-style universes. :)02/05 05:58
koninkjeheh :)02/05 05:59
faxhttp://i.imgur.com/1qOPB.png here are the rules for lambda-cube02/05 05:59
faxwell these are the rules: http://i.imgur.com/z9NIS.png02/05 05:59
dolioAnyhow, if you look at some Agda 1 code, one of the things that gets done right away is defining object-level Pi.02/05 06:01
doliohttp://www.dcs.ed.ac.uk/home/pgh/amenities.agda02/05 06:05
glguy_universe polymorphism is marked "experiemental" and I've seen it said on the mailing list that it is subject to change02/05 07:45
glguy_What aspects of it are unfinished and eligible for major change?02/05 07:45
glguy_it seems pretty straight-forward from the uninformed point of view02/05 07:46
copumpkinmaybe how the levels are represented?02/05 07:48
* glguy_ switches computes02/05 07:49
glguyWhy does Rel operate at an arbitrary level?02/05 07:54
glguywhen would I want Set 0 -> Set 0 -> Set 10, for example?02/05 07:55
glguyI guess because the resulting set was already going to be based on some Set 9?02/05 07:55
Saizanyeah02/05 08:09
glguyIs there a practical example where a program uses more than about Set 2?02/05 08:25
Saizanpratical examples? in my Agda? :)02/05 08:27
* Saizan doesn't know02/05 08:27
glguyDo you know where the rules for what level something is in are written down?02/05 08:35
Saizanno, but in that thread Nils pointed to the release notes, iirc02/05 08:36
glguyok02/05 08:36
* glguy switches network interfaces02/05 08:36
glguyAre "inductive families" specifically the data types that use indexes?  data A B : THIS -> STUFF -> Set where ?02/05 09:00
Saizanas opposed to only parametrization? i think so but i'm not sure02/05 09:02
lpjhjdhI'm trying to find the maximal element in a list so I first made a datatype MaxIn indexed by a max, a list, and a proof that it really is a max.  I was then going to rebuild an input list as a MaxIn02/05 09:17
lpjhjdhbut it's proving kind of cumbersome, is this a bad approach?02/05 09:17
lpjhjdhI wrote MaxIn just find, it's the rebuilding that's goofy02/05 09:17
lpjhjdhfine*02/05 09:17
Saizanhow does MaxIn look like?02/05 09:18
lpjhjdhhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=25283#a2528302/05 09:19
Saizani don't think i'd have (∀ y → y ∈ xs → y ≤ m) as an index, maybe as a field, but i think it should be derivable from the rest02/05 09:20
lpjhjdhah, that makes sense, thanks02/05 09:21
lpjhjdhso do you mean I could write: findMaximal : {m : Nat}{xs : List Nat} -> MaxIn m xs -> forall y -> y in xs -> y <= m02/05 09:24
lpjhjdhhmm, maybe I won't actually need the MaxIn, just the lemmas I wrote to give the proofs of an element's maximality02/05 09:26
Saizanyeah, i meant that02/05 09:28
glguyInteresting, in the darcs version of the standard lib, \ex is the type of the dependent pair and \Sigma is just a convenient wrapper02/05 09:32
Saizani guess someone was tired of seeing the extra type parameter in normalized types?:)02/05 09:34
glguyit seems like it means that the goals are just that much less helpful02/05 09:37
glguyyou get to guess what the first type was02/05 09:38
glguysuppose you have: val : A × Set \n val = ?02/05 09:39
glguyGoal: ∃ (λ _ → Set)02/05 09:39
Saizanright02/05 09:39
Saizanbut you can turn on the display of implicit parameters02/05 09:39
Saizanor you can type ? , ?02/05 09:39
glguythere might have been a value that had that tuple type yo ucould have used02/05 09:40
Saizansure02/05 09:41
Saizanthe extra type argument didn't bother me, so i'd probably prefer Sigma as the real type too, unless there's some other reason02/05 09:43
dolioglguy: Universe polymorphism isn't necessarily useful in practice because things need to work at very high universes.02/05 19:30
dolioBut it isn't uncommon to want, say, List Set, and defining a List1 in addition to List isn't a great solution.02/05 19:31
dolioAnd yes, inductive families are indexed data definitions. They allow you to define a whole family of types T x at once, inductively. The family as a whole is closed, inductively, under the constructors.02/05 19:45
* pigworker is experimenting with this IRC client.02/05 20:58
doliopigworker: So, in OTT, is there any kind of distinction between propositional false and the empty set, such that the former doesn't entail arbitrary computational sets (if you take my meaning)?02/05 21:01
pigworkerIIUC you're asking whether the false Prop eliminates over Set or not; the false Prop does eliminate over Set02/05 21:03
dolioYeah, I suppose that's what I'm asking.02/05 21:03
dolioI've been thinking off and on about the EPTS stuff, with regard to erasibility in inductives...02/05 21:04
dolioAnd it occurred to me that given the definition of Squash in Mishra-Linger's thesis, and its eliminator, I don't think you can prove Squash 0 -> 0.02/05 21:05
dolioOr Squash 0 -> A for arbitrary A.02/05 21:05
dolioOnly Squash 0 -> Squash A.02/05 21:05
dolioSo in a sense, you can't prove that Squash 0 is uninhabited, assuming you take that to mean that it entails the empty set.02/05 21:07
pigworkerno escape from Squash, huh? even stronger than double negation!02/05 21:08
dolioActually, it depends.02/05 21:09
* pigworker has just found an annoying bug/feature in Agda's implicit syntax machinery02/05 21:09
dolioHe has a section on the elimination rule for 0, in which he mentions that you can make its type elim_0 : (P : 0 -> Set) => (z : 0) => P z, => being irrelevant pi...02/05 21:10
dolioIf that's the elimination rule, then you can prove Squash 0 -> 002/05 21:11
dolioHowever, there are problems with that rule.02/05 21:11
dolioIf elim_0 : (P : 0 -> Set) => (z : 0) -> P z, then you can't escape from Squash.02/05 21:12
dolio(I think.)02/05 21:13
pigworkerSo the idea is that irrelevant application can unpack Squash?02/05 21:13
dolioSquash 0.02/05 21:15
dolioOr, in general, yes, I suppose.02/05 21:15
dolioBecause Squash holds something irrelevant, so you can only use it in irrelevant spots.02/05 21:15
dolioelim_Squash : (A : Set) => (t : Squash A) -> (P : Squash a -> Set) => ((x : A) => P (poof @A @x)) -> P t02/05 21:17
dolioSo, specialized to 0, you have to provide: f : (z : 0) => 0, but I don't think you can write such a term.02/05 21:18
dolioHe refers to the irrelevant 0 elimination as 'empty type target erasure', if that means anything to you. Evidently it can lead to normalization of erased terms getting stuck on elim_0.02/05 21:23
pigworkerI'd be suspicious of (x : 0) => 0 if irrelevance-erasure is performed before computing *open* terms02/05 21:24
dolio(x : 0) => 0 is actually equivalent in some sense to Squash 0 -> 0.02/05 21:26
dolioIn that A => B is equivalent to Squash A -> B in the non-dependent pi case.02/05 21:27
dolioI suppose (x : 0) => 0 is rather obviously suspect, because it would have to erase to M : 0, plus an application of generalization.02/05 21:31
dolioAnd there should be no closed term with type 0.02/05 21:31
dolioBut if the 0 argument to elim_0 is irrelevant, then elim_0 is just such a term, in a sense.02/05 21:33
pigworkerThis is the kind of issue which makes run-time erasure mechanisms fit badly with proof erasure.02/05 21:42
dolioYeah.02/05 21:43
pigworkerMore precisely, in open terms, there are proofs it's ok to *identify* but not to *erase*.02/05 21:46
* pigworker has just mailed the Agda list with some trouble.02/05 21:48
pigworkerI've been worried for some time that Agda's implicit syntax machinery is suspiciously clever. It turns out that sometimes it's also suspiciously stupid.02/05 21:57
dolioHeh.02/05 21:58
dolioI recall being in situations where I could enter things from a shed that wouldn't subsequently check. I wonder if it's related to this.02/05 21:58
pigworkerMy guess is that it tries to solve (f a b) = (f a' b') by solving a=a' and b=b', even when f is defined and not necessarily injective.02/05 21:59
kosmikusI think I encountered such issues as well. But this was quite some time ago, and clearly a bug. I think your issue is somewhat more tricky.02/05 21:59
doliohttp://code.google.com/p/agda/issues/detail?id=21202/05 22:00
faxhi kosmikus02/05 22:00
pigworkerIf unification makes unforced moves, it becomes dependent on the order in which constraints come up. One symptom of such a dependency is phantom refinements.02/05 22:00
kosmikushi fax02/05 22:01
dolioThat got merged with 118, of course, which has lots of other examples.02/05 22:01
kosmikusyes, that bug report looks familiar02/05 22:02
pigworkerdolio: That's a different problem to the one I'm raising.02/05 22:04
dolioOkay.02/05 22:04
pigworkerMoreover, that's not a Dybjer-Setzer IR definition. level should not be in scope when declaring type02/05 22:05
pigworkerIR definitions are least fixpoints of endofunctors on Sigma Set \ S -> D for some decoder type D (often Set). When you declare a constructor, you may decode only its recursive arguments. Agda doesn't quite see it that way.02/05 22:08
dolioHuh, apparently you can circumvent the positivity checker using this bug.02/05 22:11
dolio118, that is.02/05 22:11
faxI've never proved false02/05 22:12
fax:(02/05 22:12
pigworker118 looks like definitions arriving too late to save a postponed constraint; lack of such-and-such-checking on refinement is surely a different problem.02/05 22:15
stevanhi guys, any suggestions on how one might go about merging the three datatypes here: http://web.student.chalmers.se/~stevan/csallp/html/Formulas.html into one? here is a failed attempt: http://patch-tag.com/r/stevan/csallp/snapshot/current/content/raw/prototype/UlfDataTypes.agda . thanks.02/05 22:38
Saizansince you've a fixed set of labels you could use the naive encoding of row types02/05 22:47
Saizanprobably not the most idiomatic way02/05 22:48
stevanrow types?02/05 22:49
Saizanit's a form of subtyping02/05 22:55
Saizansince basically NQF <: QF <: Fm there02/05 22:56
doliostevan:  You can make dnf work by doing case analysis on t1 and t2, but it won't be pleasant.02/05 22:57
dolioAt least, I think you should be able to.02/05 22:57
Saizanyeah, that would work02/05 22:58
* Saizan tries to remember how the row types encoding worked02/05 22:59
dolioAt least, examining t1 and t2 should lead to contradictions of some kind when they're not nqf.02/05 23:01
dolioMight be hard to set up.02/05 23:02
Saizananother option is to push constraints down rather than calculating the type of the result02/05 23:17
stevanhmm, how do you mean push constraints down?02/05 23:20
faxso whats new02/05 23:21
* pigworker reads logs; has gone brown; poetic justice?02/05 23:29
Saizanstevan: well, take the index as a parameter and add some proof obligations inside the term02/05 23:35
Saizanso that the Type index is always a variable in the definition of Expr and you won't have problems with unification02/05 23:36
Saizanthe obligations should be implicit arguments, and their types should be given by predicates that return \top or \bot , since a value of type \top can be inferred02/05 23:37
Saizanthat's my random thought anyway :)02/05 23:37
stevanah ok, i think i see what you mean now02/05 23:40
--- Day changed Mon May 03 2010
stevani can't find anything on row types, you don't happen to have an url or something, Saizan ?03/05 00:04
dolioLook for papers by Daan Leijen or Simon Peyton-Jones on extensible records.03/05 00:55
stevanthanks03/05 00:59
lpjhjdhwhen is agda unable to solve some constraint?03/05 03:26
lpjhjdhin a pattern match03/05 03:26
lpjhjdhagda is saying .r != r, doesn't the . mean that the term is precisely r?03/05 05:17
glguy.r is probably an implicit variable somewhere03/05 05:18
lpjhjdhit is, I see now when I try to name it, it won't admit .r03/05 05:19
lpjhjdh:(03/05 05:19
glguyThat’s saying the same thing03/05 05:20
lpjhjdhso I've been trying to write a typechecker for the lambda calculus with essentially references using an effect system and have hit a bit of trouble while trying to extend a context and was hoping someone might be able to enlighten me03/05 17:31
lpjhjdhthe typing rule for a lambda abstraction extends the body expression's context by mapping its introduced variable to a type and a region03/05 17:32
lpjhjdhbut I don't have a rule for selecting regions so I can't prove they will be the same for equal expressions03/05 17:32
lpjhjdhor at least that is what I believe to be the issue03/05 17:32
lpjhjdhis there an object anyone could recommend that gives a precise rule for selecting unique names?03/05 17:33
liyanghalp. I don't understand corecursion. :(03/05 22:07
liyangAnd hpaste doesn't seem to work. D:03/05 22:08
liyangSee here: http://pastebin.com/EVSLxkfq03/05 22:10
liyangHow exactly does the productivity checker work anyway? Both ∶D and D∶ are guarded as far as I can see.03/05 22:11
copumpkinid is in the way I think03/05 22:15
copumpkinthat's an interesting CoNat :P03/05 22:16
Saizanwould D∶ = suc (id (♯ D∶)) pass the checker?03/05 22:17
liyangcopumpkin: I don't understand what ‘in the way’ means here.03/05 22:19
copumpkinSaizan: I don't think so03/05 22:20
copumpkinliyang: there's some rule about there only being "constructors" around recursive calls03/05 22:20
copumpkinI don't really know the details or why it's implemented that way03/05 22:21
copumpkinSaizan: yeah, it doesn't pass03/05 22:21
Saizanan arbitrary function could force too much of the recursive call03/05 22:22
copumpkinhttp://snapplr.com/xfkw03/05 22:22
Saizanthough i hope there's room for improvement in the productivity checker03/05 22:23
Saizanmaybe with some laziness analysis :)03/05 22:23
copumpkinit seems like it should be able to see through my example03/05 22:23
liyangSaizan: it's still the wrong colour. :(03/05 22:23
copumpkinliyang: it's really annoying sometimes... when I did a naive translation of luqui's control-monad-omega to agda, I had to write a mini "language" in an ADT in agda, along with an interpreter for it03/05 22:25
copumpkinwhich complicated the proof of the function so much that I was unable to complete it :P03/05 22:25
copumpkin(because I needed my recursive terms to be constructors of some type)03/05 22:26
Saizani wonder if you the anamorphisms pass the productivity checker, in general03/05 22:27
Saizans/you//03/05 22:27
dolioWhat do you mean in general?03/05 22:27
dolioThe problem with D: is that it's not directly guarded by constructors, I believe.03/05 22:29
dolioAgda's checker actually admits things that the usual categorical theory wouldn't.03/05 22:31
liyangdolio: which D: do you mean?03/05 22:31
Saizani mean if for every coinductive type you define you can also define the corresponding unfold03/05 22:31
dolioFor instance, it makes no sense, purely from a coalgebra perspective, for sticking the non-recursive ∞ around recursive arguments to turn it into a greatest-fixed point.03/05 22:32
dolioSaizan: You can do that, I think.03/05 22:32
dolioliyang: Actually, your D: works here.03/05 22:35
dolioWait, I'm wrong.03/05 22:36
dolioI typed :D instead.03/05 22:36
copumpkinwow, dolio is using smilies!03/05 22:37
liyangdolio: was about to ask which version you were using…03/05 22:37
dolioAnyhow, consider tail : U -> U ; tail (u t) = ♭ t03/05 22:37
dolioThen D: = u (# tail D:)03/05 22:38
dolioThat has the same form, but it's not going to work.03/05 22:38
liyang*nod*03/05 22:38
--- Day changed Tue May 04 2010
copumpkinhave there been any interesting recent additions to the agda std lib?04/05 06:51
copumpkinor to agda itself for that matter04/05 06:51
liyangI seem to have reached some sort of mutual understanding with the productivity checker.04/05 16:37
faxmutual?04/05 16:37
liyangNot quite. There was scope for a bad pun there which I've evidently failed to take advantage of.04/05 16:39
fax:J04/05 16:39
faxI am still scared to touch anything coinductive04/05 16:40
Saizanliyang: eheh, so what did you discover?:)04/05 16:41
liyangYesterday I was asking about how to get around Agda not accepting e.g. inf = suc (# (id inf)) as terminating.04/05 16:41
liyang(hang on, fiddling with yesterday's example.)04/05 16:43
liyang(By turning all those function that get ‘in the way’ to constructors of an auxiliary datatype, and interpreting them later.)04/05 17:15
liyangI'm not sure if my example has made it any clearer. :-/04/05 17:15
faxI wonder if that can be automated04/05 17:18
faxbecause everyone seems to be doing it04/05 17:18
Saizanthat's pretty ugly04/05 17:20
Saizani'd rather have some non-termination monad and a way to project values out by proving liveness04/05 17:21
liyanghttp://pastebin.com/s8gBrGUq04/05 17:21
liyang(Yes, it is ugly.)04/05 17:21
liyang(Suggestions for improvements welcome. As are comments that would help me understand exactly what it is I'm doing here.)04/05 17:33
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=14829 <- another example from copumpkin04/05 17:34
Saizanwell, the idea is sort of like implementing a lazy eval interpreter04/05 17:36
Saizanthere should be a paper on this technique04/05 17:39
faxhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=56204/05 17:39
faxthere is a lazy monad with fixed points04/05 17:40
faxhttp://www.cs.st-andrews.ac.uk/~eb/partial.php04/05 17:41
faxSK Combinator in coq04/05 17:41
faxslides describing it http://www.comlab.ox.ac.uk/ralf.hinze/WG2.8/22/slides/tarmo.pdf04/05 17:42
faxComputation by Prophecy  http://www.cs.nott.ac.uk/~vxc/publications/Prophecy_TLCA2007.pdf04/05 17:43
faxhttp://www.cs.nott.ac.uk/~vxc/publications/rec_coind.v04/05 17:44
faxthat's the code from General Recursion via Coinductive Types http://www.cs.nott.ac.uk/~vxc/publications/Recursion_Coinductive_LMCS_2005.pdf04/05 17:44
faxand https://lists.chalmers.se/pipermail/agda/2008/000667.html factorial in agda04/05 17:45
Saizanmh, i guess "the evolution of an agda programmer" would be very weird :)04/05 17:49
fax:D04/05 17:53
liyangThanks, all of that's going to take me a while to digest…04/05 17:55
liyangSo, after all that head-banging last night, and it turns out Nisse already wrote a paper about it: http://cs.nott.ac.uk/~nad/publications/danielsson-productivity.html04/05 20:23
faxyeah that's where the eval stuff came form IIRC04/05 20:24
faxthere's also that one about an ad-hoc monolithic productivity checker04/05 20:24
liyangI haven't been keeping up with the literature lately. :-/04/05 20:26
liyang(/That/ one?)04/05 20:26
* fax neither04/05 20:34
liyangI'm not sure what you're referring to with that ad-hoc monolithic productivity checker. :(04/05 21:00
faxhttp://www.cs.nott.ac.uk/~nad/publications/danielsson-aim9-talk.pdf04/05 21:01
faxhttp://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=10904/05 21:01
guerrillaroll/unroll and fold/unfold are the same concept when talking about \mu abstraction, right?04/05 21:46
faxno I don't think so04/05 21:46
guerrillareally? ok. i'll have to look closer04/05 21:46
guerrillai don't recall having seen fold/unfold used before until i started looking at "Termination Checking with Types" by Abel04/05 21:47
guerrillagreat paper on implementing recursion btw04/05 21:48
--- Day changed Wed May 05 2010
glguy:( trying to "load" a file containing the McCarthy 91 function causes Agda to go off into neverland05/05 01:17
dolioTest case failed, I guess.05/05 01:18
dolioHow did you define the function?05/05 01:21
glguyI'll paste in a moment05/05 01:52
glguyI tried letting it run since I said that earlier05/05 01:52
glguyand came back to all my memory paged out05/05 01:52
glguyhttp://fpaste.org/hxkQ/05/05 01:55
* glguy → Home05/05 02:02
glguyhttp://www.galois.com/~emertens/rlistrec/Induction.List.html is there a simpler way to define rlistrec ?05/05 04:36
glguyhttp://www.galois.com/~emertens/rlistrec/Induction.List.html I think that this version is simpler and rlist-view will be more reusable05/05 08:54
glguyoh... "rlist-view" is already implemented as "Data.List.initLast"05/05 09:31
Saizani'm never going to be able to prove ConvergeNow (1 ∷ .Factorial.♯-0 (fibs-aux g) tt xs) (1 ∷ .Factorial.♯-2)05/05 17:48
Saizanam i?05/05 17:48
faxwhy not??05/05 17:48
Saizan data ConvergeNow {a : Set} (x : a) : a -> Set where05/05 17:48
Saizan    converge-now : ConvergeNow x x05/05 17:48
Saizanwell, because i've no clue on how to handle those .Factorial.#-n05/05 17:49
Saizanare they convertible to something i can refer to?05/05 17:49
Saizani can give you more of the definitions if that helps05/05 17:50
faxwell I like to look at stuff but you should know I have never done anything with codata and I have no idea about it05/05 17:51
faxso I am not very likely to have an idea to fix it05/05 17:51
faxor finish05/05 17:51
npouillardSaizan: I guess you should bisimulation instead of equality05/05 17:52
npouillardif they are Data.Stream's I sugest Data.Stream._≈_05/05 17:53
npouillardinstead of your ConvergeNow which look the same as Relation.Binary.PropositionalEquality._≡_05/05 17:54
Saizanhttp://github.com/Saizan/partial/blob/master/Factorial.agda <- the goal is the first one in fix-fibs-ind05/05 17:55
Saizannpouillard: oh, right05/05 17:55
* Saizan tries to abstract the equality used from the Convergence module05/05 17:57
npouillardSaizan: I don't think you need both \infty and codata in the definiton of D05/05 18:00
Saizanah, i must have missed that when i converted dolio's code to \infty05/05 18:02
npouillardI sugest to use \infty instead of using codata05/05 18:04
Saizanyeah, fixed that, thanks :)05/05 18:05
* glguy doesn't understand when Agda uses the things that it learns from casing05/05 18:19
Saizani don't understand that completely either05/05 18:20
glguywhy do I need to "rewrite eq" in this code to get the type of 'p' to use what was learned when casing on initLast xs?  http://www.galois.com/~emertens/rlistrec/Induction.List.html05/05 18:21
Saizani.e. just matching with refl won't work?05/05 18:22
glguynope, the type of the refl isn't simple enough05/05 18:22
glguyif you were to case on the eq you'd end up with:   .(initLast xs) with-== refl05/05 18:23
* Saizan waits for ghc to load the modules05/05 18:27
glguyThe Induction.WellFounded.Inverse-image module is from the darcs version of the stdlib05/05 18:27
Saizanyup, pulled that05/05 18:32
Saizanig euss the problem is that the need to scrutinize (initLast (ys ++ y ∷ [])) appears only after you've seen that xs is not []05/05 18:33
Saizanso what you'd like to be rewritten is not in the context yet when the rewriting (i.e. the matching) happens05/05 18:34
Saizanthe question is if it's feasible to keep this information around and apply it to the new context05/05 18:35
Saizanthis assuming the question was something like "why doesn't it work by just matching on (initLast xs)?"05/05 18:37
glguySo is what I have there the "simplest" you can write that case of body?05/05 18:44
glguyOh, I think it works if I case on them the other order05/05 18:47
glguyOK, check out that link again05/05 18:48
glguyso in  "with a | b" the things we learned from casing on 'a' are used to rewrite the types of b05/05 18:49
* glguy was just referred to Data.List.Reverse05/05 18:53
npouillardpigworker: hi05/05 19:06
npouillardI was trying SHE today and while the cabal install worked fine, I got trouble with the darcs repo05/05 19:07
pigworkerhi05/05 19:07
npouillardabout some missing patches...05/05 19:07
pigworkerweird; let me try a build from scratch05/05 19:07
npouillardit was the darcs get05/05 19:08
npouillard... a darcs problem, more than a SHE one05/05 19:08
npouillardmaybe a call to darcs repair in the public repo05/05 19:09
pigworkerdarcs get; cabal install just worked for me05/05 19:10
npouillardoh05/05 19:10
npouillardhttp://personal.cis.strath.ac.uk/~conor/pub/she <== is this the right URL05/05 19:10
npouillardit tells that  http://personal.cis.strath.ac.uk/~conor/pub/she/_darcs/patches/20090906150800-4d78e-028efb8f8ab10771d5a6a241e44d035633bdd5a1.gz is missing05/05 19:11
pigworkergood point; I just did a pull over ssh, not http; will try again; (darcs repair sees no trouble)05/05 19:11
pigworkerI just managed to get "darcs get http://personal.cis.strath.ac.uk/~conor/pub/she" to work ok.05/05 19:13
pigworkerthanks for the clue; not sure how to chase it05/05 19:14
* npouillard tried from another machine (with a better internet connection) and it worked05/05 19:15
pigworkergood: I just checked the public repo and that patch is present, with the same permissions as the others05/05 19:17
glguySo what is Nils' nick? I keep getting email answers to my questions that I ask on IRC? Is he reading logs, perhaps?05/05 19:18
glguy(one two many ?s)05/05 19:18
glguyha, damn: too*05/05 19:18
glguy(and I love the email, I'm just curious)05/05 19:19
glguyDoes Agda phone home when I make a type error, perhaps?05/05 19:20
faxhaha05/05 19:20
npouillardpigworker: Is there differences between the darcs version and the one on hackage?05/05 19:22
npouillardhttp://personal.cis.strath.ac.uk/~conor/pub/she/_darcs/patches/20090721161456-4d78e-cb10bcea05ecee5aed80ec015a644d0ba1bcda37.gz: HTTP response code said error)05/05 19:22
npouillardbut wget works on it05/05 19:23
pigworkeryes, the darcs one is different and much more recent05/05 19:23
pigworkerhow odd: I can't see what's different about that patch05/05 19:25
npouillardvery strange maybe a darcs bug...05/05 19:25
pigworkerI don't know enough about darcs, but I do know that the public repo lives under darcs version 1. Maybe I should request an upgrade, but I prefer to avoid making work for sysadmins.05/05 19:27
pigworkerI should update the hackage version, but I've forgotten how.05/05 19:28
glguyNot implemented: type checking of with application05/05 22:57
glguywhen checking that the expression :(05/05 22:57
Associat0rjoin #proglangtheory05/05 23:05
faxA coinductive monad for prop-bounded recursion05/05 23:07
faxhttp://www.plpv.org/plpv07/plpv07-megacz.pdf05/05 23:07
faxAssociat0r please _DO NOT_ do that05/05 23:13
--- Day changed Thu May 06 2010
* glguy_ prospose a new implementation of Data.List.Reverse06/05 07:31
glguy_http://www.galois.com/~emertens/rlist/Data.List.Reverse.html06/05 07:31
glguy_current version: http://www.cs.nott.ac.uk/~nad/repos/lib/src/Data/List/Reverse.agda06/05 07:31
glguy_new one was easier to reason about (for me) and is possibly easier to follow on inspection06/05 07:32
glguy_(but that might be cause I wrote it and am more familiar)06/05 07:32
glguy_and by reason about I mean use when proving06/05 07:34
glguy_Saizan: you alive?06/05 08:05
Saizanglguy_: yup06/05 08:06
glguy_since no one else is and you just joined I'll repost http://fpaste.org/PagH/06/05 08:07
glguy_You don't even hvae to respond if you don't want to06/05 08:07
glguy_At some point I'm going to have to extend the Induction.* modules to be more universe polymorphic...06/05 08:09
* Saizan looks at the code06/05 08:09
glguy_It has implications like the elements and relations that related them of a well-founded relation being stuck in the same level06/05 08:10
Saizanhaving rev defined in a let makes it hard(impossible?) to prove reverseView-[], reverseView-∷ʳ i guess?06/05 08:16
Saizans/let/where/06/05 08:16
glguy_the [] one is there for symmetry06/05 08:17
glguy_the ::r one isn't hard to prove but it would be tedious to have to do the "rewrites" all the time06/05 08:18
glguy_and a bit less resiliant if the implementation ever changed06/05 08:18
glguy_the old version was pretty opaque, for me at least06/05 08:19
glguy_i couldn't figure out how to write the equation forms06/05 08:20
Saizanmh, i haven't had my tea yet, they both look quite opaque to me, but i appreciate that you've splitted up in smaller lemmas06/05 08:22
glguy_I mean "opaque" as in I could figure out how to coax out any values06/05 08:24
glguy_couldn't06/05 08:26
glguy_(taking care of the baby is destroying my spelling tonight... too much rushing about)06/05 08:26
Saizani guess i'd have to try proving something with both of those to tell06/05 08:28
glguy_You'd just have to try to prove reverseView-∷ʳ on the old implementation06/05 08:36
dolioHmm... Type checking HOAS with dependent types is tricky.06/05 09:00
dolioOr at least, it's looking like it's not any easier than various other methods.06/05 09:01
Saizanglguy_: is it even possible?06/05 09:11
glguy_Saizan: I'm not comfortable saying that it isn't possible06/05 09:12
glguy_I wasn't able to06/05 09:12
Saizanah, ok, this is what i was referring to with "Saizan : having rev defined in a let makes it hard(impossible?) to prove reverseView-[], reverseView-∷ʳ i guess?"06/05 09:13
Saizanis there a cong for Setoid's or do i have to require additional properties?06/05 09:43
Saizanconsidering that you can make the rationals as a setoid over pairs i guess i do06/05 09:44
Saizanglguy_: btw, this style of abstracting from the implementation by exposing equations feels like doing twelf in reverse06/05 09:49
glguy_Is that good or bad or indifferent?06/05 09:49
Saizanit's a sign that perhaps a functional logic hybrid language would be better06/05 09:51
glguy_NAD commented the he prefers "correct by construction" to deconstructing the implementation06/05 09:53
Saizanmh, i'm not sure i understand what that means here06/05 09:57
glguy_rather than providing the equations that describe the program I think he liked programs that carried their properties in their results06/05 09:57
glguy_He pointed me to Data.Nat.DivMod as an example06/05 09:58
glguy_Whether or not his comment was actually relevant here that was the module he referred to06/05 09:58
Saizanok, but Reverse is already something like DivMod06/05 10:00
Saizanextensionally there is only one way to build a value of type Reverse xs, the problem is that intensionally there are many and that gets in the way06/05 10:01
Saizanthough i guess we could make a datatype that talks about the ways you can build a Reverse xs06/05 10:02
glguy_yikes06/05 10:03
glguy_Does this concept have a name: (A : Set) (P : Pred A _) (i : A) (x y : P i) → x ≡ y06/05 10:05
glguy_?06/05 10:05
glguy_errr06/05 10:05
glguy_oh, right, that's what I meant. for example: A = List .B and P = Reverse06/05 10:06
Saizanit's a well-known one, but i'm not sure if it has a name by itself, uniqueness of proof? it's related to proof irrelevance06/05 10:08
Saizanbtw, do you have an example where you need reverseView-∷ʳ ?06/05 10:08
glguy_I've since deleted it06/05 10:10
glguy_the module I was using it in is in flux atm06/05 10:10
glguy_I'm playing with a predicate for lists are that "descending" wrt some _<_06/05 10:11
glguy_and I was using it to do:  Descending (xs ::r x) -> Descending xs06/05 10:12
Saizanoh, ok, since it's a bit surprising that you need it06/05 10:13
Saizanso maybe you could've done without06/05 10:14
glguy_maybe, but in general I'm not happy with functions that I can't prove seemingly obvious things about06/05 10:14
* Saizan tries to prove the lemma by going though (A : Set) (P : Pred A _) (i : A) (x y : P i) → x ≡ y06/05 10:16
glguy_I have to go to bed now ,but I'll check the channel log later to hear if it worked06/05 10:18
Saizanunique : ∀ {A : Set} {xs : List A} (x y : Reverse xs) → x ≡ y06/05 11:23
SaizanreverseView-∷ʳ : ∀ {A : Set} xs (x : A) → reverseView (xs ∷ʳ x) ≡ xs ∶ reverseView xs ∶ʳ x06/05 11:23
SaizanreverseView-∷ʳ xs x = unique _ _06/05 11:23
Saizanin retrospect it's fairly obvious06/05 11:23
Saizannow i've to finish writing unique06/05 11:24
Saizanglguy_: http://gist.github.com/392000 <- here it is06/05 11:41
Saizansince i got disconnected the moment i linked it, here it is again: http://gist.github.com/392000 <- proof of the lemma for glguy_06/05 11:44
Saizan(i guess what i said above about extensionality/intensionality is quite bogus)06/05 11:49
glguy_Saizan: well done06/05 17:01
glguy_I'm going to have to learn more about heterogeneous == now06/05 17:02
faxwhat's to know??06/05 17:03
glguy_how to make use of it06/05 17:03
glguy_I haven't opened the module before today06/05 17:04
Saizana definition of Reverse which doesn't use ::r in the index would make the whole thing much simpler i suspect06/05 17:05
* glguy_ heads to work06/05 17:13
glguySaizan, http://www.galois.com/~emertens/rlist/Data.List.Reverse.html#2836 (yeah, same thing you did, but with more pattern matching :) )06/05 18:53
* glguy wanted to work through it as an exercise in using ≅06/05 18:56
Saizanglguy: hah, looks less painful to write :)06/05 19:29
glguyI didn't know about ∷ʳ-injective in Data.List.Properties before reading your code06/05 19:30
glguyI got pretty far reimplementing that function before I looked closely enough to see what that was06/05 19:31
--- Day changed Fri May 07 2010
rntzI can't find any documentation on the "constructor" syntax I've been observing in the standard library07/05 01:56
rntzcan anyone point me to some?07/05 01:56
dolioThat's a somewhat recently added feature for records.07/05 01:57
dolioIt lets you specify a name for an automatically generated constructor. Previously you'd have to write a function yourself using the record { ... } syntax.07/05 01:58
dolioThat's all it does, though. It doesn't let you pattern match with that constructor.07/05 01:58
dolio(At least, as far as I know.)07/05 01:59
rntzThanks.07/05 02:01
Saizanrntz, dolio: with a recent enough Agda you can pattern match too07/05 08:40
dolioReally? Sweet.07/05 08:55
dolioSaizan: By the way, you fooled around with PHOAS a while back, right?07/05 08:58
Saizandolio: yeah07/05 08:59
dolioDid you do any type checking? Or just stuff in the style of the paper, where the types are enforced by construction?07/05 08:59
Saizanthe latter07/05 09:00
npouillardSaizan: I would be interested to look at some PHOAS code in agda too07/05 09:01
dolioI've been fooling with switching an interpreter I wrote to PHOAS internally (because something is wrong with the current string-variables and alpha renaming code, and I have no idea what it is)...07/05 09:03
dolioBut type checking is proving difficult.07/05 09:03
Saizannpouillard: http://code.haskell.org/~Saizan/SystemFpred.agda <- cast can be avoided by postulating extensional equality for functions iirc07/05 09:04
dolioPrimarily (I think) because it uses multiple operations that each internally use different instantiations of the PHOAS.07/05 09:05
dolioSo the operations are well defined on Term c, but the internal operations don't work on the same Term' c v.07/05 09:05
dolioAnd working with Term c directly isn't great, because it's opaque.07/05 09:06
Saizantried working with the different instantiations in parallel?07/05 09:06
Saizanthough Agda won't know that they agree on the structure..07/05 09:07
dolioWell, I'm writing in Haskell, so that doesn't matter so much.07/05 09:07
dolioIt's worth a shot.07/05 09:08
npouillardSaizan: what is inj?07/05 09:09
Saizannpouillard: it's how i inject monotypes into polytypes07/05 09:10
npouillardWhy do you need it?07/05 09:11
Saizanto keep the type system predicative07/05 09:11
Saizan_[_]_ : ∀ {t1 : tvar -> ty} → term (Π t1) → (t2 : type tvar ) {m : T (isMono tvar t2)} → {t1' : ty} → t1 $ t2 ≡ t1' → term t1' <- here i require that t2 which is used for type instantiation is a monotype07/05 09:13
npouillarddo you plan to add a tower of universe?07/05 09:15
Saizaninj is mostly useful to hold the proof so i can do "⌊ inj m {p} ⌋p = ↑ ⌊ m , p ⌋m" i guess.07/05 09:17
Saizanit's been a while since i've touched this code, the ugliness of Subst scared me off i think :)07/05 09:18
npouillardSaizan: sure, but here you are more restrictive than predicative07/05 09:18
Saizannpouillard: ah, do you have an example?07/05 09:19
npouillardid₁ : ∀(α : 1) α → α07/05 09:26
npouillardid₁ = Λ(α : 1) λ(x : α) x07/05 09:28
npouillardid₀ : ∀(α : 0) α → α07/05 09:28
npouillardid₀ = Λ(α : 0) λ(x : α) x07/05 09:28
npouillardid₁ [∀(α : 0) α → α] id₀07/05 09:29
npouillard.07/05 09:29
Saizanah, i see07/05 09:29
Saizani guess mine is predicative restricted to just one level07/05 09:30
npouillardyes07/05 09:31
Saizandolio: i guess the best way is to instantiate to the product07/05 11:38
Saizana datatype introduces a module?07/05 13:37
npouillardno I don't think so, a record does, though07/05 13:37
--- Day changed Sat May 08 2010
glguyhttp://www.galois.com/~emertens/doubleneg/doubleneg.html08/05 11:44
glguyI thought this was kind of a fun use of the PreorderReasoning module08/05 11:44
glguywhere my relation is λ A B → A → B08/05 11:44
Saizancool :)08/05 11:54
Saizanbut what have you proved there?08/05 11:56
glguythat the first line   ->  the last one08/05 11:57
glguythat isn't necessarily interesting08/05 11:57
glguyI just wanted to use curry08/05 11:57
glguyand that notation08/05 11:57
glguyI'm sure that there is something interesting to be done with that notation08/05 11:57
Saizanoh, ok then08/05 11:59
glguyI just hadn't though to use it for -> before08/05 11:59
glguythought*08/05 11:59
Saizanit gives a very old-school logic feeling, too bad that i can't seem to find a way to see the corresponding lambda term from that08/05 12:02
faxlet A (m : Nat) : Nat -> Nat ;08/05 18:14
fax<= Nat.Ind m ;08/05 18:14
fax= Nat.suc ;08/05 18:14
fax= Iter (A xf^1) ;08/05 18:14
faxroot ;08/05 18:14
faxfrom Ackermann.pig08/05 18:14
Saizando you understand the tactic language?08/05 18:16
faxno08/05 18:17
* Saizan neither08/05 18:17
faxI think if you just try random stuff it does the right thing sometimes08/05 18:17
faxI am waiting until there are enough examples that I don't have to actually figure anything out08/05 18:18
faxI can just paste things together08/05 18:18
Saizanheh08/05 18:18
faxoh08/05 18:19
faxand universes08/05 18:19
faxUnorderedPairs.pig is realy nice too08/05 18:20
Saizanxf^1 is the inductive hypothesis i guess08/05 18:21
pedagandfax, Saizan, I'm told that nobody does08/05 18:38
pedagandthe xf^1 kind of names are names automatically generated by Pig, so they are ugly08/05 18:39
faxautomatically generated names? oh no!!08/05 18:39
pedagandyeah...08/05 18:39
faxthis is a bane for back compatability in Coq08/05 18:39
pedagandbut there will be a fix, Adam is working on that08/05 18:39
faxyou have to sometimes go through pages of proof scripts changing everything from x to y08/05 18:39
pedagandthat's a cheap hack for us, right now. But it won't stay long08/05 18:41
pedagandsome discussions about a "high-level" language have started. So, we should be able to define functions by pattern-matching one day.08/05 18:42
pedagandfax, List.pig is probably easier to understand. Fibo, Ackermann & co have been implemented to stress-test the unification machinery. I find myself stressed when I look at them.08/05 18:48
faxhehehe08/05 18:48
faxit is really exciting to see this happening!08/05 18:49
pedagandwell, thanks for your interest :-)08/05 18:56
Saizanpedagand: btw, is there a way to dump a proof script to a file after you've completed a definition?08/05 19:06
Saizanthe elaborated term is even worse to read :)08/05 19:06
Saizan*completed a definition interactively08/05 19:07
pedagandyou can dump the development (that is, a roughly pretty printed representation of the proof tree) but there is nothing to store the proof script08/05 19:07
pedagandI personally use rlwrap, which stores things in an history file08/05 19:07
pedagandI think Adam uses the emacs buffer08/05 19:07
Saizanah, right08/05 19:08
pedagandthe real solution would be either this high-level language or a ProofGeneral interface08/05 19:09
pedagandI don't think we will spend our energy on connecting to ProofGeneral, as the high-level language should come soon08/05 19:10
Saizanmakes sense08/05 19:11
Saizanxf : (m : Nat) -> < plus^1 m xf : Nat > <- this binding is a bit puzzling instead08/05 19:12
Saizanhttp://pastebin.com/cyY77t4z <- in this context08/05 19:12
Saizani guess the xf in the type really refers to xf^1 above08/05 19:13
Saizans/really/actually/08/05 19:13
pedagandbleh, indeed, that's strange08/05 19:14
pedagandI guess, that's a candidate for a bug report :-)08/05 19:16
pedagandbtw, I think you should Nat.ind on m, rather than n08/05 19:22
Saizantrue08/05 19:22
pedagandor do "<= [n] Nat.Ind n", where [n] specify that anything in context before n are "parameters" (global context)08/05 19:23
pedagandthe [n] trick should disappear, super-Adam was working on computing parameters automatically on Friday08/05 19:23
Saizanah, i was wondering what [..] did08/05 19:23
Saizaninfer xf gets the type right08/05 19:23
Saizanso i guess it's a pretty printing problem08/05 19:24
pedagandit's a cheap hack, once again: to determine where the global context stops, local context starts08/05 19:24
pedagandyes, I suspected that too08/05 19:24
Saizanis there a name for those lambdas that get listed? to use it in the issue title08/05 19:24
pedagandI call that the context08/05 19:25
Saizank08/05 19:25
faxhas anyone thought about hwo to do category theory in epigram08/05 19:41
pedagandfax, according to the OTT paper, we are supposed to have it easy08/05 19:47
pedagandI thought about trying some things but lack of time, etc.08/05 19:47
pedagandhem, when I say "easy", I mean "easier" than before, right. Don't misread me :-)08/05 19:48
Saizanany news on the equality for coinductives?:)08/05 19:50
pedagandsorry, what's the story about that, again?08/05 19:51
Saizanthat equality should move towards something more like bisimulation, while currently it's just the structural one you get by default08/05 19:53
pedagandha, ok. That sounds like a question for the Boss :-) me, poor peon, have not been aware on any move on that side08/05 19:55
Saizanhehe, i should send a mail to the list :)08/05 19:55
pedagandI'm told that there will be a pigweek sometime soon, so you should definitely manifest your interest(s)08/05 19:56
Saizanthose are in-person events, right?08/05 19:57
pedagandyep08/05 19:58
pedagandbtw, I've a naive Agda question (being on #agda, I'm trying to be on-topic :-))08/05 19:59
pedagandSaizan, I reckon that you've looked at models/Desc.agda08/05 20:00
pedagandyou might have noticed the "reflFun" postulate08/05 20:00
pedagandI feel bad about it for some weeks now. Is there a way to achieve the same thing, without introducing a postulate?08/05 20:00
pedagandreflFun is (rougly): (f : (a : A) -> B a)(g : (a : A) -> B a)-> ((a : A) -> f a == g a) -> f == g08/05 20:01
faxthis is not derivable in agda08/05 20:02
faxit does have eta but that is stronger than eta08/05 20:02
pedagandyeah, I suspected that because it's the motivating example for OTT. Out of curiosity, when you need something like that in a proof, how do you work around it?08/05 20:04
pedaganddo you rephrase your theorem? Or you introduce this kind of postulate?08/05 20:04
Saizanyou could make it a module argument but that wouldn't change much, or we could look at where it's used an try to see if something weaker fits08/05 20:04
* fax tends to give up.. maybe other people have better methods08/05 20:04
pedagandfax, :-)08/05 20:04
faxyou can use a differen equivalence relation than Identity08/05 20:05
faxlike one that has extensionality built in for function types08/05 20:05
faxbut then you have to prove everything is a morphism if you want to rewrite08/05 20:05
faxit gets a unweildy fast08/05 20:05
Saizanpedagand: i got the same problem when writing down Conor's correctness proof for unification, the solution was to carry around additional properties for the functions involved, it was a pain :\08/05 20:06
pedagandSaizan, it is used in IDesc.agda, to prove that the hosted and embedded Desc are equivalent. But don't waste your time with that, that was curiosity08/05 20:06
pedagandfax, ha ok, I wasn't aware of that machinery. Thanks08/05 20:06
pedagandis it some kind of "setoid" way of doing?08/05 20:07
faxyeah08/05 20:07
faxit's pretty awful08/05 20:07
faxthat is one reason why epigram is so exciting08/05 20:07
pedagandbut Epigram is awful for other reasons: syntax, UI, etc. :-D08/05 20:08
pedagandthanks for your answers, I'll find back my sleep, that's great08/05 20:09
Saizani wonder if you can still prove cong and trans if you add reflFun as a constructor of _==_08/05 20:10
pedagandI wonder if I want to know the answer :-)08/05 20:10
faxwow that is an interesting idea!08/05 20:10
Saizanyou need to make the type an index rather than a parameter though..08/05 20:12
pedagandnaivety again: would "_==_" still be an inductive type?08/05 20:12
pedagandhum, judging by the silence, that was a stupid question :-)08/05 20:15
* fax is trying something08/05 20:16
glguyI didn't see the original question to answer :)08/05 20:16
Saizanit should still be inductive08/05 20:17
Saizanat least, agda accepts it :)08/05 20:17
faxsubst : forall {A : Set} (P : A -> Set) (a : A) -> P a -> forall b -> a == b -> P b08/05 20:18
faxI don't know how to prove this for it though08/05 20:18
faxI mean the predicate P probably needs to be respecting the equivalence08/05 20:18
faxwhich means it's basically setoid again08/05 20:18
doliopedagand: I think the 'real' solution is to use setoids.08/05 20:19
faxhttp://pastie.org/951702.txt08/05 20:19
dolioBut they're quite tedious.08/05 20:19
Saizanyeah, and cong is the same08/05 20:20
pedaganddolio, ok, thanks08/05 20:20
dolioI usually just postulate extensionality. :)08/05 20:21
pedaganddolio, when you say "postulate extensionality", is it a postulate similar to reflFun? Or something even more powerful?08/05 20:32
dolioreflFun is extensionality.08/05 20:33
dolioFor functions, at least.08/05 20:33
pedagandbut without definitional equality collapsing with propositional equality, isn't it?08/05 20:34
Saizanwell, you can pattern match against "reflFun f g p" to get f to be definitionally equal to g in the current context08/05 20:36
pedagandI recall asking Conor, he told that this wasn't really extensionality, just an annoying stuck term. But I can be misinterpreting his saying.08/05 20:36
Saizanand right, it won't reduce to refl08/05 20:37
faxthat's the frustratong things about adding axioms (other than inductive types)08/05 20:37
dolioYeah, it will stick if it ever has to reduce reflFun. I'm not sure I've ever been in a situation where it has to do that, though.08/05 20:38
faxyou cannot add anything new to the convertion rule08/05 20:38
faxI think plastic (which is irritatingly closed source) lets you do this08/05 20:38
pedagandha ok, I think I get your (and Conor's) point now08/05 20:39
pedagandthanks08/05 20:39
doliopedagand: You can postulate 'lem : (P : Set) -> P \/ Not P' and do classical reasoning if you want, too.08/05 20:40
faxyou could probably by pass the problem of no reduction by using a reflective  blah blah this is way too complicated for anyone to actually try in practice08/05 20:41
dolioBut, any results you get from that might get stuck.08/05 20:42
pedagandyeah, I see: in a sense, you can act "as if" your system was extensional / classic, but when you need to compute over these things, it tells you to go away. Did I got it?08/05 20:42
dolioWhich makes it non-constructive, I guess. :)08/05 20:42
Saizanpedagand: yeah08/05 20:44
dolioYeah, 'lem P' won't reduce any further. But elimination of P \/ Not P relies on elements of that type being either inl p or inr np.08/05 20:45
dolioSo you've added an extra element 'lem P' that you can't compute over.08/05 20:45
pedagandGood, thanks.08/05 20:46
Saizanare there interesting datatypes of the form "data T : .. -> Set .. where con : .. -> (t : T ..) -> .. something involving t .." ?08/05 20:47
faxself indexed types?08/05 20:48
dolioThey'd have to be inductive-recursive, I expect.08/05 20:48
Saizanwell, not necessarily, i meant that t might be used in a later field too08/05 20:49
dolioOh, or mutually inductive in that case.08/05 20:49
dolioSaizan: Inductive-recursive universes are easily of that form.08/05 20:51
doliodata U : Set where pi : (s : U) (f : T s -> U) -> U ; T : U -> Set ; T (pi s f) = (S : T s) -> T (f S)08/05 20:51
Saizanoh, right, i had it under my nose :)08/05 20:53
Saizanwithout IR the only way is to make it an argument of some polymorphic function i guess08/05 20:53
--- Day changed Sun May 09 2010
* dolio thinks he may have finally figured out what's blowing up in his interpreter.09/05 02:04
glguySo what are the implications of ∃ becoming a record?09/05 05:20
glguyHow is it different now than when it was a data?09/05 05:21
dolioIt get eta expanded during normalization.09/05 05:21
dolioSo you get p = (fst p, snd p) definitionally.09/05 05:22
glguyah09/05 05:22
glguyI've actually had to define that lemma before09/05 05:22
glguyIs eta-expansion different than eta-conversion?09/05 05:24
glguythe opposite of eta-conversion?09/05 05:24
dolioeta conversion refers to treating it as an equation, I think.09/05 05:25
dolioExpansion is when you use it as a rewrite rule from p to (fst p, snd p). Reduction is the opposite.09/05 05:25
glguyIs there a case when you have a inductive type (but not an inductive family) where you might want a single constructor data type now?09/05 05:27
dolioUsing eta reduction as a rule in your normalization tends to cause problems with confluence, though09/05 05:28
dolioProbably not, since I've been told that you can match on constructors defined for records now.09/05 05:29
glguypreviously it was a syntactical reason and not a theoretical reason?09/05 05:29
dolioPreviously you had to choose between pattern matching and eta equality.09/05 05:29
glguyDo we not have to choose now because of new research or new implementation?09/05 05:30
dolioWell, I don't think there was ever any doubt that pattern matching on records could be implemented. It just hadn't been.09/05 05:30
glguyIsn't there some doubt that dependently-typed pattern matching should be implemented?09/05 05:31
glguySomething about axiom K and some other stuff I didn't know about09/05 05:31
dolioI don't think K is that controversial.09/05 05:32
dolioUnless you're into homotopy lambda calculus or something.09/05 05:32
* glguy goes back to wikipedia again :)09/05 05:33
glguyWhile I work out the consequences of axiom K my son is working out the consequences of rolling over onto his back09/05 05:34
glguyhe works so hard to flip over and then is very unhappy when he succeeds09/05 05:34
dolioHeh.09/05 05:35
glguyhomotopy is bringing up lots of people talking about how coffee mugs are like toruses09/05 05:35
dolioYeah, I don't think there's much out there on homotopy lambda calculus. It's, like, one guy's research project.09/05 05:36
dolioBut I've seen it stated that there's more than one proof of x = x in it, which contradicts K.09/05 05:37
dolioHomotopy has to do with topology, of course.09/05 05:37
doliohttp://www.math.ias.edu/~vladimir/Site3/home.html09/05 05:38
doliohttp://www.andrew.cmu.edu/user/awodey/preprints/homotopy.pdf09/05 05:38
dolioI'm not 100% sure the second one is relevant, but it sounds like it is.09/05 05:38
glguyDoes "refl" ever carry any information? After type checking wouldn't it be safe to erase?09/05 05:39
dolioI think so. But you can only erase it at runtime, if I understand correctly.09/05 05:39
glguyerase at runtime?09/05 05:40
dolioIf you erase equality proofs when you're checking open terms (like during type checking), then you'd be potentially erasing false hypotheses.09/05 05:41
dolioLike \(eq : x = (x -> x) -> <infinite loop goes here>09/05 05:41
glguybut that function would never be called09/05 05:42
glguyanyway09/05 05:42
glguysince you never had an eq to call it with when you compiled09/05 05:42
dolioYou could require it to be normalized during type checking.09/05 05:43
dolioLike, if it's called f, and you try to type check "refl : f = g", then to decide f = g, it has to normalize f and g.09/05 05:44
dolioBut f will loop on normalization.09/05 05:44
dolioAnyhow, the point is, you can erase it (probably) when you're emitting code, but not before you type check.09/05 05:45
glguyright, i was thinking after type-checking09/05 05:46
dolioI know. Just wanted to spell it out. Because there are other schemes where you can do some level of erasure during checking. But that won't work for equality.09/05 05:48
--- Day changed Mon May 10 2010
jonrafkindwhat does an empty pair of parenthesis mean in agda? as in: evalφ t (prim f s) ()10/05 02:00
glguyabsurd pattern10/05 02:26
glguyno value of that type exists so you don't need to provide an implementation10/05 02:26
glguyexample : 1 ≡ 0 → ℕ10/05 02:27
glguyexample ()10/05 02:27
jonrafkindok, thats what I thought. thanks10/05 02:27
jonrafkindcode.haskell.org seems to be dead, anyone have a link to the agda source?10/05 02:32
jonrafkindnm, the haskell guys restarted it10/05 02:43
pedaganddoes anybody know the "pedantic" name for projection of pairs? Like beta for lambda, iota for inductive types, and so on10/05 14:44
pedagandI think I heard (maybe even wrote) \pi-rule once, but I come to doubt about it...10/05 14:45
Saizani've often seen \pi_1 and \pi_2 to refer to those10/05 14:48
Saizani don't remember a name for both at once though10/05 14:49
pedagandok, good. Thanks10/05 14:49
pedagandwell, I guess, it's really two rules, but two rather boring and similar rules :-)10/05 14:50
pigworkerChapter 2 of Zhaohui's book calls them \sigma http://books.google.com/books?id=z3uicYzJR1MC&pg=PA21&lpg=PA21&dq=Luo+ECC&source=bl&ots=grlf2h9WfY&sig=vjVNDMzibE7m9gMNBEP3X2-j9zE&hl=en&ei=3Q_oS93POMqrsAbgw8GOBA&sa=X&oi=book_result&ct=result&resnum=4&ved=0CCAQ6AEwAw#v=onepage&q=Luo%20ECC&f=false10/05 14:55
pedagandha, so I shall abide by the Luo  (hem, sorry about that pitiful joke). Thanks10/05 15:07
pigworkerso you should (so you should be)10/05 15:17
--- Day changed Tue May 11 2010
* dolio now understands the true horror of using string variables and alpha renaming.11/05 00:56
ccasinalpha conversion and fresh variables: the single biggest source of compiler bugs?11/05 01:10
dolioI thought, "I'm not generating induction principles and stuff, so I don't need fancy locally nameless stuff like pigworker suggests." But, I was wrong.11/05 01:12
ccasinyeah, free and bound variables are just different beasts11/05 01:14
--- Log closed Tue May 11 04:05:12 2010
--- Log opened Tue May 11 04:05:17 2010
-!- Irssi: #agda: Total of 26 nicks [0 ops, 0 halfops, 0 voices, 26 normal]11/05 04:05
-!- Irssi: Join to #agda was synced in 80 secs11/05 04:06
--- Day changed Wed May 12 2010
doliopigworker: Ping.12/05 00:42
pigworkerdolio: not long for awake12/05 00:42
dolioI'll make it short, then. Have you considered adding a 'let ... in' sugar for applicatives to SHE?12/05 00:42
doliolet x <- fx ; y <- fy ; ... in e ==> pure (\x y ... -> e) <*> fx <*> fy <*> ...12/05 00:43
pigworkerYes, I have, but not with those semantics.12/05 00:44
pigworkerIf you do it that way, you have to be clear that x is not in scope for fy, which is odd for that sugar.12/05 00:45
dolioIs there a way where it can be in scope?12/05 00:46
dolioOr do you mean 'let ... in' isn't appropriate syntax?12/05 00:46
pigworkerMy thinking is just that inside idiom brackets, let should desugar to do. Moggi-style12/05 00:47
pigworkerI mean, if you use the result of one computation to determine the next computation, that's yer actual monad.12/05 00:47
dolioRight.12/05 00:47
dolioI was actually thinking of situations where I wanted to use it with applicatives.12/05 00:48
pigworker"let" is the original Moggi syntax for monadic bind and that's exactly as it should be12/05 00:48
dolioBut writing (\x y z ... -> ...) <$> ... is awkward.12/05 00:48
dolioor (| (\x y z ... -> ...) ... |)12/05 00:49
pigworkerFor reordering or duplicating values?12/05 00:49
dolioThe thing I was doing recently that made me think of it was pretty printing inside a fresh name generator.12/05 00:50
doliodo px <- pp x ; py <- pp y ... ; return (px <> py <> ...)12/05 00:50
dolioBut that doesn't require the full power of a monad.12/05 00:51
pigworker(| pp x <> (| pp y <> ... |) |) ?12/05 00:51
pigworkermy not-really-a-parser isn't any good at operator precedence, so the flat version isn't available just now12/05 00:53
dolioThat'll desugar into something like (<>) <$> pp x <*> ((<>) <$> pp y <*> ...)?12/05 00:55
pigworkeryes12/05 00:55
dolioThat works, then, I guess.12/05 00:55
dolioAnyhow, what I was doing reminded me that I'd seen a suggestion that do-alike sugar for applicatives would be a series of non-recursive, independent bindings, followed by a pure expression involving those bindings, which was exactly what I was doing.12/05 00:57
dolioI don't know whether it comes up enough to warrant sugar, though.12/05 00:57
dolioAt the time, it was suggested that this was rather like let in Lisp, but I suppose that's actually more like do.12/05 00:58
pigworkerIt could be tidier with better parsing, but you get pure-functions-effectful-arguments with the usual syntax. I agree that naming helps when things are more tangled up.12/05 00:58
Saizansuch as when you're pattern matching12/05 01:00
pigworkerSaizan: I'm not sure what you mean12/05 01:01
Saizan"pure (\p1 p2 ... -> e) <*> fx <*> fy <*> ..." is quite akward since the patterns are far from what they refer to, and you can't massage it into an expression with no new bindings like with <> above12/05 01:02
Saizanunless you use a named function instead of the lambda12/05 01:03
Saizanwhere pN is a pattern more complex than a variable12/05 01:04
pigworkerI see. pN had better be irrefutable12/05 01:04
Saizanyeah12/05 01:05
pigworkerTupling is a nasty way out of the problem.12/05 01:07
pigworkerI don't think "let" has the right associations, but I do take the point that some way to name the values near the computations would be good.12/05 01:11
dolioYeah, I'm not married to 'let' by any means.12/05 01:12
pigworkerSomething like (|p <- c in f blah... |) yields (| (\ ~p -> f) c blah... |)12/05 01:18
pigworkerIt would, of course, be possible to decide how to desugar idiomatic "let" on the basis of a dependency check, but that seems flaky to me.12/05 01:21
dolioThat sounds like it'd be more work than having two different syntaxes.12/05 01:24
pigworkerYes, especially without a real parser.12/05 01:24
pigworkerG'night!12/05 01:37
--- Day changed Thu May 13 2010
Saizanhttp://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=385 <- anyone tried reflection yet?13/05 23:15
--- Day changed Fri May 14 2010
dolioSaizan: I thought about writing a propositional solver like this, but never really followed through.14/05 00:03
dolioOh, I didn't know about the quoting stuff, though.14/05 00:04
Saizanyeah, i should have specified i was referring to the new stuff :)14/05 00:08
guerrillai'm just passing the description of \lambda2 (CoC) in Barendgret's "Lambda Calculi with Types".. and I'm wondering why is the dependent sum type often not introduced? I've seen a few other calculi recently that introduce \Pi without any mention of \Sigma at all. is it because it can be derived or is it just to simplify the descriptions?14/05 21:36
guerrilla\lambdaP2 i meant.14/05 21:37
guerrillajust curious :)14/05 21:38
Saizanafaiu, \Sigma can be derived if you add something like \==14/05 21:44
guerrillayeah. i also figured, if Bool is built-in to a dep.type system.. (true, ..) and (false, ..) may suffice14/05 21:58
guerrillabbiab.14/05 22:01
--- Day changed Sat May 15 2010
dolioguerrilla: The calculus of constructions doesn't have sigma, and you can't encode it. You can encode all inductive types, but not with their strong induction principles.15/05 03:22
copumpkinso you can't have sigma in coq?15/05 03:23
dolioCoq is the calculus of inductive constructions.15/05 03:23
dolioThe calculus of constructions is just a dependently typed lambda calculus. Adding strong inductive types is an extension beyond that.15/05 03:24
copumpkinah15/05 03:25
dolioBut, it's in the same family as stuff like System F and F_omega, which don't have separate inductive types, either, although in those, you couldn't have strong elimination principles anyway.15/05 03:26
dolioSo System F is in a sense just as good as it would be if it were extended with some notion of inductive declaration.15/05 03:27
dolioExcept possibly from an efficiency perspective.15/05 03:28
dolioInductive types might be redundant if you have access to parametricity in the language, though.15/05 03:31
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=2493815/05 03:33
nappingHow does the unicode lexing work? It seems Lexer.x defines identchar only as [ $digit $alpha $op ], where $alpha = [ A-Z a-z _ ] and so on15/05 06:36
nappingis Agda/src/full/Agda/Syntax/Parser/Lexer.x the actual lexer?15/05 06:48
RLais it possible to separate cases into separate functions?15/05 12:36
RLai have a function definition with lots of cases and it makes code so unreadable15/05 12:37
RLait would be nice if i could split it up15/05 12:37
Saizani think the only pratical way is to redefine your datatype15/05 12:53
Saizani.e. instead of "data A where B C D E : A;" you could use "data BC where B C : BC; data DE where D E : DE; data A where bc : BC -> A; de : DE -> A"15/05 12:55
RLaow15/05 13:07
Saizananother way would be to define an ad-hoc induction principle i guess..15/05 13:12
Saizansomething like : (P : A -> Set) -> ((x : A) -> isBC x -> P x) -> ((x : A) -> isDE x -> P x) -> (x : A) -> P x15/05 13:13
Saizanwhere e.g. isBC B = \top; isBC C = \top; isBC _ = \bot15/05 13:14
RLahm, i'm going to try to split case result instead15/05 13:15
RLai can't split datatype15/05 13:15
RLaand i better avoid clever tricks i do not understand15/05 13:15
Saizanyou could keep both the A and the splitted up A and define a conversion function i guess15/05 13:16
RLahm, another question15/05 13:29
RLawhat are variables with dot (.) prepended?15/05 13:30
Saizandot patterns are those whose value is inferred from other patterns15/05 13:35
Saizanthough i think i've seen .x in the types of the goal simply to indicate that such x is an implicit parameter that you didn't explicitly bind15/05 13:36
dolioIt's not really inference, when pattern matching is what you're talking about.15/05 13:40
dolioIt's that the value of (part of) some argument is determined by the value of some other pattern.15/05 13:40
Saizansorry, i used the verb in a non-technical sense15/05 13:40
RLahm, i'm starting to realize what it is15/05 13:44
RLawhat would be the best way to return multiple values from a function?15/05 13:48
Saizanare you using the standard library? if so there's Data.Product15/05 13:49
RLabut if i want to avoid it, i should create my own data type?15/05 13:50
Saizanyeah15/05 13:50
* Gammu Discounts!! Our Special Limited Time Offers Up To May,22!!!New BranD!! Notebooks,Plasma and LCD TV's.Buy your electronic needs at our unique prices. Laptop Sony VAIO® VGN-FW590FFD-575,57$!!!Apple MacBook® Air MC234LL/A-695,27$!!! http://www.elplace.com/15/05 23:00
--- Day changed Sun May 16 2010
copumpkinmaybe I should buy my electronics at elplace.com16/05 00:25
copumpkincan't argue with unique prices16/05 00:25
pigworkeruniqueness of prices requires an extra axiom16/05 00:29
pigworkersorry16/05 00:30
copumpkincan I get linear prices instead of unique ones?16/05 00:30
pigworkerNo. They've been used up already.16/05 00:31
RLado you need something or just want to buy :)16/05 00:32
* Saizan wonders why one has to provide the context separately when quoting a term16/05 00:34
Saizans/term/goal/16/05 00:34
Saizanit feels like working in a language without first-class functions :)16/05 00:34
copumpkin:O16/05 00:36
Saizanhttp://patch-tag.com/r/gallais/agda/snapshot/current/content/raw/src/prop_logic/Examples.agda <- like at the bottom here16/05 00:38
copumpkinI need to look up this quoting stuff16/05 00:42
RLawhole agda looks still like deep magic for me16/05 00:43
Saizanhttp://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=385 <- i started from here, though [1] and the above patch-tag repo are most illuminating16/05 00:44
jotikHello!16/05 20:56
jotikenv2con : ∀{Γ} → Env Γ → Con -- Is there a way to declare this function inline as a lambda expression?16/05 20:57
jotikenv2con {Γ} γ = Γ16/05 20:57
Saizan\ {Γ} (γ : Env Γ) -> Γ16/05 21:09
copumpkinthat works?16/05 21:09
copumpkinwe need an agdabot! :P16/05 21:09
Saizanhehe16/05 21:10
jotik\{Γ : Con} (γ : Env Γ) -> Γ -- this worked16/05 21:21
jotikthanks!16/05 21:21
copumpkincool16/05 21:21
jotikwow, I can even put lambda expressions inside type signatures16/05 21:22
Saizaneven let .. in .. expressions!16/05 21:45
--- Day changed Tue May 18 2010
kaoosHi, if anybody could take a look at http://paste2.org/p/836142 and perhaps help me, or point me in the right direction on how to complete the last of the functions, I would be very grateful, thanks18/05 18:36
kaoosI'm trying to prove that a function (Nat -> Nat) that always output a even value is not surjective18/05 18:38
copumpkinpattern match on x?18/05 18:42
kaooshmm yes, however - if I do so, the goal reads '?0 : (toEven zero | even zero) \== 1 → \bot"18/05 18:48
copumpkinwell zero should be fairly trivial18/05 18:48
copumpkinyou can probably get away with a () in the pattern18/05 18:48
kaooshm, yeah, \lambda () works18/05 18:49
copumpkinyeah, or that18/05 18:49
kaoosbut of course not for the (suc x) case18/05 18:49
copumpkinyeah :P18/05 18:49
copumpkinanyway, I need to run18/05 18:49
copumpkinwill bbl18/05 18:49
copumpkingood luck :)18/05 18:49
kaoosok, thanks!18/05 18:49
stevancodolio: hey, what happend to http://code.haskell.org/~dolio/agda-share/categorica/ ? :-/18/05 19:10
codoliostevan: I had to restart my repository because storing the agda-generated html in it destroyed it.18/05 19:11
codolioAnd I haven't gotten around to adding the category stuff back.18/05 19:11
stevanok18/05 19:12
codolioDon't store agda-generated html in a darcs repository, by the way. :)18/05 19:14
stevani usually have a www: entry in a Makefile nearby which does agda --html and scp:ies the output to the webserver. :-)18/05 19:17
dolioI think something I wrote triggered lots of re-generation of standard library html.18/05 19:17
dolioAnd the generated html seems to have lots of random numbers in it.18/05 19:18
dolioSo I ended up with like 25,000 changes to process.18/05 19:18
stevan:-/18/05 19:20
dolioAnd, of course, I would have just accepted them all, but darcs doesn't seem equipped to handle that many changes at once.18/05 19:20
dolioIt just hung for as long as I cared to wait.18/05 19:20
--- Day changed Thu May 20 2010
copumpkindoes anyone know of any nice set of proof exercises?20/05 01:42
copumpkinfor some reason I feel guilty when I use Bool in agda20/05 08:06
npouillardcopumpkin: that it is not always a bad idea, you can have a property on the side ∀ x → (f x ≡ true) ⇔ P x20/05 08:08
copumpkinyeah, I know there are a few good times to have it and I think this is a good one20/05 08:09
copumpkinbut I still feel a little dirty using it20/05 08:09
copumpkinmaybe I'll think of something better later :P20/05 08:09
copumpkinI really want a graph datastructure where nodes can express properties about their neighbors20/05 09:03
copumpkinthe std lib graph doesn't allow that easily20/05 09:03
copumpkinomg kmc20/05 09:08
kmcomg (?)20/05 09:12
copumpkinyep20/05 09:15
Panarchyhi20/05 11:31
PanarchyMy Professor just mentioned AGDA20/05 11:31
PanarchyHow difficult a language is this to learn?20/05 11:31
dolioThat might depend on your background.20/05 11:33
PanarchyKK20/05 11:55
--- Day changed Fri May 21 2010
copumpkindoes anyone have any ideas about my question yesterday about creating a graph data structure that allows you to specify properties about a vertex's neigborhood? I can do it in an ugly manner but I was wondering if anyone had thought about building a datastructure to support this directly21/05 01:52
Saizanthis property would holds for all the vertexes?21/05 02:28
copumpkinSaizan: possibly. If I had that I could probably encode per-vertex properties too21/05 03:21
copumpkinthat was a deep discussion with Panarchy last night21/05 03:22
Saizanoh, i missed that21/05 03:23
copumpkinhttp://snapplr.com/rrwq21/05 03:23
Saizanah, i didn't catch the sarcasm :)21/05 03:25
copumpkinany ideas about the graph?21/05 03:37
copumpkindid that kaoos guy with the toEven function ever succeed in his proof?21/05 06:04
dolioI'm not sure. Using booleans is a recipe for failure, though.21/05 06:09
copumpkinyeah, I'm just trying his thing now cause I'm bored21/05 06:09
copumpkinwell, that was easy21/05 06:12
copumpkinvery ugly proof though21/05 06:12
copumpkindolio: how would you rewrite it without bools?21/05 06:14
copumpkinhttp://paste2.org/p/836142 was his original code21/05 06:16
* copumpkin still doesn't really understand how to eliminate absurd patterns from negation proofs21/05 06:21
glguycopumpkin: do you mean with things like:  \ ()21/05 06:21
glguythe absurd lambda?21/05 06:22
glguyor \bot-elim?21/05 06:22
copumpkinyeah, or just putting () in a pattern21/05 06:22
copumpkinI can prove things fine using those, but I wouldn't know how to prove the same thing without them21/05 06:22
copumpkinnot sure if that makes sense21/05 06:23
copumpkinfor example, in the proof of the above I wrote a helper forall n -> suc (suc n) == 1 -> \bot21/05 06:23
copumpkinits implementation is an absurd pattern with no body21/05 06:23
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=25607#a2560721/05 06:27
copumpkinoh21/05 06:27
copumpkinthat seems pretty obvious now :)21/05 06:27
copumpkinmuch nicer21/05 06:27
copumpkinI'm not sure I understand the horner encoding of variable identity in the agda ring solver21/05 07:07
copumpkinI should reread the paper21/05 07:11
copumpkincoq is rather ugly21/05 07:20
copumpkineven just the naming schemes people use in it, from what I've seen21/05 07:20
guerrillaif a pure type system is strongly normalising then type checking in it is decidable, right?21/05 12:20
dolioguerrilla: That might depend on how much you think you can add before it's no longer a pure type system.21/05 13:24
dolioIf it's just a lambda calculus parameterized by rules for sorts and whatnot, then yes.21/05 13:25
dolioIf adding an extensional identity type is allowed, then no.21/05 13:26
guerrilladolio: thanks. yes, i meant the former case, literally a PTS as defined by Barengredt21/05 13:32
guerrillathe paper "Pure Type Systems with Denitions" by Severi and Poll adds both global and local definitions while preserving strong normalisation21/05 13:34
guerrillai thought it might be fun to implement but was just curious if it type checking in it would still be decidable21/05 13:34
guerrillait doesn't explicitely state whether it is or not, only that it's strongly normalising, so i though that decidability might have been an obvious consequence of that or something21/05 13:35
guerrillabut when i was reading about another extended PTS (I think with GADTs built-in or something like that), it said the reason it was not decidable was because of beta-reduction (which is used in the beta-conversion rule of any PTS)21/05 13:43
guerrillas/rule/typing rule21/05 13:43
dolioHmm21/05 13:44
dolioWell, regular PTS have checking methods that would seem to reliably terminate if you have strong normalization.21/05 13:45
guerrilladefinitely21/05 13:45
guerrillaas long as the number of sorts is finite21/05 13:45
dolioWell, even with infinite sorts, you just need them to have decidable equality.21/05 13:46
guerrillayeah, i thought so too. i think it may have been stated differently than how i just said it21/05 13:47
guerrillaif it has finite sorts it is decidable, if not, it may not be21/05 13:47
guerrillabut CoC with infinite sorts is not decidable. that was explicitely proven somewhere..21/05 13:48
dolioIt was?21/05 13:48
guerrillayeah, 1sec. let me find where that came from21/05 13:48
guerrillai thought it was "Pure Type Systems for Functional Programming" by Roorda.. but apparently not21/05 13:52
dolioWell, I have a program that does check CoC with infinite sorts. I'd be surprised to learn that it loops somewhere.21/05 13:52
guerrillai think to get it to happen, you have to do something really convoluted21/05 13:53
guerrillacoquand '8721/05 13:53
guerrillaerr '8621/05 13:53
guerrillasection 1121/05 13:53
guerrillablah, no sorry again wrong.21/05 13:53
guerrillanevermind this, i can't find it and it's irrelevant anyway :P21/05 13:54
dolioI mean, it checks lots of other things too. All pure type systems.21/05 13:55
dolioThe sorts are just a parameter, and it just requires Eq in Haskell.21/05 13:55
guerrillayep21/05 13:55
guerrillathinking about it, it seems like it should. but i don't trust myself on that21/05 13:56
dolioI guess it requires the rules, too. But that's just Sort -> Sort -> Sort.21/05 13:56
guerrillayep21/05 13:56
dolioAnd in the case of infinite CoC, it's 'rule _ 0 = 0 ; rule i j = max i j'.21/05 13:56
guerrillayeah, i'm going to use an axiom and rule table though, just to be pedantic21/05 13:57
guerrillaRoorda already did this, http://www.cs.chalmers.se/~jwr/pure/21/05 13:58
guerrillajust making sure i can (and making it a little bit prettier, hehe)21/05 13:58
guerrillahis thing also adds a totally diferent formalism for definitions.. and also adds gadts.21/05 13:59
guerrillaand i think either and both additions makes it undecidable21/05 14:00
dolioI suppose given the axiom of choice, you might be able to define a set of rules that is uncomputable.21/05 14:00
guerrilla(described in his master's thesis)21/05 14:00
guerrillai guess so.. s1 -> s2, s2 -> s121/05 14:00
guerrillahehe21/05 14:00
guerrillaor maybe that'd reject all with pi abstractions21/05 14:01
guerrilla*shrug*21/05 14:01
dolioIncidentally, saying that CoC with infinite universes is undecidable is tantamount to saying that Coq does not have decidable type checking (since Coq is actually extended beyond that).21/05 14:03
dolioWhich would also surprise me.21/05 14:03
guerrillai'm aware of that :) but it could be possible. i also really doubt it though21/05 14:05
dolioWell, in this paper, they have case expressions.21/05 14:05
dolioI can believe that checking case expressions with GADTs can't be done well.21/05 14:06
guerrillai agree21/05 14:06
dolioGHC makes you annotate them manually, I think.21/05 14:06
guerrillayeah, i'm also not convinced it's necessary. the question of whether something is a term or a type constructor seems pretty subjective to me and should remain an artifact of a nice abstraction layer21/05 14:07
guerrilladata constructor i meant21/05 14:07
guerrillai may retract that later though :P21/05 14:09
dolioOh, one issue with CoC, I suppose, is cumulativity.21/05 14:11
dolioMy checker doesn't do anything like that.21/05 14:11
dolioThat would make CoC with infinite universes fail to be injective by this paper's definition.21/05 14:12
guerrillaok21/05 14:12
dolioBecause (i,j,k) is a rule for all k >= max i j.21/05 14:12
guerrillayeah.. i see21/05 14:13
guerrillabtw, anyone know a good latex package to write seq.calc/typing rules in?21/05 14:16
doliohttp://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/nd.html21/05 14:17
dolioI haven't used those much, but they seemed all right.21/05 14:17
guerrillaperfect21/05 14:17
stevancopumpkin, dolio: the surjectiv thing: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25582#a2558221/05 17:01
dolioguerrilla: So, I think I understand what the problem is now.21/05 18:08
dolioguerrilla: If you have infinite sorts, and an infinite number of axioms/rules like '(i,j) j > i' and so on, then the only general PTS checking algorithm you could use is, when you need to use an axiom/rule for a given input, try them all, using a search of some kind.21/05 18:11
dolioBut, that will only work if the term you're checking is well-typed (and your search is good enough to find the solution). If it isn't well typed, you'll never finish rejecting all the possibilities, so you can't decide when a term is ill-typed.21/05 18:12
dolioOr, may not be able to.21/05 18:12
dolioHowever, that doesn't mean there aren't better algorithms for particular type systems. For instance, I think Luo's ECC has decidable checking, despite having an infinite cumulative hierarchy, because instead of having a bunch of rules, he has a subtyping relation between sorts (and pi types), and an algorithm for inferring the least type by that relation.21/05 18:15
doliostevan: Yeah, when I actually worked through it, using booleans didn't seem like much of a handicap. However, in general, when you're working in a dependent type theory, I think it's advisable to split your predicates into something Set/Prop valued that you can use as proofs, and a decider that returns a proof if the predicate is in fact decidable.21/05 18:20
guerrilladolio: yes, ECC seems to be decidable, i just read that a few minutes ago.21/05 23:13
guerrilladolio: check this out, ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/tlca95.ps.gz21/05 23:14
guerrilla"Extensions of Pure Type Systems" by Barthe21/05 23:14
guerrilla(same guy that created the elmt(.|.) etc. stuff)21/05 23:15
guerrillagoing back to the gadt thing, now i'm thinking.. adding non-dependent sum types would preserve SN21/05 23:20
--- Day changed Sat May 22 2010
dolioguerrilla: I don't really understand the point of the K-rules.22/05 01:33
dolioIsn't K equivalent to (\x y -> x)?22/05 01:33
dolioI suppose it is interesting that adding K is equivalent to adding definitions and the other stuff, since K looks so trivial.22/05 01:36
guerrilladolio: yeh, it seems K = id. but built into the TT22/05 02:33
guerrillathink it was just to make a point of.. given an addition, show what effects (if any) this has22/05 02:34
dolioI suppose none of those extensions could really be said to add much power to the type theory.22/05 02:39
dolioI added definitions to my PTS interpreter without even thinking about it.22/05 02:39
dolioBut K appears to be a useless addition, despite being equivalent from a proving strong normalization perspective.22/05 02:41
guerrillayeah, you just have to be careful to not have definitions introduce recursion on accident22/05 02:42
guerrillai think its nice to have it part of the theory though22/05 02:42
guerrillajust.. aesthetics though22/05 02:42
dolioI find it a bit more surprising that subsets and quotients are equivalent to the other two.22/05 02:43
dolioAlthough those two don't really add anything that you couldn't do by hand, I guess.22/05 02:44
dolioAt least in that setting.22/05 02:45
guerrillayeah, the more i look into this22/05 02:45
guerrillait seems that a PTS like CoC can pretty much express everything we want. everything else seems to be sugar22/05 02:45
guerrillaand having just started learning stratego/xt, this is a convenient conclusion22/05 02:47
dolioWell, CoC can't do strong induction principles. That's a genuine addition.22/05 02:49
guerrillayeah, good point22/05 02:49
guerrillawas thinking of trying to generalise \lambda\mu to extend a PTS to do that22/05 02:50
guerrilla"Termination Checking with Types" by Abel for example22/05 02:51
dolioSetoids aren't much fun to work with in my experience, either. So quotient types and the like are handy, if not genuinely offering more power.22/05 02:51
guerrillayeah, i agree with the former, but haven't worked with quotient types much22/05 02:52
guerrillas/much/at all22/05 02:52
guerrillado you know ECC?22/05 02:55
dolioI've read a fair amount of Luo's book.22/05 02:56
guerrillayeah, i just found it22/05 02:57
guerrillaquestion then..22/05 02:57
guerrillahe adds dep.sum types, but is that restricted to Prop?22/05 02:58
guerrilla(i'll read it tmrw, but it's near 4am now)22/05 02:58
dolioDependent sums are specifically left out of Prop, as I recall.22/05 02:59
guerrillaok22/05 02:59
guerrillathat would make more sense22/05 02:59
guerrillamy follow-up then would be why to even have them :P22/05 02:59
dolioYou can make a sum with a Prop in it, but to do so you have to promote the Prop to a Type_i.22/05 02:59
guerrillaah22/05 03:00
dolioBecause they're useful for regular types, too?22/05 03:00
dolioLike, typing algebraic structures.22/05 03:01
guerrillano i meant, if they were restricted to only prop, that doesnt sound terribly useful22/05 03:01
dolioOh, okay.22/05 03:02
dolioYeah, that would probably make less sense.22/05 03:02
dolioEspecially since if they lived in Prop, I think the only way to maintain strong normalization is to only allow the rule (Prop, Prop, Prop).22/05 03:03
dolioSince he mentions that strong impredicative sums allow you to essentially have Prop : Prop.22/05 03:04
guerrillaick22/05 03:07
--- Day changed Mon May 24 2010
pigworkerI wish Agda would infer types for helper functions by Miller unification.24/05 12:53
Saizanif that would reduce the need to annotate functions defined via pattern matching in where clauses i'd like it too :)24/05 14:33
dolioThat's one of the few things I miss of the inference in Haskell.24/05 14:55
pigworkerGenerally, I reckon it should be ok to write f blah = mutter (g x y) where  g pat = exp ... inferring type g (x : X)(y : Y) -> T, where T is the type pushed into the application. We'd need to ensure that T does not depend on any vars whose types depend on x and y, but otherwise, it should work.24/05 15:24
--- Log closed Mon May 24 16:43:11 2010
--- Log opened Mon May 24 16:55:57 2010
-!- Irssi: #agda: Total of 27 nicks [0 ops, 0 halfops, 0 voices, 27 normal]24/05 16:55
-!- Irssi: Join to #agda was synced in 76 secs24/05 16:57
--- Log closed Mon May 24 17:12:08 2010
--- Log opened Mon May 24 17:12:38 2010
-!- Irssi: #agda: Total of 27 nicks [0 ops, 0 halfops, 0 voices, 27 normal]24/05 17:12
-!- Irssi: Join to #agda was synced in 70 secs24/05 17:13
soupdragonwhat about a proo assistant based on category theory?24/05 21:24
soupdragonrather than type theory?24/05 21:24
soupdragonproof24/05 21:24
soupdragonhow can I make it24/05 21:25
soupdragonI tried to immerese category theory in type theory but it sinks24/05 21:25
stevanis that code available somewhere? :-)24/05 21:28
stevansomeone ought to have tried to make a proof assistant based on CT? i can't seem to find anything with google tho...24/05 21:42
soupdragonthe reason I want this is so I can do the book Computation Category Theory24/05 21:42
copumpkinbased on what aspect of CT?24/05 21:44
dolioIf you want to make a proof assistant/language out of category theory, presumably you can't just look at the definitions of categories in general and such.24/05 21:46
dolioRather, you have to look at foundational theories, like the Category of Categories as a Foundation.24/05 21:47
stevanthe notion of computation in CT isn't clear to me...24/05 21:47
dolioBecause those are the sort of theories that have existence claims, rather than just deducing things from definitions.24/05 21:48
dolioSimilarly, type theory is foundational. "Pi types exist. Sigma types exists. Inductive types exist...."24/05 21:48
dolioI don't know if that'll give you an easy proof environment, though.24/05 21:51
dolioType theory works nicely for that because it's essentially a fancy higher-order logic.24/05 21:51
dolioBut viewing logics as a category gets you something that doesn't immediately resemble logic.24/05 21:52
* pigworker has just blogged about Ornaments (with links to code). Knackered now.24/05 22:40
pigworkerI wonder how to compute the proposition asserted by a categorical diagram.24/05 22:48
dolioWow.24/05 23:07
* Saizan tries to replay the List -> Vec passage at home24/05 23:27
--- Day changed Tue May 25 2010
_Cactus_hi25/05 14:35
_Cactus_I have a question about using 'with' views to prove equivalence25/05 14:35
_Cactus_basically, if I have foo with (bar x)  foo | y, how can I prove bar x == y on the right-hand side?25/05 14:36
Saizanthere's the inspect idiom25/05 14:37
Saizanfrom Relation.Binary.PropositionalEquality25/05 14:37
_Cactus_thanks, I'll check that25/05 14:38
_Cactus_ah25/05 14:41
_Cactus_now I see :)25/05 14:41
liyangHere's a lemma, there's a lemma and another little lemma. Fuzzy lemma, funny lemma, lemma lemma, shed. http://is.gd/coLk4 #agda25/05 17:35
_Cactus_hi25/05 21:10
_Cactus_is there a way to do efficient arithmetics with Agda? unary's just not cutting it for me...25/05 21:10
_Cactus_and writing an e.g. decimal representation library would be way over my league25/05 21:11
copumpkinyou could make yourself a binary natural type25/05 21:11
copumpkinoh25/05 21:11
dolioIf you declare your naturals BUILTIN, it will use the underlying Haskell Integer implementation.25/05 21:11
_Cactus_oh25/05 21:11
_Cactus_really?25/05 21:11
dolioYes.25/05 21:11
_Cactus_for what operations?25/05 21:11
dolio+ and *25/05 21:11
_Cactus_let me check if this is enough to speed up _|?_25/05 21:12
copumpkinI remember when I was doing the rational arithmetic though25/05 21:12
Saizanthat's true only for evaluation, right?25/05 21:12
Saizani mean, not typechecking25/05 21:12
copumpkineven with the builtin naturals, it was really really slow at normalizing terms25/05 21:12
copumpkinyeah :/25/05 21:12
dolioI'm not sure why it would use different methods for type checking than for C-c C-n, but perhaps.25/05 21:13
dolioActually, I suppose I do know.25/05 21:14
dolioType checking can occur on open terms.25/05 21:14
Saizanyeah, maybe it's actually checking which kind of terms the arguments are25/05 21:15
_Cactus_am I right in seeing that _divMod_ is written in such a way that native + and * will not speed it up?25/05 21:15
dolioC-c C-n has the same problem if you add postulates, though.25/05 21:16
dolioYou can declare subtraction builtin, too.25/05 21:17
dolioThat will help divMod a little.25/05 21:17
* _Cactus_ looks for documentation on BUILTINs25/05 21:21
_Cactus_I see that there are some BUILTIN declarations in the std library's Data.Nat25/05 21:25
_Cactus_should that be enough?25/05 21:25
stevanyes25/05 21:25
_Cactus_hmm25/05 22:06
_Cactus_I'm using Data.Nat, and it doesn't seem to use native ints for anything25/05 22:06
stevanwhat did you try?25/05 22:13
_Cactus_I may have screwed that up :)25/05 22:16
_Cactus_is there an equivalent of haskell's "seq" for agda? or is everything strict by default?25/05 22:16
dolioNeither.25/05 22:18
_Cactus_so const (1 + 2) "Foo" doesn't evaluate 1+2, right?25/05 22:18
dolioProbably not.25/05 22:18
_Cactus_ooookay. so how do I test if bignum + bignum' is calculated "fast", if I can't show it from main? (since show is horribly slow for large numbers)25/05 22:19
dolioC-c C-n25/05 22:19
dolioAsk the emacs mode to normalize something large.25/05 22:19
dolioLike 20! or something.25/05 22:19
_Cactus_and that doesn't use show?25/05 22:20
dolioIf the built-in is working right, it will show like a base-10 numeral.25/05 22:21
_Cactus_thanks, that seems to work25/05 22:22
_Cactus_sooo.. I see now that I've had machine-native + and * all along... now back to the beginning, is there a way to speed up _|?_?25/05 22:22
copumpkin_Cactus_: get a faster computer25/05 22:23
copumpkin:)25/05 22:23
_Cactus_I mean asymptomatically :)25/05 22:24
copumpkinunary numbers are optimal25/05 22:24
copumpkin_Cactus_: I honestly have no clue :)25/05 22:24
_Cactus_I thought e-ary numbers were optimal :)25/05 22:24
dolioOkay, BUILTIN doesn't optimize equality checking in types, at least.25/05 22:26
stevanwhat are you using _|?_ for? do you need the proofs it creates?25/05 22:28
copumpkindoesn't Rational use it all the time everywhere?25/05 22:29
copumpkinoh maybe not25/05 22:30
_Cactus_stevan: yes, because I'd like to use _|_ in the specification25/05 22:43
stevanis it typechecking or running your stuff that takes long time?25/05 22:46
_Cactus_running25/05 22:46
stevantried compiling it? :-) not sure if that helps tho.25/05 22:50
_Cactus_yes25/05 22:52
_Cactus_as an added bonus, I don't know how I'll display the results in the compiled program, because Data.Nat.Show is so slow:)25/05 22:52
stevanok :-), hmm... i'm running out of ideas. perhaps use the ffi to haskell to call it's show somehow?25/05 23:00
stevanwhy do you wanna run programs on big instances anyways?! you have a proof of it working? isn't that enough? :-p25/05 23:01
_Cactus_well what if the proof is of the existance of some object but I need the actual value?25/05 23:04
_Cactus_I thought that's the whole point of a proven program... that I prove that it will find the right answer, then run it to actually get the answer25/05 23:07
stevanok, yes25/05 23:08
_Cactus_but anyway, I have to leave now25/05 23:08
_Cactus_I'll come by again with the same problem :)25/05 23:08
stevansure, see you25/05 23:09
--- Day changed Wed May 26 2010
pigworkerFWIW, http://personal.cis.strath.ac.uk/~conor/fooling/Bin.agda is a stab at binary numbers.26/05 00:21
Saizananyone used sized types here?26/05 19:24
dolioI've begun before, but got quickly distracted.26/05 19:31
Saizandolio: do you have some code using them?26/05 19:38
dolioI doubt it.26/05 19:47
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=25726#a25726 <- they let you write fold the right way!26/05 19:55
Saizanit seems the implementation in Agda is incomplete, e.g. there's no subtyping26/05 22:25
copumpkin?26/05 22:30
copumpkinoh, the sized types26/05 22:30
Saizanyup26/05 22:31
--- Day changed Thu May 27 2010
* copumpkin is trying a kind of proof he hasn't tried before27/05 01:06
copumpkin:o27/05 01:06
Saizan:O27/05 01:07
copumpkinthis is tricky!27/05 01:13
copumpkinbut I'm avoiding telling y'all what it is cause I'm sure you'll get it in one minute27/05 01:13
Adamantcopumpkin: the rest of the folks here might, I won't.27/05 01:14
Adamantbrain is already fried for the day.27/05 01:14
copumpkinnot even sure it can be proved27/05 01:30
copumpkinseems like it should though27/05 01:30
* Saizan is curious27/05 01:31
* copumpkin tickles Saizan 27/05 01:31
copumpkinI want to try a little longer, then I'll show you :P27/05 01:31
* Saizan makes a tea then and reads some more on sized types27/05 01:33
copumpkingah, this should be easy27/05 01:47
copumpkinSaizan: I'm trying to prove that the keep function Yitz sent to -cafe is impossible27/05 01:47
copumpkinbut the types are all forcing each other27/05 01:47
copumpkinproving something like fix is impossible is pretty easy27/05 01:48
Saizanhow is the thread called?27/05 01:50
copumpkincurrying combinators27/05 01:50
Saizanthe first proposed type, right?27/05 01:52
Saizankeep :: ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b27/05 01:52
copumpkinyeah27/05 01:52
copumpkinI've almost convinced myself that the proof is impossible27/05 01:53
copumpkinbut I'm also convinced that the function can't exist27/05 01:53
pigworkercompleteness of Djinn?27/05 02:00
copumpkin:)27/05 02:00
copumpkinI mean, I trust djinn27/05 02:00
copumpkinbut I'd still like to prove it in agda27/05 02:00
pigworkerDjinn is complete for intuitionistic propositional formulae27/05 02:01
Saizancopumpkin: seen on #haskell the proof of Not (Not (((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b)) ?27/05 02:01
copumpkinoh I got it27/05 02:01
copumpkinmaybe not27/05 02:02
copumpkinhmm, I'm kind of bothered now27/05 02:05
copumpkinI have a Set-level hole that I can't seem to fill27/05 02:07
copumpkinbut the value-level stuff typechecked fine27/05 02:07
copumpkinI guess when agda can't figure out something's a function type and you put a ? in as a parameter, it doesn't make it into a hole27/05 02:10
doliocopumpkin: I wouldn't necessarily expect to be able to prove that that type is uninhabited easily.27/05 02:12
copumpkinmaybe not, but it seems impossible to do?27/05 02:13
dolioAnd if it's classically valid, then you won't be able to prove that at all.27/05 02:13
copumpkinunless I'm missing something27/05 02:13
copumpkincan I prove that I can't prove it? :P27/05 02:13
copumpkinI can make an argument for it27/05 02:14
dolioYes.27/05 02:14
copumpkinI guess that's what @djinn just did in #haskell27/05 02:14
* copumpkin sighs27/05 02:14
dolioIf Foo is a (propositional) classical theorem, then Not (Not Foo) is an intuitionistic theorem.27/05 02:15
copumpkinyeah27/05 02:15
copumpkinbut not vice versa?27/05 02:15
dolioWhich means that you can't prove Not Foo.27/05 02:15
dolioUnless your logic is inconsistent.27/05 02:15
copumpkinyeah27/05 02:15
copumpkinI guess I just confused agda enough to typecheck, minus a Set hole that couldn't be filled27/05 02:16
pigworkeryou should be able to prove the unprovability of Foo, but only by formalising provability27/05 02:16
dolioRight.27/05 02:16
dolioYou'd have to write djinn in agda, more or less.27/05 02:16
pigworkerin other words, prove the completeness of djinn27/05 02:16
copumpkinisn't showing Not (Not Foo) enough to show that Not Foo can't be proven?27/05 02:17
dolioI thought about doing that once, but then I looked at djinn, and it was way more complicated than I expected.27/05 02:17
copumpkini.e., if you give me a proof of Not Foo, I'll give you absurdity?27/05 02:17
copumpkinoh I see27/05 02:17
copumpkinI misread what pigworker said :)27/05 02:17
pigworkerdjinn has an amusing termination proof (plug PAR 2010 gig)27/05 02:18
Saizancopumpkin: what i made djinn prove in #haskell is quite irrelevant27/05 02:20
Saizani made it prove ∀ {t b u t1} -> Not (Not (((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b)), but we'd need Not (Not ((∀ {t b u t1 : Set} -> ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b)))27/05 02:21
Saizanand afaiu those two are not equivalent27/05 02:21
copumpkinoh27/05 02:22
copumpkinwell I still have my informal argument that it's not possible, but it may be flawed :)27/05 02:22
pigworkerhow about forall hmm . ((thingy -> hmm) -> hmm) ?27/05 02:23
Saizanwe'd still have to put the quantifiers inside thingy i think, and djinn doesn't allow that27/05 02:24
dolioWhat was copumpkin trying to prove? "forall ... Not ..." or "Not (forall ...)"?27/05 02:25
copumpkinnot (forall ...)27/05 02:26
copumpkinis that wrong?27/05 02:26
dolioNo. But it'd be an anti-classical result.27/05 02:26
dolioKind of like the one with injective type constructors, or impredicative set.27/05 02:27
copumpkinah27/05 02:27
Saizanthe informal statement was "there's no total function of type ..." so the most appropriate interpretation should be not (forall ..) right?27/05 02:27
pigworkernot and forall are not readily exchangeable, but this is notnot27/05 02:27
dolio(Which lets you prove Not (forall P. P \/ Not P))27/05 02:27
copumpkinSaizan: that's what I thought27/05 02:27
dolioIn other words, I don't think you'd be able to prove it unless you found something that would get a new flag for Agda.27/05 02:29
dolioOr used one of the existing ones.27/05 02:30
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=25737#a25737 is my informal argument27/05 02:30
copumpkinin pseudo-haskell/agda without the explicit foralls on type variables27/05 02:31
dolioIf you turn on injective type constructors, you can get 'Not (forall P -> P \/ Not P)', which probably lets you prove the Not (forall ...) version.27/05 02:31
copumpkinhmm27/05 02:31
dolioSince that gives you LEM, and thus classical logic inside the Not.27/05 02:32
dolioAnd LEM gives you double-negation elimination, and that should let you go from 'forall ... Not (Not P)' to 'forall ... P'.27/05 02:34
dolioSo you can use djinn's proof of Not (Not P).27/05 02:34
pigworkerexactly: negative statements behave classically27/05 02:35
copumpkinhm, interesting27/05 02:36
pigworkernegative statements have not computational content, so their classical content is as constructive as possible27/05 02:37
copumpkinI see27/05 02:38
Saizandoes "∀ {F : Set -> Set} -> (∀ x -> Not (Not (F x))) -> Not1 (Not1 (∀ x -> F x))" hold classically? i can't seem to be able to prove it (with vanilla agda at least), Not1 is Not for Set127/05 02:39
dolioClassically, yes.27/05 02:41
dolioEliminate the Not Not, introduce the Not1 Not1?27/05 02:41
Saizanoh, right.27/05 02:42
dolioYou could permute the Nots with the foralls (turning it into exists in between), but that's probably harder.27/05 02:42
dolioBoy, the function djinn found sure is large.27/05 02:46
dolioI wonder if that's really necessary.27/05 02:46
copumpkinis it possible to write _|_ -> a without using an absurd pattern?27/05 02:55
pigworkeryou just did27/05 02:56
copumpkins/write/write a function of type/ :P27/05 02:57
pigworkerultimately, no27/05 02:57
pigworkerAFAIK, that's the only primitive falsity elimination27/05 02:58
dolioYou can if you define _|_ = forall a. a.27/05 02:58
dolioBut that won't work so nice.27/05 02:59
copumpkinwell, so much for my fun proof I guess27/05 03:03
* copumpkin finds something else "bite-sized" to prove27/05 03:04
copumpkinat least I proved that fix is impossible to write :)27/05 03:04
copumpkin(unfortunately, it was the world's simplest proof)27/05 03:14
* copumpkin is still looking for a good way to make a graph type where nodes can express properties about their neighborhoods27/05 03:17
dolioOh, I had my thinking backwards.27/05 03:17
copumpkinoh the suspense!27/05 03:19
copumpkindolio: how was your thinking backwards?27/05 03:22
Saizan(Not1 (Not1 (∀ {a : Set} ->(Not (Not a) -> a))) <- i can't find a way to prove this)27/05 03:22
dolioI was thinking you could use Not LEM to prove Not type-of-keep, because LEM implies type-of-keep.27/05 03:22
Saizanheh, no27/05 03:23
dolioSaizan: It may not be possible. Not (Not classical-prop) is only necessarily intuitionistically valid for propositional statements, not statements in first-order logic or higher.27/05 03:26
dolioSaizan: In fact, if you could prove that, then the anti-classical proof from injective type constructors would have resulted in a proof of false.27/05 03:29
Saizani suspected something like that27/05 03:30
dolioSame with impredicative set in coq.27/05 03:30
dolioBut there's still an option for that, so presumably it's not outright contradictory.27/05 03:30
dolioAs far as anyone knows.27/05 03:30
Saizanso there's no embedding that handles quantifiers?27/05 03:31
dolioI don't know if there's no embedding, but not that one.27/05 03:32
copumpkin"record types not allowed in mutual blocks" :(27/05 03:32
copumpkinthat seems like a strange limitation27/05 03:33
Saizanhttp://plato.stanford.edu/entries/logic-intuitionistic/#BasProThe <- hah, that's DNS27/05 03:34
Saizanwell, not that, the thing above :)27/05 03:34
copumpkinI don't suppose there's a way to get the visibility in types to go backwards?27/05 03:39
copumpkinlike T x -> (x : Nat) -> ...27/05 03:40
dolioNo.27/05 03:40
copumpkindamn, this is going to force my "list" cons type to be backwards :P27/05 03:41
copumpkinah well, worse things have happened27/05 03:41
copumpkin"Record types are absolutely not allowed to be recursive so allowing them in mutual blocks would mean some extra (non trivial?) checks to make sure everything is safe."27/05 03:43
copumpkinhow are (agda) records more powerful than regular data types?27/05 03:43
dolioThey have eta.27/05 03:43
copumpkineta?27/05 03:45
dolioNormalization of records involves eta expansion.27/05 03:46
doliot = record { x = t.x ; y = t.y ; ... }27/05 03:46
dolioAgda lets me make recursive records, though, so that quote is out of date.27/05 03:48
dolioOr there's a bug.27/05 03:48
copumpkinyeah, a later comment changed it27/05 03:48
copumpkinwas just curious27/05 03:48
copumpkinbut the records still can't live in mutual blocks27/05 03:48
dolioI'm not sure how they accomplished it. It seems like you could eta expand (some) recursive records indefinitely.27/05 03:50
copumpkinyeah, they say it can hang the typechecker if you do that27/05 03:50
Saizanrecords don't have any positivity check27/05 03:52
dolioReally?27/05 03:52
Saizanyeah, you can't recurse over them anyway27/05 03:53
dolioThat's not true.27/05 03:58
copumpkinpff who needs records anyway27/05 04:02
Saizan... i just proved false.27/05 04:03
copumpkinyay!27/05 04:03
copumpkinI love it when that happens27/05 04:03
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=25741#a2574127/05 04:04
Saizani guess the termination checker wasn't that informed some constructors are fake.27/05 04:05
dolioYes, I just did that.27/05 04:05
dolioSubmitting a report.27/05 04:05
copumpkin:)27/05 04:05
* copumpkin hopes that one day he too will be able to prove false27/05 04:06
dolioYou can construct non-terminating elements of U without using the constructor, too.27/05 04:06
Saizanyeah, but you can't use them to inhabit \bot27/05 04:07
dolioActually, you can.27/05 04:10
* Saizan wants to see this27/05 04:13
dolioYou have to use a different type.27/05 04:15
dolioU = U -> A27/05 04:15
Saizanoh, sure, you can just blatantly write fix.27/05 04:18
copumpkinugh, my graph type is not strictly positive27/05 04:25
copumpkinmaybe this is doomed to failure27/05 04:25
doliocopumpkin: Coq allows some degree of switching the order of visibility with its notation.27/05 04:27
dolioBut that'd require fancier parsing/syntax than Agda's current mixfix stuff.27/05 04:27
copumpkinah :/27/05 04:27
dolioThat's how they get nice stuff like { x : A | P x } ==> Sig A (\x -> P x), too.27/05 04:28
copumpkinah :/27/05 04:29
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=25742#a2574227/05 04:31
copumpkincan anyone see a way of making that work? it seems inherently non-positive, but I still want it :P27/05 04:34
dolioNot off hand.27/05 04:35
copumpkinnot even sure how usable it would be if I succeeded27/05 04:36
copumpkinbut it seems like something one might want27/05 04:36
Saizanyou could make up an universe for things of type "Graph Node Edge n → Set" :)27/05 04:39
copumpkin:O27/05 04:39
* copumpkin has not the power to create universes of his own27/05 04:39
copumpkinmaybe I should just settle for separate proofs about graphs27/05 04:41
copumpkinso going back to the proof that keep has an impossible type27/05 04:59
copumpkinit's possible to prove that some types are impossible, and impossible for others27/05 05:00
copumpkinis there a way to determine ahead of time which will be which?27/05 05:00
copumpkinor some way of describing features of a type that make it impossible to prove impossible?27/05 05:01
copumpkin(in constructive logic, at least)27/05 05:01
dolioIf it's just a propositional statement, and it's classically valid, then you can't prove that it's uninhabited.27/05 05:03
dolioBecause Not (Not P) is intuitionistically valid, meaning you can't prove Not P.27/05 05:03
dolioThat's with all the quantification on the outside in each case.27/05 05:04
dolioIt's not that forall .... P being a classical theorem implies that Not (Not (forall .... P)) is an intuitionistic theorem.27/05 05:05
* pigworker just bashed out this STLC beta-eta-long-normalizer http://personal.cis.strath.ac.uk/~conor/fooling/Nobby.agda27/05 13:40
Saizan_the Nat's are supposed to be de-brujin indexes right?27/05 14:24
pigworkerbelieve it or not, they're just names27/05 14:25
Saizan_oh, good, "... | inl y = unq (su y) T (var y)" makes more sense then :)27/05 14:26
Saizan_how'd you define _<_ for Brouwer's Ordinals? i.e. data Ord : Set where z : Ord; s : Ord -> Ord; limit : (Nat -> Ord) -> Ord27/05 16:19
pigworkerx < z is empty; x < s y = x <= y; x < limit f = Sigma Nat \ n -> x <= f n; x <= y if x is y or x < y27/05 16:36
Saizan_thanks27/05 16:46
copumpkinoh for that graph structure I wanted, I can just turn off the positivity checker27/05 22:10
copumpkinwhich is evil, but ah well :P27/05 22:10
dolioYou could prove false, and say that it's a graph.27/05 22:55
copumpkindolio: yeah27/05 23:33
copumpkinhow much can you do with agda's reflection? would it be possible to serialize arbitrary terms?27/05 23:36
stevanthere is a "unknown" term in the agda syntax in agda, so i'd guess it doesn't work for arbitrary terms atm atleast?27/05 23:47
stevani translated pigworker Noddy into something easier (on the eyes): http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25776#a2577627/05 23:49
--- Day changed Fri May 28 2010
Saizancopumpkin: you mean serialize to disk?28/05 00:08
copumpkinwell, get full access to the entire structure, so it could eventually be serialized if someone wrote a Binary-like module for agda28/05 00:08
Saizanyou can only get a term that represent the current goal though28/05 00:10
copumpkinoh28/05 00:10
copumpkinhmm28/05 00:10
Saizanit's something more TH-like than Java-reflection-like28/05 00:10
doliostevan: Heh, I thought you meant that you got rid of the 2-letter type names and such. But you meant that you added unicode.28/05 00:29
stevan:-)28/05 00:30
* Saizan still needs to work out how the Nats work28/05 00:31
dolioEven if you can only get the current goal quoted, it's conceivable that you could get it to quote arbitrary terms.28/05 00:34
dolioBy making a combinator that turns an arbitrary term into a goal by wrapping it thinly.28/05 00:35
dolioPerhaps the type of quoteGoal avoids that, though.28/05 00:36
stevanisn't there a quote keyword which takes a string and quotes it to an agda term also?28/05 00:36
Saizanthere's "quote <identifier>" which gives you the corresponding QName28/05 00:38
Saizanand quoteGoal doesn't really have a type..28/05 00:39
pigworkernew constructor patterns for records appear to be strict28/05 00:44
dolioThey appear to behave exactly like constructors for inductive data.28/05 00:46
dolioYou can even define recursive records, and write structurally recursive functions by pattern matching.28/05 00:46
pigworkerThat fails to respect the definitional equality: they should be lazy.28/05 00:46
dolioAnd they pass the termination checker.28/05 00:46
dolioAlso, records aren't positivity checked.28/05 00:49
dolioI filed a report about that last part, but you might want to mention the laziness.28/05 00:52
pigworkerwill do28/05 00:57
pigworkerBy the way, Nobby was just the warmup for http://personal.cis.strath.ac.uk/~conor/fooling/DepNobby.agda28/05 01:12
dolioGood ol' dependent composition. Such a friendly type.28/05 01:31
copumpkinyou actually using the dependent-ness of it?28/05 01:33
dolioI don't know. It's hard to see anywhere in DepNobby.28/05 01:33
dolioI guess it must be used somewhere.28/05 01:34
dolioWhy not be fully general, if you can, though?28/05 01:34
copumpkinoh, I have no problem with it28/05 01:35
copumpkinwas just curious :) I hadn't looked at DepNobby yet28/05 01:36
Saizansometimes the extra implicit parameters get in the way28/05 01:37
copumpkincould (in theory) agda's inference be any better than it is now, by the way?28/05 01:38
dolioYes, unless Agda is smarter than I think it is, it's hard to imagine that it specializes to the non-dependent case.28/05 01:39
dolioSince it needs to figure out that we mean \ {_} -> g when g is written.28/05 01:39
dolioOr something like that; I didn't go look at the type.28/05 01:40
Saizanyeah, i was referring to something like that28/05 01:40
Saizancopumpkin: i imagine so, pigworker mentioned a possible improvement the other day using Miller unification(?)28/05 01:41
copumpkinoh yeah28/05 01:41
pigworkerDependent composition usually specialises to simpler variants by Miller unification (which Agda does, a bit).28/05 08:16
copumpkinis there a way to get something like GHC's type families (with pattern matching on type constructors) in agda?28/05 08:54
copumpkinit seems like with agda's flexibility you could break parametricity that way28/05 08:54
pigworkerThere's no pattern matching for Set. But you can make a universe and pattern match on its codes (as I did in DepNobby).28/05 09:00
copumpkinah yeah28/05 09:02
kosmikusl.28/05 10:03
kosmikussorry28/05 10:03
* Saizan wonders if you can have an inductive datatype of transfinite sequences28/05 15:14
--- Day changed Sat May 29 2010
Saizani seem to be able to define via well-founded recursion (see nats, merge, ham) things that appear to behave like infinite streams (see take):29/05 00:13
Saizanhttp://code.haskell.org/~Saizan/coord/Ord.html29/05 00:13
Saizanthe two things don't quite fit together to me, comments?:)29/05 00:14
soupdragoncan you prove false with it?29/05 00:17
Saizani don't think so29/05 00:21
* Saizan removed the useless postulates29/05 00:25
TheOnionKnightdoes that still work if you remove the ∞ from Stream? (it looks like it should but I'm not sure)29/05 00:28
Saizanyes, but then you need to use well-founded recursion even to define map29/05 00:29
Saizanno, wait29/05 00:29
TheOnionKnightthe induction principle for Stream should give you map f (y' j<i) for any j<i so it shouldn't be needed for map I don't think29/05 00:31
Saizanyeah, you're right29/05 00:31
Saizanah, repeat is the one i was thinking of29/05 00:32
Saizani knew there was one since i added ∞ for that reason :)29/05 00:33
Saizanwhich was the paper where they make up a small edsl + whnf evaluator to define streams via higher order functions like map or zipWith?29/05 00:42
TheOnionKnightthis one http://www.cs.nott.ac.uk/~nad/publications/danielsson-productivity.html ?29/05 00:47
Saizanyes, thanks29/05 00:48
TheOnionKnightnp29/05 00:48
nappingIs there any way to do local pattern matching?29/05 01:52
nappingIf it is possible to infer a type for a hole, it seems like you could have a (case exp | pat = body | pat2 = body2)29/05 01:54
nappingequivalent to defining a function lem : <inferred type>; lem <free vars> with exp; ... | pat = body; ... | pat2 = body229/05 01:54
nappingIt's a pain to manually copy large intermediate types as a lemma so I can do pattern matching under a lambda29/05 01:56
* Saizan agrees29/05 01:58
nappingis there something special about inference for holes that would prevent translating a case as I suggested above?29/05 01:59
Saizani don't know, but sometimes you have metavariables in the type of the hole, in those cases it probably wouldn't work29/05 02:00
Saizanif you ask on the mailing list you'd probably get some more authoritative answer :)29/05 02:01
nappingdo you know anything about extensional equality, or how to avoid it?29/05 02:01
nappingI29/05 02:01
nappingI've been using hypothesis of Extensionality, which then leads to working under lambda and problems with lemmas29/05 02:02
TheOnionKnightSaizan: you may have noticed but ... your Stream-like things don't appear to behave quite like streams. http://codepad.org/lRHrNX9F29/05 02:02
soupdragoneeeeek29/05 02:02
soupdragonnapping why do you use extensionality?29/05 02:02
nappingfor now I'm just messing around trying to prove monad laws29/05 02:03
copumpkinTheOnionKnight: :O29/05 02:03
SaizanTheOnionKnight: hah, evil :)29/05 02:03
nappingso some sort of looser equivalence than \== is probably what I want eventually29/05 02:03
nappingbut I haven't stumbled across anything like that in the standard library29/05 02:04
Saizannapping: there's some recent experimental work on using this thing called observational equality in Epigram 2, though that's not really usable yet29/05 02:04
soupdragonI wish epigram 2 was ready!29/05 02:05
nappingIs there some sort of pointwise equality setoid somewhere in the standard library?29/05 02:06
SaizanTheOnionKnight: i guess i'd need some sort of parametricity condition :)29/05 02:07
Saizanit shouldn't be hard to define i think? though i'm not sure if a setoid would be more comfortable, rather than less29/05 02:08
nappingIt might need a universe of types29/05 02:09
Saizancopumpkin: btw, do you have that thing you wanted to prove about streams up somewhere?29/05 02:09
nappingOne odd thing with extensionality or maybe the emacs mode is that refining (ext _) clears all the highlighting, but then retypechecking complains at the _29/05 02:12
copumpkinSaizan: hmm, do you remember more specifically what it was?29/05 02:13
copumpkin(sorry chinese food arrived and disconnected me!)29/05 02:13
Saizancopumpkin: about the Omega monad i think29/05 02:13
copumpkinoh29/05 02:13
copumpkinthat was about colists29/05 02:13
copumpkindolio eventually proved it quite elegantly :)29/05 02:14
copumpkinI probably have the shitty code lying around though if you still want it29/05 02:14
Saizannapping: ah, i've heard other cases where refining and typechecking didn't quite agree29/05 02:14
Saizancopumpkin: if it's easy to find :)29/05 02:14
copumpkinSaizan: http://pastie.org/982656 :P29/05 02:18
copumpkinfeeling masochistic?29/05 02:18
Saizancopumpkin: thanks :)29/05 02:18
copumpkinwhat are you going to do with it? :o29/05 02:19
copumpkincry? :P29/05 02:19
Saizanhttp://code.haskell.org/~Saizan/coord/Ord.html <- i seem to have found a way to mix well-founded recursion and coinductive types, i want to see how far it goes29/05 02:20
copumpkinoh cool29/05 02:20
copumpkinlet me see if I can find Colist.NonEmpty29/05 02:20
copumpkinsince I made that and then deleted it29/05 02:20
copumpkinoh, I lost it29/05 02:21
copumpkinbut it's pretty mechanical29/05 02:21
Saizani see29/05 02:24
copumpkina bit of a pain, sorry :)29/05 02:24
Saizanwell, that's half the point :)29/05 02:26
copumpkinnot the right kind of pain though :P29/05 02:26
jmcarthurcopumpkin: :O29/05 02:55
copumpkin:O :O29/05 02:56
jmcarthurwill agda ever get any sort of type erasure?29/05 02:58
jmcarthurof course, usually when i ask a question about agda features it's already been done or it's theoretically impossible29/05 02:59
Saizanthere's a fair amount of published and implemented research on erasing types and proofs from languages like agda29/05 03:04
copumpkinit seems like agda's compiler side isn't getting much love29/05 03:04
copumpkinwhich is fine by me, but it'd be nice to see it become more general-purpose29/05 03:04
Saizanthat's my impression too29/05 03:05
Saizancopumpkin: http://code.haskell.org/~Saizan/coord/DiagonalOrd.html <- i got stripe defined, the proof will have to wait :P29/05 03:59
copumpkinoh nice, without the custom DSL29/05 04:00
Saizanyeah, just some juggling with sizes29/05 04:01
soupdragonSaizan ace29/05 04:01
soupdragonI have no idea how this wokrs29/05 04:01
copumpkinso sizes are hints to the termination checker that you're getting closer to the goal, even though it can't see it?29/05 04:01
soupdragonYou're sure that you can't prove false with this?29/05 04:02
copumpkinbecause that was my problem when I translated luqui's code directly29/05 04:02
copumpkinit translated into fairly pretty agda but was horribly pink29/05 04:02
copumpkinwhich is why I had to jump through all those horrible hoops to make the special language29/05 04:02
Saizansoupdragon: i've not postulated anything, but i'd have to prove the consistency of Agda to be sure of that29/05 04:02
soupdragonyeah I mean specifically this29/05 04:03
soupdragonnot agda in general29/05 04:03
Saizancopumpkin: i use well-founded recursion on the Acc argument when the productivity checker doesn't like what i write29/05 04:04
* copumpkin doesn't even know what well-founded means :)29/05 04:04
* copumpkin looks it up29/05 04:04
Saizanwell, it's well-founded on the ordinal i, which gets transformed into structural recursion on Acc, to be more precise, i guess29/05 04:05
copumpkinah, I see29/05 04:05
Saizansoupdragon: how'd you go about checking if we can prove false with this?29/05 04:06
soupdragonjust like if you can see a way29/05 04:07
Saizancopumpkin: however i'm not so sure what these things actually are..29/05 04:07
Saizani could easily prove false if there was an ordinal o such that o < o or equivalently o = suc o, but that's hopefully impossible29/05 04:09
copumpkinyay29/05 06:36
copumpkinanother convert to the Church of Agda29/05 06:36
danharajHey, I only read the brochure so far.29/05 06:36
danharajI'm also picking up C# to join a friend on a project, so my conversion will take a while more.29/05 06:37
* BMeph counts the seconds before copumpkin starts handing out tambourines...29/05 06:37
danharajSo, what is the nicest way to work with Agda on windows?29/05 06:47
danharaj(no emacs)29/05 06:47
copumpkinwith emacs29/05 06:51
copumpkin:P29/05 06:51
danharajBah, I don't want to grow a neckbeard.29/05 06:52
danharajSo is there an ide? or should I just roll with Notepad++ like a gangsta?29/05 06:59
copumpkinemacs is the ide29/05 07:00
copumpkinmany have resisted emacs in the past for agda29/05 07:00
copumpkinall have succumbed29/05 07:00
danharajle sigh.29/05 07:01
danharajFine I'll do it, only because I already have emacs installed. I just lost interest within 5 words in the manual.29/05 07:01
danharajCurious: What does the name agda mean?29/05 07:01
copumpkinwow, nad was harsh on my feature request :P29/05 08:54
copumpkinI figured out a way around my non-positive type for that weird graph I wanted to build29/05 08:58
copumpkinI just give each node access to its neighbors instead of the whole graph29/05 08:59
copumpkinnot ideal, but it'll work I think29/05 08:59
pigworkerfiled bug report, based on strict record constructor matching: SR fails! http://personal.cis.strath.ac.uk/~conor/fooling/RecConBug.agda29/05 11:35
Saizanbreaks SR in the sense that both goo and goo' normalize to the same term but they don't get the same type?29/05 14:21
stevandanharaj: the name comes from a swedish song, http://youtube.com/watch?v=oKUscEWPVAM29/05 14:46
pigworkerSaizan: yes; goo' is defined to be the normal form of goo.29/05 15:20
--- Day changed Sun May 30 2010
Saizanyou're in a maze of twisty little Any datatypes, all alike..30/05 01:40
tomberekhello30/05 12:23
Saizanhi30/05 12:46
tomberekSaizan: hehe30/05 12:47
tomberekwas curious about some Agda, reading tutorial, installing30/05 12:47
Saizangood30/05 12:47
tomberekSaizan: your thoughts30/05 12:52
tomberekon the Haskell / Agda relationship ?30/05 12:52
Saizanwell, in agda a lot of what you'd want to do with GADTs and type hackery in haskell is much simpler and saner and i like the ability to prove properties of my code. though i've some occasional fights with the termination checker.30/05 13:10
Saizanoh, and i tend to miss typeclasses :)30/05 13:11
wmgreetings everyone30/05 21:09
wmi'm trying to compile http://www.cs.cmu.edu/~drl/pubs/ml09sectyp/ml09sectyp.tgz30/05 21:10
wmand there are dozens of name clashes using the darcs version of agda30/05 21:10
wmas in30/05 21:10
wmThe modules Nat.Nat and Nat clash.30/05 21:11
wmwhen scope checking the declaration open Nat.NatOP public30/05 21:11
wmi'm now renaming the modules like Nat to Natm which is ugly30/05 21:11
wmhas anzone thought of good naming conventions for those cases?30/05 21:12
nockerhi30/05 23:25
nockerwhat does agda wstand for?30/05 23:26
dolioI'm not sure anyone here is going to know the answer to that.30/05 23:27
dolioThe Agda people here use is Agda 2, which presumably got the name from Agda 1. But I think the implementors aren't even the same.30/05 23:27
--- Day changed Mon May 31 2010
tomberekhello31/05 01:20
danharajWhat is the best way to install and set up agda on 64-bit windows? the wiki says that the prebuilt packages are not for 64-bit31/05 04:10
Saizantried "cabal install Agda"?31/05 04:11
danharajah, that could work.31/05 04:11
danharajIs agda really that closely allied with Haskell?31/05 04:12
Saizanwhat do you mean?:)31/05 04:13
danharajUsing the same package infrastructure, being able to import haskell functions... what else is there :p31/05 04:13
danharajCan you derive haskell code in agda?31/05 04:14
Saizanah, well, it's just that Agda is implemented as an haskell library :)31/05 04:15
danharajo rly31/05 04:15
Saizani don't think there's any easy to use code extraction facility, but i didn't look for it31/05 04:15
Saizanthough the compiler probably emits haskell31/05 04:16
danharajWhen I tried to cabal install agda, I got an error about a file not having a newline at the end.31/05 04:31
danharajSo I downloaded the cabal tarball and fixed it, it looks like it built correctly, but who should I notify about this error?31/05 04:31
Saizanhttp://hackage.haskell.org/package/Agda <- the mantainer, or maybe directly on the bug tracker31/05 04:37
Saizani guess it's something windows specific31/05 04:37
danharajI guess I have to learn emacs now :|31/05 04:42
danharajI have to say, Agda does not invite me into its home with cookies and milk.31/05 04:42
dolioIt's worth it.31/05 04:42
dolioYou'll miss the features when you go back to write Haskell or whatever.31/05 04:43
danharajFor a second I wasn't sure if you meant emacs or agda :p31/05 04:43
dolioThe features of the emacs mode.31/05 04:43
dolioThings like "tell me what type of thing I need to put in this hole in my code."31/05 04:44
danharajthat's a feature I did not care for in visual studio.31/05 04:45
dolioI imagine it's a little less interesting there.31/05 04:46
danharajyes I suppose agda types are decidedly richer that C++ types.31/05 04:46
dolioWell, that's not necessarily true if you want to look at things a certain way, but I doubt the visual studio tool would extend in the same way.31/05 04:48
danharajalright, so are there any tutorials that simultaneously teach agda and emacs? Because I am new to both.31/05 04:49
dolioNot that I know of. Truth be told, I don't use all that much emacs fanciness (I think).31/05 04:50
dolioC-n and C-p go down and up. C-f and C-b go right and left. C-e and C-a go to the end/beginning of the line. C-d deletes a character.31/05 04:52
Saizanyou really use those to move the cursor?31/05 04:53
dolioYes.31/05 04:53
* Saizan is amazed31/05 04:53
dolioC-space sets a mark. C-w cuts the stuff between your cursor and the mark. C-y pastes. C-k cuts the rest of the line. C-s starts a forward search, C-r a backwards search...31/05 04:54
Saizani guess the advantage is that you don't have to move the right hand from its usual position31/05 04:54
dolioC-x C-s saves C-x C-c quits. And the rest you can probably learn by looking at the agda menu, and the right-click menu for a shed.31/05 04:55
danharajI'm on a dvorak layout, so f p b n are kind of in awkard positions for moving like that.31/05 04:55
danharajso  how does agda mode work? What does that even do?31/05 04:55
Saizanyou can use the arrow keys too31/05 04:55
danharaja and e are perfect :p31/05 04:56
danharajM-a M-e31/05 04:56
dolioAnyhow, in agda mode, you can type stuff like 'foo x y z = ?' and load the file, and it will type check everything, and if successful you'll get something that looks like 'foo x y z = { }0', where that last part acts sort of like 'undefined' in Haskell, in that it will take on any type, but you'll be able to enter commands to manipulate the definition in various ways.31/05 05:00
dolioLike, there's a command for 'expand the definition to do case analysis on x'.31/05 05:00
dolioOr, 'tell me what type the hole needs to be'.31/05 05:00
dolioOr 'see if this term is the right type, and fill it in if so.'31/05 05:01
dolioAnd other stuff I use less, like 'try to figure out what the term should be by yourself.'31/05 05:01
danharajso how do I turn on agda-mode?31/05 05:07
doliohttp://wiki.portal.chalmers.se/agda/agda.php?n=Main.README-2-2-631/05 05:09
dolioI think that should say.31/05 05:09
dolioEvidently you run "agda-mode setup".31/05 05:10
danharajI did that in the command line. Now how do I invoke the agda-mode commands in emacs? Are they now always available?31/05 05:11
dolioHow did you start emacs?31/05 05:11
danharaj'emacs' in the command line31/05 05:12
dolioIt'll probably auto-load it if you start it with 'emacs Foo.agda'.31/05 05:12
danharajah31/05 05:12
danharajand how would I load it otherwise?31/05 05:12
dolioI think you can do meta-x and type in agda-mode.31/05 05:13
danharajah yes, I think you're right.31/05 05:13
danharajI think I need haskell-mode too, as it says it cannot load haskell-indent31/05 05:13
Saizanyup31/05 05:13
danharajwhat does ~ stand for in paths? Specifically for windows, would that be the toplevel directory of the drive? e.g. C:\ or F:\?31/05 05:22
dolio~ is your home directory.31/05 05:24
dolioI'm not sure what it means on windows. Probably something inside Documents and Settings.31/05 05:24
danharajhuh, alright everything seems to be in order. Thanks guys.31/05 05:31
danharajThat's enough wrestling tonight X_X31/05 05:31

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