--- Log opened Sat Jan 01 00:00:58 2011
Saizanis there an algorithm for transforming recursive definitions accepted by the termination checker into definitions that use eliminators? at least for the inductive cases?01/01 13:14
dolioSaizan: Look for Eliminating Dependent Pattern Matching.01/01 21:30
--- Day changed Mon Jan 03 2011
stevanpigworker: hi, you reckon partial refinements a la the "when is a type refinement an inductive type" paper are possible in the ornament setting? the deletion of info you mention in the discussion isn't quite the same thing, or?03/01 10:55
pigworkerstevan: It's trivial to do partial refinement in the ornament setting.03/01 12:12
roconnorWhere can I get Simmon's and Licata's Abstraction Theorem code?03/01 14:59
stevanhmm03/01 21:22
stevani'll have to give that a try...03/01 21:23
--- Day changed Tue Jan 04 2011
sullydoes there exist a pastebin with agda syntax highlighting?04/01 02:24
sully(I think I know the answer to this question.)04/01 02:24
pumpkinno, but one is coming as soon as I get some time to polish up my agda syntax highlighter so chrisdone can put it into hpaste.org04/01 02:25
pumpkinI've given up trying to give ETAs on it though04/01 02:25
sullyoh, cool04/01 02:26
-!- Irssi: #agda: Total of 33 nicks [0 ops, 0 halfops, 0 voices, 33 normal]04/01 10:08
--- Day changed Wed Jan 05 2011
yrlnrypigworker: I am intrigued by your very recent tweet "I think it's important to emphasize the extent to which a bit of dependent typing can improve basic hygiene standards, with not much proof."05/01 16:15
yrlnryI would be grateful if you could elaborate a bit.05/01 16:15
pigworkerI just mean that there's plenty of stuff you can do if you just want a little more precision, but maybe not total correctness, without writing much more than the type and the program.05/01 16:25
Saizanwhich is roughly the area haskell gadts try to cover05/01 16:29
pigworkeryeah, and the benefits are already clear; the static-dynamic separation is annoyingly rigid, though05/01 16:35
yrlnry What kind of stuff?05/01 16:39
Saizani'd like some guarantee about forcing/erasure for those gadts values that are known at compile time though, and maybe something like coq modulo theories for type families, so i wouldn't even need to pattern match on proof terms to make things typecheck05/01 16:41
--- Day changed Thu Jan 06 2011
copumpkinhttp://hpaste.org/42787/data_airty06/01 01:22
copumpkindamn typos06/01 01:22
copumpkinanyway, is that just crazy talk?06/01 01:22
copumpkinI feel like it would be possible for me to write my families manually like that with equality proofs and sigmas06/01 01:25
copumpkinwithout the data notation06/01 01:25
pigworkerseems a bit lurid to me; can't you parametrize by a universe or something?06/01 01:27
copumpkinoh, I don't need it06/01 01:28
copumpkinit just occurred to me and was wondering if it was possible06/01 01:28
pigworkerit takes some heavy staring to see why it might make sense; I'm surprised it's rejected, but pleased06/01 01:30
copumpkinwould epigram reject it?06/01 01:32
copumpkineither of them06/01 01:32
copumpkinbeware the whore naturals06/01 04:10
copumpkinhttp://snapplr.com/vkbv06/01 04:10
copumpkinpigworker: do you know what happened to the 5th part of your lectures on http://www.cs.uoregon.edu/Activities/summerschool/summer10/curriculum.html ?06/01 17:14
copumpkinthe link is a 40406/01 17:14
pigworkernot a clue06/01 17:14
copumpkindamn, I've emailed the site maintainer06/01 17:15
copumpkinI'll see if they know :)06/01 17:15
pigworkermy involvement with the video stopped when they pressed stop06/01 17:15
copumpkinah okay06/01 17:16
djahandarieOoh, these are neat06/01 17:56
copumpkinthey sure are06/01 17:57
copumpkinonly one missing is pigworker's last though06/01 17:57
djahandarieLunch break is over though, will need to continue this video journey another day :(06/01 17:58
dantenpumpkin, the forth video contains both lecture 4 and 506/01 20:32
dantenfourth *06/01 20:33
pumpkinoh, weird06/01 20:38
pumpkinhadn't gotten there yet, so didn't notice :)06/01 20:38
djahandarieIt is slightly odd when someone joins the room and replies to something they weren't here for, lol06/01 20:39
dantenhehe, always reads the logs :)06/01 20:40
pumpkin:P06/01 20:41
pumpkinI've received emails from NAD about things I've said in here06/01 20:41
pumpkinand he's never in here06/01 20:41
pumpkinspeaking of which, I really need to get around to implementing the changes I said I'd make in the agda syntax highlighting support06/01 20:42
dantenI'm only receiving bug reports from him..06/01 20:42
danten;)06/01 20:42
pumpkinif I didn't know better, I'd think that orangesquash.org.uk domain belonged to me06/01 20:43
pumpkinwhose is it, anyway?06/01 20:43
dantendunno06/01 20:43
dantenI think Laney06/01 20:44
jeltschHi, is there a MIME type for Agda source code?06/01 21:13
sullyhm06/01 23:03
sullywhen I try to load the "lists as polynomial functors" example from "Dependently Typed Programming in Agda"06/01 23:03
sullyemacs colors it yellow06/01 23:03
copumpkinit might be due to universe polymorphism?06/01 23:03
copumpkinwhat are the unresolved metas?06/01 23:03
sullyhow do I determine that?06/01 23:04
copumpkinit should print things like _206: Sort06/01 23:05
copumpkinin the status window06/01 23:05
sullySort _16706/01 23:05
copumpkinoh yeah06/01 23:05
sully_168 : _16706/01 23:05
copumpkinyeah06/01 23:05
copumpkinso you probably have a f : {A} -> A -> ...06/01 23:05
copumpkinor something like that06/01 23:05
copumpkinwhere you just want to change that to {A : Set}06/01 23:05
sullythat did it06/01 23:06
sullythanks06/01 23:06
copumpkinnp06/01 23:06
* sully also a little bit lost at this point in the tutorial06/01 23:06
copumpkinhow so?06/01 23:06
sullyI feel like while the polynomial functor stuff might be great motivating examples for people who know anything at all about category theory06/01 23:07
copumpkinoh :P06/01 23:07
copumpkinyeah06/01 23:07
sullyyeah06/01 23:07
sullymostly the problem is that I know absolutely nothing about category theory06/01 23:07
copumpkinhave you used much haskell?06/01 23:08
sullyexcept that it involves things like functors and arrow and endofunctors and Zygohistomorphic prepromorphisms06/01 23:09
sullyno, not much06/01 23:09
copumpkinlol06/01 23:09
copumpkinalright06/01 23:09
sullyI've played around with it some06/01 23:09
copumpkinthe functor-ness of this isn't too essential06/01 23:09
sullyto get some understanding of typeclasses and monads06/01 23:09
copumpkinbut have you come across things like nat = mu x. 1 + x ?06/01 23:09
sullybut I've spent most of my time in Standard ML06/01 23:10
sullyyeah.06/01 23:10
copumpkinthat's pretty much what this is about06/01 23:10
copumpkinlist a = mu x. 1 + a * x06/01 23:10
copumpkinmu is the mu they have in there06/01 23:10
copumpkinand you get * and + and 1 and 006/01 23:10
sullywell, I guess actually I've spent most of my time in C, but... :P06/01 23:10
* sully nods06/01 23:10
copumpkinactually no 006/01 23:10
sully(or maybe C++; every intership I've ever had has involved writing C++)06/01 23:11
sully(sigh.)06/01 23:11
copumpkinbut it's basically arithmetic of that sort, and it turns out any such structure can be mapped generically, which makes it into a functor06/01 23:11
* sully nods06/01 23:11
sully(a friend of mine took a category theory class so that he could understand the statement "A monad is just a monoid in the category of endofunctors, what's the problem?")06/01 23:14
copumpkin:P06/01 23:14
sullyapparently all of the pieces came together on the last day of class06/01 23:15
copumpkinawesome06/01 23:15
--- Day changed Fri Jan 07 2011
Saizandolio: iirc you said with IR you can embed a whole tower of universes into Set, do you have the code handy?07/01 11:18
doliohttp://code.haskell.org/~dolio/agda-share/universes/07/01 11:19
dolioHierarchy, in particular.07/01 11:24
Saizanbtw, was IRDataHierarchy typechecking as it is? it doesn't pass the positivity check on Fix with darcs Agda07/01 11:28
dolioI don't remember.07/01 11:29
dolioIs Fix not part of the universes?07/01 11:29
dolioBecause if so, that's kind of interesting.07/01 11:30
dolioBack when Conor first proposed it, when I went to generate html, I had an old version of the agda executable that rejected it due to a positivity check.07/01 11:31
dolioBut an updated Agda at the time allowed it.07/01 11:31
Saizanmy current one doesn't, Fix is used in the decoding function of one of the universes there07/01 11:32
dolioYes. But stuff that comes later in the file wouldn't cause it to fail the positivity checker.07/01 11:32
dolioIt fails here, too.07/01 11:33
dolioFor whatever version I have.07/01 11:33
dolioI actually found it hard to believe that it was accepted.07/01 11:33
Saizananyhow, i see in Hierarchy that the "trick" is to spell it out to agda that the base universe doesn't have a code for U07/01 11:34
dolioWell, there's no universe inside it.07/01 11:35
dolioIf you look at the IRDataHierarchy one, you can see that I use ⊥ as the lowest universe, but then make the eventual U never rever to that.07/01 11:36
Saizanyeah, but i was trying to do the same with a single data definition, instead of two, and the positivity checker stopped me07/01 11:36
dolioSo the lowest universe that you actually use would have a code for a lower universe, but it's just the empty type.07/01 11:37
dolioAnd that way of coding things is a little nicer.07/01 11:38
dolioBecause you don't have to do case analysis on various 'ns' to figure out whether you're in the lowest universe, and thus need to use different codes.07/01 11:39
dolioAll U n have the same codes.07/01 11:39
Saizani see07/01 11:39
dolioPi and such over different universes is still a mess, though.07/01 11:40
dolioConceivably you can define any Pi type that Agda will accept with its built-in universes, but all the lifting into lub universes is a lot of busy work.07/01 11:41
dolioEspecially if you want to parameterize over the levels.07/01 11:41
dolioAnd I've tried writing a Pi combinator that auto-lifts its two arguments into a lub universe, but it ended up being very difficult for reasons I can't really recall.07/01 11:42
Saizanwhat's also maybe suboptimal is that the image of T doesn't give you types like (a : Set) -> a -> a, but (a : U) -> T a -> T a07/01 11:44
Saizanthough i guess the former would cover too many things07/01 11:45
dolioYeah, the thing is, terms with type T (pi u \a -> a => a) or whatever needn't be parametric.07/01 11:53
dolioSince the Us are defined inductively, you can do type case, effectively.07/01 11:54
dolioWhich kind of trivially guarantees that they don't have a type like (a : Set) -> a -> a, because terms with that type must be parametric.07/01 11:55
doliopigworker: So, it seems that the Agda positivity checker has gone back to rejecting your induction-recursion encoding.07/01 12:31
dolioAs of early December, at least.07/01 12:33
pigworkerdolio: I'll investigate.07/01 13:05
dolioApparently you're working in a fragile area.07/01 13:07
dolioAs you may recall, I have an old copy of the agda executable that also rejects it.07/01 13:07
dolioI don't know what tweaks they've been doing to the checker, but it's switched its opinion of your code twice now (at least).07/01 13:08
dolioAlso, SHE seems not to compile on GHC 7.07/01 13:12
dolioOr maybe it's a new mtl thing.07/01 13:13
dolioWith redundant applicative instances.07/01 13:13
copumpkinyeah, I ran into that too yesterday (the SHE not compiling)07/01 14:45
copumpkinif you just comment out an alternative instance it works07/01 14:45
pigworkercopumpkin: which alternative instance?07/01 16:07
copumpkinthere's one for L, which is StateT, in HaLay.hs07/01 16:08
pigworkernow derived?07/01 16:08
pigworkerI mean, supplied?07/01 16:08
copumpkinapparently that's already magically an instance07/01 16:08
copumpkinyeah07/01 16:08
pigworkerabout time07/01 16:08
copumpkinit might be new in mtl 2, assuming you don't have an upper bound on your mtl dependency?07/01 16:09
copumpkinyeah, you don't07/01 16:09
copumpkinso it was using mtl207/01 16:09
doliomtl2 just repackages transformers, which has the applicative instances.07/01 16:09
pigworkerI'm clueless about this stuff.07/01 16:10
copumpkinalso, you mentioned in one of those videos that SheSingleton could be a GA data family (I love those, and use them all over the place)07/01 16:10
pigworkeroh, it is now, I think07/01 16:10
copumpkinoh cool07/01 16:10
copumpkinhadn't looked07/01 16:10
copumpkinGHC should support custom code preprocessors with associated custom error postprocessors!07/01 16:11
dolioWhat's new in 0.3, by the way?07/01 16:12
copumpkinthe superclass instance stuff that people have been talking about in that huge thread, I think07/01 16:12
dolioThat was in 0.2.07/01 16:12
pigworker0.3 is a bugfix on 0.2, which added default superclass instances07/01 16:12
copumpkinoh07/01 16:12
dolioAh.07/01 16:12
pigworkerI noticed I'd screwed up the (trivial, non-)treatment of fundeps, and other things like that.07/01 16:13
pigworkerdolio: is it my Alg-IIR.agda file which no longer positivity-checks?07/01 16:14
dolioRight.07/01 16:14
pigworkerif so, that's an incentive not to upgrade...07/01 16:14
dolioHeh.07/01 16:15
pigworkerbut I still have botched record constructors, which is really annoying07/01 16:15
dolioI was considering bringing it up on the mailing list.07/01 16:15
Saizanthe two might be related, does it check if Sg is a data?07/01 16:15
pigworkeryou tell me; I'm not getting the symptoms07/01 16:16
dolioAlthough, I guess the lesser Descs don't require more powerful datatypes than they encode themselves.07/01 16:19
dolioAnd there's no reason for me to suspect that an inductive-recursive definition of codes for inductive-recursive definitions should be less likely to work.07/01 16:20
pigworkerno, and Func is strictly positive in X, by the looks of things07/01 16:21
dolioI think what it comes down to is that part of the definition is too opaque for the checker to see through.07/01 16:22
dolioAnd in those situations, it assumes the worst.07/01 16:22
pigworkeryeah07/01 16:22
djahandarieWhoa, this ala thing is pretty neat07/01 17:19
djahandarie...and it doesn't even need SHE does it?07/01 17:24
icarrollI'm wondering how to use records like haskell type classes. Is there any documentation or code I could look at?07/01 23:53
icarrollI've done a number of searches and haven't found anything.07/01 23:53
icarrollI guess no one's home07/01 23:59
icarroll:(07/01 23:59
--- Day changed Sat Jan 08 2011
doliopigworker: It breaks termination? I wasn't expecting that.08/01 00:40
pigworkerI was.08/01 00:51
doliopigworker: So, 'progress : {A : Set} {x y : A} -> x == y -> x == y ; progress _ = trustMe' is a problem?08/01 15:38
dolioSame as making equality proofs irrelevant?08/01 15:38
pigworkerThe rules are that you only use the unsafe trustMe to define extensionality. After that, no cheating!08/01 16:41
pigworkerer, sorry, dolio: ping, see above08/01 16:42
pigworkerBut you're right, if that was the unsafeTrustMe, there would be trouble.08/01 16:44
doliopigworker: One part of the original message was about whether it was safe to use trustMe as long as you only added consistent axioms.08/01 19:08
dolioEven just adding extensionality will cause non-normalizing terms?08/01 19:09
pigworkerIf you implement extensionality with primUnsafeTrustMe, you get non-normalizing terms.08/01 19:32
pigworkerdolio: and if you implement extensionality with the safe primTrustMe, you lose canonicity08/01 19:36
dolioWell, the latter doesn't surprise me, if I understand canonicity correctly. You'd have values of type f == g that get stuck on primTrustMe because they aren't definitionally equal.08/01 19:40
doliof and g aren't, even.08/01 19:40
dolioIs there a simple example of where getting stuck like that prevents a loop?08/01 19:41
pigworkeryou certainly need to get stuck sometimes to prevent loops08/01 19:46
pigworkertaking refl : f == g is rather unstuck, when f and g are only extensionally equal08/01 19:49
dolioWell, yes, it's unstuck.08/01 19:53
dolioI guess, if you have a false (forall x. f x == g x) in your context, you can then get an inappropriate refl : f == g?08/01 19:53
dolioWhich should actually be stuck on the assumed (forall x. f x == g x).08/01 19:54
dolioOr something like that.08/01 19:54
pigworkeryou don't even need a false statement of that form08/01 19:54
pigworkeralthough you do need a false statement somewhere08/01 19:55
pigworkerthe "only consistent axioms" condition is a red herring, as you can always have a false hypothesis08/01 19:55
dolioRight.08/01 19:56
pigworkerI'd spill the beans, but I'm fed up being a spoilsport. People should learn to spoil their own sport.08/01 20:05
dolio:)08/01 20:05
--- Day changed Sun Jan 09 2011
pigworkerDoes Agda allow irrelevant .(a : A) -> B a these days?09/01 16:43
Saizanthat's a parse error, even09/01 17:02
--- Day changed Mon Jan 10 2011
djahandariepigworker, I have a version of your ala with (Newtype n' o10/01 04:38
djahandarieAgh10/01 04:38
copumpkinaghla?10/01 04:38
djahandarie(Newtype n o, Newtype n' o') => and one with just (Newtype n o) =>10/01 04:39
djahandarieSeems like you decided to switch from one to the other at one point though I'm not sure why :o)10/01 04:39
pigworkerdjahandrie: I can't remember what the issues were. There's no especially good reason to force the inner and outer newtypes to coincide on the nose.10/01 08:58
djahandarieOkay. I guess I'll just find out for myself then heh10/01 09:04
--- Log closed Mon Jan 10 14:16:52 2011
--- Log opened Mon Jan 10 14:17:47 2011
-!- Irssi: #agda: Total of 33 nicks [0 ops, 0 halfops, 0 voices, 33 normal]10/01 14:17
-!- Irssi: Join to #agda was synced in 79 secs10/01 14:19
--- Day changed Tue Jan 11 2011
copumpkinI wonder how I'd go about proving that applicative parsers recognize no more than context-free languages11/01 19:32
dolioSounds difficult.11/01 19:34
dolioActually, it might not be as difficult as it sounds at first, I guess.11/01 19:35
dolioBecause the beauty of applicatives is that the 'T' in 'f T' is superfluous.11/01 19:36
dolioYou cannot observe the T to decide what kind of parsers to make.11/01 19:36
copumpkinI guess I'd need to come up with a convenient (for this proof) definition of what it means to be context-free11/01 19:36
dolioSo what you need to do, is figure out what recognizer operations the applicative combinators correspond to, and prove that those recognize context free languages.11/01 19:37
djahandarieMaybe you could connect it with the SK combinator calculus? *random thought*11/01 19:37
--- Day changed Wed Jan 12 2011
djahandariepigworker, possibly of interest to you http://althack.org/Data-Newtype.html :)12/01 00:31
djahandarieGoing to throw it on Hackage later today12/01 00:32
pigworkerYes, it is interesting. I can't remember whether the associated type version works better or worse, but fundeps are fine for now...12/01 00:34
djahandariepigworker, I did the associated type version12/01 00:34
djahandarieBut it blows up on GHC < 712/01 00:34
djahandarieSo I decided to go with this for now12/01 00:34
pigworkercurious; a bit of a rat's nest, that12/01 00:35
djahandariehttp://althack.org/Newtype.hs the code12/01 00:36
copumpkinnoooo12/01 00:36
copumpkinwho needs GHC < 7 anyway12/01 00:36
djahandarieIt'd be nice if there was some way to force GHC to automatically write these instances...12/01 00:36
djahandarieMaybe I could write an extension?12/01 00:37
* djahandarie has never ventured into those lands12/01 00:37
copumpkinthere's a more general deriving mechanism being written as we speak12/01 00:37
copumpkinso with any luck that'll come in the not-too-distant future12/01 00:37
djahandarieDoesn't deriving always somehow related to the type that then newtype wraps though?12/01 00:37
djahandarierelate*12/01 00:37
copumpkinthis is a general deriving mechanism for anything, not just newtypes12/01 00:38
djahandarieAh, neat12/01 00:38
pigworkergenerating Newtype instances from newtype declarations would not be so tricky with SHE12/01 00:38
copumpkinof course, you wouldn't want these instances unless you ask for them12/01 00:38
djahandarieNo, make them anyways!!12/01 00:38
copumpkinlol12/01 00:38
pigworkerbut it's nicer if it's built in12/01 00:38
copumpkinyeah12/01 00:38
sullywhat does BUILTIN LIST do, exactly?12/01 03:27
sullydoes it allow convenient notation for lists, and if so what is the syntax?12/01 03:27
sullyor, alternately, is any of this documented anywhere?12/01 03:28
copumpkinI hadn't even come across that12/01 03:28
dolioIt makes agda do certain list computations using Haskell lists behind the scenes, I think.12/01 03:34
dolioThe same is true of built-in pragmas for natural numbers. They're why you can actually do appreciable arithmetic in Agda.12/01 03:35
dolioIf it were actually doing unary computations something like 10^10 would probably force you to reboot.12/01 03:36
--- Log closed Wed Jan 12 11:10:25 2011
--- Log opened Wed Jan 12 11:10:32 2011
-!- Irssi: #agda: Total of 40 nicks [0 ops, 0 halfops, 0 voices, 40 normal]12/01 11:10
-!- Irssi: Join to #agda was synced in 83 secs12/01 11:11
--- Day changed Fri Jan 14 2011
jlouisThat hole thing in Agda2's Emacs mode is badass14/01 18:57
jlouisIt basically programs the solutions to the exercises for you14/01 18:57
Saizaneven more so with the auto command14/01 19:03
ccasinAre agda's irrelevant arguments basically an implementation of ICC*, or are the something else?14/01 19:08
ccasin*they14/01 19:08
Saizan..there are so many -CC14/01 19:10
ccasin:)14/01 19:20
ccasinHere I'm thinking about the algorithmic variant of the implicit calculus of constructions14/01 19:20
ccasinI think the paper was by Barras and Bernardo14/01 19:21
ccasinit's also essentially the same system as EPTS, from Nathan Linger's thesis14/01 19:21
jlouisHeh, I am in a tutorial where all ASCII is now UTF8. I guess I can as well learn the stdlib :)14/01 20:38
jlouisthough, where is 'refl' located?14/01 20:43
jlouisor rather something that lets me do the equivalent of an ascii ==14/01 20:46
SaizanRelation.Binary.PropositionalEquality14/01 20:46
jlouisSaizan: thank you!14/01 20:58
dolioIrrelevant arguments are like EPTS/ICC/etc.14/01 21:15
dolioExcept you can't be dependent over them yet.14/01 21:15
dolioSo, .A -> B, but not .(x : A) -> B x14/01 21:15
doliomini agda has the latter, though, I think.14/01 21:16
copumpkinoh14/01 21:16
dolioAmongst other things.14/01 21:16
ccasindolio: thanks14/01 21:39
jlouisHeh, this STLC from the tutorial is around 10 times as large as one in Twelf :P14/01 22:43
jlouisline-wise14/01 22:43
dolioTwelf has lambda terms as built-in language constructs.14/01 22:43
jlouisexactly, it is alsmost cheating14/01 22:44
jlouisbut I am not sure it will keep being like that as I build larger things14/01 22:44
jlouisTwelf has no library for instance14/01 22:44
dolioI suppose I should say, twelf has them as a built-in data structure (with very nice properties).14/01 22:48
dolioAgda has lambda terms built in, but they're used primarily for computation.14/01 22:49
--- Day changed Sat Jan 15 2011
sullydoes there exist documentation of what all the BUILTINs are?15/01 20:07
sully(I think I already know the answer to most questions beginning with "does there exist documentation" when agda is being discussed, but...)15/01 20:08
--- Log closed Sat Jan 15 20:38:48 2011
--- Log opened Sat Jan 15 20:38:55 2011
-!- Irssi: #agda: Total of 35 nicks [0 ops, 0 halfops, 0 voices, 35 normal]15/01 20:38
-!- Irssi: Join to #agda was synced in 85 secs15/01 20:40
--- Day changed Sun Jan 16 2011
freiksenetis "indexed type" a synonym to "dependent type'?16/01 15:53
ccasinsometimes it is used in a more specialized way16/01 16:01
ccasinto refer to types that have non-uniform dependent arguments16/01 16:02
ccasinfor example, vec's natural number argument, but not its type argument16/01 16:02
freiksenetaha.16/01 16:02
freiksenetccasin: thanks16/01 16:03
ccasinno problem16/01 16:04
skire uniform dependent arguments, i tried to write16/01 16:28
ski  foo (A : Set) (a : A) : P a -> ...16/01 16:28
ski  foo A a (...) = ...16/01 16:28
skibut it didn't like that type signature :/16/01 16:29
ski(it seemed to me that if that worked in `data' declarations, it would also work in normal bindings)16/01 16:29
ccasinin data declarations it has a special meaning though16/01 16:29
skiyeah .. but i was wanting "the same" meaning in `foo' above16/01 16:29
ccasinfair enough16/01 16:30
skithough maybe that's sortof useless .. hm16/01 16:30
skihm, i suppose `foo' is not a good example16/01 16:31
ski  bar (n : Nat) : ...16/01 16:31
skiis better16/01 16:31
skiso i was thinking this should enforce `bar' to be "parametric" in the `n' argument16/01 16:31
skiso each defining equation would start with `bar n' (not matching on `n')16/01 16:32
skibut now that i think on it again, i'm not sure one could stop `n' from being matched on "later" (and if one could, would it be useful ?)16/01 16:32
ski(at the time i was playing with alternate definitions for a type. one used `data', another was a plain definition, defining the type to be `Unit' in one case, &c.)16/01 16:33
skifwiw, this was it :16/01 16:36
ski  trans_=<_<_O : {m n o : Ordinal} -> n >=O m -> n <O o -> m <O o16/01 16:36
skii wanted to say in the type (so that it was statically checked), that the definition didn't (by itself) match on the `n >=O m' argument16/01 16:37
Saizanyou could use the irrelevant arguments feature there, maybe16/01 16:38
ski(it would in the recursive case pass that argument to another (mutually recursive) function which would match on it, however)16/01 16:38
skihm .. how does that work ?16/01 16:38
Saizanthe syntax would be: trans_=<_<_O : {m n o : Ordinal} -> .(n >=O m) -> n <O o -> m <O o16/01 16:39
ski(i mean if you say `data Foo (n : Nat) : Set where F : Bar n -> Foo n', nothing is hindering `Bar' for being indexed on its natural number argument .. only `Foo' is forbidden from that)16/01 16:39
Saizanbut then you can use that argument only in an irrelevant position16/01 16:39
skiok, so then i couldn't pass it to another function that matches (non-irrelevantly) on it, right ?16/01 16:39
Saizanyeah, unless you use the result of that function only in a place marked as irrelevant16/01 16:41
skiyeah16/01 16:41
Saizanthe release notes for 2-2-8 should have the details16/01 16:41
skianyway, you see how with `data Foo (n : Nat) ...' only `Foo' is forbidden to "match" on `n' ?16/01 16:42
skii wanted that, for an ordinary definition16/01 16:42
Saizani don't think there's any support for that16/01 16:42
skiok16/01 16:42
ski(another thing i was wanting was to have uniform arguments after non-uniform ones .. but i suppose that's not possible :)16/01 16:46
ski(that would allow me to say `m =<O n' instead of `n >=O m' above :)16/01 16:46
ski(.. of course i can make a definition, but that doesn't help me when matching, since i can't make "derived constructors/patterns")16/01 16:47
Saizanhow would you use such a property btw? it doesn't seem like you can derive much from knowing trans_=<_<_O won't match on (n >=O m)16/01 16:49
skiwell, i'm not sure :)16/01 16:51
skii wanted the `data' and the equality definitions to correspond more to each other16/01 16:51
ski(i can't say exactly where uniform arguments of `data'-definitions are used either, btw)16/01 16:52
Saizanfor data they are mostly useful when quantifying over them in constructors would put the type you're defining in a higher universe, otherwise it's just a syntactical convenience16/01 16:57
skiah, ok16/01 16:58
skiinteresting16/01 16:58
Saizane.g. data List : Set -> Set where [] :: (A : Set) -> List A would be a type error because ((A : Set) -> List A) : Set116/01 17:04
ski*nod*16/01 17:26
dolioYou can make new indexed types using parameterized types and existing indexed types (like the equality type), though.16/01 17:32
dolioSo parameters for types are somewhat different than irrelevant arguments.16/01 17:32
dolioIf a type had an irrelevant parameter, that would be even more restrictive. The type would not be able to depend on that argument, so it effectively would be forced to be phantom.16/01 17:33
dolio(I think, at least.)16/01 17:34
--- Day changed Mon Jan 17 2011
jlouisHas anybody tried to build something like (List N) where N can be ordered and the list is sorted by force of a dependent type?17/01 20:05
dolioYes. I'm sure that's been done.17/01 20:05
dolioI've probably done it at some point.17/01 20:05
jlouisI tried with non-empty lists where I have SList N N where the latter N is the minimal element in the list17/01 20:06
cadsI have a question about agda.17/01 20:07
cadsI want to try an experiment, to learn it17/01 20:07
jlouisdolio: do you have a hint as to what you did?17/01 20:07
cadsAnd what I'd like to do is to take the basic definitions and theorems from my calculus course and formalize them in agda17/01 20:07
jlouismy stdlib-fu is too weak to be able to grab the right tools in the toolbox unfortunately17/01 20:08
cadsis it easy to do this, or do I have to work with some nontrivially finitized constructive version of the theory?17/01 20:08
dolioFormalizing calculus would be a lot of work.17/01 20:08
jlouisyou'd need the Reals for starters, right?17/01 20:09
cadsthe definitions are very simple but they almost all rely on quantification over uncountable sets, or infinite sequences and stuff17/01 20:09
cadsjlouis, definitely17/01 20:09
cadsdolio, what would be the steps I'd have to take to accomplish it?17/01 20:10
dolioIt rather depends.17/01 20:10
cadscould I use some existing analysis framework and specialize it to plain calculus of one variable?17/01 20:11
dolioYou could try developing constructive reals, and doing calculus with that.17/01 20:11
dolioOr you could postulate a bunch of axioms about real numbers that are sufficient to just reason in the way that calculus requires.17/01 20:11
cadsreally I just want to hold something that can prove every problem in my book that has a solution17/01 20:11
dolioBut I don't expect either one of those options to be very easy.17/01 20:12
cadssomething built from what was available, and provably correct17/01 20:12
cadshmm17/01 20:12
dolioIt's possible there are Coq libraries for this sort of thing.17/01 20:12
cadsbasic caclulus doesn't invoke many of the real strange properties of the reals17/01 20:13
cadsdolio, that gives me an idea17/01 20:15
doliojlouis: So, playing a bit now, it's a little more of a pain than I thought.17/01 20:16
cadsI'll write the definitions from the book and see what properties of the real numbers I'm required to postulate for them to make sense17/01 20:16
dolioAt least, for a 'the head is less than the head of the tail' layout.17/01 20:16
jlouisdolio: yeah. Perhaps one should go with the idea of bounds instead17/01 20:18
Saizanhttp://www.e-pig.org/epilogue/?p=690 <- this should be portable to agda17/01 20:19
doliojlouis: There's an easy inductive-recursive formulation using All.17/01 20:20
jlouisSaizan: mmm, I considered that as well17/01 20:20
jlouisdolio: I still need to grasp what inductive-recursive means :)17/01 20:20
dolio_::_ : forall h t -> All (h <) t -> SList17/01 20:20
jlouisJust to be clear, All P t means that P(x) forall x in t ?17/01 20:22
dolioRight.17/01 20:22
dolioSo, the head is less than (or equal to) all the elements of the tail.17/01 20:22
dolioAnd All is mutually defined by recursion.17/01 20:23
jlouisI can see how one should be able to insert elements based on discriminating on that17/01 20:24
doliohttp://hpaste.org/43107/sorted_lists17/01 20:24
dolioOn a side note, why does Data.Unit have a <=?17/01 20:25
dolio_ <= _ = True17/01 20:25
jlouisthe unit element is equal to the unit element?17/01 20:25
dolioRight.17/01 20:26
jlouisthough the < doesn't make much sense17/01 20:26
dolioEmpty doesn't have one.17/01 20:26
jlouisperhaps it is out of convenience17/01 20:26
jlouisEmpty has no inhabitation?17/01 20:26
dolioRight. For all elements e and e', e <= e' vacuously.17/01 20:27
dolio_<=_ : E -> E -> Set ; () <= ()17/01 20:28
jlouisI dunno really, but with () you can at least construct an element (namely ()) whereas that is impossible with Empty. Maybe that is the subtlety of the difference ?17/01 20:29
jlouisI've been hacking Agda for... 2-3 days at max, so I can always claim lack of knowledge and innocense :)17/01 20:30
jlouisdolio: I've been trying some discrimination against the definition you gave, but this fails: Any clue? http://hpaste.org/paste/43107/sorted_lists_annotation#p4310817/01 21:53
jlouissomehow I don't think x <=? y is the way to go17/01 21:53
jlouisin particular, I have a hard time generating a specimen of All17/01 21:54
dolioI expect you're going to want to prove a lemma like 'x < y -> All (_<_ y) zs -> All (_<_ x) zs'.17/01 21:55
jlouisI've thought about a transitivity lemma of some kind for if All (_<=_ hd) tl and x <= hd, then surely I must be able to show All (_<_ x) tl17/01 21:55
jlouisheh, that *almost* agrees modulo notation17/01 21:55
jlouisI'll play around with it17/01 21:55
jlouishttp://hpaste.org/paste/43107/sorted_lists_annotation#p43112 heh that is kind-of a screeching halt I came to17/01 23:32
jlouisThe problem is mangling of 'All' again. We'd like to use the neg p proof we have been handed to show that _<=_ hd bounds (insert x tl), but.. that must require some mutuality probably17/01 23:34
jlouisspeaking of which... Twelf has several termination strategies. What does Agda have in that department?17/01 23:35
Saizanalmost nothing17/01 23:38
Saizanthere's a flag to disable the termination checker and another to increase the "depth", but other than that you can't control it17/01 23:39
jlouisok17/01 23:39
Saizanbtw, this SList is supposed to be in decresing order, or am i reading it wrong?17/01 23:41
Saizanah, yeah, it's me, i was reading (_≤_ hd) as a section17/01 23:42
jlouisI started with the optimistic idea of defining sparse vectors like this17/01 23:47
jlouisbut this is a fine stepping stone17/01 23:47
Saizanhttp://hpaste.org/paste/43107/sorted_lists_annotation#p43113 <- seems to work17/01 23:58
Saizanthe holes would need a ¬ (x ≤ hd) -> hd ≤ x lemma17/01 23:59
--- Day changed Tue Jan 18 2011
jlouismm18/01 00:01
jlouisSaizan: it is interesting how the lemma needs to inspect the top two elements of the list18/01 00:05
jlouisI was down that road but stopped it because "that never leads to anything, heh"18/01 00:05
Saizanwell, insert x tl inspects the first element of tl18/01 00:08
jlouisexactly18/01 00:09
jlouisSaizan: what is the strategy for showing: ¬ (x ≤ hd) -> hd ≤ x ? I have a hard time arguing around \bot-elim18/01 00:32
jlouiswith compare x y  and eliminate impossible cases?18/01 00:33
jlouiswith x <=? y and play with yes p / no neg-p instances?18/01 00:33
jlouisthe latter doesn't seem to work18/01 00:34
jlouissplit on x , split on y, handle the four cases by deciding on x <=? y ?18/01 00:34
jlouisok, that last thing worked18/01 00:37
jlouisonly, no decider was needed, thanks rubber duck :)18/01 00:37
Saizan:)18/01 00:39
Saizanyou need only 3 cases actually18/01 00:39
Saizan  lemma2 : ∀ {x hd} -> ¬ (x ≤ hd) -> hd ≤ x18/01 00:40
Saizan  lemma2 {x} {zero} ¬p = z≤n18/01 00:40
Saizan  lemma2 {zero} {suc n} ¬p = ⊥-elim (¬p z≤n)18/01 00:40
jlouisah, yes18/01 00:40
Saizan  lemma2 {suc n} {suc n'} ¬p = s≤s (lemma2 (λ x → ¬p (s≤s x)))18/01 00:40
jlouisif {y = zero} collapses18/01 00:40
jlouisThe automatic refinement and automatic search is a neat improvment over my Twelf-hacking18/01 00:41
Saizanby automatic refinement you mean pattern matching changing the types?18/01 00:42
jlouisC-c C-r18/01 00:42
jlouisyou can basically just go looking for what Agda wants and then slowly let it give things18/01 00:43
Saizanah, yeah, i wish i learned about it earlier18/01 00:45
skijlouis : both `=<' and `<' makes sense for both `Unit' and `Empty' ..18/01 07:42
dolioThey make sense, but I'm skeptical that they're of use more often than they need to be hidden to avoid conflicting with, say, the Nat versions.18/01 07:58
skihm .. can one associate unique values with types, somehow ?18/01 07:59
skii.e. like type classes, only with a guarantee that the instance is unique18/01 07:59
ski.. though i suppose that mightn't be that useful in this circumstance anyway18/01 08:00
dolioI don't think so, unless you'd accept defining a set of codes, and then an interpretation into sets and a function that gives the 'instances' for those types.18/01 08:02
skim .. for `Unit' and `Empty' there should be unique "weak"(?) and strict partial orders18/01 08:05
skibut obviously not for naturals and more complicated stuff18/01 08:05
skianyway, i was thinking the orders for `Unit' and `Empty' might be useful to (semi- ?)automatically derive orders for more complicated types18/01 08:06
skii suppose they at least could be useful to manually derive orders, in a principled way18/01 08:07
skie.g. you could have combinators combining orders over constituent types into orders over compound types18/01 08:07
dolioYou could.18/01 08:08
ski`lexicographic <A <B : WellOrder (A * B)',&c.18/01 08:08
dolioIt's far more frequent for me to import both Data.Unit and Data.Nat, though, than it is for me to need the ordering for, say, List Unit.18/01 08:09
skii wouldn't mind writing `=<U' or something like that for the order over `Unit'18/01 08:10
ski(and similarly for naturals, &c.)18/01 08:10
jlouisski: how do you justify () < () ?18/01 12:34
jlouisI somewhat don't grok its reflexive18/01 12:34
skijlouis : the `() < ()' doesn't prove reflexivity, it only defines `_<_' for `Empty'18/01 13:53
jlouisski: oh!18/01 13:53
ski  _<_ : Empty -> Empty -> Set18/01 13:53
ski  () < ()18/01 13:53
skithere's zero cases to consider, in the definition18/01 13:53
* jlouis nod18/01 13:54
skihowever, this `_<_' still *is* reflexive, yes18/01 13:54
jlouishow about the Unit then?18/01 13:54
jlouisassuming Unit is the one-element inhabited type18/01 13:54
ski`_=<_' as well as `_<_' can be defined, but only the former is reflexive (naturally)18/01 13:55
skiin the former, `U =< U' is defined to be `Unit', so reflexivity will give `U' as proof for `U =< U' (the only case)18/01 13:56
skiin the latter, `U < U' is defined to be `Empty', so reflexivity would need to prove `U < U' which is `Empty', which shouldn't be possible18/01 13:57
jlouisah, something clicked now18/01 13:57
skiin the case of `_<_' for `Empty' (as well as `_=<', of course), there simply is no case to begin with. reflexivity similarly is provable simply because there's no element `e' in `Empty' to prove `e < e' (or `e =< e') for18/01 13:58
ski(it's vacuously true)18/01 13:59
--- Day changed Wed Jan 19 2011
roconnorgiven a least fixed point of a Functor F, we have A ~ F (A).  What is the usual names for the two directions of the isormophism?  fold and unfold?19/01 16:20
dolioin and out19/01 16:35
roconnorthanks19/01 16:43
--- Day changed Thu Jan 20 2011
copumpkinjlouis: what's this clever agda code from you I hear of on the twitterverse?20/01 17:07
jlouiscopumpkin: Ralf defined 'Huttons Razor + an Exit (exception)' and then he asked, among other stuff: Define a function pure : Exp -> Bool. .. but it is so much more fun to do: data Exp : Bool -> Set where... of course :)20/01 17:40
jlouishttps://gist.github.com/4d2bdfb2d59116d641e620/01 17:40
jlouislast 5 lines or so20/01 17:40
copumpkincool :)20/01 17:45
copumpkinthat could be done in haskell too though20/01 17:46
jlouiscopumpkin: Yes, GADTs right?20/01 17:47
jlouisor an indexing trick?20/01 17:47
copumpkinyeah, GADTs20/01 17:48
copumpkinand type families to do the boolean operation20/01 17:48
jlouisIt is just that dependent types comes more natural to me than GADTs+families20/01 17:48
jlouisfor some odd reason20/01 17:48
djahandarieOther way around for me :P20/01 17:48
djahandarieThen again I still haven't done enough with Agda20/01 17:49
jlouisI've been hacking a bit of Twelf and Coq before this20/01 17:50
copumpkindoes coq have inductive families?20/01 17:53
copumpkinprobably, I guess20/01 17:53
Saizanin haskell you'd actually need a typeclass if you wanted a boolean to pattern match on :)20/01 17:54
ccasincopumpkin: yes, but pattern matching on them sucks20/01 17:54
ccasinboth in the sense that it is terribly inconvenient and in the sense that it is actually a little weaker20/01 17:56
kosmikusjlouis: you're at Dagstuhl then? what's the topic of the meeting?20/01 17:59
jlouiskosmikus: nope, I am just trying to learn to juggle agda20/01 18:05
copumpkinccasin: ick20/01 18:06
ccasincopumpkin: things are getting better though.  mattam write a coq plugin that elaborates nicer agda-style pattern matching into coq (plus an assumption of Axiom K, which it the thing it is missing)20/01 18:07
ccasinand there is reason to hope both the plugin and the missing axiom will make their way into coq proper20/01 18:07
copumpkinwhat is this axiom K I keep hearing about?20/01 18:07
ccasinit's also called the uniqueness of identity proofs20/01 18:07
ccasinforall (A B : Set) (P Q : A = B), P = Q20/01 18:08
copumpkinah okay20/01 18:08
copumpkinwait, only on sets?20/01 18:09
ccasinno, I think any sort20/01 18:09
copumpkinor A B : Set, x : A, y : B, p q : x == y, p == q20/01 18:09
ccasinoh, right20/01 18:09
ccasinthat :)20/01 18:09
copumpkinI see20/01 18:09
ccasinI think maybe with just one Set, and no first assumption of equality20/01 18:09
ccasinnot sure if it matters20/01 18:09
ccasinlet me see20/01 18:10
ccasinyes, its statement in the coq stdlib is:20/01 18:10
ccasinforall (U : Type) (x y : U) (p1 p2 : x = y), p1 = p220/01 18:11
ccasinhttp://coq.inria.fr/stdlib/Coq.Logic.EqdepFacts.html20/01 18:11
ccasinSorry for the slipup :)20/01 18:11
ccasinaccording to that page, Axiom K actually refers to an equivalent variant.  I like it because it's quicker to write "Axiom K" than "Uniqueness of identity proofs"20/01 18:12
ccasinanyway, this is independent of coq but true in agda, and it is important for "good" pattern matching.  There is some push to add it to coq, though20/01 18:14
copumpkinah interesting20/01 18:23
copumpkinit's because inductive families carry implicit equalities around a lot?20/01 18:23
ccasinyes20/01 18:26
ccasinin agda, when you pattern match it does all these substitutions on the types in the context20/01 18:27
ccasinto resolve those equalities20/01 18:27
copumpkinyeah20/01 18:27
ccasinyou can use this nice behavior to derive UIP20/01 18:28
ccasinin coq, the pattern matching isn't so clean20/01 18:28
copumpkinUIP?20/01 18:28
ccasinuniqueness of identity proofs :)20/01 18:28
copumpkinoh okay :P20/01 18:28
copumpkinhow computationally meaningful are the implicit arguments to constructors of http://www.cse.chalmers.se/~nad/listings/lib/Data.Nat.html#875 ?20/01 19:02
copumpkincause otherwise a proof of n <= m is basically isomorphic to n20/01 19:03
copumpkineven if not, the implicit m argument to s<=s has exactly the same structure as the smaller number20/01 19:04
ccasinI'm not sure what "computationally meaningful" means here20/01 19:09
ccasinbut I agree proofs of n <= m have n constructors20/01 19:09
ccasinerr, (n+1), counting 020/01 19:10
copumpkinwell, Fin is basically equivalent to Nat, at runtime20/01 19:10
copumpkinso could possibly be represented efficiently too20/01 19:10
ccasinyes, I think so too for this datatype20/01 19:10
copumpkinso Fin, <=, and Nat all look roughly the same at runtime, and any implicit parameters their constructors may have can usually be figured out from context (as far as I can tell)20/01 19:11
ccasinI guess, one question to as is20/01 19:12
ccasinoops20/01 19:12
ccasinignore that, sorry20/01 19:12
copumpkin(it seems like Dec P could also be represented as a Bool at runtime, if P isn't decomposed for computation)20/01 19:12
ccasinyes20/01 19:13
ccasinOf course, with this representation a proof of (n <= m) doesn't give you enough information to figure out m20/01 19:13
copumpkinit seems that any time you have an n <= m, you acquired it by <=?'ing two numbers, so it's non-local, but the information should be available somewhere :P20/01 19:14
copumpkinthat's pretty sketchy though, I guess20/01 19:14
ccasinI agree, in a vague way :)20/01 19:14
copumpkinwell, n <= m ~~ (n, m)20/01 19:14
copumpkinit'd be cute to have a compiler with fancy automated reasoning that for every natural, attempted to automatically prove (using presburger solver or real-closed field solver, or smt of some other sort) that n <= 2^wordsize, and if so, represents the number as a native word20/01 19:17
* copumpkin dreams on20/01 19:17
copumpkinit'd be nice if the standard library Category could be put into another namespace (Agda.Category.Functor/Monad?) somehow, making room for categories with proofs as the most general namespace version20/01 20:21
dolioexists n. n <= m is one possible implementation of Fin (m+1).20/01 20:55
dolioAnd if you use a sigma instead, you have redundant information.20/01 20:57
dolioStoring both the n and the proof.20/01 20:57
copumpkinyep20/01 20:57
dolioAlso, from what I gather, I wouldn't hold your breath for K in Coq.20/01 20:58
dolioSince it seems to be getting used for work on the models of type theory in which K is inconsistent.20/01 20:58
ccasindolio: I guess that is voevodsky's work?20/01 22:08
dolioHim at least.20/01 22:08
ccasinI am still vaguely hopeful - mattam has indicated that he wants it and he's on the official coq team now20/01 22:08
dolioAlthough I can't say I know any other folks on the job.20/01 22:08
ccasinperhaps we will get it as an optional flag20/01 22:08
dolioYeah, that's a possibility.20/01 22:09
ccasinI think these are the people working on the voevodsky stuff:20/01 22:09
ccasinhttp://www.math.ias.edu/sp/univalent20/01 22:10
ccasinthough, as far as I know, he's the only one hacking in coq20/01 22:10
ccasinwell, scratch that20/01 22:10
ccasinthe second name on that site is Coquand20/01 22:10
dolioHe's the one you see on the mailing list, at least.20/01 22:10
ccasinso I guess I'm wrong :)20/01 22:10
ccasinyeah, actually, the whole description here is pitched in terms of using proof assistants.  I thought they were just doing semantics.  Neat!20/01 22:11
dolioIf you talk to Conor, I think he'll tell you that K isn't necessary for nice matching. What you need is some variety of substitutive heterogeneous equality20/01 22:12
dolioAnd K just allows you to get that.20/01 22:12
dolioOf course, I don't think Coq is more likely to adopt that as an alternative to K.20/01 22:13
ccasinyeah, that sounds right20/01 22:13
ccasinK is just what coq is missing20/01 22:13
ccasinit's totally plausible that a different notion of definitional equality will do the same job20/01 22:14
ccasinin fact, we're working on one in Trellys :)20/01 22:14
copumpkinwho the hell called it K?20/01 22:15
dolioIn Martin-Loef type theory, identity types are I, and identity elimination is J.20/01 22:15
dolioSo K is next in line.20/01 22:15
ccasininteresting20/01 22:15
ccasinpeople call it "Streicher's axiom K"20/01 22:16
ccasinso maybe he is to blame20/01 22:16
dolioProbably. But I can make up a rationale, at least. :)20/01 22:16
ccasincertainly - I totally bought it :)20/01 22:17
--- Day changed Fri Jan 21 2011
lpjhjdhIs it possible to show something like the following?  http://hpaste.org/43178/xsxs21/01 02:02
lpjhjdhI have no idea how to reduce x ∷ subst (Vec .A) n+0≡n (xs ++ [])21/01 02:02
lpjhjdhI know the standard library just uses a more reasonable notion of equivalence21/01 02:03
Saizanpattern match on n+0≡n, providing the right implicit n21/01 02:03
dolioYes, it is possible.21/01 02:04
lpjhjdhinteresting, I'll give it a shot, thanks21/01 02:05
lpjhjdhactually I'm uncertain I understand what that grants me, would you mind explicating a bit?21/01 02:05
Saizanmh, maybe it doesn't help21/01 02:06
Saizanthat should reduce the subst away though21/01 02:06
lpjhjdhah, thanks21/01 02:07
lpjhjdhso since I know the shape of n to be "suc k" it reduces to "cong suc k"21/01 02:11
lpjhjdhSorry I don't actually quite understand how this is reducing actually.  So I have a vector of size "k+1" and match with "n+0=n {m}"21/01 02:16
lpjhjdhbut then I'm not sure how to match on the result of type "m + 0 = m"21/01 02:17
lpjhjdhbleh, sorry keep mixing up notation meatn to say "m+1"21/01 02:18
* Saizan is not finding a way to solve this either21/01 02:19
dolioI may have been over-zealous. If it is possible, it's likely to be painful.21/01 02:20
dolioBecause heterogeneous equality handles the non-definitionally-equal indices much better.21/01 02:21
Saizanyeah21/01 02:22
lpjhjdhI see, an interesting exercise.  I'm content letting it go having brilliant folks such as yourselves note that it's painful :)21/01 02:23
lpjhjdhthanks for the help21/01 02:23
dolioFor instance, trying to prove subst P eq Px = Px'21/01 02:23
dolioEr.21/01 02:23
dolioTrying to prove that in general is hard.21/01 02:23
dolioThat doesn't type as stated.21/01 02:24
lpjhjdhOkay, so in general is it much easier to just come up with a good notion of equivalence and then prove things respect it?21/01 02:26
dolioThe problem here is that n + 0 and n are provably equal, but not definitionally equal. Heterogeneous equality is approximately the same as the regular homogeneous equality, but it doesn't require the types of the two terms to be definitionally equal.21/01 02:28
lpjhjdhAh, thanks21/01 02:29
dolioYou could look at the limitation of the homogeneous equality as being a little artificial.21/01 02:30
dolioA concession to decidable checking, rather than 'this really should not work.'21/01 02:31
--- Day changed Sat Jan 22 2011
BMephJust curious, but does anyone see Agda getting to the point where it feels as clunky for an Agda user to work with Haskell, as it feels for a Haskell programmer to work with Ocaml?22/01 21:34
Saizanfor some things yes22/01 21:34
Saizanthough agda feels clunkier when termination checking hinders higher order programming22/01 21:35
Saizana simple thing that's quite clunky in haskell is the lack of type application22/01 21:36
dolioActually programming with Haskell already feels klunkier than Agda, tool-wise.22/01 21:45
BMephSaizan: Thanks; looks like I may try moving Agda higher up on my "things to investigate" list.22/01 21:46
sullythe automatic case splitting is dead sexy.22/01 21:50
sullydownsides of Agda include: as the type system becomes more expressive, the ability for mortals to understand it decreases drastically22/01 21:57
sullyfor example: http://pastebin.mozilla.org/97181822/01 21:58
--- Day changed Mon Jan 24 2011
nappingAre there any examples of reflection on terms with binders?24/01 02:03
nappingI don't see how to turn the AST back into typed results24/01 02:03
* Saizan doesn't remember how binders are represented24/01 02:05
nappingIt's a DeBruijn notation, but it seems to have very little type information24/01 02:06
nappingWell, I guess I could target a "Maybe" type24/01 02:06
Saizan var     : ℕ → List (Arg Term) → Term <- what does that list contain? (taken from the release notes)24/01 02:11
codolioThe std lib says var is a variable applied to arguments.24/01 02:11
Saizanthen i see, lambdas are not even annotated24/01 02:14
dolioNot in the reflection, at least.24/01 02:15
dolioIt looks like it has a flag that says whether it's annotated, but not what the annotation is.24/01 02:15
Saizanthe Explicit? i think that only distinguishes between \ x -> and \ {x} ->24/01 02:22
dolioOh, duh.24/01 02:23
nappingit seems type annotations are not preserved at all24/01 02:23
nappingbut I don't need them yet24/01 02:24
dolioYeah. I don't remember how this stuff works, really.24/01 02:24
copumpkinnapping: maybe poke around the terrifying presburger solver?24/01 02:24
dolioInterpreting a Term back into Agda is going to be tricky business as written.24/01 02:24
dolioIn fact, you can't really do it at all, because there's no way to turn 'unknown' into its original form.24/01 02:25
Saizani think you are supposed to have a function Term -> Maybe WhatYourSolverActuallyHandles24/01 02:25
Saizanand not work with Term further24/01 02:25
nappingI want to tern phoas terms into DeBruijn terms24/01 02:25
dolioBwahaha! Voevodsky should switch to Agda. Coq just assumed that he wanted his identity type to be in Prop. :)24/01 02:34
dolioActually, he doesn't want K, though, so I guess he can't.24/01 02:35
nappingWhat's he working on?24/01 02:35
dolioI'm watching his presentation on univalent foundations of mathematics.24/01 02:36
dolioWhich is essentially using homotopy types instead of sets as your basis. And it turns out that intuitionistic Martin-Loef type theory is the logic of homotopy types, conveniently.24/01 02:37
ccasindolio: how watchable is that talk for people who don't know anything about homotopy theory?24/01 02:37
ccasinI've been too afraid to check it out24/01 02:37
dolioI don't know anything about homotopy theory, really.24/01 02:38
dolioSeems all right so far.24/01 02:38
Saizanthe one from that talk about normalizing proofs so we can believe them even if the system is inconsistent was Voevodsky too?24/01 02:39
dolioThis is a different talk, I think.24/01 02:40
nappingThere is some discussion like that in Luo's book24/01 02:40
dolioIt was a 3-lecture series. One is by Steve Awodey on the connection between identity types and homotopy...24/01 02:40
dolioAnother is on how to use Coq, which I'm not planning to watch.24/01 02:40
ccasinSaizan: this idea has always seemed a little odd to me24/01 02:41
dolioAnd this third is by Voevodsky about how you'd go about proving stuff in his new foundations using Coq.24/01 02:41
ccasinmost theorems are functions, and normalizing something of type (x : nat) -> foo x24/01 02:41
ccasindoesn't tell you whether every application is normalizing24/01 02:41
ccasinwhich is presumably what one cares about.24/01 02:41
Saizanyeah24/01 02:42
dolioYeah, I don't really get what he was driving at in that regard.24/01 02:42
dolioAlthough it occurred to me later that you can normalize things of the form (exists x. foo x) and be confident in them (I think).24/01 02:43
dolioAnd then (forall x. exists y. foo x y) remains useful as a scheme for generating many (exists y. foo e y) that you can be confident about.24/01 02:44
ccasinyes24/01 02:44
dolioBut that's still very limited.24/01 02:44
ccasinbut still only as many as you can check24/01 02:44
nappingIs it covered in the talk?24/01 02:46
nappingLuo was writing in the context of a normalizing calculus24/01 02:46
dolioIs what covered?24/01 02:46
dolioThe point of the other talk was, "assume that pretty much all mathematics are inconsistent. What then?"24/01 02:47
dolioAnd the idea was, if you work in something like type theory, you can normalize your proofs to have confidence in them.24/01 02:47
dolioEven if you can prove falsehoods.24/01 02:47
nappingSo Luo was more about cut elimination, and normal forms being obviously sound24/01 02:48
dolioI mean, Voevodsky was operating on the premise that even Peano arithmetic is inconsistent.24/01 02:50
dolioSo whatever system Luo was working in would probably also be inconsistent by consequence.24/01 02:50
ccasinunless LEM is to blame :)24/01 02:53
dolioBut, we can still trust normal forms for propositions that don't involve universal quantification, because bad proofs all loop, presumably.24/01 02:54
ccasinyeah24/01 02:54
dolioI think if PA is inconsistent, even Heyting arithmetic is in trouble, because you can encode the former into the latter by double negation, and prove all the same theorems.24/01 02:58
dolioSo if false is a theorem in PA, then not (not false) is a theorem in HA, but that's equivalent to false.24/01 02:59
ccasinwhy is (not (not False)) equivalent to False?24/01 03:00
dolioDid I get that wrong?24/01 03:00
dolio((False -> False) -> False) -> False24/01 03:00
doliof k = k id?24/01 03:01
ccasinah, right, sorry24/01 03:01
ccasinhad too many falses in my head :)24/01 03:01
ccasinthis makes me a little uncomfortable24/01 03:03
ccasinif LEM is so powerful, why is it so easy to show it doesn't break consistency24/01 03:03
ccasinwell, I guess easy is relative, one has to do the double negation encoding24/01 03:04
dolioI don't know how easy it is to show that PA is equivalent to HA.24/01 03:04
dolioAnd you can't do the same for set theory, as far as I know.24/01 03:05
ccasinyes, one can prove the consistency of constructive set theory in classical set theory24/01 03:06
ccasinso hopefully it shouldn't be so easy to show that the latter's inconsistency implies the former's?24/01 03:07
ccasinmaybe I am thinking about this wrong, though24/01 03:07
dolioDo you mean the reverse?24/01 03:08
dolioI don't think showing the consistency of constructive set theory would imply the consistency of classical set theory.24/01 03:08
ccasinright, the opposite24/01 03:09
dolioIf classical set theory proves the consistency of constructive set theory, though, then proving classical set theory consistent would prove constructive set theory consistent, presumably.24/01 03:09
ccasinclassical ZF proves constructive ZF's consistency24/01 03:09
ccasinat least, that's the folklore24/01 03:09
ccasinso it seems conceivable that classical set theory is inconsistent but constructive set theory isn't24/01 03:10
dolioAnyhow, for propositional logic, you can double negate to turn classical propositions into constructive propositions, and I believe you get all the same theorems.24/01 03:11
ccasinyes24/01 03:11
dolioThis fails for first-order logic.24/01 03:11
ccasinOK, I am reassured24/01 03:11
dolioSo it's interesting that it still works for arithmetic statements.24/01 03:11
ccasinhmm24/01 03:13
ccasinso, I'm trying to remember my constructive logic class24/01 03:14
ccasinI think there is a double negation encoding that works for FO, right?24/01 03:14
ccasinit's just a little more complicated than directly double negating everything24/01 03:14
dolioI don't know.24/01 03:14
ccasinbut it probably double negates the atomic formulas, presumably including False24/01 03:14
ccasinso we are back where we started24/01 03:15
ccasinlet me see24/01 03:15
ccasinhttp://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_negative_translation24/01 03:15
dolioI don't know, then.24/01 03:20
dolioI'd guess that classical ZF proving constructive ZF consistent is wrong.24/01 03:20
dolioUnless constructive ZF gets rid of more than excluded middle.24/01 03:21
nappingWell, looks like time to try the Agda reflection24/01 03:32
nappingFinally finished the Coq version with a quoter in Ltac - it's a huge pain working under binders24/01 03:32
dolioHmm, I can see why he wouldn't want to work on this in Agda...24/01 03:59
Saizaneverything would be of h-level 2?24/01 04:00
dolioWell, I can try not to use K.24/01 04:00
dolioBut, it's disguised in pattern matching.24/01 04:00
dolioSo, I'm left in a situation where I don't know when I should be allowed to use pattern matching to prove what I want to prove.24/01 04:01
lpjhjdhso I'm making a little abstract machine that executes instructions within an environment mapping variables to values and with a stack and was wondering how you suggest I encode a few instructions that require non-empty env and/or stack.24/01 07:27
copumpkinrepresent the stack in the type24/01 07:28
copumpkinor ask for a proof of non-emptyness with the instruction24/01 07:28
lpjhjdhwhat would the former entail?  Which type I mean to say24/01 07:28
lpjhjdhasking for a proof of non-emptiness seems reasonable24/01 07:29
lpjhjdhto implement I mean24/01 07:29
copumpkinyou could do something like an indexed monad, indexed by the size of the stack24/01 07:30
copumpkinthen24/01 07:30
copumpkindata Lang : Nat -> Nat -> Set -> Set where24/01 07:31
copumpkinor maybe it'd be parametrized by the type, since there isn't enough information to have multiple types in it24/01 07:31
copumpkinbut anyway24/01 07:31
copumpkinactually24/01 07:32
lpjhjdhsorry what would the third index Set be?24/01 07:32
copumpkindata Lang (A : Set) : Nat -> Set where24/01 07:32
copumpkinPush : forall {n} -> A -> Lang A n -> Lang A (suc n)24/01 07:32
copumpkinPop : forall {n} -> A -> Lang A (suc n) -> Lang A n24/01 07:33
lpjhjdhaha, thanks24/01 07:33
copumpkinwell, pop wouldn't take an A too24/01 07:33
copumpkinbut you know what I mean24/01 07:33
lpjhjdhyeah24/01 07:33
copumpkinalternately, you could do something like24/01 07:34
copumpkindata Lang : List Set -> Set -> Set where24/01 07:34
copumpkinhmm24/01 07:35
copumpkinthat doesn't work out as cleanly24/01 07:35
copumpkinbut anyway, parametrize it by the list of types of elements on the stack24/01 07:35
copumpkinso you can have a heterogeneous one24/01 07:35
lpjhjdhlanguage is so simple it only contains naturals, should try extending it once I work this out24/01 07:36
copumpkincool24/01 07:44
copumpkinit's worth thinking of it as a free monad, possibly24/01 07:45
copumpkinor a free indexed monad24/01 07:45
copumpkinwhere the index is the state of the stack before the operation and after24/01 07:45
lpjhjdhmy algebra is quite bad, have to read up on free structures to fully appreciate your suggestion.  A few chapters of category theory for the working mathematican.  Many thanks.24/01 07:51
--- Log closed Tue Jan 25 00:29:55 2011
--- Log opened Tue Jan 25 00:30:04 2011
-!- Irssi: #agda: Total of 34 nicks [0 ops, 0 halfops, 0 voices, 34 normal]25/01 00:30
-!- Irssi: Join to #agda was synced in 86 secs25/01 00:31
--- Day changed Wed Jan 26 2011
stevanhi,  bug or feature: http://hpaste.org/43325/s ?26/01 14:45
Saizanusually η x represents a recursive occurrence with index x, rather than representing the current index26/01 17:28
Saizananyhow, not unifying n and suc n sounds like a feature, since Nat is inductive26/01 17:29
Saizanstevan: ahah! where strikes again26/01 17:52
Saizanso, sorry, i wasn't awake enough to read the -- Works part26/01 17:52
Saizanit's a known infelicity, it appears also in "outrageous coincidences .."26/01 17:53
Saizanhttp://code.google.com/p/agda/issues/detail?id=44&q=where26/01 17:54
Saizanjlouis: godlike even?:)26/01 20:25
jlouisgodlike26/01 20:25
jlouisI pray to goddess Agda26/01 20:25
jlouisthat it will type and termination check my terms26/01 20:25
Saizanah, in _that_ sense26/01 20:26
pumpkindjahandarie: it may be more productive to ask agda questions in here :P26/01 22:32
djahandarieGood point26/01 22:32
pumpkinRel a b = a -> b -> Set26/01 22:32
pumpkinso first write Rel (what's its type?)26/01 22:35
pumpkinI wouldn't bother making all sorts of category abstractions if you just want to do this26/01 22:35
pumpkinjust state your axioms26/01 22:35
djahandarieHmm26/01 22:35
djahandarieThe category axioms?26/01 22:36
pumpkinyep26/01 22:36
pumpkinso start with Rel : Set -> Set -> Set1; Rel a b = a -> b -> Set26/01 22:37
pumpkinid : forall a. Rel a a26/01 22:37
djahandarieThat was the easy one :P26/01 22:39
pumpkindid you write it?26/01 22:39
pumpkinyou probably need something else26/01 22:39
djahandarieNo, I was thinking of the type for the associativity axiom26/01 22:40
dolioSyntax error.26/01 22:40
pumpkindolio would make a terrible compiler26/01 22:42
pumpkinit reminds me of the cmm compiler in ghc26/01 22:42
dolioAt least I gave you more information than, "problem"26/01 22:43
pumpkinyou mean that dot?26/01 22:43
pumpkinit was a pseudoagda-ey thing :P26/01 22:43
dolioYes.26/01 22:44
pumpkinid : forall a -> Rel a a26/01 22:44
pumpkindjahandarie: you're going to want equality at some pont26/01 22:46
pumpkinpoint26/01 22:46
pumpkinyou can define it yourself or pull in Relation.Binary.PropositionalEquality26/01 22:46
djahandarieCan you show me a full example of something simpler?26/01 22:47
Saizane.g. to show that (Nat,_+_) is a monoid, you'd have to make defs with the following types: forall n -> n + 0 == n; forall n -> 0 + n == n; forall x y z -> x +26/01 22:53
Saizanx + (y + z) == (x + y) + z26/01 22:54
--- Day changed Fri Jan 28 2011
Ceruleanhey. I think code.haskell.org is down (surprise surprise..?) -- anywhere other 'canonical' spot to get the repo from?28/01 21:46
--- Day changed Sat Jan 29 2011
dolioOh shit. --without-K.29/01 01:13
dolioNow we can entice Voevodsky.29/01 01:13
Saizan:O29/01 01:16
Saizanhe might like universe polymorphism29/01 01:16
copumpkinso what's this stuff about not having K, and why will it attract the guy whose name I can't remember how to spell?29/01 23:52
dolioK is uniqueness of identity proofs.29/01 23:55
copumpkinyeah29/01 23:57
dolioIn univalent foundations, identity of sets is actually isomorphism, so only bot and top have unique identity proofs.29/01 23:57
copumpkinbut why was having K keeping Mr. X away?29/01 23:57
dolioK is inconsistent with his work.29/01 23:58
copumpkinoh29/01 23:58
dolioThere's some videos linked in the dependent types reddit.29/01 23:58
dolioIf you watch, one of the main ideas is that Martin-Loef type theory is the internal language of these certain types of categories of homotopy types, or something like that.29/01 23:59
dolioBut Martin-Loef + K is not.29/01 23:59
dolioThey don't mention the latter fact, but K collapses the higher-dimensional structure.29/01 23:59
--- Day changed Sun Jan 30 2011
dolioEverything above level 2 or so. Because you can prove everything happens 'on the nose' instead of just up to higher equivalence levels.30/01 00:00
copumpkinhm :o30/01 00:02
dolioIn essence, it's like: we have the internal language of a category, except we also have an axiom that says all morphisms are the identity.30/01 00:07
dolioThat limits what categories your language applies to.30/01 00:07
copumpkinyeah, I see30/01 00:07
--- Day changed Mon Jan 31 2011
rribeiroHello... I'm trying to learn a bit of agda... I'm trying to implement a matrix transposition algorithm31/01 16:44
rribeiroI'm using the Data.Vec module from the standard library as a base for the implementation of matrix's31/01 16:45
rribeiroranspose : {m n : ℕ} → Matrix m n → Matrix n m31/01 16:46
rribeirotranspose [] = []31/01 16:46
rribeirotranspose (ns ∷ nss) = (map head ns) ∷ (transpose nss)31/01 16:46
rribeirowhen I've typed these code... I've got the error msg31/01 16:47
rribeirozero != .n of type N31/01 16:47
rribeiroany clue?31/01 16:47
ccasinrribeiro: to start with, .n here is the "n" parameter of your function31/01 16:50
ccasinI'm not sure how you implemented matrixes, but here is my guess at what is happening31/01 16:50
ccasinin the first case, you pattern match on the empty list31/01 16:50
ccasinthis means that one dimension of the matrix, the "m" one, must be 031/01 16:51
ccasinbut it doesn't give us any information about the second dimension31/01 16:51
ccasinso the input matrix has type  "Matrix 0 n" for some arbitrary n31/01 16:51
ccasinNow you return another empty vector31/01 16:51
ccasinwhich has type "Matrix 0 n' " for any n'31/01 16:51
ccasinbut, because of your type, you needed to return something with the type "Matrix n 0"31/01 16:52
ccasindoes that make sense?31/01 16:52
rribeiroccasin, Ok...31/01 16:52
rribeiroccasin, thank you!31/01 16:53
ccasinno problem31/01 16:54

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