/home/laney/.irssi/irclogs/Freenode/2011/#agda/June.log

--- Log opened Wed Jun 01 00:00:16 2011
augurdolio: x301/06 00:01
auguri feel as tho induction-recursion is induction where some of the params/indices are calculated by recursion01/06 00:02
augurbut im probably wrong01/06 00:02
dolioIt's a simultaneous definition.01/06 00:02
augurhmm01/06 00:02
augurexample?01/06 00:02
dolioWhere you define constructors of a family F <v> by induction.01/06 00:03
augurhmm01/06 00:03
dolioAnd they're allowed to make reference to a function defined by recursion over F <v>.01/06 00:03
augurexample? :P01/06 00:03
dolioA simple example is lists of unique values.01/06 00:04
dolioSuppose we have an equality test for T.01/06 00:04
doliodata Uniq : Set where nil : Uniq ; cons : (x : T) -> (xs : Uniq) -> x notElem xs -> Uniq01/06 00:05
augursupposing01/06 00:05
augurok01/06 00:05
dolio_notElem_ : (x : T) -> (xs : Uniq) -> Set01/06 00:05
augurok01/06 00:06
dolioActually, scratch that, you don't even need a test.01/06 00:06
Eduard_MunteanuYup... emb (Fin.zero {n}) = Fin.zero {ℕ.suc n}    emb (Fin.suc {k} n) = Fin.suc {ℕ.suc k} (emb n)01/06 00:06
copumpkinEduard_Munteanu: do you even need to explicitly look at those implicits?01/06 00:06
doliox notElem (cons y ys _) = (x /= y) * (x notElem ys)01/06 00:06
copumpkinEduard_Munteanu: I'm pretty sure it can infer them for you01/06 00:06
Eduard_MunteanuAh, I think so.01/06 00:07
* Eduard_Munteanu tries 'max'01/06 00:07
dolioSo, you're simultaneously defining Uniq and _notElem_.01/06 00:08
Eduard_MunteanuWait, I can't write 'max' for Fin 0...01/06 00:08
Eduard_MunteanuErm, well I could set it to zero, but anyway.01/06 00:08
copumpkinEduard_Munteanu: no you couldn't01/06 00:08
xplatyes you can.  max () ()01/06 00:08
Eduard_MunteanuAh, right.01/06 00:09
copumpkinnope01/06 00:09
xplat(can write it, not can set it)01/06 00:09
copumpkinmax : forall {n} -> Fin n01/06 00:09
* Eduard_Munteanu actually tries writing it now...01/06 00:09
copumpkinthat's me being dumb01/06 00:09
copumpkinmax : forall {n} -> Fin (suc n)01/06 00:09
copumpkin:)01/06 00:09
Eduard_MunteanuAh. :)01/06 00:09
copumpkinyou couldn't write it otherwise01/06 00:09
augurdolio: are you really simultaneously defining it tho??01/06 00:10
augurwell i guess you are01/06 00:10
dolioYes.01/06 00:10
augurboth depend on one another01/06 00:10
xplatoh, the ONE-argument max01/06 00:10
dolioIt requires the mutual keyword in Agda.01/06 00:10
augurok01/06 00:10
augurdolio: do you know anything about ornamentation?01/06 00:10
xplatyeah, you can't write that to work on Fin 001/06 00:10
Eduard_Munteanumax {n} = fromℕ n :)01/06 00:10
dolioOf course, regular definitions are sort of a special case of inductive-recursive definitions.01/06 00:11
Eduard_MunteanuWell, I suppose I could pattern-match further so I don't use fromN01/06 00:11
dolioWhere you don't even bother to specify the recursive function, and don't make use of it in the type.01/06 00:11
dolioNo, I've never read about ornaments.01/06 00:11
Eduard_MunteanuWait why mutual?01/06 00:12
dolioYou need to use the mutual keyword for mutually recursive definitions.01/06 00:12
dolioOtherwise Agda assumes definitions can be processed one at a time.01/06 00:12
djahandarieWhy is it set up that way anyways?01/06 00:13
xplati worked out that syntax example from earlier a bit further, but now it's too big to display as a screenshot :I01/06 00:13
Eduard_Munteanumax {zero} = zero     max {suc n} = suc (max {n})01/06 00:13
Eduard_MunteanuOr the point was to avoid implicits?01/06 00:13
dolioIt makes it easier on the compiler if you manually annotate your strongly connected components, I think.01/06 00:13
xplatEduard_Munteanu: you could hardly write that while avoiding the implicits01/06 00:14
Eduard_MunteanuAh, I thought dolio was telling me max needed mutual01/06 00:14
dolioAlthough augustss isn't happy about it.01/06 00:14
Eduard_MunteanuNow for the view...01/06 00:15
augurhmm01/06 00:15
dolioI'm not sure there's any stronger reason than it makes things easier to implement.01/06 00:15
auguranyone know of any really good papers about getting indices to really do a lot of work?01/06 00:15
Eduard_Munteanu< copumpkin> the view will give you the embedding or the max   -- so view : forall {n k} -> Fin n -> Fin k ?01/06 00:16
Eduard_MunteanuOr did you mean the embedding _and_ max?01/06 00:17
Eduard_Munteanu*sigh*01/06 00:29
Eduard_Munteanuview : (n k : ℕ) → Fin n → Fin k    view n k a with Data.Nat._≤?_ (ℕ.suc n) k01/06 00:29
augurno ey01/06 00:30
Eduard_Munteanu... | yes a = ?    ... | no a = ?      but Agda doesn't like the 'yes a' there. Any ideas?01/06 00:30
augurEduard_Munteanu: my suggestion is this:01/06 00:30
augurdont fill in the cases01/06 00:31
augurjust do ... | answer = ?01/06 00:31
augurload it up01/06 00:31
augurand then C-c C-c on answer01/06 00:31
augurand let agda figure out what the cases should be01/06 00:31
auguritll put in all and only the cases it DOES like01/06 00:31
Eduard_MunteanuAh, yeah, I don't even need to spell out "yes" or "no"01/06 00:32
Eduard_MunteanuAh, right, I didn't import Relation.Nullary.Core.Dec01/06 00:32
augurblah01/06 00:33
augurmy body feels like im hungover :\01/06 00:33
Eduard_MunteanuThanks , 'with' works now01/06 00:34
copumpkinEduard_Munteanu: the view is an indexed datatype01/06 00:40
copumpkinEduard_Munteanu: then you'd have a function that views any Fin01/06 00:41
copumpkinforall {n} -> (f : Fin n) -> EmbMax f01/06 00:41
copumpkinif you finish that and want more to do, there's also the invert function01/06 00:43
copumpkinFin n -> Fin n01/06 00:43
augurcopumpkin: can you think of any relatively simple functions that are uniquely determined by some property they have?01/06 00:44
copumpkinthat embMax view I just mentioned is uniquely determined01/06 00:46
copumpkinby its type01/06 00:46
copumpkinbut that's not painfully simple01/06 00:47
augurhm01/06 00:47
augurim just looking for something that isnt obnoxiously complicated01/06 00:47
augurthat i can use as a simple example of doing definition by property satisfaction01/06 00:48
copumpkinwork with functions on booleans01/06 00:51
copumpkinit seems like there should only be one group on the booleans?01/06 00:52
copumpkinmaybe not01/06 00:52
augurhmm01/06 00:53
auguri think maybe i'll try to do the Theorems-for-Free stuff backwards01/06 00:53
auguror at least one of them01/06 00:53
auguror maybe something like map01/06 00:53
copumpkinnot sure you can even prove something like : (f : forall a. a -> a) -> (A : Set) -> (x : A) -> x == f x01/06 00:55
copumpkinin fact, I'm pretty sure you can't01/06 00:55
augurey?01/06 00:56
xplatcopumpkin: wat?01/06 01:12
copumpkinwat?01/06 01:12
copumpkinso, hypothesis: there is exactly one group on the booleans01/06 01:12
copumpkintoo lazy to exhaustively check01/06 01:13
xplatfalse: && and || are both groups01/06 01:13
xplater, not groups, monoids01/06 01:13
copumpkinyeah, I knew that01/06 01:13
copumpkinbut neither of those is a group01/06 01:13
xplatokay, groups.  xor is a group.  equiv has ... \all x -> x equiv true == x.  is false its own inverse?  yes, false equiv false == true01/06 01:14
xplatbut is it associative?01/06 01:15
copumpkinI'd hope so01/06 01:16
copumpkinisn't that just transitivity of == ?01/06 01:16
copumpkinokay, not transitivity01/06 01:17
copumpkinquickcheck? :P01/06 01:17
dolioSmallcheck.01/06 01:18
copumpkin@check \x y z -> ((x == y) == z) == (x == (y == z))01/06 01:18
lambdabot  "OK, passed 500 tests."01/06 01:18
copumpkin@check \x y z -> ((x == y) == z) == (x == (y == (z :: Bool)))01/06 01:18
lambdabot  "OK, passed 500 tests."01/06 01:18
dolio@scheck \x y z -> ((x == y) == z) == (z == (y == (z :: Bool)))01/06 01:18
lambdabot  "Falsifiable, after 1 tests:\nTrue\nFalse\nFalse\n"01/06 01:18
dolio@scheck \x y z -> ((x == y) == z) == (x == (y == (z :: Bool)))01/06 01:18
lambdabot  "OK, passed 500 tests."01/06 01:18
xplatagrees with my result.  so, equiv is a group.01/06 01:20
xplati think they're isomorphic through 'not'01/06 01:20
xplat(which is why i suggested it in the first place)01/06 01:22
copumpkinyes!01/06 01:23
xplatyou could also use http://math.andrej.com/2011/01/22/alg/01/06 01:24
copumpkinwell, I'm now wondering if there's some definition of property such that forall properties P, structures on Bool appear twice (so there's a multiple of two of them)01/06 01:25
copumpkinbut that thing looks cool01/06 01:25
dolioSo, what you get with homotopy type theory...01/06 01:26
dolioIs that if P : Set -> Prop...01/06 01:26
dolioAnd P T, and T is isomorphic to U, then P U.01/06 01:26
dpiponiWhy doesn't this pass the strict positivity test: http://hpaste.org/47320/not_working when this does: http://code.haskell.org/~Saizan/UCodes.agda ?01/06 01:50
augurhm!01/06 02:00
auguri can derive a definition for map!01/06 02:00
augurrelational map, anyway01/06 02:00
AnAdorableNickeee\la01/06 02:06
augurcopumpkin: chekidout01/06 02:08
augurhttps://github.com/psygnisfive/algebraic-syntax/blob/master/Map.agda01/06 02:08
dpiponiNow it's down to μ₁ working when μ₂ doesn't :-( http://hpaste.org/47321/not_working_annotation01/06 02:08
augurSaizan: you checkit too :D01/06 02:13
djahandarieHmm. I forget who in here actually mentioned that Oregon summer school...01/06 02:17
djahandarieAh, ccasin?01/06 02:17
augurwhat summer school :o01/06 02:18
djahandarieHaven't I mentioned this to you before augur? :p http://www.cs.uoregon.edu/Activities/summerschool/summer11/01/06 02:25
auguroh that one01/06 02:25
augursome people have discussed it, me being one, yeah01/06 02:25
auguri wonder if i can plausibly take the propositional definition of map and just drop it down into the value domain01/06 02:31
auguronce i know map f nil nil = \Top ; map f (x :: xs) (y :: ys) = f x y * map f xs ys01/06 02:32
augurcan i just drop that into01/06 02:32
augurmap f nil nil = true ; map f (x :: xs) (y :: ys) = f x y && map f xs ys01/06 02:32
auguri mean, its certainly true that it works in this case but is it general, i wonder01/06 02:32
augurprobably01/06 02:34
augursets are just values and whats one value vs another, i suppose01/06 02:34
xplatyou can generally only turn real predicates into boolean predicates if they are decidable01/06 02:51
augurxplat: hm!01/06 02:52
augurwell thats ok01/06 02:52
auguri only care about decidable things01/06 02:52
augur:)01/06 02:52
cayleeSilly question - so in Observational Equality, Now! it references their development in Agda as being available as a standard example. ...where? I swear I didn't see it in the standard lib or anything.01/06 03:19
Eduard_Munteanucaylee: what sort of stuff are you looking for?01/06 03:26
Eduard_MunteanuDo they actually say it's in the stdlib?01/06 03:26
cayleeNo, they just say that it's available as an example with the distribution of Agda - of course this was 3 years ago I believe01/06 03:29
cayleeand I was wondering if the OTT development was still anywhere to be found01/06 03:29
Eduard_Munteanucaylee: hm, maybe it's in the Agda latest darcs / package01/06 04:09
Eduard_Munteanu?01/06 04:09
Eduard_MunteanuThere is an examples/ dir there.01/06 04:09
copumpkinEduard_Munteanu: did you succeed!?01/06 04:10
augurcopumpkin: did you look? :o01/06 04:15
copumpkinnot yet01/06 04:16
augur:(01/06 04:16
copumpkingimme a few to finish this video01/06 04:16
Eduard_Munteanucopumpkin: ah no, I took a break, had to work on some C code :)01/06 04:19
copumpkinhttp://vimeo.com/16534403 is nice01/06 04:30
augurcopumpkin: :|01/06 04:37
copumpkinI'm on the phone!01/06 04:37
augur:|01/06 04:37
augurso mean01/06 04:37
copumpkinlol01/06 04:37
Eduard_MunteanuWhat HTML5 codecs is Vimeo using? I'm using Firefox 4, but it's complaining.01/06 04:49
copumpkinaugur: looking now01/06 05:06
augur:D01/06 05:06
copumpkinaugur: I'm confused01/06 05:06
augurok01/06 05:06
copumpkinmap-theorem : ∃ (∀ {X Y n}01/06 05:07
copumpkin                 → (X → Y → Set) → Vec X n → Vec Y n01/06 05:07
copumpkin                 → Set)01/06 05:07
copumpkin                (λ map → (X Y : Set) (n : ℕ) (f : X → Y → Set) (xs : Vec X n) (ys : Vec Y n)01/06 05:07
copumpkin                       → map f xs ys ↔ ((i : Fin n) → f (proj xs i) (proj ys i)))01/06 05:07
copumpkinthat type01/06 05:07
auguryes01/06 05:07
copumpkinit feels like it should have more parentheses01/06 05:08
augurwhy01/06 05:08
copumpkin(∀ {X Y n} → (X → Y → Set) → Vec X n → Vec Y n)01/06 05:08
copumpkinthat alone is the type of a map for vectors01/06 05:08
copumpkinsort of, anyway01/06 05:08
copumpkinoh I see01/06 05:08
augurno no01/06 05:08
auguryeah01/06 05:08
copumpkinyeah, I'm dumb01/06 05:08
augurits relational map01/06 05:09
augurnot functional map01/06 05:09
copumpkinyeah01/06 05:09
copumpkinokay, ignoe me01/06 05:09
auguri shouldve put the Vec's on the line after that01/06 05:09
augurto make it more symmetric01/06 05:09
copumpkinlooks cool01/06 05:10
copumpkinhowever01/06 05:10
copumpkin        map f nil nil = ⊤01/06 05:10
copumpkin        map f (x :: xs) (y :: ys) = f x y ∧ map f xs ys01/06 05:10
copumpkinthat kind of thing is where I'd probably start making my own types01/06 05:10
augur?01/06 05:10
copumpkinthat's basically defining a type, right?01/06 05:11
auguryes01/06 05:11
augurwell01/06 05:11
augurnot quite01/06 05:11
augurbut i mean, sure01/06 05:11
copumpkindata MapRel (X Y : Set) : {n} -> Vec X n -> Vec Y n -> Set where01/06 05:11
copumpkinnil : MapRel nil nil01/06 05:11
copumpkincons :  blahblah01/06 05:11
augurwell01/06 05:12
augurim not sure how that would integrate with the definition discovery component01/06 05:12
augursee, the point is01/06 05:12
augurthe value for map f nil nil wasnt decided on, it was discovered01/06 05:12
augurthe first case for the proof p determined that the value of map f nil nil should be something that's provable in some general fashion01/06 05:13
copumpkinyou discovered it, but you haven't proved that it's the only definition01/06 05:13
copumpkinand it isn't the only definition01/06 05:13
auguroh im not saying it is01/06 05:14
auguri said it's _a_ definition01/06 05:14
augurthats all im interested in right now01/06 05:14
copumpkinah01/06 05:14
augurgiven some property that the function must have, can we find a definition01/06 05:14
augurand how01/06 05:14
copumpkinwell, creating an inductive family to define your relation can be a process of discovery too, just as much as that function :)01/06 05:14
copumpkinjust saying it'll be more fun to work with later if you do it that way, but I see that isn't the point01/06 05:15
augurim not sure how to do that with this01/06 05:15
copumpkinyeah, you can't use holes in the same way01/06 05:17
augurwell01/06 05:18
auguri could leave some of it missing and add it when i need more cases01/06 05:18
augurbut im not sure what that would do for me01/06 05:18
copumpkinwell, in general, it lets you pattern match on the proof and get more information by doing so01/06 05:22
copumpkinrather than pattern matching on something that then gives you more information about something else which you also match on01/06 05:23
auguroh sure, but the point isnt really to define map in a way thats usable and informative01/06 05:23
augurrather, to discover the stucture of such a definition01/06 05:23
copumpkinyeah01/06 05:23
augurso what do you think of the general structure of the method, copumpkin01/06 05:25
auguri suppose its something of a proof pattern01/06 05:25
auguror something01/06 05:26
copumpkinit looks rather indirect01/06 05:26
copumpkinit lets you do what you want to do with it01/06 05:26
copumpkinbut it feels like there should be a more straightforward way?01/06 05:26
auguri know01/06 05:26
auguri'd like to find a more straightforward way too!01/06 05:27
augurcopumpkin: im not really sure how to clarify it any further tho01/06 05:32
copumpkinthis will make it all clear: http://www.youtube.com/watch?v=lBC6z6xcnFM01/06 05:32
auguri feel like what you'd want to do is put the proofs for each case along side the definition cases01/06 05:33
auguror indeed, derive the definition cases from the proofs somehow01/06 05:33
augurbut im not sure how to achieve that01/06 05:34
augurcopumpkin: any ideas?01/06 06:05
Eduard_MunteanuHow can I see what a meta refers to without correcting errors?01/06 11:14
FavoniaHi, is it possible to specify an implicit argument while using a function in a mixfix way?01/06 13:32
Saizanno01/06 13:55
sshcSaizan: Is there a particular reason ou defined _==_ as _\==_?  The tutorial uses the former name.01/06 14:05
Saizansshc: the stdlib uses the latter01/06 14:10
* sshc nods01/06 14:10
xplati came up with a new way to avoid the 'all yellow' problem with my <_>,<_> operator, but it doesn't work because no modules are allowed in mutual blocks01/06 15:28
xplatargh01/06 15:34
xplatonce again i tried defining it outside the abstract block, once again every occurrence fails to solve for two objects01/06 15:35
ccasindjahandarie: yeah, it was probably me - are you coming?01/06 15:48
ccasinit's going to be fun!01/06 15:48
xplatit seems like it can't figure out the destination of arrows f and g from \< f , g \>01/06 15:51
djahandarieccasin, yep!01/06 15:51
xplator from the type of same01/06 15:51
djahandarieHow many people usually show up at these things anyways?01/06 15:51
ccasindjahandarie: I think it's pretty big, say 100 people.  They might have a list on the website already, let me see01/06 15:52
djahandarieOh wow, that's pretty big01/06 15:53
djahandarieWas expecting like ~35-4001/06 15:54
ccasinlooks like last year there were 95 or so.  I'd guess it will be a similar size this year01/06 15:54
ccasinsorry, make that 86 last year01/06 15:55
xplatso this year there should be 9901/06 15:56
djahandarieI'll have to do my best to absorb all information possible01/06 15:57
djahandarieI hope some of the lectures go into hardcore category theory01/06 15:57
ccasinsure, but don't stress out about it too much - the best part is hanging around with 100 other type theory nerds for two weeks01/06 15:57
ccasinlectures or not01/06 15:58
ccasinyou're bound to learn loads01/06 15:58
djahandarieHardly stressing out about it, more interested in efficent absorbtion. :p01/06 15:58
ccasin:)01/06 15:58
copumpkinthey'll all be like "wtf is this young dude doing here??"01/06 15:59
xplati don't get this at all, the abstract type of <_,_> should be plenty to recover the targets of its arguments01/06 15:59
* djahandarie prepares his assimilation beam01/06 15:59
djahandariecopumpkin, I'm not /that/ young looking :p01/06 15:59
copumpkinyou should go around telling everyone you're in middle school, just to fuck with them01/06 15:59
djahandarieHaha01/06 15:59
copumpkinmake them feel really bad about themselves01/06 15:59
* copumpkin just received an RSA securid!01/06 15:59
copumpkinzomg01/06 15:59
copumpkinnow I can get hacked just like the big guys did01/06 16:00
xplatcopumpkin: help!  i want to get this over with so i can start porting to stdlib :(01/06 16:01
djahandarieHmm, only lecture that mentions categories is "Programming languages in string diagrams"01/06 16:01
copumpkinxplat: what's wrong? sorry, haven't really been following :)01/06 16:01
copumpkinwhat code is this?01/06 16:01
xplatcopumpkin: Category.Object.BinaryProducts.Abstract.HomReasoningP defines <_>,<_> as 'the same thing as <>-cong₂ plsthx'01/06 16:03
copumpkinoh, that thing!01/06 16:03
xplatcopumpkin: but unlike the former it fails (100% of the time) to solve A and B, which are the targets of the arrows being <_,_>·d01/06 16:04
xplatcopumpkin: this problem goes away if it's defined in the abstract block, but i don't know why it goes away, nor why it exists in the first place01/06 16:05
copumpkinI remember looking at this last time you mentioned it and maybe it's a bug? could be worth posting to the mailing list01/06 16:05
xplatalso, i can't figure out any way to have it appear in the right scope if it's defined in the abstract block01/06 16:05
djahandarieI keep on ending up at linear logic and linear type theory in my internet traversals. Maybe I should do something with it.01/06 16:07
copumpkinhave you read the ATTaPL chapter on it?01/06 16:08
djahandarieI haven't, maybe I'll do that01/06 16:08
ccasindjahandarie: I highly recommend Frank Pfenning's lecture notes too, for a good introduction.  They are somewhere on his website01/06 16:08
xplatlinear logic is well-known as the only field of knowledge that allows you to use an upside-down ampersand as a legitimate piece of math notation01/06 16:08
djahandarieHeh01/06 16:09
djahandariecopumpkin, do you have symmetric monoidal categories in your lib?01/06 16:09
xplatnot symmetric yet01/06 16:09
djahandarieOnly braided?01/06 16:09
copumpkinnot even braided01/06 16:10
xplatno, just monoidal01/06 16:10
djahandarie:(01/06 16:10
copumpkinwe have cartesian and monoidal01/06 16:10
copumpkin:)01/06 16:10
djahandarieHow about closed?01/06 16:10
copumpkinfeel free to add braided or symmetric01/06 16:10
copumpkinnope01/06 16:10
copumpkinor add closed :P01/06 16:10
djahandarieI don't think I could actually do any of the proofs for these01/06 16:11
copumpkinclosed might take some work if I want to start with closed non-monoidal and then move up01/06 16:11
copumpkinI need extranatural transformations I think before I can even write that01/06 16:11
xplati'm a little fuzzy on what closed actually means without a monoidal product you want to be able to curry01/06 16:11
djahandarieSame01/06 16:12
copumpkinhttp://ncatlab.org/nlab/show/closed+category01/06 16:12
xplatcopumpkin: lmncltfy?01/06 16:13
copumpkinlol01/06 16:13
copumpkinyeah!01/06 16:13
djahandarieHaha01/06 16:13
* djahandarie already got off that page and started reading about Cat_g01/06 16:14
djahandarieStop linking me to ncatlab when I'm at work! ;)01/06 16:14
djahandarieI really need brush up on adjoints and pullbacks and such01/06 16:15
* copumpkin screams: http://www.reddit.com/r/programming/comments/ho20s/imperative_vs_functional_programming/c1x6n1z01/06 16:17
djahandarieThis looks like a good link01/06 16:18
* copumpkin wants to strangle someone01/06 16:18
xplatwhy am i following this link?  surely nothing good can come of this01/06 16:18
ccasinhaha, if you don't like objects you are a climate change denier01/06 16:18
ccasinpriceless01/06 16:18
copumpkinwell, my previous point was that I found it hard to believe that people had actually done research claiming that it's "more natural" to believe in OO01/06 16:19
copumpkinsince it's impossible to control all variables that would be required to make such a strong claim01/06 16:19
xplati would definitely believe that it is more natural for rhesus monkeys to program in OO01/06 16:20
xplatgeneralizing this result to humans seems premature01/06 16:21
ccasinyes, this style of argument is silly.  We'll never all agree on what style of programming is the "most natural to humans".  But we can agree on which style of programming humans have had the best success reasoning _about_01/06 16:22
ccasinI, for one, like writing correct programs :)01/06 16:22
ccasinI suppose there aren't many imperative programmers left to convince in #agda...01/06 16:25
xplatthe cited paper is interesting but only slightly on-point01/06 16:26
djahandarieOh, great comments on the article itself too01/06 16:31
augurheyo01/06 16:51
xplati hope i can get this working somehow, because it is far nicer to write something like01/06 18:12
xplat↑⟨ ⟨ assoc ⟩,⟨ ⟨ assoc ⟩,⟨ refl ⟩ ⟩ ⟩01/06 18:12
xplatrather than ↑⟨ ⟨⟩-cong₂ assoc (⟨⟩-cong₂ assoc refl) ⟩01/06 18:14
copumpkinyeah01/06 18:44
copumpkinI'd honestly send an email to the mailing list01/06 18:44
augurcopumpkin!01/06 18:45
augur:D01/06 18:45
copumpkinyo dawg01/06 18:45
augurlets figure out how to make this proof more elegant!01/06 18:45
copumpkinhow about let's work01/06 18:46
augurthats what i said!01/06 18:46
copumpkinI have a day job :P01/06 18:46
augurday jobs are for chumps01/06 18:46
copumpkinyour job is to do this stuff, mine is not :P01/06 18:46
copumpkin:)01/06 18:47
augurim not really sure how to avoid the use of internal definitions and with01/06 18:48
augurand i think that forces a certain structure onto things01/06 18:49
xplatcopumpkin: i'm trying to create a small example01/06 18:55
augurxplat: have you seen my little deduction of relational map? :D01/06 18:59
xplatargh01/06 19:00
xplatmy small example works correctly!  damn it.01/06 19:00
auguris it talk like a pirate day already?01/06 19:00
copumpkinARR matey01/06 19:01
copumpkin@arr01/06 19:01
lambdabotI'll crush ye barnacles!01/06 19:01
copumpkin> (arr (+1) >>> arr (*2)) 501/06 19:02
lambdabot  mueval-core: Time limit exceeded01/06 19:02
copumpkino.O01/06 19:02
augurhmm01/06 19:02
xplatnae, that'd be 'arr, my small example ain't half near as yellow as a lily-livered spaniard!  scupper me wi' a cutlass, arr.'01/06 19:02
augurmaybe i can define some sort of eliminator-like thing that breaks down existential proofs into their cases01/06 19:03
xplator something like that01/06 19:03
augurim not sure how that'd really work tho01/06 19:03
augurno it probably couldnt actually01/06 19:03
xplatdoes the stdlib define product of setoids anywhere?01/06 19:39
dolioI suspect not.01/06 19:42
copumpkinSetoids don't get much love01/06 19:43
xplatwell, they are kind of a pain to use :(01/06 19:50
xplati am totally failing at reducing this to a smaller test case01/06 19:50
xplatokay, here's an example of how setoids are a pain to use: there's a way to define a functionspace setoid from one setoid to another setoid or family of setoids01/06 19:52
xplatbut for a functionoid you have to write f : (Q ⟶ A)01/06 19:53
xplatbut the setoid of functionoids is Q ⇨ A01/06 19:54
xplatand there's no nice inline way to get from one to the other (either direction) without importing either Setoid.Carrier (with frozen level arguments if you open, ugh) or else reconstructing Q ⇨ A from Q and A yourself01/06 19:56
xplatbasically this comes down to the fact that the translation from setoid to Set forgets all the setoid structure so you have to pass it separately01/06 19:58
xplatof course i can't figure out a better way to do this because if you wrap it in a sigma/record of which setoid it is you'll need to prove things are in the same setoid before you compare them01/06 19:59
xplatwhich is even more awkward01/06 20:00
xplat(and is an example of how the type system treats sigmas as second-class compared to pis even with all agda's special record support)01/06 20:02
dolioWhat was the type on f? Windows is not advanced enough to display it.01/06 20:04
dolioAnyhow, I agree they're a pain to use.01/06 20:05
djahandarieSame, can't see the type of f. Unless that is actually suppose to be a box.01/06 20:09
xplattype of f is Q \r-- A01/06 20:10
xplatsetoid of functionoids is Q \r7 A01/06 20:10
xplatanyway, you end up with types like  ∀ {A B C : Setoid ℓ e} {f f′ : C ⟶ A} {g g′ : C ⟶ B} → Setoid._≈_ (C ⇨ A) f f′ → Setoid._≈_ (C ⇨ B) g g′ → Setoid._≈_ (C ⇨ A ×̃ B) ⟨ f , g ⟩ ⟨ f′ , g′ ⟩01/06 20:11
augurdolio!01/06 20:41
copumpkinBerengal!!01/06 20:54
xplatsay, why won't blah : 0 \== 0 ; blah = _ resolve?01/06 21:00
copumpkinit can only infer _ if it's a record01/06 21:00
copumpkinI'd assume it could be made a little bit more clever01/06 21:00
xplatso only for records will it refine a _ to a constructor without unifying wiht a constructor that already exists01/06 21:26
xplateven if the type of the _ is a data with only one constructor01/06 21:27
copumpkinyeah, it doesn't know that the indices allow the constructor to be introduced01/06 21:33
dolioEta expansion will turn the _ into record {}.01/06 21:45
dolioBut there's no eta expansion for data.01/06 21:45
augurcopumpkin: how do i eval something in aquamacs?01/06 22:53
FavoniaSaizan: thanks (for your reply in the morning)01/06 22:57
SaizanFavonia: heh, np01/06 22:59
FavoniaHello everybody, is there any difference between ∀ {x : A} → ... and {x : A} → ? I only noticed the difference when it is ∀ {A} → ... and {A} → .... Also, is ∀ {A} equivalent to ∀ {A : Set} ?01/06 22:59
augurSaizan! :o01/06 23:00
Saizan∀ {x : A} → ... and {x : A} → are the same01/06 23:00
Saizan{A} -> ... is illegal01/06 23:00
Saizanand ∀ {A} -> .. is the same as {A : _} -> ..01/06 23:01
augurso copumpkin: i think i've found a bit of a general pattern going on here01/06 23:01
Favonia{ A : _} ? cool!01/06 23:01
FavoniaI've never thought that the underline can be used in the signature :P01/06 23:02
Saizanit can be used anywhere :)01/06 23:02
augurfor the map case, anyway01/06 23:02
FavoniaSaizan: so I guess forall is actually a syntax sugar, right?01/06 23:03
xplatcrap!  i've created an example with setoids, and it doesn't have the problem either01/06 23:03
augurfor map it looks like you have this thing,   H R = ∀ X Y n (f : X → Y → Set) (xs : Vec X n) (ys : Vec Y n) → R X Y n f xs ys01/06 23:03
augurand the type of the witness is H (λ _ _ _ _ _ _ → Set)01/06 23:04
SaizanFavonia: yep, it's so you can avoid giving type signatures to parameters01/06 23:04
augurand the type of the proof is H (λ X Y n f xs ys → map f xs ys ↔ ((i : Fin n) → f (proj xs i) (proj ys i)))01/06 23:04
xplatFavonia: you do see a difference with ∀ A -> B and A -> B01/06 23:05
augurcopumpkin: im not sure what such a beast as H is, but01/06 23:05
xplatin the former, A is the parameter name and the type is _, in the latter A is the type and there is no name01/06 23:05
augurnor what the operation is that turns  H ...  into H ...'01/06 23:05
FavoniaSaizan: cool. if ∀ {A} is translated into {A : _}, what will "∃ blah" be translated to?01/06 23:05
Favoniaxplat: I see01/06 23:05
xplati guess if you wanted to be obscure as possible you could write _ -> B :)01/06 23:06
Favoniaxplat: haha01/06 23:06
Saizanthere's no ∃ syntactic sugar, but Data.Product defines a ∃01/06 23:06
FavoniaSaizan: thanks. I'll take a look on it01/06 23:06
xplat\exists and sigmas in general have no magic, except for the occasional syntax declaration someone might have done01/06 23:07
FavoniaAlso a general question: are there any general libraries for basic number theory? or example, what would you suggest if I want to prove that the number of primes is countably infinite :P01/06 23:08
xplatso you have to write things like \Sigma[ x \: A ] B where \: isn't an actual : but kind of looks like one01/06 23:08
FavoniaI see there are Coprime and GCD01/06 23:08
Favoniaxplat: hmmm01/06 23:09
xplatthere is syntax magic to define records, but nothing for one-off sigmas01/06 23:10
Favoniaxplat: I am sorry but what is "one-off" sigmas?01/06 23:11
Favoniaxplat: I see the line "syntax Σ A (λ x → B) = Σ[ x ∶ A ] B" in the std lib01/06 23:14
--- Day changed Thu Jun 02 2011
xplat'one-off' means a specific type you use only in one place02/06 00:06
xplatpi types get special treatment for that situation, sigma types do not02/06 00:07
xplatthat syntax line kind of fakes up what it might look like if they did02/06 00:07
xplatbut if it were built-in it would be more consistent with the syntax of functions and other binders02/06 00:08
augurxplat: i think its important that you can build sigmas from prods02/06 00:17
auguri mean, important in the underlying sense02/06 00:18
augurthat sigmas aren't necessarily primitive, so long as you have dependent functions02/06 00:18
augurhmm02/06 01:32
augurthe new OAAO paper is like twice the original length02/06 01:32
augurinteresting02/06 01:32
augurhmm interesting02/06 14:15
auguris there a way to show some sort of natural correspondence between \ () and \top ?02/06 14:16
auguror well.. i suppose a natural correspondence between something like02/06 14:17
augur\bot -> X and \top02/06 14:17
augurwhere \() ~ tt02/06 14:17
augurmaybe.. \bot -> Set ~ \top perhaps02/06 14:19
augurno i think its really \ () : \bot -> Set ~ \top : Set02/06 14:23
augurthats the relation thats important02/06 14:23
auguri suppose it could go by way of \bot -> Set ~ \top tho02/06 14:24
augur\ () ==type==> Zero -> Set ==iso==> One   but is there a general thing iso that will do that more generically? hm.02/06 14:26
augurhmm02/06 16:37
augurwhy wont this syntax definition work: syntax caseP z (λ x y → f x y) xs = case xs []→ z [ x ∷ y ]→ f x y02/06 16:37
Eduard_Munteanuaugur: I don't think you're supposed to have that 'f x y' part on the rhs there02/06 16:38
Eduard_MunteanuHave you seen the one for bind?02/06 16:39
auguroh maybe thats it02/06 16:40
Eduard_Munteanu'f' should be enough I think02/06 16:40
Eduard_MunteanuThe lambda on the lhs should bring x and y into f's scope, granted f must take two parameters.02/06 16:40
augurmm nope, not working either02/06 16:40
Eduard_MunteanuI'm also worried about that 'case'.02/06 16:41
Eduard_MunteanuDoes it say you don't have alternating holes and non-holes?02/06 16:41
augurits just giving me a parse error02/06 16:42
Eduard_MunteanuCould you repaste what you have?02/06 16:42
augursyntax caseP z (λ x y → F) xs = case xs []→ z [ x ∷ y ]→ F02/06 16:42
augurSyntax/algebraic-syntax/Map.agda:25,21: Parse error y<ERROR> → F) xs = case xs []→ z [ x ∷...02/06 16:43
Eduard_MunteanuHrm, I didn't try using two things in a lambda.02/06 16:44
augurahh thats the problem02/06 16:44
augurhow obnoxious02/06 16:44
augurthats stupid02/06 16:45
Eduard_Munteanuaugur: try defining _∷_ as _,_, and replace x ∷ y by some 't'. Then you can use projections I guess.02/06 16:45
augurmeh. its not that important02/06 16:46
Eduard_MunteanuAre you trying to define case-of expressions for lists?02/06 16:48
augurEduard_Munteanu: yeah, for convenience02/06 16:52
auguri looked and didnt see a predefined one02/06 16:52
Eduard_MunteanuI'm not sure you can make it pattern-match, though.02/06 16:53
Eduard_MunteanuThe _∷_ in your syntax won't do anything wrt the list _∷_02/06 16:54
augurofcourse not02/06 16:54
augurbut im not asking it to!02/06 16:55
augurcaseP does the pattern match02/06 16:55
Eduard_MunteanuIn which case it's more like an if-empty-then_else_ :)02/06 16:55
augurcase_[]->_[_::_]->_ is just sugar!02/06 16:55
Eduard_MunteanuDamn, case expressions would be really nice to have.02/06 16:56
auguri dont actually need them for definitions02/06 16:56
augurits for types02/06 16:56
augurim trying to define a proposition thats provable differentially02/06 16:57
augurP [] = \top ; P (x :: xs) = ...02/06 16:57
augurehh no i can get away with using something else actually02/06 16:59
augurwhats a good code font :|02/06 17:53
augurahh courier 13 is what im seeing for the library02/06 17:55
auguri shall continue using monaco 1302/06 17:57
augurmonaco 12 even!02/06 18:39
Eduard_MunteanuI use DejaVu Sans Mono.02/06 18:48
Eduard_Munteanu11, I think02/06 18:49
Eduard_MunteanuProportional fonts might look nicer depending on what sort of unicode magic you might be writing, I guess.02/06 18:50
auguri use unicode /everywhere/02/06 18:51
* djahandarie thinks augur is very much the opposite of himself02/06 18:51
djahandarieI wonder what sort of category I am02/06 18:53
auguror at least what kind you're in02/06 18:53
augurthe category Hum02/06 18:53
augurfor hummus02/06 18:55
auguri want to write code in the font that is used for lagda documents :|02/06 19:36
sshc"    z =/= b : {n : Nat}   ->            zero   =/= succ n02/06 20:29
sshc" Why can't "z" and "b" be replaced with "_"?02/06 20:29
sshcAgdaBasics.agda:674,5: Parse error _<ERROR> =/= _ :02/06 20:30
sshc{n : Nat} -> ...02/06 20:30
copumpkinhuh02/06 20:30
copumpkinyou want it part of the operator02/06 20:30
copumpkin_=/=_02/06 20:30
auguryou dont put spaces there, sshc02/06 20:30
copumpkin\==n is a nicer symbol, too02/06 20:30
augurand you dont put the arguments in the lhs of the type02/06 20:30
sshcOh.  I see02/06 20:31
augurso you couldnt do z =/= b even if you wanted to, afaik02/06 20:31
nappingunless that's supposed to be a constructor z=/=b?02/06 20:31
sshcnapping: It was.  I read the tutorial wrongly02/06 20:32
nappinghave you done much with the inequality?02/06 22:17
nappingsshc, you might also try02/06 22:17
nappingdata _≢_ {A : Set} : A → A → Set where02/06 22:17
napping  different : {a b : A} → .(a ≡ b → ⊥) → a ≢ b02/06 22:18
nappingit's kind of interesting, with the irrelevant argument you can prove02/06 22:18
nappingneq-eq : {A : Set} {a b : A} (p q : a ≢ b) → p ≡ q02/06 22:18
nappingyou can even extract a refutation02/06 22:18
nappingneq-not-eq : {A : Set} {a b : A} → a ≢ b → a ≡ b → ⊥02/06 22:19
auguri feel like this isnt terribly surprising02/06 22:26
augurwell, the refutation extraction anyway02/06 22:27
augurneg-not-eq (different ref) = ref02/06 22:27
nappinghow is that allowed?02/06 22:28
augurhow isnt it?02/06 22:28
nappingwell, that component is marked irrelevant02/06 22:29
augurwell then unmark it irrelevant!02/06 22:29
auguri dont really get the whole irrelevant thing02/06 22:29
augurat least in constructors like that02/06 22:29
nappingThe point is to mark it irrelevant so different equality proofs are equivalent02/06 22:29
auguri get it when pattern matching -- duplication of information, etc.02/06 22:30
augurbut i dont know how it would work for constructors02/06 22:30
nappingYou definition is accepted anyway02/06 22:30
augurwell then!02/06 22:30
nappingsomething seems broken02/06 22:33
nappingdata irrtest : Set where Irr : .ℕ → irrtest02/06 22:34
nappingshouldn't allow extract : irrtest → ℕ; extract (Irr n) = n02/06 22:34
copumpkinhow do you write neq-not-eq?02/06 22:38
nappinghmm, maybe I ended up with an irrelevant version02/06 22:39
nappingbut, you are allowed to match irrelevent things with absurd patterns02/06 22:39
copumpkinhm02/06 22:40
copumpkinI see02/06 22:40
nappingthis is frustrating, I don't see how to tell if a definition is relevant or not02/06 22:40
nappinghttp://hpaste.org/47371/irrelevance02/06 22:41
nappingIt fails at the very last step02/06 22:41
copumpkinwait, 7 doesn't fail?02/06 22:42
nappingno02/06 22:43
nappingonly 16/17 fails02/06 22:43
copumpkinit does fail on 702/06 22:44
copumpkinin my agda02/06 22:44
nappinghmm, maybe mine is old02/06 22:45
napping2.2.1002/06 22:46
copumpkinyeah, I built mine a few days ago02/06 22:47
copumpkinthat line 7 should definitely not typecheck02/06 22:47
nappingI'll rebuild02/06 22:50
nappinghmm, seems to be up to date with respect to hackage02/06 22:50
copumpkinthat one may just be broken02/06 22:52
copumpkinI'm sure you can derive a contradiction if 7 typechecks02/06 22:52
nappingwell, that's what I tried to do at 16, but it didn't02/06 22:52
nappingIt turns out that extract gives you a "_ : bool"02/06 22:53
nappingan ignored bool, which is condiered equivalent to any other ignored bool02/06 22:53
augurso copumpkin02/06 22:53
augurexplain to me these irrelevant thingies02/06 22:53
copumpkinbasically says they can't be computationally relevant02/06 22:58
copumpkinyou can use them in other irrelevant contexts02/06 22:58
copumpkinbut otherwise it'll prevent you from doing that02/06 22:59
augurim not sure i follow but ok!02/06 22:59
dolioThe irrelevance in Agda allows the type system to check that your don't actually look at certain arguments when producing results.02/06 23:24
dolioOr certain parts of their arguments.02/06 23:24
dolioAnd since your functions don't look at them, they can be erased.02/06 23:25
dolioDuring type checking, even.02/06 23:25
--- Day changed Fri Jun 03 2011
augurso tired x.x03/06 00:16
augurdolio! :D03/06 00:17
auguralso, copumpkin03/06 00:17
auguri have a modified version of the mapR file03/06 00:17
augurhttps://github.com/psygnisfive/algebraic-syntax/blob/master/Map.agda03/06 00:18
auguri added a really dumb, simple induction as a starting point, and also clarified some of the mapR reasoning03/06 00:19
auguralso theres a bunch of notes that might be useful in coming up with the right combinators03/06 00:19
nappingCan you prove {A : Set} (f g : A → ⊥) → f ≡ g?03/06 19:46
Saizanno03/06 19:48
nappingok. It's easy enough to show pointwise03/06 19:49
Saizani wonder what could go wrong if all bottoms were definitionally equal03/06 19:50
nappingyou mean all empty types?03/06 19:51
Saizans/bottoms/elements of \bot/03/06 19:51
nappingbot-eq : (x y : ⊥) → x ≡ y; bot-eq () ()03/06 19:51
nappingthey already are.03/06 19:51
Saizanthat's propositionally03/06 19:51
Saizanbot-eq _ _ = refl won't typecheck03/06 19:51
Saizanwhile it would for s/\bot/\top/03/06 19:51
Eduard_Munteanu\bot isn't the only empty type though03/06 19:52
nappingtrying to identify different empty types is hard03/06 19:52
Saizani'd be happy if it worked for datatypes with no constructors :)03/06 19:52
nappingwhat do you mean it works for top?03/06 19:53
nappingI don't see that either03/06 19:53
Eduard_MunteanuWell you ask that for stuff that's isomorphic to \bot03/06 19:53
doliotop is defined as a record, so it eta expands into the same thing in both cases.03/06 19:53
nappingAh03/06 19:53
nappingFor little things like this, I usually just redefine \== and so on, rather than picking up the reloading cost of importing from the standard library03/06 19:54
nappinga single-constructor data type does not work like that03/06 19:54
Saizanyeap03/06 19:55
Eduard_MunteanuWhat about stuff like    isBot : (A : Set) -> (A -> \bot) \x (\bot -> A)      bot-eq : (x y : Set) -> {_ : isBot x \x isBot y} -> x \== y03/06 19:55
Saizanthat bot-eq doesn't have much to do with the one above, btw03/06 19:56
Eduard_MunteanuAh, oops, it has more to do with napping's stuff03/06 19:57
nappingDid you see my question yesterday about irrelevance?03/06 19:57
nappinghttp://hpaste.org/47371/irrelevance03/06 19:57
Saizananyhow that can't be proved, i think03/06 19:57
nappingIt's a case of functional extensionality, I was wondering if the empty result type made it easier somehow03/06 19:57
nappingThe "oops" in the paste fails to typecheck, but surprisingly the rest are fine03/06 19:58
Saizanthe fact that extract doesn't need to be marked somehow is what's surprising for me03/06 19:59
augurSaizan: have i shown you my derivation of mapR?03/06 19:59
nappingYes, pretty much03/06 20:00
nappingIf it was .extract : irrtest -> Bool, or extract : irrtest -> .Bool I wouldn't be suprised03/06 20:00
nappingbut as it is, there seems to be no way to require or even to check whether a function has become (partially?) irrelevant03/06 20:00
Saizanextract doesn't typecheck with darcs agda, btw03/06 20:01
nappingSo it's changed from 2.2.1003/06 20:01
augurSaizan: https://github.com/psygnisfive/algebraic-syntax/blob/master/Map.agda03/06 20:01
auguri'd like your opinion03/06 20:01
augursome of it is leftovers from previous versions03/06 20:03
augurthe important bits are the derivation of empty-theorem and mapR-theorem03/06 20:03
dolionapping: extract doesn't generate complaints?03/06 20:06
dolioIf it doesn't, then you need to report a bug.03/06 20:08
Saizanaugur: what kind of opinion?03/06 20:12
augurSaizan: any!03/06 20:12
augurespecially if its the sort that might point in the direction of a cleaner way to do such derivation of definitions :p03/06 20:12
Saizanwell, when you know that the type you're looking for has to be equivalent to a function type the are fairly mechanical rules to deduce the equivalent "table"03/06 20:19
auguroh?03/06 20:19
Saizanwhich is the stuff MemoTrie is based on03/06 20:19
augurwhat should i read03/06 20:19
Saizane.g. "Type Fusion" by Hinze03/06 20:24
Saizan(which talks about isomorphic types anyhow)03/06 20:24
nappingdolio: Saizan says it does in the darcs version03/06 20:24
nappingI could mention it on the list, if you think it would help03/06 20:25
Saizanhttp://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.3272 <- or this03/06 20:25
augurSaizan: im not sure i understand03/06 20:27
dolionapping: Not if it's already fixed, probably.03/06 20:35
copumpkinnapping: didn't I say it did in the darcs version too, yesterday? :P03/06 20:36
nappingI remember you saying you expected it to fail on "extract"03/06 20:44
nappingbut not saying that it was actually fixed03/06 20:44
copumpkinhttp://snapplr.com/0h8t03/06 20:44
copumpkinI guess I didn't actually say it was fixed03/06 20:44
copumpkinjust that it didn't typecheck on mine :)03/06 20:44
nappingI guess I didn't think very carefully what version you would have built a few days ago03/06 20:46
nappingReading that right after I recompiled the broken 2.2.10 didn't help :)03/06 20:47
copumpkinby the way, http://hpaste.org/47411/not :P03/06 20:47
copumpkinI'm not sure what eelis is on in #coq03/06 20:47
nappingYeah, it's of course an instance of extensionality03/06 20:48
nappingand pointwise equivalence is proven how he suggests, at least in Coq03/06 20:48
copumpkinyeah03/06 20:48
nappingIs code.haskell.org down?03/06 20:49
copumpkinnot for me03/06 20:49
nappingit seems to be from here03/06 20:49
nappingcommunity.haskell.org (178.63.91.44) ?03/06 20:58
Saizanyep03/06 21:00
augurSaizan: can you explain the connection? i dont really see it03/06 22:17
auguri skimmed the papers you pointed me to and dont see any explanations there of how to use properties to derive definitions..03/06 22:18
Saizanaugur: see Example 6.103/06 22:23
Saizanof Type Fusion03/06 22:23
Saizanwell, actually, the whole section 603/06 22:24
Saizanit starts by noting that (Nat -> A) ~~ Stream A, and then proceeds to generalize that for a fairly wide family of types03/06 22:25
auguri see a bunch of stuff on tabulation, but i dont see how that connects up03/06 22:25
Saizanso, as i said, when you want a type that's isomorphic to some function space, you can use that03/06 22:26
Saizanaugur: well, look further03/06 22:26
Saizanor deeper03/06 22:26
augurwhat03/06 22:27
augurthis does not make any sense03/06 22:27
Saizanaugur: sorry, i seem to always fail to communicate with you, and i don't want to try harder atm03/06 22:27
auguri have no idea how functions-from-naturals-as-streams has anything to do with deriving the definition of a function from a property it must have..03/06 22:29
Saizanwhat if that property it must have happens to be "isomorphic to Nat -> A"?03/06 22:30
Saizanas your Map-theorem example is "isormorphic to Fin i -> .."?03/06 22:31
Saizanfor those special cases you can use what i linked.03/06 22:32
nappingThis stuff doesn't seem to be useful for "deriving the definition of a function from a property it must have"03/06 22:32
nappingWhat it does do, is let you show that the space of functions is isomorphic to a table form03/06 22:32
nappingIt sounds like that might actually be what you are trying to prove03/06 22:32
augurSaizan: its actually not about isomorphisms03/06 22:33
augur<-> isnt an isomorphism, its merely simultaneous-inhabitance03/06 22:33
Saizanyeah, you can derive that from an isomorphism03/06 22:33
nappingmore generally, it can help to prove things about functions on finite domains, if it's easy to check concrete examples03/06 22:34
augursure, but isomorphism is stricter03/06 22:34
Saizaneven infinite domains03/06 22:34
augur1 <-> N is easily satisfied03/06 22:34
augurbut theres no isomorphism03/06 22:34
Saizani know03/06 22:34
auguri just really dont see how this is relevant. ill read the paper tho03/06 22:35
nappingYou can't check properties on infinite domains by truth tables03/06 22:35
augurbut dont for a second thing ill feel like im getting anything out of it!03/06 22:35
augurthink**03/06 22:35
Saizannapping: he wants some technique to derive a type T by knowing it is logically equivalent to some other one03/06 22:37
Saizannapping: so, if that other one happens to be a function space the table is a candidate at least03/06 22:38
augurSaizan: well thats not what _i_ want but maybe its what hinze wants?03/06 22:40
Saizanaugur: then sorry, i completely failed to get the point of your agda code03/06 22:41
augurwell03/06 22:41
augurthe .. point was that we're asserting the existence of a function of some type, and that it satisfies a certain property03/06 22:41
augurthe question is to use that property to discover a possible definition03/06 22:41
augurin the mapR case, we're saying that a function with the properties of a map exists03/06 22:42
Saizanok, both your examples matched my description though03/06 22:42
augurand then we're using that property to whittle away at what the proof to see what the definition of map is.03/06 22:42
augurwe know its type already, thats not at issue03/06 22:42
augurwhat is at issue is its /value/03/06 22:43
Saizanit's value is a type though.03/06 22:43
Saizan*its03/06 22:43
auguronly because its easier to prove stuff using types03/06 22:43
augurits nicer to use propositions than truth values03/06 22:44
augurmapR f xs ys == true <-> ... would work just as well03/06 22:44
augurbut would probably be nastier to give an inhabitant for03/06 22:44
augurand mapR would ofcourse fail to be usable as a type-level predicate, too03/06 22:45
Saizananyhow, i don't mind if you don't read the paper :)03/06 22:46
augurim going to read it03/06 22:47
augurits just im not sure how the paper really relates properties to definitions03/06 22:48
augurat least, it doesnt _seem_ to be about that sort of thing, and doesnt _seem_ to discuss such an issue03/06 22:48
augurnot in any way that i can see03/06 22:48
augurbut its not a long paper so03/06 22:48
--- Day changed Sat Jun 04 2011
augurbweeeeeoo04/06 03:23
Saizanwhat is the topology of \bn ?04/06 18:06
augurcopumpkin: give me ideas04/06 20:10
copumpkinnope04/06 20:10
copumpkinat my gf's house, doing stuff :P just wanted to check something on the computer04/06 20:10
augurand now you're here to give me ideas! :|04/06 20:11
copumpkinnope04/06 20:12
augurlame :|04/06 20:12
auguroh man, only like04/06 20:12
augurwhat04/06 20:12
augurtwo months until hacphi04/06 20:12
--- Day changed Sun Jun 05 2011
augurbyorgey!05/06 04:17
sshcWhy can't Agda infer that "[]" can be List A here?05/06 21:11
sshcdata _⊆_ {A : Set} (a : List A) (b : List A) : Set where empty : [] ⊆ b05/06 21:11
sshcAgdaBasics.agda:697,3-1705/06 21:11
sshc[] != a of type List A05/06 21:11
sshcwhen checking the constructor empty in the declaration of _⊆_05/06 21:11
Saizanthe problem is that "a" and "[]" aren't the same list05/06 21:13
Saizandata _⊆_ {A : Set} : List A -> List A -> Set where empty : {b : _} -> [] ⊆ b -- this would work05/06 21:15
sshcSaizan: Same error05/06 21:27
sshc"  empty : {b : _} -> [] ⊆ b05/06 21:27
Saizanhave you changed the " : List A -> List A -> Set" part too?05/06 21:27
sshcOh.  "Unsolved metas"05/06 21:29
augursshc: what is []05/06 21:30
sshcdata List (A : Set) : Set where []   : List A _::_ : A -> List A -> List A05/06 21:31
auguraha ok05/06 21:34
augursorry i wasnt really paying attention :p05/06 21:34
sshcI think I'm going to give up and see how it is defined in the tutorial05/06 21:45
augursshc: what are you trying to define now05/06 21:45
sshcaugur: ≤05/06 21:46
sshcEr05/06 21:46
sshcSubset type05/06 21:46
augurah05/06 21:46
augurmm05/06 21:46
sshc_⊆05/06 21:46
augursubset for .. sets?05/06 21:46
sshcLists05/06 21:46
augurso sublist05/06 21:46
augursublist is going to be tricky no doubt05/06 21:46
augurbecause there are multiple ways for one list to be a sublist of another05/06 21:46
augurbut if what is intended is a contiguous sublist, thats easier05/06 21:47
sshcIt's not what is intended, but that's probably good practice before I do the real one05/06 21:47
* sshc tries05/06 21:47
sshcI'm not sure how to define "empty" even for that, though05/06 21:50
sshcdata _scl_ {A : Set} (a : List A) (b : List A) : Set where empty : [] scl b05/06 21:51
sshcAgdaBasics.agda:705,5-2105/06 21:51
sshc[] != a of type List A05/06 21:51
sshcwhen checking the constructor empty in the declaration of _scl_05/06 21:51
sshcWhat exactly does that error message mean?05/06 21:54
auguryou shouldnt put a and b as parameters to the datatype05/06 21:56
augurdata _scl_ {A : Set} : List A -> List A -> Set where empty : {b : List A} -> [] scl b05/06 21:57
--- Day changed Mon Jun 06 2011
auguris there a notion of equality that makes it possible to test the equality of objects by reference as well as structure06/06 02:35
augurso that two infinite objects can be compared?06/06 02:35
auguri mean, its hard to evaluate (haskell)  let ones = 1 : ones in ones == ones   without something like that06/06 02:36
Favoniadoes anyone have good references for K rule? I am wondering what it is and why it leads to inconsistency with homotopy types. (btw, the Agda option seems not to guarantee that K rule is disabled :( )06/06 16:45
nappingOh, you have an example?06/06 16:47
nappingIt's not a great reference, but there's file:///usr/local/share/doc/coq/html/stdlib/Coq.Logic.EqdepFacts.html06/06 16:48
nappingalso http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/06/06 16:48
djahandarienapping, I think you just linked to a file on your box :p06/06 16:48
nappingAh, so I did06/06 16:49
Favoniadjahandarie: I can find it anyway :p thanks, google!06/06 16:49
nappinghttp://coq.inria.fr/stdlib/Coq.Logic.EqdepFacts.html06/06 16:49
nappingThe second link I posted seems more likely to be informative06/06 16:50
djahandarieYeah, that's a good article06/06 16:50
Favonianapping: thanks :)06/06 16:52
nappingI think K holds on any simply connected types06/06 16:53
Favoniaabout my last question, is it guaranteed that the K rule is disabled in Agda by adding "--without-K" ? it says "disable the K rule (maybe)". hmm... "maybe"?06/06 16:54
nappingAh, I thought you were claiming you had a proof of K.06/06 16:54
nappingNo, nobody is entirely sure whether that makes it impossible to prove K06/06 16:54
nappingBut probably. I think Conor McBride's thesis on eliminating dependent pattern matching would be the place to start06/06 16:54
Favonianapping: so you're saying that, they adopt some other mechanism in hope to "prevent" K rules, right?06/06 16:55
nappingJust see if you can redo all the proofs for the subset of pattern matching allowed by --without-k, while only assuming J06/06 16:55
napping;)06/06 16:55
Favonianapping: so the "maybe" means that K might be still provable. did I understand your saying correctly?06/06 16:56
nappingMore like they ban the kinds of pattern matching which definitely require axiom K to translate into eliminators06/06 16:56
nappingSo the rest should be justifiable only in terms of J, but nobody has proven it06/06 16:56
napping"Might still be provable", yes06/06 16:57
Favonianapping: I see. Thanks. :)06/06 16:58
nappingTo be more specific, I don't think anyone has reason to believe that it is still provable, but no solid proof either way06/06 16:58
nappingAlso, if I read that article right, K is actually valid on any of the types you can define in Agda today06/06 16:58
xplataugur: equality by reference is meaningless in agda, and propositional equality is the minimal/most refined equivalence relation that can be reified as a type/proposition06/06 18:13
xplataugur: (proof: you can write subst and use it to inject proofs of propositional equality into any equivalence relation)06/06 18:15
xplator actually into any reflexive relation period06/06 18:15
augurO_O06/06 18:20
auguri didnt mean in agda06/06 18:22
xplatoh06/06 18:23
xplatwhat did you mean, then?06/06 18:23
augurjust more generallt06/06 18:23
xplatin order to have equality of reference, you need to have a domain where equality of reference makes sense06/06 18:24
xplatyou don't need equality of reference to prove things about equality of codata, though06/06 18:24
xplatthat's what bisimulation is for06/06 18:25
augurhmm06/06 18:25
augurxplat: have you see my mapR derivation code06/06 18:26
xplataugur: i have seen, but not looked.  or is it the other way around?06/06 18:27
augur:p06/06 18:27
nappingUsually the other way around06/06 18:45
augurwell xplat, i want as many opinions as possible!06/06 18:49
doliocopumpkin: BTW: I got Agda installed here.06/06 20:31
dolioThe font situation is still pretty abysmal, though.06/06 20:31
dolioThe fill-in-the-gap fonts listed on the wiki are pretty hideous.06/06 20:33
xplatthe fonts i have are ugly as sin, too06/06 20:33
xplatand i don't mean the fun kind of sin06/06 20:34
dolioUbuntu managed to cobble together a pretty decent collection of glyphs.06/06 20:34
dolioI can't say the same for windows.06/06 20:34
xplathm, i'm on ubuntu06/06 20:34
xplatbut i seem to get a bunch of symbols and things in handwriting fonts06/06 20:35
xplat\==, greek letters ...06/06 20:35
dolioWell, technically, I'm talking about kubuntu, but that probably doesn't matter much.06/06 20:35
xplati have no idea why, the console font doesn't get this fugly06/06 20:35
xplatthe glyph substitutions i see in a terminal are pretty sane06/06 20:35
copumpkindolio: oh, on your work computer?06/06 20:36
copumpkinah, looks like it :)06/06 20:36
dolioYeah.06/06 20:36
dolioIt wasn't actually as bad as I was expecting.06/06 20:36
copumpkindo you have the same emacs server issue on windows?06/06 20:36
dolioNo.06/06 20:37
dolioI couldn't figure out how to make cabal-install or darcs work, though.06/06 20:37
copumpkinah06/06 20:37
dolioSo I had to check it out on your laptop and e-mail myself a copy.06/06 20:37
xplati'm disappointed that no carrier pigeons feature in this story06/06 20:38
dolioGmail may use pigeons. You never know.06/06 20:38
copumpkindolio: I'm going to send you some stuff on a usb key via carrier pigeon06/06 20:38
copumpkinit might take a while to get there06/06 20:38
copumpkinnot sure how fast carrier pigeons are06/06 20:39
dolioIf they use pigeons for ranking pages....06/06 20:39
copumpkinoh yeah06/06 20:39
xplatdolio: it would explain a lot, wouldn't it?06/06 20:39
xplat(i'm a little bitter at google over a search i did this morning, although they usually still rank decently)06/06 20:40
dolioOh, also, was the place you went Pho Basil?06/06 20:41
xplat(it really gets old fast when you're clicking through shopping results trying to find maintenance information on your dead power brick while your laptop is running off a mostly-depleted battery ...06/06 20:42
xplat... and most of the results that aren't shopping are keyword-faking wannabe guru sites)06/06 20:43
xplatbtw the most common conclusion was that the brick isn't user-servicable and they cold-weld it shut, so i ended up buying a new one :(06/06 20:44
copumpkindolio: yep!06/06 20:47
xplatthat sounds delicious06/06 20:48
doliocopumpkin: All right. I tracked down the right one, then.06/06 20:49
dolioThere are a surprising number of places that serve pho in the area.06/06 20:50
dolioCompared to Cincinnati, at least.06/06 20:50
xplatindeed i was in boston myself last time i had pho06/06 20:50
xplatalthough that place has closed06/06 20:51
copumpkinoh no!06/06 20:52
xplatit was that 'pan-asian noodle' place right smack in the middle of everything, so probably not the most authentic pho in boston, but it was a cool restaurant concept06/06 20:53
xplatif it was asian and it was noodly and it wasn't an obscure specialty in its own homeland, they would try to approximate it for you :-706/06 20:55
copumpkinI want biang noodles06/06 20:56
copumpkinthey have the distinction of requiring the most strokes in the usual character for them06/06 20:56
copumpkinhttp://en.wikipedia.org/wiki/File:Bi%C3%A1ng_(regular_script).svg06/06 20:56
dolioWow. That's like a character that contains 6 other characters.06/06 20:58
copumpkinoh yes06/06 20:58
copumpkinif you want truly crazy06/06 20:58
copumpkinjapan invented a rather sketchy 84-stroke one06/06 20:59
copumpkinit's rather uninteresting though06/06 20:59
copumpkinhttp://en.wikipedia.org/wiki/File:Taito_2_l.png06/06 20:59
dolioSee, now that just looks lazy.06/06 21:00
copumpkinyeah06/06 21:00
xplattechnically i think that countains at least 10 other characters06/06 21:01
xplatbiang, that is06/06 21:01
copumpkinyeah, it's quite a few06/06 21:01
copumpkinI'm sure it'd be pretty easy to come up with a mnemonic for all of them06/06 21:01
copumpkinall the constituents are pretty common and easy06/06 21:01
copumpkinhorse, moon, sword, heart, word, at least06/06 21:02
xplatroad, heart, bird, moon, say, and 3 more uniques, if the meanings haven't drifted too much since kanji split off06/06 21:02
xplatoh, was it horse?  i always mix up horse and bird, they look similar to me06/06 21:03
copumpkin06/06 21:03
copumpkinthat's horse06/06 21:03
copumpkinbut yeah06/06 21:03
copumpkinit also has a ~six stuck on the top, I guess06/06 21:04
copumpkinalthough it isn't quite six06/06 21:04
xplatyeah, what is that anyway?06/06 21:04
xplatwhich one is sword?06/06 21:04
xplat(taito certainly seems a lot more compressible)06/06 21:06
xplat鳥馬-bird&horse06/06 21:07
copumpkinwell, it isn't so much sword06/06 21:08
copumpkinas a very "swordy" component that shows up in many choppy characters06/06 21:08
copumpkinthe two vertical bars06/06 21:08
copumpkin06/06 21:09
copumpkinthe thing on the right there06/06 21:09
xplatah06/06 21:14
xplatso two leaders next to a horse, below a word with two threads, flanked on the left by the moon and the right by a choppy bladey thing, all of which is standing on a heart with a hole above it, and the whole thing happens in the road06/06 21:17
xplati think my mnemonic generator overheated06/06 21:18
dolioThat description definitely makes me think of noodles.06/06 21:19
xplatThis noodle was a poor-man's meal in the countryside, but has recently become popular in trendy restaurants due to its weird character name.^[citation needed]06/06 21:20
augurcopumpkin06/06 21:36
auguryour intro to agda video was marred by errors, from what i could tell. i really wanted to watch it, really really, but i couldnt06/06 21:36
augur:(06/06 21:36
augurbut on the bright side, you're totally adorable06/06 21:37
copumpkinaugur: errors?06/06 21:43
auguryeah06/06 21:43
copumpkinthanks :P06/06 21:43
copumpkinbut what kind of errors?06/06 21:43
auguri'd have to go back and watch, but they were sloppy mistakes06/06 21:43
copumpkin:o06/06 21:44
augurlike your definition of the evenness function06/06 21:44
copumpkinwhat about it?06/06 21:44
copumpkinthe slides are up06/06 21:44
auguryou had one case defined as even (suc (suc n)) = even (suc (suc n)) and said it should terminate but agda cant tell this is true06/06 21:44
augurlink to slides!06/06 21:44
auguror no sorry06/06 21:45
augurit was halve not even06/06 21:45
copumpkinI didn't say it should terminate06/06 21:45
auguryou certainly did sir06/06 21:45
copumpkinI'm not sure why I would've said that06/06 21:45
augurneither am i!06/06 21:45
copumpkinthe whole point of that slide was that the termination checker can help you catch bugs06/06 21:45
augurill find you the video with a timestamp tho06/06 21:45
copumpkinI'll survive06/06 21:45
copumpkinhttp://dl.dropbox.com/u/361503/Agda%20and%20dependent%20types.pdf06/06 21:46
xplatyou mean you won't terminate?06/06 21:46
copumpkinnot for a while, I hope :)06/06 21:46
xplatpage 5 of your slides in evince is the slowest thing in the entire universe06/06 21:49
xplatnot counting web browsers and typechecking my agda modules06/06 21:49
xplatpage 6 too, i bet it's those red circles06/06 21:49
auguroh, no, copumpkin, i totally maligned you06/06 21:50
augurim sorry06/06 21:50
auguri misheard your doesnt as does.06/06 21:50
copumpkinI mean, I was pretty nervous, so I probably did make other mistakes :P06/06 21:50
augurthank god. copumpking [ sexiness ]+= 106/06 21:50
copumpkinlol06/06 21:51
xplati'm glad someone finally recognizes that an individual's knowledge of computer programs is determined by eir sexiness06/06 21:54
copumpkinxplat: I wonder why they're so slow06/06 21:54
copumpkinthey're find06/06 21:54
copumpkinthey're fine here, is what I meant06/06 21:54
xplathm, this page doesn't have circles and it's still slow06/06 21:54
copumpkin:o06/06 21:55
augurxplat: other way around06/06 21:55
auguralso, spivak pronouns06/06 21:55
augurplease tell me you're an orion's arm fan06/06 21:55
xplatyour "-- no sections" comment doesn't have a :( .  i am disappoint06/06 21:55
xplataugur: we've had this discussion before06/06 21:56
copumpkinspivak pronouns?06/06 21:56
augurxplat: have we06/06 21:56
augurlets have it again, it mustve been good06/06 21:56
copumpkinxplat: oh yeah, I am disappoint too, but I guess I forgot to put it on06/06 21:56
augurcopumpkin: http://en.wikipedia.org/wiki/Spivak_pronoun06/06 21:56
xplat'e, em, eir, eirs, eirself'06/06 21:56
copumpkinoh okay06/06 21:56
auguri like old school spival06/06 21:57
copumpkinI thought it was some reference to the speaker who came after me :)06/06 21:57
augurtho really all spivaks are nifty06/06 21:57
augur'eir' is a cool looking possessive pronoun :D06/06 21:57
augurSpivak wrote calculus on manifolds! :o06/06 21:58
augurthe very same spivak!06/06 21:58
xplati am more of an old-schooler myself06/06 21:59
augurxplat: be an orions armer06/06 21:59
augur:D06/06 21:59
xplati have enough arms already06/06 22:01
xplatwell, not true really, i lack a gripping hand06/06 22:01
xplat(or maybe i have two)06/06 22:02
augurorionsarm.com06/06 22:02
xplatwhat, there's an rpg?!06/06 22:03
xplatpost-singularity roleplaying sounds kind of hard06/06 22:03
augurwell, i imagine someones got an RPG going06/06 22:05
augurbut mostly its worldbuilding06/06 22:05
parcsis it just or me or does agda-mode have no syntax highlighting?06/06 22:42
Saizanload the file06/06 22:42
parcsah, i'll try that once agda has finished recompiling...06/06 22:44
dolioThe highlighting is more intelligent, but it calls out to the Agda implementation, so you don't get any color until you've type checked things, generally.06/06 22:53
dolioAnd once you've checked, the color will bleed into what you type until you next check.06/06 22:53
Eduard_MunteanuThat's a bit annoying.06/06 23:12
dolioThe bleeding, or the general situation?06/06 23:13
Eduard_MunteanuThe need to typecheck.06/06 23:13
dolioIt's conceivable you could do better.06/06 23:15
Eduard_MunteanuI also wonder if the scoping restrictions could be relaxed, so you could have some f defined after it's used like in Haskell.06/06 23:15
dolioThat I don't know.06/06 23:16
dolioIt can probably be made more lax.06/06 23:16
Eduard_Munteanu'mutual' seems to do something like that.06/06 23:16
dolioBut even in mutual blocks, types are checked in order of occurrence.06/06 23:17
dolioSo later definitions are not available in the types of earlier ones.06/06 23:17
Eduard_MunteanuOh.06/06 23:17
dolioAs I recall.06/06 23:18
Eduard_MunteanuI suppose it's got something to do with parsing rather than typechecking, no?06/06 23:18
dolioI don't think it has to do with parsing.06/06 23:18
dolioOf course, in induction-recursion, you use later definitions in the types of constructors earlier.06/06 23:19
dolioBut that's a slightly different case.06/06 23:19
doliofoo : ... bar ... ; foo = ... ; bar : ... ; bar = ...  won't work, as I recall.06/06 23:19
dolioEven in a mutual block.06/06 23:19
--- Day changed Tue Jun 07 2011
augurwhat is the response to Quine's critique of higher order logic as being not a logic due to the lack of a proof theory, in light of CoC etc.?07/06 05:06
augurand what refinements of the notion of impredicativity exist that admit of the good cases (ones = 1 : ones) but not the bad ones?07/06 05:23
dolioones = 1 : ones doesn't have anything to do with impredicativity.07/06 05:33
augurdolio: sure it does: ones is defined in terms of itself. thats an impredicative definition07/06 05:54
dolioThen recursive definitions are also "impredicative."07/06 06:07
augurthis is i think true!07/06 06:07
augurwell, with the exception of the fact that that sort of self reference can be factored out by the relevant combinators07/06 06:08
dolioThe combinators are all that exist.07/06 06:08
augurwhereas ones recursion afaik cant07/06 06:08
dolioNo.07/06 06:08
dolioones is defined by corecursion.07/06 06:08
augurright07/06 06:08
dolioSo what's the problem?07/06 06:09
augurones is still impredicative!07/06 06:09
dolioNope.07/06 06:10
augurno?07/06 06:10
augurbut it IS self referential07/06 06:13
dolioThe self-referential definition is sugar for a primitive corecursion combinator.07/06 06:15
augurahh07/06 06:16
augurwhats a corecursion combinator :o07/06 06:16
dolioIt's like a recursion combinator, only for corecursion.07/06 06:17
augur:P07/06 06:19
augurwhats an example of one, i should say07/06 06:19
doliounfoldr07/06 06:20
augurhmmmm07/06 06:31
xplatunfoldr is basically a paradigm example like foldr is for recursion07/06 06:32
xplatnot the most powerful scheme available, but the most basic and structural07/06 06:34
augurhmm07/06 06:36
augurok07/06 06:36
augurill be off. see you07/06 06:36
Eduard_Munteanucofix :P07/06 06:58
augurunfoldr : forall {X Y} -> (Y -> Maybe (X x Y)) -> Y -> List X, where (X x Y) is the functor for List ..07/06 07:09
augurhmm07/06 07:09
augurwell, Maybe (X x Y) rather07/06 07:10
augurhmm.. F X Y = 1 + X x Y; unfoldr : forall {X Y} -> (Y -> F X Y) -> Y -> List X07/06 07:10
augurbut List X = mu (F X)07/06 07:11
augurso unfoldr : forall {X Y} -> (Y -> F X Y) -> Y -> mu (F X)07/06 07:11
augurmore generally, i suppose, unfoldr : forall {Y} -> (Y -> F Y) -> Y -> mu F ??07/06 07:12
auguror less generally, i guess, but07/06 07:12
augurah right, this is looking familiar actually07/06 07:13
augurY -> F Y, thats a coalgebra07/06 07:13
auguri suppose it should be comu not mu07/06 07:14
mixiscan i have the case split put arguments in the positions indicated by the underscores instead of prefix style?07/06 12:15
xplataugur: comu is called nu07/06 12:32
xplatmixis: do you mean the automatic case split?07/06 12:35
mixisxplat: C-c C-c07/06 12:41
mixisalso, a way to generate the first line of the body with a goal on the rhs after having typed the signature would be neat07/06 12:49
xplatif you start with mixfix i think it will at least sometimes stay that way, but if it feels it has to insert an implicit argument it definitely won't07/06 12:49
mixisi had a 3 argument function with 2 underscores in the name and that got changed07/06 12:51
xplatit definitely isn't as smart as it could be07/06 12:52
mixiswell, then i'll be looking at Agda.Interactoin for a while07/06 12:54
xplati already actually have a whole wishlist for agda-mode (and agda in general) that i haven't got around to working on any of yet07/06 12:55
xplathttps://gist.github.com/97952407/06 12:58
xplatthey're really more like 'it seems like this should be doable' than having an actual plan :-707/06 12:59
mixisundo with reload: does that mean undo with automatic reload?07/06 13:13
mixiseh, undo withOUT reload in your list07/06 13:15
xplatmixis: undo that undoes the state changes (highlighting, filled goals, etc).  effectively the same as automatic reload, but hopefully it could be done faster if you don't go too far into the undo stack07/06 14:32
joe6just wanted to check on your experiences, I have an spi eeprom device that I am trying to program from my pic. I notice that the bytes written are being read back as 0xff, all the time. Anything simple that I could be missing?07/06 15:45
joe6oh, sorry. should not have posted this here07/06 15:56
joe6I meant to post it somewhere else..07/06 15:56
dolioThis is where I go for all my eeprom advice.07/06 15:56
xplatreally?  i just ask my bartender07/06 16:00
dolioYour garbage man might be better for that.07/06 16:01
augurroly poli dolio07/06 16:38
augurhmm07/06 18:55
auguri wonder if i could phrase these propositional types as relations...07/06 18:56
augurand then use AoP style manipulations07/06 18:56
augurdata Diag (X : Set) : X -> X -> Set : Set n where diag : (x : X) -> IsA X x x07/06 19:00
auguror something like that07/06 19:00
augurer, that should be Diag X x x obvviously x307/06 19:00
copumpkinhow is that different from refl and _\==_ ?07/06 19:01
copumpkinwith less implicitness07/06 19:02
augurcopumpkin: well, you're probably right!07/06 19:05
augurexcept that its supposed to be the relational type X07/06 19:05
augurthe content is the same but the intention is different07/06 19:06
auguranyway, thats just me dicking around trying to figure out the shape of things, nothing important07/06 19:06
augurbrb!07/06 19:06
augurhmm07/06 19:37
augurcan AoP relations be represented as actual relations07/06 19:41
augureg X <- Y = X -> Y -> Set07/06 19:41
augur?07/06 19:41
augurpr X x Y -> Set, whichever is preferable07/06 19:42
djahandarieNice, JS backend is UP!07/06 20:27
djahandarieTime to use Agda for my day job07/06 20:27
xplatcopumpkin: i've got a working example of the yellow menace that is one file, but it's 190 lines (wc -l)07/06 20:28
copumpkinoh wow07/06 20:29
copumpkinmay I see?07/06 20:29
xplathttp://hpaste.org/47565/inference_fail_v107/06 20:33
xplatit should be possible to cut it down further07/06 20:35
copumpkinI see07/06 20:40
xplatit's still pretty non-minimal07/06 20:44
copumpkinyeah07/06 20:44
xplati basically found the least annoying-looking yellow line from the pentagon proof and pulled all its dependencies into the file07/06 20:45
xplatthey've been simplified some, but not much07/06 20:45
copumpkinI'm guessing it must be something about being hidden in that module07/06 20:46
xplatyeah07/06 20:46
xplati got rid of the Category type and record by just breaking out the fields that are used as postulates07/06 20:46
xplata lot of stuff is brought in just for Product.⟨⟩∘ so if i postulate that i can probably kill like a third of the file07/06 20:50
xplatwell maybe a quarter07/06 20:50
xplatnew version has a 'good' version of badproof for comparison and the end of the old file is now at line 12407/06 21:12
copumpkincool07/06 21:14
augur!07/06 21:26
auguri've found a paper thats /even closer/ to what im looking for :O07/06 21:26
augurcopumpkin: Pointwise Relational Programming - de Moor and Gibbons07/06 21:31
augur:X07/06 21:31
augurhmm no it doesnt look like itll do what im looking for after all :(07/06 21:33
auguroh well07/06 21:34
xplatokay, now down to 59 lines07/06 21:34
xplatcopumpkin: http://hpaste.org/47571/inference_fail_v207/06 21:41
xplatit turned out to still fail without using actual equational reasoning07/06 21:42
copumpkinoh cool07/06 21:42
xplatso i could get rid of SetoidReasoning and Setoid and even IsEquivalence and the example got *much* smaller07/06 21:42
xplatcopumpkin: any suggestions before i post it to the mailing list?07/06 21:46
xplathem07/06 21:50
xplatif i take the (useless) implicit parameters off HomReasoningP then it works07/06 21:50
xplatbut they weren't useless originally!07/06 21:50
xplatFFFFFFFFFFUUUUUUUUUUU--!!07/06 21:52
sshcI'm wondering how I could match with a finite list on the type-level (in a data constructor, in this case)07/06 21:52
sshcdata _scl_ {A : Set} : List A -> List A -> Set where empty : {b : List A} -> [] scl b notLarger : … scl []07/06 21:53
xplatwhy would there be any constructors (other than empty) for ... scl []?07/06 21:54
xplatalso, it's easier to do subsequence than sub(consecutive)list07/06 21:57
xplatfor subsequence you could call your constructors 'skip', 'advance', and 'done'07/06 21:58
xplatthose names should help you figure out the types07/06 21:58
Saizanif you want to make a constructor for the case where the first argument of scl is a cons you do it like constr : (x : A) (xs : List A) -> ... -> (x :: xs) scl ..., if that was the question07/06 21:59
xplat(but don't feel slow if you need more hints too)07/06 22:00
sshc< xplat> also, it's easier to do subsequence than sub(consecutive)list — What's the difference betwen the two?07/06 22:01
xplatsshc: 1,3,5 is a subsequence of 1,2,3,4,5 but not a sublist of it07/06 22:02
xplatman, i wish i committed more versions of this file so i could bisect and figure out where i went wrong condensing this07/06 22:07
guerrill1is unification required for type inference even when the types of all terms can be inferred directly (e.g. using Church-style function abstraction and/or inj0 and inj1 annoated with the disjunction type)?07/06 22:13
xplathm, maybe the original problem is that the thing was being autogeneralized since the module took implicit parameters (instead of taking a record that took implicit parameters)07/06 22:15
xplatguerrill1: if your language provides enough type information or a simple enough type system that you don't have to do unification or constraint solving when inferring types, you are supposed to call it 'type propagation' instead07/06 22:18
Saizanin "bidirectional type checking" they still call it inference though07/06 22:19
Saizan(the part where you extract the type from the term)07/06 22:19
sshcfstElem   : {a : A} -> {as : List A} -> {b : A} -> {b : List A} -> {a \== b} -> {as scl bs} -> (a :: as) scl (b :: bs)07/06 22:23
sshc{a \== b} cannot appear by itself. It needs to be the argument to a07/06 22:23
sshcfunction expecting an implicit argument.07/06 22:23
sshcwhen scope checking {a \== b}07/06 22:23
sshc(These are subsequences, actually)07/06 22:23
xplatsshc: implicit arguments must have names07/06 22:24
xplatanyway, congrats, you now have an _isPrefixOf_ type named _scl_ :)07/06 22:25
Saizanbtw, you could do without a \== b by using just one variable07/06 22:28
guerrill1oops, sorry.. "< guerrill1> Saizan: i think that is what i'm doing. given a term and a type, i infer the type of the term and compare it to the given type."  "< guerrill1> by compare, i mean using an equivalence relation that i'm still not done writing..."07/06 22:28
SaizanfstElem   : {a : A} -> {as : List A} -> {bs : List A} -> {_ : as scl bs} -> (a :: as) scl (a :: bs)07/06 22:28
sshcOh.  Interesting :)07/06 22:29
xplatwhich one of those is easier kind of depends on what you're going to do with it07/06 22:30
xplatyour original version generalizes better to different equivalence relations07/06 22:30
Saizanbidirectional typechecking is specifically about splitting your terms' syntax into a part where you can deduce the type from and one where you've to push the type into to make sense of what you have, these two parts usually end up being mutually recursive07/06 22:31
guerrill1Saizan: ok thanks, reading up on it now...07/06 22:33
guerrill1Saizan: so, given ctx, M, τ, you can't just do (τ ≡ inferType ctx M) to verify that M : τ, thus moving most of the work into the theory and implentation of ≡?07/06 22:34
Saizanguerrill1: you can if your language is simple and/or annotated enough, otherwise it's pretty useful to make use of that τ during "inferType" (which wouldn't be named so), instead07/06 22:36
guerrill1it would seem that my method destroy sthe locality and clarity of where a type error occurs, but that could be moved into ≡ ,i think...07/06 22:37
guerrill1ok, i think my language is annotated enough. i designed it this way, since i wanted type checking to be as simple and clear as possible; plus, the core code is a translation from a higher-level language anyway...07/06 22:39
guerrill1i just keep seeing tons of references to unification and its making me feel like i was missing something07/06 22:39
Saizan≡ doesn't seem like it'd have any hope to give a sensible type error, since it doesn't look at the term at all07/06 22:42
Saizanand making τ available to inferType doesn't mean you'd use unification07/06 22:42
guerrill1indeed, that is true07/06 22:43
guerrill1at least you could say what doesnt match up to what when retuning on error from ≡07/06 22:43
Saizananyhow the most common use of unification is to fill in information that the user left implicit, but if your input is machine generated this is not relevant07/06 22:43
guerrill1ok cool07/06 22:43
Saizanthough e.g. typecheking even a fully annotated Agda program requires unification to handle pattern matching07/06 22:44
guerrill1ok, i don't have that issue, i went a different route regarding pattern matching07/06 22:45
guerrill1so unification is for a) filling in implicit/missing type information b) better error reporting and c) dependently type pattern matching (ML-TT or COC)07/06 22:46
guerrill1(regarding type checking only of course, obviously useful for resolution and other areas)07/06 22:46
Saizanthe b) was unrelated to unification07/06 22:47
guerrill1ok07/06 22:47
guerrill1Saizan: thanks. i have a bit more confidence that what i'm doing makes sense now.07/06 23:05
guerrill1xplat: you too07/06 23:05
augurhmm..07/06 23:10
augurinteresting07/06 23:11
augur(x : X) -> (g x) . r . (h x)   isnt a relation but theres a way to make it one07/06 23:13
augur\x -> (g x) . r . (h x)    rather07/06 23:13
augur\x y -> (g x) . r . (h y)   plus some identity constraint on x and y07/06 23:14
augurwell, i suppose what i intend is not g x but x g07/06 23:15
augur\x y -> (x g) . r . (h y)  == \x y -> x (g . y . h) y07/06 23:16
augurso, to get the identity constraint07/06 23:16
augur\x y -> x < id , g . r . h > y07/06 23:16
augur~ \x y -> x id y & x (g . r . h) y07/06 23:18
augurthats interesting07/06 23:18
copumpkinxplat: sorry, kind of busy. Don't wait for me but I'll take a look at it later07/06 23:26
augurhmm hmm07/06 23:44
augurok im off07/06 23:44
--- Day changed Wed Jun 08 2011
auguris there a reverse agdamode??08/06 01:01
augurer well08/06 01:01
augura reverse completions08/06 01:01
auguris there a way to simultaneously have a variable and know its value so that you retain the type, when the type is polymorphic?08/06 03:06
augursort of like @'s in haskell?08/06 03:08
augurf xs@(x : xs') = ... xs ...  ?08/06 03:08
auguri mean, obviously you can use x : xs' in this case08/06 03:08
augurbut say .. f xs@[] = ... [] ...08/06 03:08
augurthere you cant just use [] right08/06 03:08
augurbecause it lacks the type info, but you could use xs right08/06 03:09
augurhmm no nevermind, its not necessary08/06 03:11
djahandarieHm, it's probably not possible to represent a higher coinductive type in Agda right? Probably could with something OTT-based like Epigram 208/06 03:11
* djahandarie summons dolio for commentary08/06 03:16
Saizanhigher dimensional?08/06 03:22
dolioWhat's a higher coinductive type?08/06 03:24
djahandarieLike a higher inductive type.     data circle : Set where base : circle, loop : paths base base    or whatever. I'm not sure of an actual example of a higher coinductive type though. I don't see why they wouldn't conceptually exist in the HoTT framework though.08/06 03:27
sshc_[2,2,2] isn't considered a sublist of [2], right?08/06 03:28
dolioAgda doesn't even really have coinductive types.08/06 03:28
dolioAs the equality is too intensional.08/06 03:29
djahandarieRight, weak coinducutive types or something like that? I forget the name08/06 03:29
dolioI don't think it's so obvious what the dual of the higher inductive types would be, either.08/06 03:36
dolioHigher inductive types are about adding identities between constructors and identities on the relevant type....08/06 03:37
dolioBut there are no constructors for coinductive types.08/06 03:37
guerrill4djahandarie: where'd you get that example? what is "paths" in it?08/06 03:37
djahandarieHmm08/06 03:38
doliopaths is the identity type.08/06 03:38
dolioSo, higher coinductive types are defined by deconstructors plus... additional elements of the identity type?08/06 03:39
djahandarieguerrill4,   data paths {A : Set} (x : A) : A -> Set where refl : paths x x    -- or something liek that08/06 03:39
djahandarieI've only see the coq definition of this stuff, kind of just hoping these are the correct Agda definitions :p08/06 03:39
dolioYeah, those are correct.08/06 03:40
dolioI seem to recall that the homotopy blog suggested that you can actually encode higher inductive types by their eliminator, as usual.08/06 03:43
dolioIf you don't care about the strong elimination principle, probably.08/06 03:43
dolioWhich would suggest it might be good to think about hat a higher coinductive introduction would be.08/06 03:44
dolioWhat, even. Not hat.08/06 03:44
sshcdata _sl_ {A : Set} : List A -> List A -> Set where empty : {b : List A} -> [] sl b _is-a-sublist-of_ : {a : A} -> {as : List A} -> {b : A} -> {bs : List A} -> (f : (A -> A -> Bool)) -> {_ : elemBy f a (b :: bs) \== true} -> {_ : as sl bs} -> (a :: as) sl (b :: bs)08/06 03:45
sshcWhat's wrong with the type of "example" here?08/06 03:45
sshcexample : (List Nat) sl (List Nat)08/06 03:45
sshcexample = (zero :: []) is-a-sublist-of (zero :: zero :: [])08/06 03:45
sshcSet !=< List _948 of type Set₁08/06 03:46
sshcwhen checking that the expression List Nat has type List _94808/06 03:46
guerrill4djahandarie: ok.08/06 03:55
Favoniasshc: I guess you can say "[] sl []", not "(List Nat) sl (List Nat)"08/06 04:12
sshcFavonia: Huh?08/06 04:12
sshc"example : [] sl []"08/06 04:12
sshcthe constructor _::_ does not construct an element of Bool08/06 04:13
sshcwhen checking that the expression zero :: [] has type08/06 04:13
sshcThey're not empty lists, also08/06 04:14
Favoniahmm what is f?08/06 04:15
Favoniai am confused because you have only one explicit argument in the signature of _is-a-sublist-of_08/06 04:16
Favoniafor set1, the problem is that "List Nat" is of type "Set", and a particular nat list is of type "List Nat"08/06 04:18
sshcOh08/06 04:21
sshcelemBy : {A : Set} -> (A -> A -> Bool) -> A -> List A -> Bool08/06 04:21
sshcelemBy _    _ [] = false08/06 04:21
sshcelemBy _==_ a (x :: xs) with a == x08/06 04:21
sshc... | true  = true08/06 04:21
sshc... | false = elemBy _==_ a xs08/06 04:21
FavoniaAgda is predicative by default and Set1 is the next universe with higher level. If sl is really well-typed in "(List Nat) sl (List Nat)" then sl has type "Set -> Set -> X", where X is at least Set1.08/06 04:23
Favoniasshc: the problem is that, f is an explicit argument in _is-a-sublist-of_, but in the proof of "example" "f" is not offered.08/06 04:24
FavoniaI think the signature/type of _is-a-sublist-of_ is probabily not what you want. also I guess Agda is not smart enough to automatically do the induction (like {_ : as sl bs}) for you.08/06 04:32
sshcOh!08/06 04:33
sshcYes, the definition of "example" clearly doesn't match with the type of is-a-sublist-of (which only has one explicit argument)08/06 04:34
sshcexample : (zero :: []) sl (zero :: zero :: [])08/06 04:35
sshcexample = sublist _nat==_08/06 04:35
sshcUnsolved metas at the following locations: AgdaBasics.agda:738,11-2608/06 04:35
Favoniaseems that Agda is unable to do the whole induction for you :O08/06 04:36
Favoniasshc: sorry that I can't run agda now. personally I would suggest something like _≤_ in the stdlib: data _≤_ : Rel ℕ zero where z≤n : ∀ {n} → zero  ≤ n  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n08/06 04:40
sshcexample : (zero :: []) sl (zero :: zero :: [])08/06 04:41
sshcexample = sublist {a = zero} {as = []} {b = zero} {bs = zero :: []} _nat==_08/06 04:41
Favoniasshc: you can see that the whole data structure is actually induction steps. also all the important arguments are explicit08/06 04:41
sshc^ That's still not explicit enough, apparently08/06 04:42
xplatyay, now a fresh agda rechecks the pentagon law for cartesian products in 681m peak08/06 15:01
djahandarie:o08/06 15:01
xplatremoving unnecessary imports turned out helpful08/06 15:02
djahandarieSo hexagon laws and such for braided categories are probably possible?08/06 15:04
djahandarieMaybe I should try it out08/06 15:05
xplatyeah, they probably are possible08/06 15:05
xplatwith a little work08/06 15:05
xplatcopumpkin: i fixed the problems with equational flair, it turned out the functions were being automatically generalized with extra unused implicits and that was the source of the problems08/06 15:12
xplatended up having nothing to do with abstraction or scope at all08/06 15:13
copumpkinoh good08/06 15:14
copumpkinis it a bug then?08/06 15:15
xplatalso it turns out you could probably replace Category.Category.Equiv with ‘module Equiv {A B : Obj} where { open IsEquivalence (equiv {A} {B}) public }08/06 15:16
xplatit was my bug, assuming modules with their own trailing implicit arguments would freeze like modules whose explicit arguments have implicit arguments do08/06 15:17
dpiponiDo the standard libraries contain the proof that ℤ forms a ring?08/06 16:26
dolioI don't see it. Integers look under-developed.08/06 16:33
guerrill4no number theorists using agda? :\08/06 16:36
dolioThere's a bunch of stuff about the naturals.08/06 16:36
dolioWho cares about those negative numbers. They're pretty much imaginary. :)08/06 16:36
xplatcopumpkin: Everything.agda won't build for me because it refers to a nonexistent Category.Presheaves08/06 16:43
copumpkinwhoops08/06 16:43
copumpkinmust've forgotten to add that08/06 16:43
djahandarieThere is a Category.Presheaf08/06 16:44
xplatEverything refers to both08/06 16:44
guerrill4so unification is also what makes agda's implicit arguments work?08/06 16:46
copumpkinxplat: just remove the import... I never finished that module anyway08/06 16:47
xplati just pushed anyhow, it built most of the modules fine and i was pretty sure i rebuilt everything i touched08/06 16:49
xplatand the number of modules that did rebuild makes me pretty sure i didn't break any dependent modules with any of the changes08/06 16:50
xplatonce everything is merged i should be able to start porting to the stdlib08/06 16:51
djahandarieYour porting it to the stdlib?08/06 16:51
djahandarieYou're*08/06 16:51
xplatyes, that is the plan.08/06 16:52
xplati'm thinking everything should just go under a single root directory, my favorite at the moment is CTL, followed by CT and Category.Theory08/06 16:52
xplater, CT, Categories, and Category.Theory08/06 16:53
xplatthe stdlib's Category should really be renamed to something like Control or Notion or Idiom, but there's no use waiting on that08/06 16:54
copumpkinyeah08/06 16:54
copumpkinI wouldn't mind any of those, but Categories seems nicest08/06 16:54
copumpkinit'd also stop us from having to open Category.Category all the time08/06 16:54
copumpkinwhich was annoying as hell08/06 16:54
copumpkindpiponi: there are binary naturals mod (2^n) (i.e., machine words) in a module I made with someone08/06 16:55
copumpkinthey have lots of algebraic structures on them :P08/06 16:55
copumpkinas in all the proofs08/06 16:55
xplati guess Categories does have that advantage, since Category.agda could become Categories.agda instead of <root>/Category.agda like in the other proposals08/06 16:56
dpiponicopumpkin: The standard libraries define Z and rings so I thought they'd already have an IsRing record for Z.08/06 16:59
xplatprobably different people added those08/06 16:59
xplatalthough you would think whoever added rings would pay attention to Z anyway since it's the initial ring08/06 17:00
dpiponiI thought I'd reproduce the first induction proof I learnt at school: http://en.wikipedia.org/wiki/Mathematical_induction#Example08/06 17:00
copumpkinoh I remember doing that08/06 17:01
copumpkinit was a lot harder to do in agda than it was in high school :P08/06 17:01
dpiponiNo doubt about that!08/06 17:01
copumpkinoh wait, it wasn't that one08/06 17:01
copumpkinit was the sum of odds is a square08/06 17:01
copumpkin seems pretty similar though08/06 17:01
dpiponiShould be about the same level of difficulty anyway.08/06 17:02
dolioCan't you do that with the natural numbers?08/06 17:02
copumpkinxplat: nah, I think it's all NAD08/06 17:02
dolioIn fact, that's what that proof is for.08/06 17:02
dpiponidolio: Maybe, but there is a substraction.08/06 17:02
copumpkinyeah, I did mine over the naturals08/06 17:02
xplatthe subtraction is trivial there, it can just be rephrased as addition08/06 17:03
dpiponixplat: Yes, but I don't want to do that, especially because I might generalise.08/06 17:04
xplatalso, induction doesn't work on Z08/06 17:04
xplatat least not plain induction08/06 17:04
copumpkincan't you have two inductive cases?08/06 17:04
dpiponixplat: I was playing with summing functions N → Z so induction is fine08/06 17:04
dpiponiAnd I was hoping to eventually get into the RingSolver thingy to make things easier for more complex cases.08/06 17:05
xplatyou can do bidirectional induction with a single base case, or bounded induction08/06 17:05
xplatbut in agda you must first prove those work :)08/06 17:06
* copumpkin pulls out the postulate block08/06 17:06
xplat08/06 17:07
dpiponixplat: Now that's a character I don't use enough in my Agda. I should use ð too.08/06 17:08
xplatðe hell you say!  :)08/06 17:09
copumpkinuse Ϝ08/06 17:15
copumpkinor ϝ08/06 17:16
copumpkinϟ or ϡ08/06 17:17
dpiponiI thought it'd be fun to use "invisible times" but no application seems to handle it correctly: http://www.fileformat.info/info/unicode/char/2062/index.htm08/06 17:18
copumpkinoh nice08/06 17:20
dolioIs bidirectional induction not what you get from the particular encoding of Z?08/06 17:25
dolioI guess it's probably not quite.08/06 17:25
xplatdolio: you need two base cases (0 and -1) and on the other hand the two proofs can make use of the sign of the number08/06 17:34
xplati'm still looking for a good excuse to use the snowman operator08/06 17:36
nappingIs there any way to prove equality is decidable with less than a quadratic number of cases in the constructors?08/06 18:48
nappingI think I recall something about converting to nat codes?08/06 18:48
xplatnapping: converting to Fin codes works better08/06 18:55
nappingyeah, it seems to work reasonably well for nullary constructors08/06 18:55
nappingis there a nice way to prove something holds for every value in a fixed Fin k?08/06 18:56
dolioYou could construct a universe of finite types, and write a generic procedure for provably deciding equality of finite types.08/06 18:56
xplatif you have constructors with arity your best bet is encoding with Eithers08/06 18:56
nappingI was thinking of a dependent sum of a fin tag and payload08/06 18:56
nappingbut a more basic question is just how to prove (f : Fin 8) -> f ≡ test-to-fin (fin-to-test f)08/06 18:57
nappingwithout writing cases like iso2 (suc (suc (suc (suc (suc (suc (suc zero))))))) = refl08/06 18:57
nappinghmm, I guess I can't really compute anything much nicer than that08/06 18:57
xplathm, does iso2 (# 7) = refl work?08/06 18:58
nappingno, and I would be surprised if it did08/06 18:58
xplatwith nullary constructors i'd have suggested proving it in the other direction, though08/06 18:58
xplatnapping: i would have been slightly surprised, but not extremely08/06 18:59
nappingwell, the cases for the other side (t : Test) → t ≡ fin-to-test (test-to-fin t) are at least flst08/06 18:59
nappingflat - like iso1 F = refl08/06 18:59
nappingI guess I might only need the one direction to get the proof to go through08/06 18:59
xplathm, come to think of it i'm not sure if you need just one direction or both08/06 19:00
napping t ≡ fin-to-test (test-to-fin t) should be enough, if I could rewrite it in Dec (a ≡ b)08/06 19:01
xplatif you need both, it might be easier to express one of the functions as a Vec08/06 19:01
nappingyeah, that's what I did for the conversion from fin08/06 19:01
Saizanhttp://code.haskell.org/~Saizan/Eq.agda <- one direction is enough08/06 19:26
nappingCan you prove y ≡ y' from (i' , y) ≡ (i' , y') ?08/06 19:45
Saizancong snd08/06 19:46
nappingthe pairs are dependent08/06 19:46
nappingand cong proj₂ does not work08/06 19:46
Saizanfirst pattern match on cong fst08/06 19:46
Saizanso, what you can prove is  y ≡ subst .. .. y'08/06 19:48
nappingwhat do you mean, pattern match on cong fst?08/06 19:50
copumpkinon i'?08/06 19:51
copumpkinwith block of cong fst and match on refl?08/06 19:51
nappingoh, to make the type of the second part reduce08/06 19:51
Saizancong fst of the equality, to make the first projections equal in the context08/06 20:03
nappingI don't see how to do that08/06 20:17
nappingcong proj\_2 of the equality isn't well typed, so you can't state it ahead of time08/06 20:17
copumpkinuse cong on heterogeneous equality?08/06 20:19
copumpkinand then bring that back to homogeneous08/06 20:20
nappingthat should work08/06 20:20
nappingIs there a nice way to prove {k : ℕ} → Decidable (_≡_{A = Fin k})?08/06 20:23
Saizanfoo : ∀ {A : Set}{B : A -> Set} -> (a b : Σ A B) -> a ≡ b -> A08/06 20:25
Saizanfoo (i , y) (i' , y') eq with cong proj₁ eq08/06 20:25
Saizanfoo (i , y) (.i , .y) refl | refl = { }108/06 20:25
Saizanalso works08/06 20:26
Saizannapping: there's one in the stdlib08/06 20:26
nappingcopumpkin: that worked nicely08/06 20:26
SaizanData.Fin.Props._≟_08/06 20:27
copumpkinthe .Props vs. .Properties has bothered me for a while :P08/06 20:28
augurheyo08/06 20:29
nappinghow it that foo supposed to be used?08/06 20:29
nappingActually, that will work fine.08/06 20:29
copumpkinI think he was just illustrating the idea of matching on cong proj108/06 20:30
nappingThat won't do to prove the projections equal in a visible way, but I just need to feed the equality to a ≢ proof08/06 20:30
nappingwell, ≅ is working great08/06 20:30
nappingIs there a nice way to define records containing functions that need to do pattern matching08/06 20:34
nappingsomething like a module?08/06 20:34
nappingor even record puns08/06 20:35
xplatnapping: the best right now is record { foo = foo ; bar = bar } where { foo x = blah; bar y = woof }08/06 20:35
xplat(sadly)08/06 20:36
xplata proper record block is on my agda wishlist08/06 20:36
nappinga where clause doesn't introduce the local definitions of your record either08/06 20:39
dolioThey're discussing ways to have pattern matching lambdas on the mailing list.08/06 20:39
nappingthat would help too.08/06 20:39
nappingSeeing the = and ;, I hoped you could write patterns directly in a record block08/06 20:39
nappingThere, finished: http://hpaste.org/47596/deciding_equality08/06 20:47
xplatcool08/06 20:48
nappingNow I should get back to the Coq proof where it wants eq_dec on a type with 14 constructors. 196 cases the naive way, before you even start comparing arguments08/06 20:50
nappingmaybe best to leave it an Axiom08/06 20:50
nappingI guess that suggests the question of whether the proof can go through without K08/06 20:51
nappingI'm guessing no, for this version with arguments.08/06 20:51
xplatyou don't need K in general, but you probably need some cases of K08/06 20:52
xplat(which ones depending on your type)08/06 20:52
xplatnot sure if they would be directly provable cases or not though08/06 20:53
xplati'm still a little uncertain on how much J buys you08/06 20:53
dolioWhere is K being used there?08/06 20:54
nappingconverting heterogeneous to homogenous equality, maybe some of the pattern matching08/06 20:55
dolioOh.08/06 20:55
nappingbeing able to project like that from a dependent equality is one of the things listed in EqdepFacts08/06 20:56
dolioThis is for equality on finite sets?08/06 20:56
nappingFor types with arguments08/06 20:57
nappingI might be able to make it go through by using more custom types rather than trying to reuse Vec and Fin and Σ08/06 20:57
xplattechnically you could make info-dec a Vec too, couldn't you?08/06 20:59
nappingit would need to be a more dependent kind of Vec08/06 21:00
xplatoh, Vec isn't dependent enough?  :(08/06 21:00
napping"A" doesn't vary by index08/06 21:00
xplatyou need HVec!  :)08/06 21:00
copumpkinI've wondered how to write HVec without writing a non-heterogeneous one before08/06 21:01
copumpkinyou can index it by a list of Set08/06 21:01
copumpkinbut that feels ugly08/06 21:02
xplator maybe you could make info : \Sigma Set (\ T -> Decidable (_\==_ { A = T }))08/06 21:02
copumpkinxplat: how would you use that?08/06 21:02
nappingwell, "info" is the one describing the arguments to the constructor with a given code, but I don't see how that would work for info-dec08/06 21:03
nappingPerhaps you mean (T : Set) -> Decidable (_\==_{A = T})?08/06 21:04
nappingthat would certainly be strong enough :)08/06 21:04
copumpkinlol08/06 21:04
xplatyou make code = \Sigma (Fin 2) (\ i -> proj\_1 (lookup i info)) and then you use them together08/06 21:04
copumpkinyou can derive LEM from that can't you?08/06 21:04
nappingsomething like that.08/06 21:04
nappingWell, yes you can.08/06 21:04
copumpkinin fact, it's almost exactly LEM08/06 21:04
xplater, info should be a Vec of the type i gave before08/06 21:04
nappingbut there have been things before that made Agda anti-classical08/06 21:05
xplatwell, i folded info-dec into info and the same technique would work on unrep, but napping already left08/06 21:29
xplatis there some kind of way to have implicit fields in a record?08/06 21:32
xplatspecifically, one with constructor08/06 21:32
Saizantry putting the field name in {..}08/06 21:33
xplatSaizan: thanks08/06 21:51
xplatwhat causes errors like this?08/06 21:51
xplatCannot instantiate the metavariable _115 to A since it contains the08/06 21:51
xplatvariable A which _115 cannot depend on08/06 21:51
xplatwhen checking that the expression info has type Vec Coder k08/06 21:51
augurxplat: sounds like circularity08/06 21:53
xplatnever mind, found it08/06 21:53
xplataugur: no, i left off a type parameter from a function when another type implicitly depended on that parameter08/06 21:53
augurahh!08/06 21:56
xplat@tell napping annotated your paste with http://hpaste.org/47598/same_great_decidability_less which illustrates what i was talking about ...08/06 22:02
lambdabotConsider it noted.08/06 22:02
sshcdata _bsl_ {A : Set} : List A -> List A -> Set where stop : [] bsl [] drop : forall {xs y ys} -> xs bsl ys -> xs        bsl (y :: ys) keep : forall {x xs ys} -> xs bsl ys -> (x :: xs) bsl (x :: ys)08/06 22:04
sshc^ Isn't this really subsequence?08/06 22:04
xplatyes08/06 22:05
sshcOkay.  Thanks.08/06 22:13
xplati guess the ultimate form of HVec would be a snoc-vector where the type of each last was dependent on its corresponding init08/06 22:16
xplatwell, it could be a cons vector too, but that wouldn't be very intuitive08/06 22:18
Saizanusually called a "telescope"08/06 22:18
xplatyeah, can you write a real telescope type in agda?08/06 22:18
xplathm, maybe a cons with l-r dependencies would be doable, but you would definitely have to resolve them before you entered the tail08/06 22:19
xplati find myself honestly unsure which direction would be less annoying :)08/06 22:20
xplati just started thinking about this because if you don't want to hand-uncurry constructors in the semi-automatic equality code you need telescop-y stuff08/06 22:22
xplat(even with that i'm not sure it's possible to write something easier to use than hand-uncurrying when you have a highly dependent constructor)08/06 22:23
Saizanhttp://hpaste.org/47599/telescope <- from the outrageous coincidences paper, using Agda's Set as the base universe though08/06 22:25
Saizanhah, forgot to make Cx : Set108/06 22:26
xplatwhich paper is that?08/06 22:26
Saizanhttp://personal.cis.strath.ac.uk/~conor/pub/DepRep/DepRep.pdf08/06 22:26
xplatthanks!08/06 22:28
--- Day changed Thu Jun 09 2011
augurare there any data types that represent graphs inherently, as opposed to just by way of, say, an edge list or adjacency matrix?09/06 01:06
auguri mean, like, a data type where the constructors are node constructors, for instance09/06 01:07
xplatwhat do you mean by 'inherently?'09/06 01:07
augurwell, a tree could in principle be represented as a pair list or adjacency matrix or some nonsense like that, right09/06 01:07
xplator 'node constructors'?09/06 01:07
augurbut the algebraic tree types are not that09/06 01:07
augurthey just directly represent tree structure09/06 01:07
auguris there an analogy for graphs? of any sort?09/06 01:08
xplatwell in principle you could have a datatype of rational trees09/06 01:08
augurrational trees huh09/06 01:09
xplata rational tree is basically a pointed finite digraph where there's a path from the basepoint to anywhere09/06 01:09
augurhmm09/06 01:09
augurhow about trees where some nodes can be "sewn together"?09/06 01:11
xplatthat's basically what a rational tree is09/06 01:11
auguraha! ok09/06 01:11
augurany pointers? google seems to have a high noise ratio for this term09/06 01:12
xplatYAML is able to serialize rational trees09/06 01:12
xplatit's not a common term, but i don't think there's a commoner alternative09/06 01:13
augurhm09/06 01:13
xplati first heard of them in connection with logic programming09/06 01:13
augurand whats the data structure for them, do you know?09/06 01:13
xplatif i google 'rational tree' (no quotes in the search term) i find several relevant papers on the first page09/06 01:14
augurhm09/06 01:15
augurok09/06 01:15
xplatin memory a rational tree is usually represented exactly the same way as a regular tree except there are no restrictions on which nodes can point to which09/06 01:16
xplatthey are a little different from true graphs though since nodes don't have identity09/06 01:17
augurxplat: sure, except in an algebraic data type thats harder to explain09/06 01:18
augursince theres no way to really say "this node and that node are actually the same"09/06 01:18
augurthey might be equal but distinct09/06 01:18
augurBranch 2 (Leaf 1) (Leaf 1)09/06 01:18
xplatso any two rational trees that have the same set of valid paths and the same sequence of labels on each path are equal09/06 01:19
auguris there one leaf or two?09/06 01:19
augurhm09/06 01:19
augurthat cant be all there is to it tho09/06 01:19
auguris it?09/06 01:19
augurhm09/06 01:19
xplatwell, you can create a form with identity too, but the basic form has that property09/06 01:19
augurright, but _all_ trees are rational trees then09/06 01:19
augurand all rational trees are normal trees09/06 01:19
augurat least in an ADT09/06 01:20
xplatno, because if you unfold a rational tree with a cycle you would get an infinite tree09/06 01:20
augurahh ok i see09/06 01:20
auguri was thinking more where you can sew nodes together as long as you dont create cycles09/06 01:20
auguri didnt think of the cyclic case09/06 01:20
augurhm09/06 01:20
xplatand if you add node identity to rational trees even the acyclic case gives you something different from normal trees09/06 01:22
xplatyou would normally do this in, e.g., the case of mutable rational trees09/06 01:23
augurhmm09/06 01:23
augursure ok09/06 01:23
augurim just looking for a data structure that represents this sort of thing in a natural way09/06 01:23
xplatbesides a pointer structure, you can also represent a rational tree as a bag of equations09/06 01:24
xplater, set of equations09/06 01:24
xplata simple example: {a = true :: b ; b = true :: a}09/06 01:25
xplater, b was supposed to be false :: a09/06 01:25
augurright, so basically the pair list thing09/06 01:25
xplatotherwise it may as well be {a = true :: a}09/06 01:26
augurhmm09/06 01:26
auguraha, hows this for a representation of (acyclic?) rational trees09/06 01:26
augur(t : Tree) x List ((i : Index t) x (j : Index t) x (i == j))09/06 01:27
augurer sorry09/06 01:28
augur(t : Tree) x List ((i : Index t) x (j : Index t) x (lookup i t  == lookup j t))09/06 01:28
augura tree and a list of triples -- two paths and a proof that the two paths point to the same thing in the tree09/06 01:28
auguris this inductive tho .. hmm09/06 01:29
xplatwell, that seems like a workable (if sometimes potentially exponentially oversized) inductive-ish definition of rooted DAGs09/06 01:32
augurhmm09/06 01:32
augurexponentially oversized?09/06 01:32
xplat(otoh although it can sometimes be exponentially oversized, it can also sometimes be exponentially undersized compared to, say, an adjacency list)09/06 01:32
augurhm.09/06 01:33
augurwell, ill just stick with implementation neutral algebraic approaches for now09/06 01:34
augurusing structured Set's09/06 01:34
xplataugur: if the graph has a lot more paths than nodes (say it's a 'snake' made of diamonds, or a 'ladder' made from 2 lists) then depending how it's computed it can have exponentially more real nodes than an adjacency list representation09/06 01:34
auguroh, but theres no reason why the list has to have ALL the paths to the objects in question09/06 01:35
augurah well i guess it would tho wouldnt it09/06 01:35
augurto ensure that things arent mistakenly disidentified09/06 01:35
augurhmm09/06 01:35
xplataugur: it wouldn't necessarily, but it could, and it could also have exponentially many copies of nodes far from the root09/06 01:35
augurhmm hmm09/06 01:36
xplatotoh, if you have a big graph with lots of nodes and lots of isomorphic subgraphs, you can represent it with logarithmically many in-memory nodes if you compute it carefully09/06 01:36
xplatso it's not always huge compared to standard reps, it just has very different, and somewhat fussy, performance characteristics09/06 01:37
xplatyou can help it perform better by judicious use of memoizing and never recording equations between paths that already have a nontrivial equation between prefixes09/06 01:41
xplatlike, never equate {abcd} and {efgh} if you already equated {ab} and {ef}09/06 01:42
xplatyou actually should probably be even more particular like that about managing the equations, but that's a start and it expresses the general idea09/06 01:43
augurok.09/06 01:50
augurits not that big a deal09/06 01:50
augurits not really something i need, just something i was curious about09/06 01:51
augurP09/06 01:51
augur:P09/06 01:51
augurso why cant i have multiple lambdas in a syntax definition?09/06 12:47
auguralso, why does   syntax Σ A (λ x → B) = x ∶ A ∣ B   give me the error   syntax Σ A (λ x → B) = x ∶ A ∣ B09/06 12:59
augurer..09/06 12:59
augurdamnit aquamacs :|09/06 12:59
augurNames out of scope in fixity declarations: Σ09/06 12:59
xplat'syntax' is considered a fixity declaration for the purpose of that message.  try putting the syntax declaration closer to the definition of \Sigma.  or outside the record definition, if \Sigma is declared as a record constructor.09/06 15:46
xplataugur: ^09/06 15:52
dpiponiI want to use Relation.Binary.EqReasoning to reason about equalities in ℕ. What's the correct way to open it? I can't see what the appropriate setoid should be called.09/06 16:24
dpiponiAh, got it. open Relation.Binary.EqReasoning (setoid ℕ)09/06 16:26
copumpkinI think the Nat module already has a module you can open for that in it09/06 16:26
copumpkinmaybe I'm misremembering though09/06 16:26
Saizansomewhere there's a \==-Reasoning that works for \== in general09/06 16:27
copumpkinyeah, I guess I'm wrong09/06 16:27
dpiponiI found an example on the web using Data.Nat.setoid but it didn't seem to exist. setoid ℕ is fine though.09/06 16:28
copumpkinoh, the module I was thinking of was the order-based reasonining on Nat09/06 16:28
copumpkinreasoning09/06 16:28
Saizanah, in Relation.Binary.PropositionalEquality09/06 16:28
copumpkinmodule ≤-Reasoning where09/06 16:28
xplatsetoid \bn?  how is that supposed to even work?09/06 16:34
xplatyou can't pattern-match on Set·s ...09/06 16:35
copumpkinyou don't need to09/06 16:36
xplatoh, maybe it's Relation.Binary.PropositionalEquality's \bn?09/06 16:36
copumpkinsetoid : ∀ {a} → Set a → Setoid _ _09/06 16:36
xplater, setoid?09/06 16:36
copumpkinyep09/06 16:36
xplatbut \==-Reasoning seems better if you already know you're using \==09/06 16:37
copumpkinyeah09/06 16:37
doliocopumpkin: Do you have slides from your Agda talk?09/06 20:30
copumpkinyep09/06 20:32
copumpkinhttp://dl.dropbox.com/u/361503/Agda%20and%20dependent%20types.pdf09/06 20:32
copumpkinthere's also the underlying keynote file if you prefer09/06 20:32
dolioNah, I just wanted to look at what you talked about.09/06 20:42
dolioI still don't know what to talk about tomorrow.09/06 20:42
djahandarieWhat are you doing tomorrow that involves you talking?09/06 20:44
dolioWe have a weekly FP/category theory/math stuff meeting at work.09/06 20:45
dolioSo I've been covering type theory stuff.09/06 20:45
dolioStarting with propositional calculus and natural deduction, then simple types, then dependent types.09/06 20:45
dolioSo tomorrow the plan was to show some Agda, for a real language with dependent types.09/06 20:45
djahandarieWhy can't I work at a good job? :(09/06 20:46
dolioYou could.09/06 20:46
copumpkinI tried to get you set up with an internship, but no, you were like "I'm too good for this"09/06 20:47
dolioThey just sent out a PDF with intern pictures today.09/06 20:47
djahandarieYes, I need to hone my skills at this PHP chopshop instead.09/06 20:47
dolioYou could have been in there.09/06 20:47
copumpkinI'm sure he still could be if we tried hard enough09/06 20:48
dolioHe can't be in the PDF they sent out today.09/06 20:48
copumpkinit's a harry potter PDF09/06 20:48
dolioUnless we use your time machine.09/06 20:48
copumpkinwith interactive content09/06 20:49
copumpkinI'm sure the PDF spec allows fully executable programs on pages these days09/06 20:49
dolioProbably.09/06 20:49
djahandarieI don't think that works when you print it09/06 20:49
copumpkinno, it does09/06 20:49
copumpkinnew special printers09/06 20:49
djahandarieWhat does it do, print out an iPad?09/06 20:50
copumpkinsomething like that09/06 20:50
dolioSo I guess I can go through defining all the basic types...09/06 20:51
dolioExplain the operator syntax.09/06 20:51
dolioAnd the holes.09/06 20:51
copumpkinand inductive families! yay09/06 20:51
dolioEquality, at least.09/06 20:52
dolioMaybe I could try to explain why sigmas are like sums, and pis like products.09/06 20:52
dolioInstead of the obvious products and functions respectively.09/06 20:52
copumpkinyeah, that'd be good09/06 20:52
dolioThat was part of my notes I didn't get to last week.09/06 20:53
dolioAnd after that I was going to talk about the adjunctions between them.09/06 20:53
dolioWhich I started doing in Agda, but I'm not sure how bad that'd get.09/06 20:53
dolioI don't really want to talk about universe polymorphism, but it requires equality at the type level.09/06 20:54
djahandarieUniverse polymorphism is like the coolest part of Agda09/06 20:54
copumpkinmeh09/06 20:54
djahandarieAlso one of the parts that I still feel like I don't formally understand09/06 20:54
dolioIt's also one of the least well grounded in literature.09/06 20:55
djahandarieMaybe you should skip dependent type implementations like Agda and go directly to HoTT (or OTT first). :p09/06 20:56
djahandarieGo towards OTT. I missed that joke.09/06 20:58
copumpkin:O09/06 20:58
guerrilladjahandarie: look at Type Checking with Universes for an intuition. it's technically not the same thing, but related09/06 21:02
dolioWow, I need to be careful not to press C-c C-a tomorrow.09/06 21:05
dolioIt's writing this stuff itself.09/06 21:05
doliomap∏ : ∀{I J} {F G : Fam (I × J)} → (F ⇉ G) → ∏ F ⇉ ∏ G09/06 21:05
doliomap∏ f = λ i x j → f (i , j) (x j)09/06 21:05
dolioOh, it can't do sums, though.09/06 21:09
augurxplat: thank you09/06 21:19
augurhas anyone read Denney's refinement paper?09/06 21:20
augurwell, his dissertation09/06 21:20
nappingAre there any examples with sized types?09/06 23:00
lambdabotnapping: You have 1 new message. '/msg lambdabot @messages' to read it.09/06 23:00
copumpkinnapping: I vaguely remember coming across some a while back in the agda repo09/06 23:01
nappingwhich repo?09/06 23:02
nappingagda-lib defines Size, but nothing uses it09/06 23:02
copumpkinhttp://code.haskell.org/Agda/examples/Termination/Sized/DeBruijn.agda09/06 23:05
copumpkinnot sure if that stuff still works09/06 23:05
copumpkinhttp://code.haskell.org/Agda/examples/Termination/Sized/SizedNat.agda09/06 23:05
copumpkinthat?09/06 23:05
nappingfor some reason, code.haskell.org is not visible from here09/06 23:07
nappingI found slides from AIM 2008, I'll see if that code works09/06 23:08
nappingseems to be accepted, with the --sized-types flag09/06 23:13
nappingI wonder if the interaction with the new coinductive definitions has ever been checked09/06 23:18
nappingIt seems ^ is supposed to be something different from ↑09/06 23:25
--- Day changed Fri Jun 10 2011
augurcopumpkin!10/06 00:04
copumpkinyo10/06 00:05
augurhows life, copumpkin10/06 00:14
copumpkinpretty good10/06 00:16
copumpkinyou?10/06 00:16
augurcopumpkin: same same. trying to finish a revision of a paper that i really should have done by now10/06 00:28
copumpkinoh man, contravariant subtyping in agda!10/06 15:04
xplatnapping sure doesn't tend to stay on long10/06 15:22
xplatstill have no idea if that hpaste annotation i did was ever read :-/10/06 15:22
xplatit's kind of annoying on github having ssh keys and a password and they pretty much have non-overlapping functionality10/06 15:33
xplati don't suppose there's some sort of secret github api via ssh10/06 15:33
xplatthe regular API only supports password auth too10/06 15:34
copumpkinnot sure10/06 15:36
copumpkin@tell napping xplat wanted you to read something10/06 15:37
lambdabotConsider it noted.10/06 15:37
xplatcopumpkin: i already tried that :)10/06 15:48
copumpkin@tell napping xplat also used @tell to tell you something, so you should read that after you read this, in case you didn't notice it in your @messages output. So yeah, it's a couple of lines above this one. Look up^^10/06 15:49
lambdabotConsider it noted.10/06 15:49
xplatlol10/06 15:49
copumpkinyou can never be too sure10/06 15:49
* xplat takes off and @tells napping from orbit. It's the only way to be sure.10/06 15:50
copumpkinoh yeah, I hadn't thought of that10/06 15:52
xplatcopumpkin: btw are you going to have time to merge my categories changes into master so i have a good base to start the porting from?  or do you want to just push the new files you missed so i can merge from my end?  (assuming you can even get at them from there ...)10/06 15:52
copumpkinoh yeah, sorry, didn't realize you were waiting on me10/06 15:53
copumpkinshould be up to date now :)10/06 15:54
djahandarieI think I'll try to fix Agda and tinker with that library today10/06 15:54
copumpkinthere's lots of stuff still todo!10/06 15:54
xplatyay10/06 15:54
copumpkin(co)equalizers10/06 15:54
copumpkinyoneda!10/06 15:54
copumpkinall the monoidal junk10/06 15:54
copumpkinkan extensions so we can finally finish them there profunctors in a cute category10/06 15:55
djahandarieEnriched categories!10/06 15:55
copumpkinCategory.Agda still bothers me10/06 15:55
copumpkinwe should probably just accept that one will be setoids and the other will be sets10/06 15:55
copumpkinor something10/06 15:55
xplator that one will be category theory and the other will be category-extras10/06 15:56
copumpkinwell, I did kind of want a distinction like that10/06 15:56
copumpkinso you're saying Setoids is more pure, and Sets is more for hardcore categorical programming in agda?10/06 15:56
copumpkinI also kind of wanted to play with that non-endo-monad10/06 15:58
djahandarieHow do you plan on handling things when it gets bicategories and such? Won't that allow like half of the definitions to be rewritten?10/06 15:58
copumpkinI dunno, I can't say I have much of a vision for this :)10/06 16:00
copumpkinI think it wouldn't be terrible to keep the simple versions of structures around unless we can make the specific generalized instances as easy to use10/06 16:00
djahandarieWait, Agda has subtyping?10/06 16:01
copumpkinI think the sized types thing behaves a bit like subtyping10/06 16:01
dpiponiHow do I eliminate lemma₁ from this: http://hpaste.org/4764510/06 17:07
dpiponiThought I could just use refl but it doesn't like that.10/06 17:09
xplati don't know why refl won't work there, what does it say?10/06 17:14
copumpkinit works for me, but is yellow10/06 17:15
dpiponiThe preceding expression headed by cong ends up yellow. Yellow isn't good, right?10/06 17:15
copumpkin    2 * suc n + n * (1 + n)    ≡⟨ cong (λ p → 2 * p + n * (1 + n)) (refl {_} {_} {suc n}) ⟩10/06 17:16
copumpkinthat works10/06 17:16
dpiponiNot 100% sure what yellow means. I guessed it was something like: "I can't rule this out but I don't have enough info to prove it correct."10/06 17:16
copumpkinas does10/06 17:16
copumpkin    2 * suc n + n * (1 + n)    ≡⟨ cong (λ p → 2 * p + n * (1 + n)) (refl {x = suc n}) ⟩10/06 17:16
copumpkindpiponi: it means that there are unsolved metavariables10/06 17:16
copumpkinunderconstrained10/06 17:16
copumpkinoften could be implicits that it can't figure out from context10/06 17:16
xplati loaded it as is and there was no yellow10/06 17:16
copumpkinxplat: well, with the explicit lemma it's fine10/06 17:17
djahandariexplat, he means get rid of lemma_1 and replace it with refl10/06 17:17
dpiponiOh! That works! But I could swear I tried exactly that.10/06 17:17
copumpkindpiponi: well, you might have passed the wrong implicit? constructors get all the parameters to the data type10/06 17:17
copumpkinso the first implicit is the universe level10/06 17:17
copumpkinthe next is the type, then comes the value10/06 17:17
* copumpkin shrugs10/06 17:18
dpiponiYes. But I did look up to exactly what those implicits were. Must have been a typo. Anyway, I'm excited I've reproduced by first high school induction, even if not over ℤ.10/06 17:18
copumpkinoh10/06 17:18
copumpkinbut actually10/06 17:18
copumpkincong on refl is pointless10/06 17:18
djahandarieImplicits have always seemed a little ugly to me10/06 17:18
copumpkinthat whole line turns into10/06 17:18
copumpkin    2 * suc n + n * (1 + n)    ≡⟨ refl ⟩10/06 17:18
copumpkinor you can just rewrite it directly10/06 17:19
dpiponiOh yeah! And it doesn't need help with the implicits either.10/06 17:19
copumpkinyeah10/06 17:19
copumpkinthis theorem is not tail recursive!!10/06 17:21
dpiponiIs that bad?10/06 17:21
copumpkinno, just being silly :)10/06 17:21
xplati just replaced the whole cong with refl10/06 17:22
djahandarieIt doesn't even matter if actual functions in Agda are tail recursive.10/06 17:22
djahandarieNo one will be running them, after all.10/06 17:22
copumpkinexactly!10/06 17:22
xplatoh, already done :)10/06 17:22
dpiponiTook me ages to figure out how to unpack all of the properties of semirings. But now I've done it once, it should be easier in future.10/06 17:22
copumpkinat some point I started an ambitious project to do extensible dependent records for universal algebra-like structures10/06 17:24
copumpkinbut then I started ripping my hair out10/06 17:24
copumpkinI wonder if I'd be more clueful now10/06 17:24
dpiponiI wonder how hard it would be to prove the infinitude of the primes.10/06 17:24
djahandarieExtensible dependent records for universal algebra-like structures?10/06 17:24
stevandpiponi: it's in the stdlib readme btw: http://www.cse.chalmers.se/~nad//listings/lib/README.Nat.html10/06 17:25
xplatyou could do something like module * = IsCommutativeMonoid *-isCommutativeMonoid and then do *.comm and such10/06 17:25
copumpkindjahandarie: talking about structures as combinations of sets, n-ary functions on those sets (where 0-ary is a "distinguished element"), and properties relating those functions to each other10/06 17:26
copumpkinit was fun, but I didn't like the way I was approaching it so put it off to another day10/06 17:26
djahandarieWhat was complicated about it?10/06 17:27
copumpkinmy main issue was with "naming" (in some abstract manner) the sets, operations, and properties10/06 17:27
dpiponistevan: thanks. I should keep my eyes more open for things called README!10/06 17:27
copumpkinso that you can share them between structures and talk about x being a subset of y10/06 17:27
djahandarieAh.10/06 17:27
xplatdoes agda allow any kind of module qualification on infix operators?10/06 17:28
copumpkindon't think so10/06 17:28
djahandarieLame, even Haskell can do that! ;)10/06 17:28
djahandarieI can see where module qualification on mixfix operators would get a little confusing though.10/06 17:28
xplatHaskell can do a *lot* more with binary operators than agda, the only thing it lacks is some flexibility in naming10/06 17:29
xplatotoh, agda can do lots of stuff with non-binary operators that Haskell can't10/06 17:29
djahandarieWhat else can Haskell do, besides sections?10/06 17:29
xplatwell, sections and qualification are basically it, but that's already a lot more10/06 17:30
kosmikusxplat: I'd argue that qualification isn't all that relevant given Agda's renaming feature10/06 17:33
kosmikusxplat: plus the possibility to open modules locally10/06 17:33
xplatkosmikus: that's like arguing that renaming modules isn't relevant since you can always make a new local module10/06 17:33
kosmikusxplat: feel free to disagree :) but I certainly miss sections more than qualified infix operators10/06 17:34
xplatwell, try writing open Category C renaming (_\o_ to _\oC_; _\==_ to _\==C_) and the same for D and E a few dozen times and you'll already start getting sick of it10/06 17:35
xplatbut yeah, i also miss sections even more10/06 17:36
copumpkinI thought there were some plans at some point to have mixfix sections10/06 17:41
copumpkinit sounds horrifying to parse, but maybe not if I read the mixfix parsing stuff10/06 17:41
Saizanif the module system was less of a language of its own you could abstract the repetitive renaming into a function10/06 17:45
xplatcopumpkin: i figure it wouldn't be so horrifying to parse if instead of the null string you indicated sections by _ glued in10/06 17:48
xplatso _+ 1 or 1 +_10/06 17:48
xplatand it's a nice generalization of 1 + 1 vs _+_10/06 17:49
xplatso it makes more sense that way anyhow10/06 17:49
Saizanexcept that currently you can have a distinct _+ identifier10/06 17:52
Saizanbut i don't think anyone would mind losing that10/06 17:53
copumpkincurrently you can already cause issues like that10/06 18:12
copumpkinwith <_+_> and _+_10/06 18:12
copumpkindo the fixity annotations allow one to take precedence over another?10/06 18:12
copumpkinthat seems kind of scary10/06 18:12
xplatargh10/06 18:16
xplati could totally write module Equiv {A B : Obj} = IsEquivalence (equiv {A} {B}) except it complains because equiv is irrelevant10/06 18:17
xplatsame thing happens if i open public :(10/06 18:19
xplatif i open privately then it lets me, and marks all the functions as irrelevant10/06 18:19
xplatwhy won't it do that for a public open?10/06 18:20
xplatgrumble grumble pointless rewriting of type signatures10/06 18:20
copumpkinyeah, that's what I wanted irrelevant modules for10/06 18:24
copumpkinthere's a ticket in the tracker for that10/06 18:24
xplati can also write something like refl = IsEquivalence.refl (equiv {A} {B}) without a type signature10/06 18:26
xplatonly if equiv is irrelevant it complains again10/06 18:26
xplatand i can't just write .refl, i have to write a whole type signature10/06 18:26
xplatargh10/06 18:26
xplatstandard library setoids do not have irrelevant equivalence either10/06 18:38
xplatand probably something would go wrong if i made hom-setoid irrelevant as a whole :(10/06 18:39
Eduard_MunteanuI'm not sure, is irrelevance supposed to change semantics? I first had the impression it was meant to provably discard arguments at runtime.10/06 18:40
xplatwell, i'm going to try just making the whole thing irrelevant and see what problems come up10/06 18:41
* Eduard_Munteanu should play with those too10/06 18:41
xplatwell, the first problem is i can't take a setoid as an irrelevant parameter in a module (?!)10/06 18:43
xplator if i can i can't figure out where to put the dot10/06 18:43
xplatthe more i use irrelevance the less it seems like it is ready for prime time10/06 18:45
xplatbut throwing it out is definitely not an option either10/06 18:45
Eduard_MunteanuWhat does irrelevance give you anyway?10/06 18:46
Eduard_MunteanuSurely it doesn't make typechecking use less memory or finish sooner.10/06 18:46
xplati'm not going to accomplish much by porting this if i end up having to make the irrelevance-annotated version of everything in the standard library anyway though10/06 18:47
xplatEduard_Munteanu: actually it does; once a closed value is supplied for an irrelevant parameter it can be erased even during typechecking10/06 18:47
Eduard_MunteanuOh. I guess it makes sense then.10/06 18:48
copumpkinEduard_Munteanu: if you have data Moo : Set where x : .Nat -> Moo, you could prove x 5 == x 710/06 19:22
copumpkinthis for example: http://snapplr.com/3z5s10/06 19:25
xplatgah, can't even use Data.Unit in Categories.Terminal10/06 19:36
copumpkinwhy not?10/06 19:36
xplat⊤ is only in Set10/06 19:36
copumpkinI've wondered about how important that is10/06 19:36
djahandarieMy client can't even display that character. :(10/06 19:36
codolioWho needs cumulativity?10/06 19:36
xplatpeople who want to have a category of categories that is cumulative and doesn't have a sigma for a bounded level10/06 19:37
codolioDefining a universe polymorphic top doesn't work very well, either.10/06 19:38
codolioUnless you like writing '\top i' everywhere.10/06 19:38
xplatapparently that's what we've been doing up to now10/06 19:38
copumpkinyeah, we have10/06 19:38
copumpkinbut it's implicit and silly10/06 19:38
copumpkinsee, I don't really know how important it is to have things like that be able to live at arbitrary levels10/06 19:38
copumpkinsame issue with discrete categories10/06 19:39
xplatand the parameter seems to infer just fine the few places it's used10/06 19:39
copumpkinusing == for morphisms10/06 19:39
xplatcopumpkin: well, without a level-polymorphic Categories.Terminal only the categories-of-categories where objects are at level 0 have finite products10/06 19:39
copumpkinfair enough10/06 19:40
copumpkinthat'd be annoying10/06 19:40
copumpkinwe could just use Lift everywhere though10/06 19:40
copumpkinthat'd probably be even more annoying though10/06 19:40
copumpkintime to port this all to mini-agda10/06 19:40
copumpkin:)10/06 19:40
djahandarieHow would mini agda help?10/06 19:41
djahandarieI should really go read more about that thing10/06 19:41
xplati just made a private unit type since no operations on it are needed10/06 19:43
copumpkinI wonder how many interesting operations there are on it :)10/06 19:44
copumpkindjahandarie: cumulativity10/06 19:44
codoliodjahandarie: Because miniAgda has cumulativity? I think it does.10/06 19:47
codolioIt has variance tracking, too.10/06 19:48
copumpkinfor sizes?10/06 19:48
copumpkinor what?10/06 19:48
codolioYou can write Mu in it.10/06 19:48
copumpkin:o10/06 19:48
codoliodata Mu (F : Set++ -> Set) where roll : F (Mu F) -> Mu F10/06 19:49
codolioSomething like that.10/06 19:49
copumpkincan it be a record?10/06 19:49
codolioMeaning that F is strictly positive in its first argument.10/06 19:49
copumpkinthat seems like fun10/06 19:49
codolioAnd there's + and -, too.10/06 19:50
codolioWhether it could be a record depends on whether recursive records are allowed. And I don't know that.10/06 19:51
codolioJust a week until my laptop allegedly ships. I wonder if they'll charge me.10/06 19:52
copumpkinoh man10/06 19:52
copumpkinthat's exciting10/06 19:53
copumpkinare you itching to write some hardcore agda again?10/06 19:53
codolioYeah.10/06 19:53
codolioAssuming the order is actually valid.10/06 19:53
djahandarieHardcore Agda, 18+ only10/06 19:54
copumpkinI don't think we have any under-18s in here10/06 19:54
copumpkincause dylukes left :(10/06 19:55
djahandarie:(10/06 19:55
augurwoo10/06 19:55
djahandarieI can pretend to be <1810/06 19:55
auguractivity10/06 19:55
augur:D10/06 19:55
djahandariehi guyz im in middle school, tryin to understand how agda works, u know, dependent types n stuff10/06 19:56
djahandarieI wonder how far I could get teaching middle schoolers Agda10/06 19:58
copumpkindjahandarie: omg go away, only hardcore agda in here10/06 19:58
copumpkindjahandarie: I don't think it's that fundamentally difficult10/06 19:59
djahandarieAgeist!10/06 19:59
copumpkinit's more types than most programmers are used to10/06 19:59
copumpkinbut people with no expectations might not have as much trouble with it10/06 19:59
copumpkinit's a fairly simple and consistent set of rules, at least if you stay away from coinduction :)10/06 19:59
copumpkinand maybe irrelevance10/06 19:59
codolioThe irrelevance stuff isn't really very hard, either, until you muck it up with all the ways Agda is different from the simpler theories in papers on it.10/06 20:02
copumpkinyeah10/06 20:03
copumpkinthe irrelevant pi thing seems kind odd and not quite fleshed out yet10/06 20:03
codolioReal coinduction isn't harder than induction, either.10/06 20:03
copumpkinyeah, but the whole story about # x /= # x seems odd10/06 20:04
codolioWhat might be harder is the Agda, "no one knows the underlying theory of this stuff," version. :)10/06 20:04
copumpkinmaybe I'm just thinking about it wrong10/06 20:04
copumpkinalso, equality of where clauses and absurd lambdas! :P10/06 20:05
codolioYeah, the implicit generativity is weird.10/06 20:06
codolioCombined with the lack of sufficiently extensional equality.10/06 20:06
copumpkinrandom idea: take the BitVector work glguy and I did, and build floats on top of it10/06 21:36
copumpkinthen model floating point algorithms10/06 21:36
copumpkinit'd be nice to have rationals though10/06 21:37
copumpkinto "ground" the floats in10/06 21:37
codolioI'm certainly dying to prove things about the IEEE spec.10/06 21:37
copumpkinI thought you might10/06 21:37
--- Day changed Sat Jun 11 2011
xplatcopumpkin: so far i'm up to Categories.Grothendieck, but i'm running out of steam11/06 03:33
xplatyet again there's an irrelevant version of something in the stdlib11/06 03:33
xplatand now i'm on Globe and there is no proof in the stdlib that <-trans is associative11/06 04:01
xplatuniqueness for < would work too11/06 04:02
copumpkinxplat: ack :/11/06 04:21
copumpkinyeah, I wish irrelevance would infect the stdlib11/06 04:21
* augur infects copumpkin's stdlib11/06 04:23
copumpkinlol11/06 04:23
guerrillaso, i get that this would fail termination checking, but aside from embedding Nat in a data strcuture that includes negativie/positive infinity, how might one implement the following: http://www.randomhacks.net/articles/2007/02/02/divide-infinity-by-211/06 05:11
guerrillainfinity = Succ infinity11/06 05:11
guerrillais what i'm referring to11/06 05:11
guerrillai'm guessing it would use coinduction somehow, but i'm not really up to speed on that11/06 05:12
dolioYes. The naturals he's using are coinductive.11/06 05:15
dolioTechnically they're also inductive, because inductive and coinductive types coincide for Haskell.11/06 05:16
augurdolio: which is to say its all coinductive in haskell, no?11/06 05:16
dolioYes, everything is inductive and coinductive.11/06 05:17
augurwell but nothing in haskell can be truly inductive due to laziness, no?11/06 05:17
dolioNo, they're all inductive.11/06 05:17
dolioThey're just not inductive sets.11/06 05:17
augurhmm11/06 05:17
dolioThey're inductive domains.11/06 05:17
augurhmm11/06 05:17
guerrillaright11/06 05:18
guerrillabut could you do something that would acheive the same results without making Nat codata?11/06 05:19
guerrilla(and without wrapping Nat)11/06 05:19
guerrillanot opposed to the latter, just curious11/06 05:19
dolioYou could turn off the termination checker.11/06 05:19
guerrillahaha yeah11/06 05:19
guerrillai like to keep it on and pretend agda is CIC^ :P11/06 05:20
dolioAgda actually does non-strict evaluation, so it'd work out.11/06 05:21
dolioExcept, perhaps, if you used the BUILTIN pragma, which makes Nat backed by Haskell's Integer, which can't encode inf = succ inf.11/06 05:22
guerrillayeah11/06 05:23
dolioHowever, if you used the infinite value in a type such that it had to be normalized, there'd be a problem.11/06 05:23
guerrillathis is an interesting solution, going the packing route: http://blog.jbapple.com/2007/02/countable-ordinals-in-haskell.html11/06 05:23
guerrillaindeed11/06 05:23
guerrillain the case i'm considering using for, it wouldn't need to be normalized11/06 05:23
dolioOrdinals are rather different.11/06 05:23
guerrillayeh, the size of the set of nats, instead of the value11/06 05:24
guerrilla(or size of any set)11/06 05:24
guerrilla"Now, according to Fokkinga and Meijer, there’s actually some pretty deep math lurking here. Apparently, Haskell’s lazy evaluation moves us from category Set to category CPO, where our initial F-algebras and our final F-coalgebras turn out to be the same!"11/06 05:26
guerrillais that what you were refering to abov?11/06 05:26
dolioYes.11/06 05:26
guerrillaok11/06 05:27
dolioAll CPOs have a bottom element and limits of monotone sequences of elements.11/06 05:28
dolioIn addition to the elements produced by the constructors along with those.11/06 05:28
guerrillainteresting11/06 05:29
guerrillayeah, i remember this from my domain theory reading11/06 05:30
dolioSo that gives your inductive types elements that match coinductive elements.11/06 05:30
guerrillanot sure what that means. "match"?11/06 05:31
dolioIt gives you the 'inf = suc inf' element, for instance, which in Set would require coinduction.11/06 05:31
dolioBecause it's the limit of _|_, suc _|_, suc (suc _|_), ...11/06 05:32
guerrillaright11/06 05:32
guerrillaok11/06 05:32
guerrilladolio: thanks for the insight11/06 05:48
_Cactus_hi11/06 05:50
_Cactus_what does 'unresolved meta' mean?11/06 05:50
_Cactus_oh11/06 05:51
_Cactus_I think I see11/06 05:51
_Cactus_ok11/06 05:53
_Cactus_so now my question becomes:11/06 05:55
_Cactus_if I have four implicit arguments for a function,11/06 05:55
_Cactus_and I need to give, at a certain invocation, the third one only (the others are inferrable)11/06 05:56
_Cactus_then what's the syntax for it, apart from {_} {_} {foo} {_} ?11/06 05:56
xplatcopumpkin: i finished porting11/06 05:59
copumpkinoh wow11/06 05:59
copumpkinmassive effort!11/06 05:59
copumpkinwhat'd you do about duplication of none-irrelevant things?11/06 05:59
xplatmassive effort = massive win11/06 05:59
xplatstill duplicated, but made closer in interface to the stdlib versions11/06 06:00
copumpkincool :)11/06 06:00
copumpkinamazing11/06 06:00
xplat_Cactus_: if you know the name of the third argument, you can write blah { name = foo }11/06 06:01
_Cactus_and what happens if 'name' is also bound in the scope?11/06 06:01
_Cactus_or is there no problem with htat?11/06 06:01
xplatcopumpkin: should i push it?11/06 06:02
_Cactus_e.g. can I do {foo = foo} if foo is also the name of the implicit argument?11/06 06:02
xplat_Cactus_: that's fine11/06 06:02
_Cactus_great11/06 06:02
_Cactus_thanks11/06 06:02
copumpkinxplat: sure!11/06 06:03
copumpkinwhat's the new module?11/06 06:03
xplatCategories.*11/06 06:04
copumpkinsounds good :)11/06 06:04
_Cactus_is there a way to pass these implicit arguments without resorting to prefix notation? so that instead of having to write _op_ {foo = foo} x y is there something like (x op y){foo = foo}?11/06 06:04
xplatall the old support modules are now unused, but there are new ones under Categories.Support11/06 06:04
_Cactus_(is there an #agda-newbies?:))11/06 06:04
copumpkin_Cactus_: sadly nope, to both questions ;)11/06 06:05
_Cactus_:)11/06 06:05
xplatthe old ones are also under Categories.Support but only for reference11/06 06:06
xplatcurrently It Works For Me with the stdlib v0.511/06 06:07
xplathopefully nothing much breaks with darcs stdlib11/06 06:07
copumpkincool :)11/06 06:07
* copumpkin goes to sleep11/06 06:11
copumpkinwill check i out tomorrow11/06 06:11
copumpkin:)11/06 06:11
guerrillaso, im curious, what are people doing for the lack of type classes in agda?11/06 06:56
guerrillai saw the implicits post on the mailing list but afaik, that's not implemented yet11/06 06:56
djahandarieIt's not like they're really needed for the majority of things. You get ad-hoc polymorphism by pattern matching on types in Agda.11/06 06:58
dolioYou can't pattern match on types.11/06 07:01
djahandarieErm. Yeah, bit of the wrong terminology there I guess.11/06 07:02
_Cactus_is there a way to tell agda that my function is injective, and give its inverse, and then if I have something like forall {x} -> f x -> y then not have to pass {x}?11/06 07:04
guerrilladjahandarie: depends on what you're doing. i use typeclasses a lot in haskell. for example, Eq a11/06 07:04
_Cactus_guerrilla: you can always just pass around records witnessing the instance11/06 07:04
guerrilla_Cactus_: yeah, i do that now. just curious if theres work for that to be able to be implicit11/06 07:05
djahandarieOkay, scratch that, not wrong terminology, just wrong. I swear I saw this somewhere but I guess it wasn't Agda.11/06 07:14
guerrillawhats the example you tried?11/06 07:21
guerrillajust curious11/06 07:21
guerrilla_Cactus_: cool syntax btw regarding the implicit arguments11/06 07:22
guerrillamaybe someday :)11/06 07:22
djahandarieguerrilla, I didn't try any code, I just tried looking it up and I couldn't find it. It was some formulation of type classes where you could group together types and write instances by just pattern matching on the type constructors in the function.11/06 07:26
guerrillahmmm, actually, i see what you mean11/06 07:27
guerrillalemi play with that for a sec and get back to you11/06 07:28
djahandarieI'm sure it doesn't work in Agda.11/06 07:28
guerrillahmm11/06 07:29
augurhttp://www.extremetech.com/article2/0,2845,2386710,00.asp11/06 07:29
augur100 to 300GHz processors11/06 07:29
augursounds good for agda type checking!11/06 07:30
guerrillauh wow11/06 07:30
guerrillayeah, first thing came to mind, stdlib will compile fast11/06 07:30
guerrillalol11/06 07:30
augur:)11/06 07:30
guerrillai wonder what the physical size is11/06 07:31
_Cactus_guerrilla: did you know that the soviet microelectronics industry failed only because the end products couldn't fit through the factory gate?11/06 07:35
guerrillai am skeptical, but i could see that11/06 07:37
_Cactus_(this was my lame attempt at a joke)11/06 07:37
guerrilla*wooosh*11/06 07:37
guerrilladjahandarie: yeh, i give up. :P did you find the reference you were looking for?11/06 07:49
Saizanguerrilla: maybe djahandarie was referring to universes, like in The Power of Pi, iirc11/06 13:29
Saizanguerrilla: and i thought the new implicits were implemented in the darcs version of agda11/06 13:30
copumpkinxplat: I was thinking if you renamed ⟨_⟩,⟨_⟩ to _⟩,⟨_ it would look like it fits in better with the equational reasoning stuff11/06 14:29
guerrillaSaizan: ah, i havet checked out darcs lately, thanks for letting me know11/06 15:11
guerrillaSaizan: and thanks for the ref on the other, looking at it now11/06 15:11
--- Day changed Sun Jun 12 2011
joe6asking this question here given the caliber of the people hanging out here: is there a hash algorithm without collisions?, without a complicated algorithm, something that can be done in assembly?12/06 00:15
joe6i have 1500 bytes available to index data in 100K bytes and I am doing this in assembly.12/06 00:17
dolioYou can't have a hash algorithm without collisions unless you know something about the space you're hashing from.12/06 00:18
joe6just curious, if there might be some smart way of doing that, without having to reload the pages?12/06 00:18
dolioSpecifically, that it's smaller than the hash space.12/06 00:18
joe6dolio, I know everything about the space available.12/06 00:18
joe6dolio: oh, ok.12/06 00:18
joe6is hash the best way to do this?12/06 00:19
joe6i currently have a linked list that I match against.12/06 00:19
joe6but, that is not scalable and provides very limited indexing capabilities.12/06 00:20
joe6i thought of huffman encoding, but it is not that simple in asm.12/06 00:20
joe6what about the SHA-1 algorithm that git uses? is it a complicated algorithm?12/06 00:20
xplatnot to go into extreme specifics, but there is no hash function that will hash a fixed number of keys with no collisions regardless of what the keys are12/06 00:21
dolioNo idea. I've not looked much at hash algorithms.12/06 00:21
joe6i have a list of patterns that I search with, and the pattern that matches, I lookup the value that it contains and send that value over.12/06 00:21
xplatif you want zero collisions, you have to adapt the hash function to the data set, because any fixed hash function has data sets it doesn't get along with12/06 00:22
joe6i have the patterns currently as a linked list, but, it just seems inefficent12/06 00:22
dolioI just know that it's mathematically impossible to hash a set of N values into a set of M values where N > M without collisions.12/06 00:22
joe6and, there is a limitation of how many patterns I can store in 1500 bytes..12/06 00:22
xplatif the hash space is really large (like sha-1's) then you can make it statistically pretty likely that you will have zero collisions with the fixed function, but then you can't use the hash value as an index directly anyway and when you fold it down to the size of your table you get collisions again12/06 00:24
djahandariedolio, not with my infinite compression algorithm!!!12/06 00:24
joe6i have 1500 bytes of ram space and 100K bytes of eeprom space, that I do not want to hit (unless required). Any suggestions that you can think of?12/06 00:25
joe6i want to keep the patterns in the ram space and take the number of the pattern that matched as an array index to the lookup-value.12/06 00:26
joe6is that a good idea?12/06 00:27
xplat1500 bytes is not much ram for search patterns, but i guess if there's nothing else you're doing with it ...12/06 00:28
joe61500 bytes is exclusively reserved for the search patterns, I mean.12/06 00:28
xplatwhat kind of search are you doing?12/06 00:29
xplatbecause a lot of data structures REALLY won't work for some kinds of searches12/06 00:30
joe6just a simple list of 8(or 10) possible alternatives strung together one after the other.12/06 00:30
xplatthat tells me nothing12/06 00:30
joe6and I have the length of each such pattern list12/06 00:30
xplati don't know what kind of pattern, what they're being matched against, or anything12/06 00:31
joe6i could have a sample pattern of : a,b,c,a,b12/06 00:32
joe6xplat: i am talking about simple stuff12/06 00:32
xplatmaybe, but i would still have to be psychic to know what it is12/06 00:33
joe6and I match it against a search space that could contain, a,b,c,d ; a,a,c: a,d,c,e :12/06 00:33
joe6and when I find the pattern that is a,b,c,a,b, then bingo, I have my match.12/06 00:34
joe6nothing serious, it is a very simple search on an 8-bit mcu12/06 00:34
joe6xplat: does that make sense?12/06 00:34
joe6and, distinct elements can be 8 or 10 (I know exactly how many, beforehand)12/06 00:35
xplatwhat are the ; and :?  is the 'search space' what you are keeping in the linked list, or is the 'sample pattern'?12/06 00:36
joe6and I will be writing out the patterns that it will be matching against, so, order of the patterns is in my control.12/06 00:36
joe6i used the : to denote the next pattern12/06 00:36
joe6sorry, the ; = :12/06 00:36
joe6typo12/06 00:36
xplatis it an exact string match, prefix match or substring match?12/06 00:36
joe6exact string match12/06 00:36
xplatdo you expect most inputs to be matches or non-matches?12/06 00:37
joe6most matches12/06 00:37
joe6very rarely, non-matches.12/06 00:37
joe6very very rarely. I should say.12/06 00:37
xplathow many inputs come in per second?12/06 00:38
xplat< 1, dozens, thousands, or millions and up?12/06 00:38
joe6xplat, maybe one pattern or < 3-4 such pattern sets12/06 00:39
joe6when I say a pattern set, I mean around 10'ish patterns12/06 00:39
joe6so, yes, dozens such patterns would be too much.12/06 00:39
xplatand how many inputs do you usually match before the pattern set changes?12/06 00:39
joe6xplat, all?12/06 00:39
joe6i wait for the pattern set to form, and then start the match12/06 00:40
xplatto form?!12/06 00:40
joe6i am not matching while processing is going on (ie., the pattern set is forming). I wait until the pattern set is complete, and then I start working on it.12/06 00:40
joe6i mean, an example pattern set is : a,b,c,d,a.12/06 00:41
joe6and then followed by a delimiter.12/06 00:41
joe6I wait to get the delimiter and then start the match.12/06 00:41
joe6i do not know if that is a good idea, but, it is(seemed) simpler than the alternative12/06 00:42
xplati feel like we don't share enough vocabulary to have this conversation12/06 00:42
joe6should I query you? do you have a few minutes?12/06 00:42
xplatokay, wait, let's establish words to use12/06 00:43
xplatan 'input' is a string, followed by a delimeter12/06 00:44
joe6yes,12/06 00:44
joe6and, also has a length12/06 00:44
joe6delimiter and length are redundant, but I have both.12/06 00:44
xplata 'key' is a string that you want to notice if it occurs as an input12/06 00:45
xplata 'key space' is a list of keys12/06 00:45
xplatto be treated as alternatives12/06 00:46
joe6hold on, input = 3,a,b,c . My search patterns are as: 3.a,b,c,4,a,b,c,d,6,a,b,c,d,e,f12/06 00:46
joe6an so on.12/06 00:46
xplatokay, so how often do new inputs come in?12/06 00:47
joe6an input such as 3,a.b,c comes in a few times per second.12/06 00:47
xplatand how many inputs do you match against a key space before the key space changes?12/06 00:48
joe6what is the key space?12/06 00:48
joe6the 3.a,b,c,4,a,b,c,d,6,a,b,c,d,e,f12/06 00:48
joe6?12/06 00:48
xplat3,a,b,c,4,a,b,c,d,6,a,b,c,d,e,f12/06 00:49
joe6it does not change, it is a static space12/06 00:49
xplatthere is only one, and it never changes, and is used to match every input?12/06 00:49
xplatover the lifetime of the device?12/06 00:50
joe6yes12/06 00:50
xplatand contains only 8-10 alternatives12/06 00:50
xplat?12/06 00:51
joe63.a,b,c,4,a,b,c,d,6,a,b,c,d,e,f,10,a,a,b,c,d,e,f,g,a,b12/06 00:51
joe6the a b or c alternatives can be 8-1012/06 00:51
joe6which is known in advance.12/06 00:51
joe6so, the number of alternatives does not change12/06 00:51
joe6neither, does the space that I search in.12/06 00:52
joe6does that make sense?12/06 00:52
xplatwhen you say 'alternatives', you mean 'a' or 'b' or 'c'?12/06 00:52
joe6yes12/06 00:52
xplatinstead of 'number of alternatives', one would say 'size of the alphabet'12/06 00:52
joe6and the 3.a,b,c or 4,a,b,c,d, is what I call Pattern12/06 00:52
joe6yes, the size of the alphabet is perfect12/06 00:52
joe6that is 8-1012/06 00:53
xplatokay, but how many patterns/keys are in the key space?12/06 00:53
joe6do not know, yet. i need to figure out how much is possible, given the algorithm.12/06 00:54
xplatwell, how many would you expect to be useful?  dozens? hundreds?12/06 00:54
joe6hundreds12/06 00:54
joe6atleat12/06 00:54
joe6atleast12/06 00:55
xplatwell, obviously you will want to store them in eeprom12/06 00:55
joe6could be around thousands too.12/06 00:55
joe6but, not more than a few thousands.12/06 00:55
xplatsince they never change you can prepare them offline on a larger computer12/06 00:55
joe6yes, I have to store in eeprom, but they do not take more than a few bytes each.12/06 00:56
joe6yes, I can prepare them as I want it in an offline computer12/06 00:56
joe6regarding the format or the content12/06 00:56
joe6or the ordering12/06 00:56
xplatand how much of the mcu's time can you devote to looking them up?12/06 00:56
xplat100%?  10%?  1%?12/06 00:57
joe6quicker the better? I am trying to minimise the eeprom lookups for searching12/06 00:57
joe6if that is possible.12/06 00:57
joe6preload the ram, lookup the eeprom only when a match is found12/06 00:57
joe6is ideal.12/06 00:57
joe6but, that gives me 1500 bytes to store my patterns into, which is not much.12/06 00:58
joe6hence, wondering if there are better ideas?12/06 00:58
joe6i think there is quite some idle cpu cycles available, so, some processing for hash might be possibel.12/06 00:59
joe6s/el/le/12/06 00:59
xplatif you absolutely want to minimize eeprom queries, and you almost always match, you should use a perfect hashing tool12/06 00:59
joe6yes, that seems to be the best idea.12/06 01:00
joe6i would not be wasting the bytes storing the patterns..12/06 01:00
joe6and the ram usage would be the utmost.12/06 01:01
xplatyes, you can store the patterns only in eeprom, and still only query at most one from eeprom to match12/06 01:01
joe6on collisions?12/06 01:01
joe6or, to doublecheck the match?12/06 01:01
xplatdoublecheck12/06 01:01
xplatthe perfect hash tool will choose a hash function that does not collide for your fixed set of keys12/06 01:02
joe6smart thinking.. thanks.12/06 01:02
joe6instead of assigning sequential numbers to the alphabet, I was thinking if there is a smarter way of doing it.12/06 01:03
joe6if that helps the hasking function12/06 01:04
joe6i am generating the inputs too, so, I could assign the alphabet any byte value (could be 1,2,3,4.. or 1,2,4..)12/06 01:05
xplati think some hash function families will do that themselves.  it depends what tool you use to generate the perfect hash.12/06 01:06
joe6i have to code the hashing function in assembly12/06 01:06
joe6for that mcu.12/06 01:07
joe6any suggestions on the hash function, please? or where i can find something that can help me out.12/06 01:07
xplatyes, you probably want a perfect hashing tool with source code so you can see what kind of hash functions it generates and write assembly to do those sorts of hashes12/06 01:07
xplaton the other hand, if you go with commercial tools you might be able to find one that already generates assembly for your mcu12/06 01:08
xplatthat would be the most convenient, it depends on your budget12/06 01:09
joe6anything opensource?12/06 01:09
joe6that you can think of?12/06 01:09
xplatgphash is opensource and the hash functions it generates are simple12/06 01:10
xplatnot sure if the license is okay for your project though12/06 01:10
joe6ok, thanks a lot. I will check it out.12/06 01:10
joe6xplat:  what about bloom filters? would they help, in this scenario?12/06 01:18
joe6found this: uri: http://www.partow.net/programming/hashfunctions/12/06 01:19
xplatjoe6: bloom filters would not help.  they only tell whether you match, and you expect to almost always match.12/06 01:21
xplatso you would always do extra work, and hardly ever save any12/06 01:21
joe6the size of the alphabet is 8-1012/06 01:22
joe6xplat: what do you think of a trie  instead of a hashing function?12/06 01:44
xplatjoe6: it would be easier, but probably take more (eeprom) memory and make more eeprom queries12/06 01:47
joe6ok, thanks.12/06 01:47
xplatthe best way to limit eeprom queries for a trie is probably to put the 'top' of the trie in ram, or even a selection of nodes weighted by how often you expect them to be visited12/06 01:48
joe6i am not able to find much from google about gpHash other than that it is used by EPOS. do you have a link or something that you can share with me?12/06 01:48
xplathm, sorry, i got the name wrong :(12/06 01:49
joe6xplat, so, would you recommend a trie over a hash?12/06 01:49
xplathttp://www.gnu.org/software/gperf/12/06 01:49
joe6xplat, that is perfect. Thanks.12/06 01:49
xplatwell, a trie is easier to create, but it's harder to keep small or to adapt to a nonuniform memory speed like you need12/06 01:51
xplatso it depends on your relative tolerance for different kinds of risks12/06 01:52
xplatwith a trie it's more likely that you'll get it working but not scaling as well as you want, with a hash it's more likely that you won't get it working at all but if it works at all it will scale well12/06 01:53
joe6let me try the hashing function, I have used hashing functions before, whereas a trie is new territory for me.12/06 01:54
xplatsince you already have a working-but-slow implementation that reduces the advantage of a trie anyway12/06 01:54
joe6but, a bitwise trie is supposedly very helpful with caching (from wikipedia).12/06 01:54
xplatan 8-bit mcu won't do that kind of caching, and it's hard to tune your own trie implementation to cache well anyway12/06 01:55
joe6oh, ok.12/06 01:56
joe6thanks a lot.12/06 01:56
joe6xplat, just from reading the introduction of gperf, I gather that the C code changes based on the given list of strings. I need to translate the C to Asm. Just curious, is the C code generated vastly different each time or is it approximately the same?12/06 02:02
joe6it would just be too much work to translate the C code to Asm, every time the list of string tables change.12/06 02:02
joe6if it does not change that much, then I could just use a simple to C -> Asm template that can be reused..12/06 02:03
xplatjoe6: the C code is generated from a template, it doesn't do anything vastly different12/06 02:04
xplatwell, i think there can be big changes depending on a few of the command line switches, but not for most switches or depending on the keys12/06 02:05
joe6xplat, ok, thanks a lot. looks like it is the way to go. the more I read about it, the more it seems to fit.12/06 02:05
joe6yes, I will probably stick with the same switches. but, am more worried about the differences due to change in inputlist..12/06 02:06
joe6xplat, thanks for your excellent suggestion and guidance.12/06 02:06
Eduard_Munteanujoe6: I'd suggest trying to do stuff in C first.12/06 02:43
Eduard_MunteanuAt least compare the size of what you get from C and from hand-written asm.12/06 02:43
Eduard_MunteanuThe compiler could be able optimize for code size, so with proper options the machine might just be able to beat you at that :)12/06 02:45
joe6Eduard_Munteanu, ok, thanks.12/06 12:24
sshcWhat is the syntax of "{! !}" in vec : {n : Nat}{A : Set} -> A -> Vec A n12/06 17:38
sshcvec {n} x = {! !}12/06 17:38
sshcIt looks like it's listed as a solution to the first exercise, but agda can't even parse that: "Unsolved metas at the following locations:"12/06 17:40
guerrillathis is a guess but agda --allow-unsolved-metas12/06 17:50
guerrillanot sure if that's what it's for though12/06 17:51
guerrillais {! !} suppose to work like Haskell's "undefined :: a"?12/06 17:57
guerrillaor it's more?12/06 17:58
sshcAh.  That would make sense in this context (so that I can write a definition myself for the exercises in the tutoria).12/06 18:03
sshcBut how is it like Haskell's undefined?  Is that special-case syntax?12/06 18:03
guerrillai just use undefined a lot for a stub to see that the rest of my code compiles12/06 18:06
Saizan{! !12/06 18:27
Saizan{! !} is what agda-mode inserts in place of a ? when you load the file, btw12/06 18:27
Saizanit's called a "hole" or a "shed", agda-mode has a few nice commands to interactively fill it12/06 18:28
guerrillaok12/06 18:37
guerrillai don't use agda-mode since i don't use emacs.. so yeah12/06 18:39
sshcSaizan: So it is special-case syntax?12/06 19:07
Saizanyep12/06 19:07
Saizanwell, i'm not even sure if i'd consider it part of the language itself12/06 19:07
Saizansshc: you've never used "?" before?12/06 19:08
sshcI'm following the tutorial, and I don't think it's ever been mentioned12/06 19:09
sshcMany of Agda's interactive features are pretty much inaccessible to me, since I use vim12/06 19:09
guerrillashachaf: ditto12/06 19:11
guerrillaoops i meant sshc12/06 19:11
Saizani strongly recommend using emacs for agda, it really helps to be able to inspect the types and context of these holes while you develop12/06 19:11
guerrillaSaizan: ah, you know me, do everything the hard way ;)12/06 19:12
guerrillabut, in reality, i just can't use emacs.. 15 years of vi... hard habit to break, would really have to fight to use emacs12/06 19:13
dolioWhat about viper?12/06 19:14
guerrilladolio: ohhhh yes, thank you for reminding me. i remember reading about it a long time ago, i forgot to try it out12/06 19:16
guerrillabookmarking and installing now so i dont forget again12/06 19:16
dolioI'm sure it's not perfect, but it's probably worth it for what agda mode gets you.12/06 19:20
sshc"I used to think that emacs was a great OS but lacked a decent editor, but then I found out that it could run vim."12/06 19:23
guerrillahahaha12/06 19:24
shachafguerrilla: Agreed.12/06 22:33
shachafOops, I meant goomba.12/06 22:33
augurboth gorillas and goombas have been marios enemy12/06 22:38
sshcWhat's the difference between "∀ {x xs}" and "∀ x {xs}"?12/06 23:33
sshcWhat does the latter expand to?12/06 23:33
dolioIn the first one, both arguments are implicit.12/06 23:35
dolioIn the second, only the second is.12/06 23:35
sshcThanks12/06 23:36
--- Day changed Mon Jun 13 2011
starcloudedhello everybody13/06 01:41
guerrillashachaf: guerrillas and gorillas are not related.. well I guess, at times, both operate in jungles :P13/06 02:49
guerrilladamnit, i meant augur. how did i screw that one up :)13/06 02:50
sshcymasory: I believe you may be correct.13/06 02:53
ymasorysshc: moi?13/06 02:54
guerrillaymasory: i think its part of the runnin joke here of addressing the worng person13/06 02:59
ymasoryguerrilla: bye bye #agda13/06 02:59
augurwhoa hey hello13/06 03:12
augurguerrilla: thats not the point!13/06 03:12
guerrillaok :)13/06 03:34
augurhmm13/06 11:41
augurim going to be teaching a friend how to program13/06 11:41
augurshould i teach him in haskell or agda?13/06 11:41
auguror scheme?13/06 11:42
augurim most comfortable with scheme, but haskell has a good mix of theoretical import and practical value13/06 11:42
auguragda is pretty theory oriented, which is a real plus, but if he ever wants to actually write a program..13/06 11:42
xplataugur: i'd say haskell or scheme, depending on exactly how much more comfortable you are with the latter than the former13/06 12:29
augurim fine with both, i just havent taught with haskell before13/06 12:30
kosmikusI'd go for Haskell. But I'm biased and believe that programming without (static) types is a dead end.13/06 12:30
augurand a lot of the SICP type stuff will be pointless to translate over, since a lot of SICP revolves around roll-your-own ADTs13/06 12:30
auguri suppose this allows me the opportunity to talk about some more mathematical stuff tho13/06 12:31
xplatsomeone actually started a haskell translation of SICP13/06 12:40
xplati don't know how far along it is13/06 12:41
auguroh?13/06 12:47
joe6xglat, how are you doing?13/06 18:06
joe6xplat, just wanted to let you know that your suggestion to use gperf has proven to be a godsend.13/06 18:20
xplatjoe6: cool, i'm glad it worked out13/06 18:21
joe6xplat, thanks again for taking the time to understand my problem and for helping me out.13/06 18:24
djahandarieWe haven't seen xglat for days. I suspect he's been killed by xplat.13/06 18:30
joe6djahandarie: yes, typo.. sorry about that.13/06 18:33
joe6the agda mailing list has been pretty busy these few days..13/06 18:33
copumpkinxplat: wanna put categories on the agda org on github?13/06 20:28
copumpkinI sent something to the mailing list to that effect, too13/06 20:35
sshccopumpkin: I'm still learning Agda, and I have a few questions about your library if you don't mind taking the time to answer them: in "record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where", does "(o ℓ e : Level)" expand to "(o : Level) (ℓ : Level) (e : Level)"?13/06 20:45
Saizansshc: yep13/06 20:46
sshc"    Obj : Set o13/06 20:46
sshc^ Why is "Set" being applied with a parameter?13/06 20:46
sshcShouldn't that be of the form "Cons : Set"?13/06 20:49
augurwargle13/06 20:49
augurmoin copumpkin13/06 20:49
copumpkinyo13/06 20:49
copumpkinsshc: that's universe polymorphism at work13/06 20:49
copumpkinSet o is "set at universe level o"13/06 20:49
guerrillasshc: Set0, Set1, etc are the same as Set zero, Set (suc zero), etc.13/06 20:54
copumpkinjust don't ask what the type of Set (as a function) is13/06 20:54
sshcInteresting.  This only applies specially to "Set", right?13/06 20:55
guerrillahe made it so this function works at various levels...13/06 20:55
copumpkinsshc: yeah13/06 20:55
copumpkinSet on its own is just Set013/06 20:55
copumpkinit's kind of wonky13/06 20:55
guerrillacopumpkin: ⊔ is max, right? and doing it this is gives you the same results as cumulativity, right?13/06 20:56
sshcMm.  Thanks.13/06 20:56
sshcAh, good, there's this: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.UniversePolymorphism13/06 20:56
copumpkinguerrilla: it's typically called lub13/06 20:56
copumpkinbut yeah, basically13/06 20:56
guerrillaleast upper bound, ok, cool13/06 20:56
copumpkinnot same results as cumulativity13/06 20:56
guerrillaoh ok13/06 20:56
copumpkinit just lets me get into the right universe13/06 20:57
guerrillayeah13/06 20:57
sshcor,13/06 20:57
sshcWas this mentioned in the tutorial?13/06 20:57
copumpkinnope13/06 20:58
sshcI don't recall seeing it13/06 20:58
copumpkinit was added after the tutorial was written13/06 20:58
sshc'k.13/06 20:58
xplatwithout cumulativity, every type is in a specific universe13/06 21:03
xplatlub helps you figure out which is the right universe for a composite, universe-polymorphic type13/06 21:03
copumpkinone thing I had trouble with, for example13/06 21:03
xplateven with cumulativity, though, you would still need something like lub so you could find the smallest universe your type exists in13/06 21:04
copumpkinmaybe I was just dumb back when I tried this13/06 21:04
copumpkinwrite a function that generates N-ary functions of (A : Set a) inputs and (B : Set b) output13/06 21:04
copumpkinN-ary : {a b : Level} -> Nat -> Set a -> Set b -> Set (suc (a \lub b))13/06 21:05
xplatof course, now there's example code for n-ary stuff in the library13/06 21:05
copumpkinoh, I see what I was doing wrong13/06 21:06
copumpkinhe has a helper function13/06 21:06
copumpkinfor determining the level of the output13/06 21:06
copumpkinso clever13/06 21:06
copumpkincopumpkin--13/06 21:06
xplatisn't the type of Set as a function Set : (l : Level) -> Set (suc l) ?13/06 21:08
xplatthis is a valid type, although it's not about to pass the termination checker, or maybe even the scope checker13/06 21:08
sshc"_»_ : {n : Nat} -> Vec Set n -> Set -> Set13/06 21:10
sshc[]        » tt = tt13/06 21:10
sshc(t :: ts) » tt = t -> (ts » tt)13/06 21:10
copumpkinxplat: yeah, you're right13/06 21:10
sshc" What's wrong with the type here?13/06 21:10
copumpkinxplat: now, what's the type of that?13/06 21:10
sshc"Set₁ != Set"13/06 21:11
copumpkinsshc: your types don't fit13/06 21:12
copumpkinmake the return type Set113/06 21:12
copumpkinor Set\_113/06 21:12
sshc^ This is my attempt at translating the pseudo-Haskell code on page 3 of "Faking dependently-typed programming" to Agda13/06 21:12
sshcs/programming"/programming in Haskell"/13/06 21:12
copumpkinit's almost correct, it just doesn't quite fit :)13/06 21:13
sshccopumpkin: I don't understand.  "_»_ : {n : Nat} -> Vec Set n -> Set -> Set1" reults in the same error13/06 21:13
Saizansshc: maybe the problem is that tt is the constructor for the unit type13/06 21:14
augurcopumpkin: X Y : Set gives you X -> Y : Set13/06 21:14
augurso the return type should be a set13/06 21:14
SaizanSet should be fine as the result type13/06 21:14
copumpkinyeah, you're right13/06 21:16
sshcSaizan: Thta doesn't seem to be the problem13/06 21:16
copumpkinit typechecks fine here13/06 21:16
copumpkinoh, I know what the problem is13/06 21:16
copumpkinyour Vec isn't universe-polymorphic13/06 21:16
copumpkinso it can't contain Set13/06 21:16
copumpkinback in the bad old days, we'd use Data.Vec113/06 21:17
copumpkinor something like that iirc13/06 21:17
sshc228 data Vec (a : Set) : Nat -> Set where13/06 21:17
sshc229     []   : Vec a zero13/06 21:17
sshc230     _::_ : {n : Nat} -> a -> Vec a n -> Vec a (succ n)13/06 21:17
copumpkinyeah13/06 21:17
copumpkinpassing Set to Vec doesn't work, cause Set : Set113/06 21:17
sshcHow can I define "Vec" universally polymorphically?13/06 21:18
copumpkindata Vec {woof} (a : Set woof) : Nat -> Set where13/06 21:19
copumpkinmake sure you have {-# OPTIONS --universe-polymorphism #-} at the top13/06 21:19
copumpkinand have imported Level13/06 21:19
xplat{-# WAVEOFFERINGS --rubber-chicken #-}13/06 21:21
sshcThat pragma seems.. non-standard-y unportable-ish, like {-# OPTIONS_GHC broda #-313/06 21:21
copumpkinthere's only one agda implementation anyway :)13/06 21:21
xplatsshc: Agda isn't standardized, so no problem :)13/06 21:22
copumpkinagda201913/06 21:23
sshc"{woof}" looks odd.  Are you sure that shouldn't be "{woof : Nat}"?13/06 21:23
xplat{woof : Level} if anything13/06 21:23
sshcImport level?  I can't use my own definition of "Nat"?13/06 21:23
sshc(Level is Nat, right?)13/06 21:23
copumpkinit's not the same thing13/06 21:23
copumpkinit looks just like Nat :)13/06 21:23
copumpkinbut I don't think you're allowed to use Nat there13/06 21:24
xplatbut the Level is not needed because the only possible argument to Set is a Level13/06 21:24
sshc% grep -nri "data.*level" . -A913/06 21:24
sshc./Support.agda:7:data Level : Set where13/06 21:24
sshc./Support.agda-8-  zero : Level13/06 21:24
sshc./Support.agda-9-  suc  : (i : Level) → Level13/06 21:24
sshcThe htree BUILTIN pragmas below seem relevant13/06 21:25
xplatthey are13/06 21:25
xplatthat's what allows you to feed Level arguments to Set13/06 21:25
sshcIf I use "{woof}" (is that ever allowed?), can the Level type be implied with implying it?13/06 21:26
xplatand they also allow the typechecker to treat Level constraints specially13/06 21:26
* sshc doesn't like "suc", because "succ" is consistent in its length and is named just like Haskell's "succ"13/06 21:26
xplatyou can call zero and suc for levels whatever you want as long as you use the right pragmas13/06 21:27
sshcs/with implying it/without defining it/, I mean.13/06 21:27
guerrillaxplat: thanks for that explanation, sorry I was afk for a momenet.13/06 21:27
xplatzero and suc, zero and succ, level-zero and level-succ, ground and upstairs13/06 21:27
copumpkinsshc: yeah, you can leave out the type and ask it to infer them13/06 21:27
copumpkinusually you need a forall in front of it13/06 21:28
copumpkinbut not on data declarations13/06 21:28
xplator module declarations13/06 21:28
guerrillaxplat: yeah, in cumulativity usually there is a relation defined axiomatically usually represented by \preceq13/06 21:28
sshccopumpkin: Okay.  Now can I do that without actually defining Level?13/06 21:28
copumpkinno13/06 21:28
copumpkinwhen it sees something get passed to Set13/06 21:28
copumpkinit goes and looks for what's attached to the builtin level13/06 21:28
xplatcopumpkin: actually, yes, you can do that without defining Level13/06 21:28
copumpkinreally?13/06 21:29
copumpkinweird :o13/06 21:29
xplatbut then you can't really refer to it much13/06 21:29
copumpkinwhat's the type of the data type then?13/06 21:29
xplatcopumpkin: it seems to work on Don't Ask, Don't Tell13/06 21:29
copumpkinlol13/06 21:29
copumpkinsound principles!13/06 21:29
guerrillasshc/copumpkin.. cool trick for n-ary functions, very clever13/06 21:30
xplati think what happens actually is that the builtin Level type already exists13/06 21:31
xplatit just doesn't have a name for itself or its constructors and such13/06 21:32
djahandarieIt's defined in the standard library13/06 21:32
djahandarieIn Data.Level or something13/06 21:32
guerrillajust Level13/06 21:32
djahandarieYeah, just Level13/06 21:32
guerrilladjahandarie: see my /msg btw?13/06 21:32
xplatthe pragmas tell the compiler to instantiate the type and associated constructors and functions from an isomorphic type to the preexisting Level stuff13/06 21:33
guerrillaexplains our confusion the other day13/06 21:33
xplatso without it, Level basically acts like a type that's been defined out of scope13/06 21:33
copumpkininteresting13/06 21:33
djahandarieguerrilla, didn't get it for some reason13/06 21:34
sshccopumpkin: categories takes hours to build for me, by the way13/06 21:34
guerrilladjahandarie: ok, just a moment13/06 21:34
copumpkinsshc: you typechecking the Everything.agda?13/06 21:34
sshccopumpkin: Yes13/06 21:34
copumpkinit's pretty heavy to typecheck some of the modules :)13/06 21:34
copumpkinespecially the Monoidal stuff, but it's a lot better than it used to be13/06 21:34
copumpkinhave you pulled recently? xplat fixed it to use way less memory13/06 21:35
xplatit helps in that case to interrupt it after the first hour, reload agda (C-c C-x C-r) and start it checking again13/06 21:35
sshcI think the modules in which Power sets (I think; might be something similar) are defined take a long time13/06 21:35
copumpkinI also started moving away from nested sigmas for some things like slice and arrow categories13/06 21:35
copumpkinthere are still a couple of places I use them though13/06 21:35
guerrillaxplat: do you know why?13/06 21:36
xplatguerrilla: not really, a long build uses more memory than a series of smaller builds but i have no idea why that is the case13/06 21:38
guerrillaxplat: maybe we could add in a re-start on a timer.. just as a temporary hack13/06 21:39
xplatsshc: Category.Power.NaturalTransformations takes a long time13/06 21:39
sshcxplat: That was one, yes13/06 21:39
xplatalthough not as long as a few other things13/06 21:39
sshcI wonder why this is wrong13/06 21:40
sshc240 data Vec {universe : Nat} (a : Set universe) : Nat -> Set where13/06 21:40
sshc241     []   : Vec a zero13/06 21:40
sshc242     _::_ : {n : Nat} -> a -> Vec a n -> Vec a (succ n)13/06 21:40
xplatif Category.Power takes a long time then either your agda is slowing down or you really don't have enough memory for this13/06 21:40
Saizanthe simplest explanation is that it doesn't "garbage collect" unneeded modules13/06 21:40
sshcAgdaBasics.agda:242,5-5513/06 21:40
sshcThe type of the constructor does not fit in the sort of the13/06 21:40
sshcdatatype, since Set universe is not less or equal than Set13/06 21:40
sshcwhen checking the constructor _::_ in the declaration of Vec13/06 21:40
sshcxplat: That one was slow too13/06 21:40
Saizansshc: it needs to be  data Vec {universe : Nat} (a : Set universe) : Nat -> Set universe where13/06 21:41
xplatcopumpkin: btw, for \<_\>,\<_\> , i don't think it would be improved by losing the outer brackets13/06 21:41
sshcAh, thaks13/06 21:41
guerrillasshc: you want universe : Level13/06 21:42
sshcguerrilla: I defined my own Level type13/06 21:42
guerrillayou can't do that13/06 21:42
xplatguerrilla: yes you can13/06 21:42
guerrillaxplat: what?13/06 21:42
guerrillaserious?13/06 21:42
xplatas long as you have the right pragmas13/06 21:42
sshc230 {-# BUILTIN LEVEL     Nat  #-}13/06 21:42
sshc231 {-# BUILTIN LEVELZERO zero #-}13/06 21:42
sshc232 {-# BUILTIN LEVELSUC  succ #-}13/06 21:42
guerrillaoh oh ok13/06 21:42
guerrillasorry, i didnt catch that part13/06 21:43
guerrillai thought you meant just a Nat data.13/06 21:43
xplatthe reason they are usually separate from Nat, though, is that Nat usually is given its own pragmas that let it be represented efficiently as an Integer in the underlying runtime13/06 21:43
sshcI see13/06 21:44
djahandarieBut Levels don't need to be efficient because there's no way someone would use like 15 of them right?13/06 21:44
xplatif you try to use the same type as Nat and Level your arithmetic will be hurtin'13/06 21:44
sshcSaizan: Polymorphisizationizing Vec seems to make some definition that use it with forall not work ("unsolved metas")13/06 21:44
xplatdjahandarie: well, it's more like Levels are optimized to be efficient at different things13/06 21:44
guerrillaxplat: next question.. how are Levels not metatheoretic?13/06 21:45
djahandariesshc, conjugation fail?13/06 21:45
xplatspecial constraint solver for constraints built with suc and \lub13/06 21:45
Saizansshc: that's probably because the universe level can't be deduced from the context13/06 21:45
xplatguerrilla: ?13/06 21:46
guerrillaxplat: wel, how can a Set depend on something of type Set?13/06 21:46
sshcdjahandarie: I'd says so.13/06 21:46
xplatguerrilla: a Level is basically just a name for a universe.  unary Set turns the name into a real universe.13/06 21:47
xplator rather, it finds the actual universe that you asked for by name13/06 21:48
guerrillahmm ok, im used to seeing Level defined as a natural number in the axioms of the underlying type theory13/06 21:48
guerrillayes, the latter makes sense13/06 21:48
guerrillamaybe i'll have to look at the source code. was there a paper on how this was done?13/06 21:49
Saizanpushing metatheoretic notions down into the object language is quite trendy in type theory, anyway13/06 21:49
* augur levitates13/06 21:51
guerrillaSaizan: i've seen quite a bit of that internalising lately too13/06 21:51
guerrillai havent finished the reading about that, but im not 100% convinced it doesnt lead to inconsistency at some point13/06 21:51
augurwhat, noone got that reference?13/06 21:51
guerrillaaugur: ah, thats the paper, eh?13/06 21:52
augurin which a full algebraic type system is implemented by pushing it down into just core types in the underlying language13/06 21:53
auguri dont know if they have a way of distinguishing isomorphic types tho13/06 21:54
augurer.. super-isomorphic types!13/06 21:54
augurnot only are the sets isomorphic, but there are isomorphisms for the elements too13/06 21:54
augurF X = 1 + A*X   vs   G X = 1 + A*X13/06 21:55
augurthis is ofcourse possible in haskell, agda, etc.13/06 21:55
augurwhere F != G13/06 21:55
augurbut if you levitate, F = G trivially13/06 21:55
guerrillahmm augur , its "The Gentle Art of Levitation", right? abstract seems to fit13/06 22:00
guerrillabut brb, must eat or will die13/06 22:00
auguryes13/06 22:00
guerrillaaugur: looks promising, but no mention of the word "consistent"13/06 22:38
guerrilla(didn't start reading, just searched)13/06 22:38
augurguerrilla: its as consistent as the underlying logic i think13/06 22:43
guerrillaaugur: ok, interesting. i'm still skeptical though, which won't change until i muster the energry to tackle this :)13/06 22:45
guerrillathese internalisations are not easy for me to wrap my head around13/06 22:46
guerrillai do beleive in internalisation, it has to be the future. i just want a proof that it works.13/06 22:46
--- Day changed Tue Jun 14 2011
copumpkinxplat: I wrote a couple of diagonal functors14/06 06:24
copumpkinand also started writing functors for "partially applied" products, both ways14/06 06:29
copumpkinwasn't sure what to call those though14/06 06:29
Johndkwhat's this14/06 08:32
Eduard_MunteanuThis is AGDAAA!14/06 08:34
Johndkok good14/06 08:34
Johndkwhat's agdaaa?14/06 08:34
Eduard_MunteanuJohndk: see the topic, /topic14/06 08:35
Johndklol so you understand this shit?14/06 08:36
Eduard_MunteanuPut shortly, it's a dependently-typed language / theorem prover with syntax partly inspired by Haskell.14/06 08:36
Johndkah14/06 08:37
Johndkscience14/06 08:37
Eduard_MunteanuJohndk: I'm curious, how did you get here?14/06 08:38
Johndkpicked a room randomly14/06 08:38
Eduard_Munteanu:)14/06 08:38
augurahaha14/06 09:34
augurjohndk has a nice way of exploring irc14/06 09:34
xplatweird.  i thought i had already pushed my stdlib port of categories, but i don't see evidence of it on github ...14/06 12:08
augurhuh. ccshan follows copumpking on twitter14/06 12:25
augurcrazy14/06 12:25
augurwow14/06 12:27
augurhe also follows travis14/06 12:27
augurwtf14/06 12:27
augurand jimmy lin14/06 12:27
augurmaybe hes a strong reciprocalist14/06 12:28
xplatcopumpkin: okay, NOW my port stuff is pushed.  it was a branch but i mistakenly only pushed master before14/06 14:24
copumpkincool :)14/06 14:24
copumpkinwas wondering actually14/06 14:24
copumpkinhave any ideas where to put those product functors?14/06 14:24
xplatyou should have said something!  :714/06 14:25
xplatmaybe Categor{y,ies}.Functor.Product?14/06 14:25
copumpkinhmm, that's better than Categories.Object.BinaryProducts.Functors14/06 14:26
copumpkin:P14/06 14:26
copumpkinalso14/06 14:27
copumpkinI think we should start bundling up categories with properties they have in a consistent manner, at some point14/06 14:27
copumpkinnot sure if you've looked at the stdlib14/06 14:28
copumpkinbut the distinction between Monoid and IsMonoid14/06 14:28
xplati haven't looked much at that *part* of the stdlib14/06 14:29
copumpkin:)14/06 14:29
copumpkinwell, I found myself wanting "a category with all binary products"14/06 14:29
copumpkinand had to pass the binary products bit separately from the category14/06 14:29
xplatthe article i read on representing categories with type classes in coq was really down on that kind of bundling14/06 14:31
copumpkinoh yeah?14/06 14:31
copumpkinhmm14/06 14:31
copumpkinmaybe not then14/06 14:31
xplatbecause bundles like that are hard to combine with proper sharing14/06 14:31
copumpkinbut then the functors take a crapload o' arguments14/06 14:31
copumpkinthen I need to pass them a category, the binary products proofs, and an object14/06 14:32
copumpkinah I see14/06 14:32
copumpkinhmm14/06 14:33
xplatit's the same reason you normally pass a Level, a Set, and a value in that set instead of combining some of them with a sigma14/06 14:34
xplat(or rather, the reason you have Sets parameterized by a level instead of a level predicate on sets)14/06 14:35
copumpkinhmm, okay14/06 14:35
xplatoh, the <_>,<_>14/06 14:36
xplatthe idea i had in my head is 'justifications are inside angle brackets, congruences are represented by the same operator as their underlying function, but partly stuck to the outsides of angle brackets'14/06 14:37
copumpkincool, that sounds reasonable14/06 14:38
copumpkinI was wondering if it was worth doing two halves of that one too14/06 14:38
copumpkinlike I have the \o-resp-\==\^l and \^r14/06 14:38
copumpkinthat would just pass refl to the other one14/06 14:38
xplatthis can't possibly work for every mixfix operator because of how the nesting works, but it can work for infix and it can work for infix surrounded by angle brackets14/06 14:38
xplatfor <_>,<_> both of the angle brackets 'belong' to the justifications, while the extra angle brackets from the surroundings become the ones from <_,_>14/06 14:40
xplatwhereas for _>o<_ , the angle brackets on the >o< match with the surrounding ones14/06 14:41
xplat(of course as soon as you need parentheses to decide operator precedence the whole thing explodes, unfortunately)14/06 14:41
copumpkinoh also14/06 14:42
copumpkinwhat should we call the programming-y CT library that will be built on top of all this?14/06 14:42
xplatif you mean what i think you mean, maybe we should use Notion or Idiom or get all traditional and use Control14/06 14:43
copumpkincontrol kind of bothers me, but the other two sound nice14/06 14:44
xplat(Notion seems to be the academically correct word, per papers like Parameterized Notions of Computation)14/06 14:44
copumpkinI was wondering how we might represent CPO\_\bot14/06 14:45
copumpkinor some usable category where initial algebras and terminal coalgebras coincide14/06 14:45
xplathm, yes14/06 14:46
copumpkinotherwise a huge wealth of esoteric *morphisms will be lost to us14/06 14:46
xplati was thinking about that too, because i want to do proofs about Haskell, but i haven't got very far yet14/06 14:46
copumpkinI mean, we could perpetuate the Hask myth14/06 14:47
copumpkinbut then people will wonder why we're missing all the combined fold/unfold thingies14/06 14:47
xplati was actually thinking of doing a small family of Hask categories, where the most basic one doesn't allow recursion at all and the fullest one has general recursion and at least some model of 'execution'14/06 14:48
copumpkinthat'd be neat14/06 14:49
copumpkinthere is that partiality monad14/06 14:49
copumpkinwe could look into adapting the ideas there14/06 14:49
xplatso that 'morally correct' reasoning could be used and would carry its domain of applicability along with it14/06 14:49
xplatdo you have a reference for the partiality monad?14/06 14:52
copumpkinhttp://www.cse.chalmers.se/~nad/listings/lib/Category.Monad.Partiality.html#114/06 14:58
copumpkinit's basically a coinductive iteratee with no input14/06 14:58
xplatheh, i didn't think there was one in the stdlib14/06 15:01
xplatamazing what you can find in there if you look14/06 15:01
copumpkinthere's all sorts of goodies buried in Everything.agda14/06 15:01
copumpkinI've spent ages looking all over it14/06 15:01
Saizanfix is not as simple as fix f = f (fix f) with that, though14/06 15:02
xplati don't think it matters for what we're talking about right now--as long as fix can be written, we could use it to model general recursion in an object language14/06 15:03
copumpkinso anyway, I was reading adjoint folds last night on the plane14/06 15:35
copumpkinand it actually talks about kan extensions in the context of programming languages!14/06 15:35
copumpkinit's also fairly easy to follow14/06 15:35
Saizanare you using it somewhere?14/06 15:40
copumpkinnope14/06 15:41
copumpkinjust felt like reading something on the plane14/06 15:41
copumpkinalso wrote some boring CT functors while I was on the plane14/06 15:41
dpiponiIn the last line of http://hpaste.org/47793 the [_,_] expressions gets marked yellow. I can't see why. Seems like a trivial ⊎-elimination to me. Anyone able to help?14/06 16:02
Saizant might be because it can't infer the "motive"14/06 16:03
Saizan*it14/06 16:03
Saizani.e. the (P : A ⊎ B -> Set l) argument14/06 16:04
Saizanthe goals buffer should tell you more about the types of unsolved metas14/06 16:06
copumpkinxplat: is the other branch ready for switching? it looks like there's some stuff missing, unless you moved it around14/06 16:11
xplatcopumpkin: i probably moved it around, but just for safety's sake, you can ask me about the specific items14/06 16:12
copumpkinthings like Terminal objects, iirc14/06 16:12
copumpkinbasically, a lot of the red items in here: https://github.com/xplat/categories/compare/port14/06 16:12
xplatCategories/Object/Terminal?14/06 16:12
copumpkinmany of them were empty anyway14/06 16:12
copumpkinwhich are fine to remove14/06 16:12
copumpkinbasically all the things with largeish numbers of lines here: http://snapplr.com/xavh14/06 16:13
copumpkinoh14/06 16:14
copumpkinit just didn't recognize the rename14/06 16:14
xplata lot of the smaller files had too many changes relative to their size to be recognized as moved versions of their prior versions14/06 16:14
copumpkinI see14/06 16:14
xplatwhich weirded me out since i used git mv for everything, but whatever14/06 16:14
xplati wonder if it would have done better if i'd committed before i moved.  i might have believed too much of git's own hype about history-insensitivity...14/06 16:16
xplater, not before i moved, after i moved but before i edited14/06 16:16
copumpkinI think git mv is just a move followed by a git add14/06 16:16
copumpkinit still uses heuristics to detect renames14/06 16:16
xplatparticularly, all the files with one line had that line changed to match their paths14/06 16:17
copumpkinyeah14/06 16:17
copumpkinthose are kind of silly to keep around anyway, but one day I'll get around to filling them in14/06 16:17
xplateven files like Categories/Enriched had so many imports and opens changed that they don't register as the same file14/06 16:19
xplat(all imports were changed in every file, in fact)14/06 16:19
xplat(and every ‘open Category.Category foo’14/06 16:20
copumpkinyeah14/06 16:23
copumpkinwe need an agda refactoring tool!14/06 16:23
copumpkinmaybe something to work on during hac phi :)14/06 16:23
xplatmaybe14/06 16:24
xplatCategories.Product probably needs a cleanup14/06 16:24
copumpkinah14/06 16:25
xplatjust killing all the stuff that's commented out14/06 16:25
copumpkinI looked at your Power stuff for the first time in a while yesterday14/06 16:25
copumpkinit's impressive :)14/06 16:25
xplatheh, thanks.  it wasn't that impressive the first 3 times :)14/06 16:25
copumpkinlol14/06 16:25
copumpkinit seems like we should have some way of transforming it to and from a functor from a discrete category14/06 16:26
xplatyeah, maybe i'll add that14/06 16:27
xplatit doesn't sound too hard14/06 16:29
xplatcopumpkin: should i push the new version of Categories/Product.agda (sans commented-out stuff)?14/06 17:07
copumpkinsure14/06 17:09
copumpkinthere are various places I commented out stuff14/06 17:09
copumpkinfeel free to get rid of it any time you see it14/06 17:09
xplatwell, i don't want to do anything on this branch that's less related to porting than any of what i've already done, but i'll keep it in mind for later14/06 17:11
xplatpushed14/06 17:13
xplatthe new version has no lambdas and no functions defined in wheres14/06 17:13
xplata rare example of where i was able to abstract agda code to the level i'm used to with haskell14/06 17:14
copumpkinvery nice14/06 17:16
starcloudedhello everybody14/06 18:01
starcloudedI just trying to compile a program using agda -c Database_con.agda but it throws an error "MAlonzo/Data/Maybe/Core.hs:9:17:14/06 18:04
starclouded    Could not find module `Database.HDBC.PostgreSQL.Connection':14/06 18:04
starclouded      it is a hidden module in the package `HDBC-postgresql-2.2.3.3'14/06 18:04
starclouded      Use -v to see a list of the files searched for."14/06 18:04
starcloudedany ideas?14/06 18:04
guerrillaanyone ever seen an example of equirecursive types where inferring of the type (\mu x . B) would infer to the type of B instead of just a sort?14/06 18:25
guerrillas/infer to/result in14/06 18:25
guerrillalike (\mu x . B) : typeOf(B) instead of (\mu x . B) : Type14/06 18:26
guerrillaor have a reason why that is a bad idea?14/06 18:40
guerrillafor example, http://hpaste.org/4780314/06 18:43
guerrillaso, i retract my hpaste in favor of the this rule: http://hpaste.org/4780614/06 19:56
guerrillaand Saizan says, this introduces the ability to define non-regular types14/06 19:57
xplati wrote this function:14/06 20:13
xplat  map⁎ : ∀ {a b p q} {A : Set a} {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) → (v : Σ A P) → Σ (B (proj₁ v)) (Q (proj₂ v))14/06 20:13
xplat  map⁎ f g (x , y) = (f x , g y)14/06 20:13
xplatbut it seems like Q can hardly ever (never?) be inferred, probably because of the nonlinear use of x14/06 20:14
xplatis there some way around that?14/06 20:15
c0pumpkinit seems like it could only be inferred if the return type is fixed14/06 20:24
c0pumpkinnothing else seems to really determine Q14/06 20:25
c0pumpkinright?14/06 20:25
xplatit seems like the second argument (after f) could determine Q14/06 20:34
xplat(∀ {x} → (y : P x) → Q y (f x))14/06 20:34
xplati guess it would be hard to factor the builtin f out of that though14/06 20:36
xplatis there a better way to write the bimap of dependent functions over a sigma?14/06 20:37
copumpkinxplat: how would it determine it?14/06 20:42
copumpkinmaybe you're right, hmm14/06 20:43
copumpkinugh14/06 20:43
xplatwhen i actually used it i ended up punting and writing a version that sacrifices dependency in the sigma for dependency in the pis14/06 20:44
copumpkinah14/06 21:04
copumpkinman, I can't wait for some hardcore agda hax at hac phi14/06 21:07
djahandarieWait, is xplat coming?14/06 21:11
copumpkinI hope so14/06 21:11
copumpkinxplat: I've forked categories to the agda organization on github, so it feels more "official" now :P14/06 22:12
copumpkinI'll still be doing most of my development on my own fork though14/06 22:12
xplatwell, i've got functors exp->functor and functor->exp14/06 22:32
copumpkinoh nice14/06 22:32
copumpkindid you see my lame diagonal addition?14/06 22:32
xplati have yet to prove these sufficiently inverse-y14/06 22:33
xplatoh, is that checked in now?14/06 22:33
copumpkinI was thinking of making the usual sequence of adjunctions14/06 22:33
copumpkinyeah14/06 22:34
copumpkinbut I'm not sure where to put those adjunctions14/06 22:34
copumpkinI hate organizing code :(14/06 22:34
xplathey, cool, you have the Power version of the diagonal too14/06 22:37
copumpkinit almost  feels like we should just make plain old binary products be instances of Power :P14/06 22:37
copumpkinbut that might get annoying14/06 22:38
xplati think it might, yeah14/06 22:38
xplatadjunctions in Categories.Functor.{Product,Coproduct}.Properties maybe?14/06 22:39
copumpkinoh, fair enough14/06 22:39
copumpkinman, them there module hierarchies are getting deep14/06 22:39
djahandarieI heard you like modules so I put a module in your module so you can modularize while you modularize14/06 22:41
copumpkinI'd like to play with abstract definitions of structures with "view" records of them14/06 22:41
copumpkinif that makes any sense14/06 22:42
xplatit probably does, with enough context14/06 22:42
copumpkinmaybe I'll play with that idea on the Adjunction module14/06 22:42
copumpkinwell let's say14/06 22:42
djahandarieLike ViewL and ViewR in Seq?14/06 22:42
copumpkinan Adjunction is an abstract entity14/06 22:42
copumpkinyou can't look inside it, and we implement it as we please14/06 22:42
copumpkinthen the adjunction module exports two (or more?) modules inside it14/06 22:43
copumpkineach of which has record in it14/06 22:43
copumpkinand that record is either the unit/counit set of fields14/06 22:43
copumpkinor the hom-set correspondence thing14/06 22:44
copumpkinnow, you can provide either of those two records, and get an (abstract) adjunction14/06 22:44
copumpkinand the abstract adjunction can be converted to either of those, if you want one particular view of it14/06 22:44
copumpkinthe abstract adjunction also lets you pull monads or comonads out of it14/06 22:44
copumpkinand do other representation-agnostic stuff14/06 22:44
copumpkinthen we could do something similar with monads14/06 22:45
copumpkinwith the various ways of getting a monad14/06 22:45
xplathm, that does have some appeal14/06 22:45
copumpkinand other structures that have multiple "definitions"14/06 22:45
copumpkinit'd make this feel more like a "programming" library14/06 22:45
copumpkinwith abstract definitions and such14/06 22:45
copumpkinand it'd let us choose the easiest representation for our own proofs14/06 22:46
copumpkinand let other modules rely only on an external interface14/06 22:46
copumpkinwhich could be either of the views of adjunctions14/06 22:46
copumpkinin practice the adjunction would probably be implemented as one of those views14/06 22:46
copumpkinso the translation would  be id for one of them14/06 22:46
copumpkinI dunno14/06 22:48
copumpkinit might get unwieldy14/06 22:48
copumpkinbut it feels more principled somehow14/06 22:48
* copumpkin crazytalk14/06 22:48
xplati should actually know this, since i touched EVERY SINGLE FILE four days ago, but is there anything that represents an isomorphism of categories?14/06 22:51
copumpkinan Iso in Cat?14/06 22:52
copumpkinbut nothing explicit, no14/06 22:52
xplatah, that's what i thought it might be14/06 22:52
copumpkinsubcategories and the like would also be nice to have14/06 22:53
copumpkinor subobject-like things in generla14/06 22:53
copumpkingeneral14/06 22:53
copumpkinis http://en.wikipedia.org/wiki/Subobject a common definition?14/06 22:57
xplatcopumpkin: actually, i don't think an Iso in Cat will work.  i think because of a lack of commutativity the two representations might not be in a common instantiation of Cat14/06 23:01
xplat*lack of cumulativity14/06 23:01
copumpkinoh14/06 23:01
copumpkintrue14/06 23:01
copumpkinwe could make lots of noise on the mailing list and bug them to implement cumulativity :P14/06 23:02
xplatthen again, maybe i screwed something up14/06 23:02
Eduard_Munteanucopumpkin: hrm, I saw Awodey define a subobject as a mono going into that object.14/06 23:02
copumpkinwell, I think one of the issues with a functor from discrete was the fact that the universes weren't very polymorphic14/06 23:02
copumpkinright?14/06 23:03
Eduard_MunteanuWhich kinda makes sense if you think of equalizers as defining particular subsets.14/06 23:03
Eduard_MunteanuThe Wikipedia stuff seems a bit contrived though.14/06 23:04
xplatcopumpkin: yes14/06 23:05
copumpkinwe could always just make Discrete more polymorphic14/06 23:05
copumpkinand use lifted equalities or something14/06 23:05
xplatthe definition of subobject i'm familiar with is an equivalence class of monos14/06 23:05
xplatcopumpkin: the problem, if there is one, is coming from Functors14/06 23:05
copumpkinoh14/06 23:06
Eduard_MunteanuOr that, yeah.14/06 23:06
xplatcopumpkin: it looks like the object level for Functors (Discrete I) C might be e \lub (\ell \lub o) for some reason14/06 23:07
xplatit's hard to tell because they're specified as _ in Functors.agda14/06 23:07
copumpkinoh :P14/06 23:08
copumpkinyou might be right14/06 23:08
xplatoh, right, it's e \lub (\ell \lub o) because actual functors have to deal with all the pieces so they will live at that level14/06 23:09
xplatcopumpkin: i looked at the wikipedia definition, and yes, i think that's the common concept14/06 23:15
xplatin practice you indicate a subobject with a mono since the equivalence classes may not be small, so in agda one would create a setoid of them i guess14/06 23:17
copumpkinyeah14/06 23:22
xplatit doesn't seem like you could even make a cumulative universe manually, come to think of it14/06 23:24
xplatat least, i can't think how to make a type 'sets of level up to n'14/06 23:25
xplatwell, maybe as an indexed data family14/06 23:25
xplatactually i think that could work14/06 23:26
xplatmaybe i'll try it later and see if i can come up with an enhanced Cat14/06 23:27
copumpkinooh14/06 23:27
copumpkinxplat: wanna join the agda organization on github?14/06 23:38
copumpkinalso, is it worth merging the port branch in now?14/06 23:41
copumpkinso we don't do more work on the obsolete structure14/06 23:42
--- Day changed Wed Jun 15 2011
starcloudedanyone could help me to make a connection to a database?15/06 00:14
copumpkinisn't that basically a haskell question?15/06 00:20
copumpkinI don't think anyone in here has ever used databases in agda :P15/06 00:20
copumpkinbut you can try and wait and see if anyone responds :)15/06 00:20
Eduard_MunteanuYou're basically asking how to write a binding, no?15/06 00:22
starcloudedyes, a binding to a database15/06 00:25
Eduard_Munteanustarclouded: did you pick a Haskell binding to use?15/06 00:29
Eduard_MunteanuYou'll have to go through Haskell (or through C if you're using the Epic backend)15/06 00:30
starcloudednot sure what you're asking15/06 00:33
Eduard_Munteanustarclouded: suppose you were using Haskell, and wanted to connect to a database. How would you do it?15/06 00:37
Eduard_MunteanuYou'd use some package that supplied a binding, right?15/06 00:38
starcloudedyes15/06 00:39
starcloudedI am using HDBC15/06 00:39
Eduard_MunteanuOk. Now you have to write a binding to HDBC from Agda.15/06 00:39
starcloudedthe thing is how can I use a type like connection? in the power of pi wouter and nicolas "The constructors of the Connection type are not visible to the library’s users"15/06 00:42
Eduard_MunteanuWell besides HDBC itself you also need the HDBC drivers (i.e. package) for the particular kind of database you want to access.15/06 00:45
Eduard_Munteanue.g.  http://hackage.haskell.org/package/HDBC-mysql15/06 00:46
starcloudedyes, I am using DHBC-PostgreSQL15/06 00:46
Eduard_MunteanuOk, so you have for example    connectPostgreSQL :: String -> IO Connection15/06 00:48
Eduard_MunteanuYou'll have to access that function from Agda.15/06 00:48
starcloudedbut for using that connectPostgreSQL Do I need something of type IO Connection?15/06 00:52
starcloudedno?15/06 00:52
copumpkindo you understand how to write this code in haskell?15/06 00:53
Eduard_MunteanuNo, look at the type. It *gives* you a IO Connection15/06 00:53
starcloudedI am watching the IO.Primitive and in there I need to define something of type Unit, for example for using the putStrLn function, putStrLn    : Costring → IO Unit15/06 00:57
Eduard_Munteanustarclouded: Unit is something isomorphic to ()15/06 01:00
starcloudedok then what is something isomorphic to Connection?15/06 01:01
Saizanyou can "postulate Connection : Set" on the Agda side15/06 01:01
Eduard_MunteanuWell, you'll use a COMPILED_TYPE pragma to relate Agda's Connection to the Haskell one15/06 01:01
Eduard_MunteanuAnd a postulate, yeah.15/06 01:02
Eduard_MunteanuHave you seen examples on how to write FFI bindings in Agda?15/06 01:03
starcloudedyes, I think this is the page http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.FFI , but I try to do the example of list and it throws me an error15/06 01:06
Eduard_MunteanuAgda libs might prove useful too, for example see: http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/InteractivePrograms.IOGraphicsLib.html15/06 01:06
Eduard_MunteanuWhat error? Maybe you can pastebin.15/06 01:07
starcloudedin the page I mentioned the list example is {-# COMPILED_DATA http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/Data.List.html#632 [] (:) #-} but the correct is {-# COMPILED_DATA http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/Data.List.html#632 [] [] (:) #-} according with the code of the interxtivePrograms15/06 01:10
Eduard_MunteanuI think {-# COMPILED_DATA List [] [] (:) #-} is wrong15/06 01:14
starcloudedlook http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/Data.List.html#16915/06 01:15
Eduard_MunteanuWell that doesn't mean it isn't wrong :)15/06 01:18
Eduard_MunteanuWhy would '[]' occur twice anyway?15/06 01:18
Eduard_MunteanuList has only two constructors.15/06 01:19
copumpkinone is the type-level15/06 01:23
Eduard_MunteanuWouldn't that go into a COMPILED_TYPE pragma?15/06 01:25
Eduard_MunteanuThat, or the syntax  {-# COMPILED_DATA D HsC1 .. HsCn #-}15/06 01:25
Eduard_Munteanuis wrong.15/06 01:25
starcloudedEduard_Munteanu: but when I wirte postulate15/06 01:33
starclouded  connect : String → IO Connection15/06 01:33
starclouded{-# COMPILED connect connectPostgreSQL #-} and I compile it says that Not in scope: type constructor or class `Connection' and Not in scope: `connectPostgreSQL'15/06 01:33
Eduard_Munteanustarclouded: you need a IMPORT pragma, do you have one?15/06 01:34
starcloudedyes15/06 01:36
starclouded{-# IMPORT Database.HDBC #-}15/06 01:36
starclouded{-# IMPORT Database.HDBC.PostgreSQL #-}15/06 01:36
Eduard_MunteanuI think you need to refer to connectPostgreSQL using the fully-qualified name.15/06 01:38
Eduard_Munteanui.e. {-# COMPILED connect Database.HDBC.PostgreSQL.connectPostgreSQL #-}15/06 01:38
starcloudedTHAT15/06 01:41
starcloudedthanks15/06 01:41
guerrillafunny, Google's results in .pt have been poisoned when searching for "weak head reduction" i keep getting this paper "Games and Weak-Head Reduction for Classical PCF" repeated hundreds of times15/06 04:44
guerrilla.gr and .us don't seem to be affected15/06 04:44
copumpkinxplat: ohai15/06 05:02
xplat| The sort of CumulativeCategory cannot depend on its indices in the type (top : Level) → Set top when checking the definition of CumulativeCategory15/06 15:23
xplatwell, so much for that plan :(15/06 15:23
starcloudedhello everybody15/06 15:39
starcloudedanyone could tell why when I include inside COMPILED pragma a postulate that has a Maybe I get this error The type Maybe cannot be translated to a Haskell type. when checking the pragma15/06 15:41
starcloudedCOMPILED dbConnect Database.HDBC.PostgreSQL.connectPostgreSQL15/06 15:41
Saizanstarclouded: you need a COMPILED_TYPE (or _DATA?) for Maybe first15/06 15:44
starcloudedpostulate15/06 15:46
starclouded  Connection : Set15/06 15:46
starclouded  dbConnect  : String → IO (Maybe Connection)15/06 15:46
starclouded{-# COMPILED_TYPE Connection Database.HDBC.PostgreSQL.Connection #-}15/06 15:46
starclouded{-# COMPILED dbConnect Database.HDBC.PostgreSQL.connectPostgreSQL #-}15/06 15:46
xplatyou need a COMPILED_TYPE or COMPILED_DATA for every type mentioned in dbConnect's type15/06 15:48
copumpkinxplat: yo!15/06 15:49
xplatcopumpkin: did you see the error i pasted?  :(15/06 15:49
copumpkinxplat: nope15/06 15:49
copumpkinwhere?15/06 15:51
Saizani'm pretty sure you can make a function (top : Level) → Set top though15/06 15:51
copumpkinSaizan: yeah, you can15/06 15:51
copumpkinbut if you ask for the type of its type, then it'll complain that it isn't a type15/06 15:51
copumpkinSet\omega15/06 15:51
xplat| The sort of CumulativeCategory cannot depend on its indices in the type (top : Level) → Set top when checking the definition of CumulativeCategory15/06 15:54
copumpkinoh15/06 15:55
copumpkinyeah, I've run into that before15/06 15:55
copumpkinhow were you trying to define it?15/06 15:55
xplatdata CumulativeCategory : (top : Level) → Set top where lift : ∀ {d o ℓ e} → Category o ℓ e → CumulativeCategory (d ⊔ o ⊔ ℓ ⊔ e)15/06 15:58
copumpkinI wonder why it's more strict about not making a Set\omega there than it is for functions15/06 16:00
copumpkinmaybe worth a mailing list post?15/06 16:00
starcloudedin Data/Maybe/Core.agda after the definition of Maybe I add {-# COMPILED_DATA Maybe Maybe Just Nothing #-}15/06 16:02
starclouded and this error is shown `Maybe' is applied to too many type arguments In the type signature for `check9': check9 :: xA -> (Maybe xa xA)15/06 16:02
xplati wonder if the level argument is somehow not being erased there15/06 16:08
xplatin fact, that's exactly what it looks like15/06 16:09
starcloudedWhen I type check this is shown The type .Level.Level.zero cannot be translated to a Haskell type. when checking the pragma COMPILED dbConnect Database.HDBC.PostgreSQL.connectPostgreSQL15/06 16:10
Saizani seem to recall a thread on that on the mailing list15/06 16:10
xplatif you do your own HMaybe type (data HMaybe (A : Set) : Set where { just (x : A) -> HMaybe a ; nothing : HMaybe a }15/06 16:11
xplatthen it should work, although that does not seem ideal15/06 16:11
copumpkinI guess that stuff hasn't been tested since universe polymorphism was added?15/06 16:12
copumpkinxplat: have any objections to me merging in the port branch this evening?15/06 17:15
copumpkintawny15/06 17:16
starcloudedthe same thing that happens with maybe happens with list, so I redefine List in my program but this error is shown The type Σ cannot be translated to a Haskell type. when checking the pragma15/06 17:45
starcloudedCOMPILED describeTable Database.HDBC.PostgreSQL.describeTable15/06 17:45
copumpkinwell, it's right...15/06 17:46
copumpkinSigma can't be made into a haskell type15/06 17:46
starcloudedso how can I refer from agda list to a list in haskell15/06 17:48
starclouded=+15/06 17:48
Eduard_Munteanustarclouded: um are you sure you're doing it right? Some of the code I linked you earlier used lists.15/06 17:56
starcloudedI just did this describeTable : Connection → TableName → IO (dbList Attribute)15/06 17:57
starcloudedand dbList is the same as List but defined in my program15/06 17:58
Eduard_MunteanuThat should do if you supply correct COMPILED_TYPE and COMPILED_DATA pragmas.15/06 17:59
Eduard_MunteanuI'm not sure how you end up with a sigma in there.15/06 17:59
starclouded{-# COMPILED_TYPE Connection Database.HDBC.PostgreSQL.Connection #-}15/06 18:00
starclouded{-# COMPILED describeTable Database.HDBC.PostgreSQL.describeTable #-}15/06 18:00
Saizanhow is TableName defined?15/06 18:01
starcloudedTablaName = String15/06 18:01
Saizanare you sure the error you pasted above is thrown by those lines?15/06 18:01
Saizanoh, also, Attribute?15/06 18:02
starcloudedThe type Σ cannot be translated to a Haskell type. when checking the pragma COMPILED describeTable Database.HDBC.PostgreSQL.describeTable15/06 18:03
starcloudedAttribute  = String × U, with el, U  like the universes defined in the power of pi15/06 18:04
copumpkinso don't use x15/06 18:04
copumpkinwrite your own product that isn't dependent15/06 18:04
Eduard_Munteanudata Pair (A B : Set) -> Set where ...15/06 18:05
Eduard_Munteanu(since x is indeed a sigma)15/06 18:06
Eduard_MunteanuActually that should be a record.15/06 18:06
starcloudedok now that I define the attribute like a record I need to bind it to something in haskell? the thing I need in haskell is something like [(String, SqlColDesc)]?15/06 18:47
Eduard_MunteanuYou need four bindings, for lists, pairs, String and SqlColDesc.15/06 18:56
starcloudedbut can I do a binding of a record type?15/06 19:03
Eduard_MunteanuHrm. I'm unsure how that works.15/06 19:05
Eduard_MunteanuYou might want to try the COMPILED_DATA pragma using the fields instead of constructors (since record only have one constructor).15/06 19:07
Eduard_MunteanuIf that doesn't work you can translate the record to a data.15/06 19:07
Eduard_Munteanudata Pair (A B : Set) -> Set where pair : A -> B -> Pair A B15/06 19:08
Eduard_MunteanuAnd you can define the projections manually   fst : \forall {A B} -> Pair A B -> A   and similarly for snd15/06 19:09
Eduard_Munteanu(e.g.   fst (pair a _) = a  )15/06 19:10
starcloudedEduard_Munteanu: this is what I did first {-# COMPILED_DATA Pair fst snd #-}15/06 19:41
starcloudedthe I postulate SqlColDesc : Set15/06 19:41
starclouded{-# COMPILED_TYPE SqlColDesc SqlColDesc #-}15/06 19:41
starcloudedThe I define the Attribute Attribute = Pair String SqlColDesc15/06 19:42
starcloudedpostulate TableType : dbList Attribute15/06 19:42
starclouded{-# COMPILED_TYPE TableType [(String , SqlColDesc)] #-}15/06 19:42
starcloudedbut when I compile it shows me an error `[]' is applied to too many type arguments15/06 19:43
* copumpkin barfs: _[_][_×-] : ∀ {o ℓ e} → (C : Category o ℓ e) → BinaryProducts.BinaryProducts C → Category.Obj C → Functor C C15/06 19:51
starcloudedany idea?15/06 19:58
Eduard_Munteanustarclouded: did you relate your Pair type to the Haskell (,) ?15/06 20:09
Eduard_MunteanuI think you need a COMPILED_TYPE pragma for that.15/06 20:10
Eduard_MunteanuAlso, I don't think TableType should be a a COMPILED_TYPE15/06 20:11
Eduard_MunteanuTableType : Set     TableType = dbList Attribute15/06 20:12
Eduard_Munteanu(without making that a postulate)15/06 20:12
Eduard_MunteanuAnd shouldn't that be    dbList (Pair String Attribute)   ?15/06 20:13
starcloudedI use that because for using the COMPILED_TYPE pragma I need the postulate15/06 20:13
Eduard_MunteanuBut TableType is merely a synonym for [(String , SqlColDesc)].15/06 20:13
Eduard_MunteanuYou should define it in Agda.15/06 20:14
Eduard_MunteanuScratch the "dbList (Pair String Attribute)" part, "dbList Attribute" is fine.15/06 20:15
Eduard_Munteanucopumpkin: _[_][_×-] : ∀ {o ℓ e} → let open ... in ...15/06 20:19
* Eduard_Munteanu ducks :P15/06 20:19
Eduard_MunteanuI suppose you could use modules for that, say WithCategory.15/06 20:19
copumpkinit's not so much that15/06 20:22
copumpkinit's just having to have the BinaryProducts parameter15/06 20:22
copumpkininstead of a CategoryWithBinaryProducts15/06 20:22
copumpkinbut that has its own issues15/06 20:23
copumpkinmaybe I should make it one of those new fancy implicit thingies15/06 20:23
Eduard_MunteanuMm, you mean letting it pick up a proof the category has all binary products using implicits?15/06 20:24
Eduard_Munteanuerm, non-canonical implicits15/06 20:26
copumpkinyeah, except they aren't called that anymore15/06 20:26
copumpkinbut I can't remember what they are called now15/06 20:26
Eduard_MunteanuFancy implicits? :P15/06 20:26
copumpkinyeah!15/06 20:26
copumpkinfancy implicit thingies15/06 20:26
Eduard_MunteanuHeh.15/06 20:26
* Eduard_Munteanu wishes the stdlib used them15/06 20:27
copumpkinI wish the stdlib even used irrelevance :P15/06 20:28
Eduard_MunteanuYeah, and that's been there for a while.15/06 20:28
starcloudedI am getting this `[]' is applied to too many type arguments no matter what my program is15/06 20:28
Eduard_Munteanustarclouded: where are you using [] ?15/06 20:28
Eduard_MunteanuI don't think you should be using it at all.15/06 20:29
Eduard_Munteanu(erm, except the dbList COMPILED_TYPE/DATA)15/06 20:29
starcloudedI relate my type Pair with haskell using {-# COMPILED_DATA Pair fst snd irc://irc.freenode.net:6667/#-}15/06 20:39
Eduard_MunteanuWhich one, the record or the data variant?15/06 20:40
starcloudeddata15/06 20:40
Eduard_MunteanuI'm not sure if it works with records.15/06 20:40
starcloudeddata Pair (A B : Set) : Set where15/06 20:40
starclouded  _,_ : A -> B -> Pair A B15/06 20:40
Eduard_MunteanuWell, then it's wrong.15/06 20:40
starcloudedwhy?15/06 20:41
Eduard_MunteanuYou can only use constructors there, not your projection functions.15/06 20:42
Eduard_MunteanuI mean in the pragma.15/06 20:42
starcloudedbut I define fst : {A B : Set} -> Pair A B -> A15/06 20:42
starcloudedfst  (a , _)  = a15/06 20:42
starcloudedsnd : {A B : Set} -> Pair A B -> B15/06 20:42
copumpkin[03:42:03 PM] <Eduard_Munteanu> You can only use constructors there, not your projection functions.15/06 20:42
Eduard_Munteanu{-# COMPILED_DATA D HsD HsC1 .. HsCn #-}15/06 20:43
Eduard_MunteanuNow now, who updated the wiki? That HsD wasn't there earlier.15/06 20:43
Eduard_MunteanuAh, NAD.15/06 20:44
starcloudedrecord Pair (A B : Set) : Set where15/06 20:44
starclouded  constructor _,_15/06 20:44
starclouded  field15/06 20:44
copumpkinEduard_Munteanu: he reads the logs in here15/06 20:45
Eduard_MunteanuNeat.15/06 20:45
starcloudedCOMPILED_DATA on non datatype when checking the pragma COMPILED_DATA Pair fst snd15/06 20:46
Eduard_Munteanustarclouded: I'd try something like {-# COMPILED_DATA Pair (,) (,) #-} with the data variant15/06 20:46
starcloudedthe same message COMPILED_DATA on non datatype when checking the pragma COMPILED_DATA Pair (,) (,)15/06 20:47
Eduard_Munteanu(which basically maps Pair to (,) and _,_ to (,), one being a type, the other a value)15/06 20:47
Eduard_Munteanu*type/value constructor15/06 20:47
Eduard_Munteanustarclouded: well, you need to use the 'data' variant it seems15/06 20:48
starcloudedso how can I do the bind with Pair if I cant use the projection functions?15/06 20:52
starcloudedwi this {-# COMPILED_DATA Pair (,) (,) #-}15/06 20:54
Eduard_MunteanuYou just use Pair, fst and snd in Agda and it'll take care of translating to Haskell stuff.15/06 20:54
Eduard_MunteanuSince you supplied that pragma, Agda knows she has to translate Pair a b to (a, b) in types for example15/06 20:55
guerrillaanyone know if the equivalence of context-free (non-regular) types is decidable? i'm looking at a few slideshows and they kind of connote that, but generated language equivalence for two context-free grammars is undecidable, afaik15/06 21:43
starcloudedanyone could help telling me how can I add an instance declaration for (Database.HDBC.IConnection (IO Database.HDBC.PostgreSQL.Connection))15/06 21:59
Eduard_Munteanustarclouded: don't bother, just specialize it.15/06 22:00
starcloudedI dont understand15/06 22:01
Eduard_MunteanuYou can include whatever code you want in COMPILED pragmas.15/06 22:01
Eduard_MunteanuSo if you want to interface with a function that uses classes, you can simply specialize it to the particular instance you want15/06 22:02
Eduard_MunteanuFor example, {-# COMPILED showInteger (show :: Integer -> String) #-}15/06 22:03
Eduard_MunteanuDoes that answer your question?15/06 22:03
Eduard_Munteanu(I'm thinking a bit ahead of what you're asking, though)15/06 22:04
starcloudedthe thing is that I need the IConnection but this type is genareted by the connectPostgreSQL I can put all this things inside the COMPILED pragmas?15/06 22:21
starcloudedany ideas?15/06 23:03
Eduard_Munteanustarclouded: your IConnection is Connection15/06 23:35
Eduard_MunteanuMind IConnection is a typeclass15/06 23:35
Eduard_Munteanuwhose relevant instance is Connection15/06 23:36
Eduard_Munteanu(from Database.HDBC.PostgreSQL)15/06 23:36
Eduard_MunteanuFor example, you have    commit :: Connection -> IO ()15/06 23:37
Eduard_MunteanuAnd you don't have to deal with typeclasses.15/06 23:38
--- Day changed Thu Jun 16 2011
* copumpkin pokes xplat 16/06 03:06
* augur pokes copumpkin16/06 03:12
* copumpkin unpokes augur 16/06 03:13
auguri dont even know how that works16/06 03:13
copumpkinxplat: I'm getting unsolved metas in Categories.Terminal16/06 04:13
copumpkinoh it was just something silly16/06 04:15
augurcopumpkin: what kinds of math do you understand?16/06 04:21
copumpkinnot many16/06 04:21
copumpkinup until I started haskell I hadn't really done much math beyond early college and high school stuff16/06 04:21
copumpkin:)16/06 04:21
copumpkinwhy?16/06 04:22
auguri want to learn the math required for GR16/06 04:22
copumpkinGR?16/06 04:23
augurgeneral relativity16/06 04:23
copumpkinoh16/06 04:23
copumpkinI'd imagine some of the people in ##categorytheory could give you some pointers there16/06 04:23
copumpkinddarius or someone16/06 04:23
copumpkinI know ddarius has spent a lot of time reading about physics16/06 04:23
copumpkin@tell xplat I merged your port in and made some minor changes and additions, and now Everything.agda seems to typecheck fine and has nothing commented out anymore :) I did make a slight change with a non-fast-forward commit pushed, but with any luck that shouldn't mess with you pulling it16/06 04:49
lambdabotConsider it noted.16/06 04:49
djahandarieOregon!16/06 04:49
djahandarieI managed to brick my video driver AND wireless driver installing Coq yesterday16/06 04:50
djahandarieSecond is fixed, first will be fixed whenever I get around to it. :p16/06 04:50
augurcopumpkin: you know, freenode has memoserv16/06 04:52
copumpkinpff16/06 04:52
copumpkindjahandarie: oh nice16/06 04:52
auguri only discovered memoserv itself like.. yesterday16/06 04:52
djahandariecopumpkin, see, this is why I don't try to fix Agda16/06 04:52
djahandarie</badexcuse>16/06 04:53
copumpkin</worstexcuseever>16/06 04:53
djahandarieI'm not sure that is valid in my excuse DTD16/06 04:53
copumpkinyou've only been giving that one for over a month now16/06 04:54
djahandarieHmm, is twitter login https?16/06 04:54
copumpkinit probably has another couple of months at least left in it16/06 04:54
copumpkinif you leave it for three or more months, the problem will clearly fix itself16/06 04:54
djahandarieThat is how I solve all problems16/06 04:55
augurcopumpkin!16/06 09:30
augurread a paper i wrote?16/06 09:30
augur:D16/06 09:30
copumpkinomg xplat16/06 16:45
djahandarieWowww16/06 16:47
copumpkindjahandarie: sup?16/06 16:47
djahandarieRooming with Mike Shulman :o16/06 16:47
copumpkinoh nice16/06 16:47
djahandarieHe is awesome!16/06 16:48
copumpkinis he telling you all about HTT?16/06 16:48
djahandarieHaha, I'm trying to force it out of him :)16/06 16:48
copumpkinand selling you coq16/06 16:48
djahandarieI think I'm going to be sold that here anyways16/06 16:49
copumpkinprobably16/06 16:49
copumpkindon't forget your roots!16/06 16:49
djahandarieWhat do you think about the Prop Set distinction?16/06 16:50
copumpkinTHE WORK OF THE DEVIL16/06 16:51
djahandarielol16/06 16:51
copumpkinit's kind of similar to our irrelevance, really16/06 16:51
copumpkinnot sure which I like better16/06 16:51
copumpkinirrelevance feels a little more fine-grained, somehow16/06 16:51
ccasinI like irrelevance better16/06 17:08
ccasinbecause the prop/set distinction makes erasure a property of the type16/06 17:09
ccasinyou have to have erased nats and unerased nats, and the are different16/06 17:09
ccasininstead of just specifying, when you use nats, whether they should be erased16/06 17:09
ccasin*they are16/06 17:09
copumpkintrue16/06 17:12
copumpkinokay, I'm sold16/06 17:12
copumpkin(you can see I have well-formed opinions of my own here)16/06 17:12
ccasin:)16/06 17:12
augurcopumpkin: read my paper? :D16/06 17:16
copumpkinsure, later16/06 17:17
copumpkinhave you put a link to it up?16/06 17:17
augursure!16/06 17:17
augurwellnowwhat.net/linguistics/AProgrammaticApproachToBracketingParadoxes.pdf16/06 17:17
augurcompletely untested haskell code, btw. :D16/06 17:17
augurwritten for a person who wont know the difference XP16/06 17:18
copumpkinlol16/06 17:18
copumpkinok16/06 17:18
copumpkinI'll read it this evening16/06 17:18
augur\o/16/06 17:20
guerrillaaugur: s/we fine/we find on first page16/06 18:43
djahandarieMike was talking about "-1"-types, 0-types, 1-types from a 2-topos where he said he liked the prop/set distinction. I think he said "-1"-types were propositions, and 0-types were sets -- not sure, he was going too fast :p.16/06 18:57
guerrilladjahandarie: reference on -1 types?16/06 18:58
djahandarieI think they're normally called 1, 2, 316/06 18:59
djahandarieNot -1, 0, 116/06 18:59
augurguerrilla: thank you16/06 18:59
djahandarieI don't have a reference16/06 18:59
guerrilladarn16/06 18:59
guerrillaaugur: np16/06 19:00
xplatguerrilla: probably they relate to 'negative thinking' which you can find on nLab16/06 19:17
lambdabotxplat: You have 1 new message. '/msg lambdabot @messages' to read it.16/06 19:17
guerrillaxplat: thanks16/06 19:18
auguritd be nice if lambdabot did that when you signed on16/06 19:18
augurnot when you said something16/06 19:18
guerrillaor just joined16/06 19:18
augurwell yeah. thats what i mean. :p16/06 19:18
guerrillanot what it hought at all.. was thinking of like data 0-thing : Set where;   and data 1-thing where; foo : 1-thing; or whatver16/06 19:24
guerrillathought*16/06 19:24
guerrillabut yeh, makes sense i guess (-1)-poset is a point...16/06 19:24
guerrilla(-2)-groupoid, also a point16/06 19:25
guerrillajust starting on learning more than cat.theory vocabulary today actually :P16/06 19:25
guerrillamore than just*16/06 19:25
guerrillareally want a class on it. not motivaed enough to do it alone.. just have to now to stud coinduction it seems16/06 19:26
guerrillareading "A Tutorial on (Co)Algebras and (Co)Induction" http://www.cs.ru.nl/B.Jacobs/PAPERS/JR.pdf16/06 19:27
xplatfor my current proof i need to prove that there is only one total function with a given type.  is that possible, and if so how do i do it?16/06 19:27
xplat(the given type is (A \== B) -> X A \=> X B for fixed but arbitrary families X and _\=>_16/06 19:28
xplathm, is that even true?16/06 19:28
Saizanwhat if X = const Foo and \=> = -> ?16/06 19:30
ccasinxplat: what do you mean by "only one"?16/06 19:34
ccasinthere is probably only one up to extensional equality16/06 19:34
ccasinbut not agda equality16/06 19:34
ccasinand the proof that there is only one up to extensional equality is _hard_16/06 19:35
ccasinyou probably can't do it inside agda16/06 19:35
djahandarieWhy not?16/06 19:35
ccasinwell, it's parametricity16/06 19:36
ccasinI think it's independent16/06 19:36
ccasin(could be wrong)16/06 19:36
xplatmaybe i only have a split epi and not an iso :(16/06 19:37
djahandarieWhat are you doing?16/06 19:38
xplattrying to prove the strongest form of equivalence i can between Exp C I and Functors (Discrete I) C16/06 19:39
copumpkinxplat: you just prove forall functions of that type, they are (extensionally) equal to the one you have16/06 19:40
xplatcopumpkin: but i need propositional equality because this function is part of one of the object indices in [_]_~_16/06 19:41
ccasincopumpkin: how do you do that, in agda?16/06 19:41
copumpkinxplat: ouch, I hate that type16/06 19:41
copumpkinI was messing with it last night and made it a bit more pleasant16/06 19:41
copumpkinccasin: proof : (f : SomeRestrictiveType -> SomeOtherRestrictiveType) -> forall x -> f x = myImplementation x16/06 19:42
xplati guess this may be an iso in epigram, but only something weaker (adjoint equivalence?  but maybe stronger than that but still weaker than iso) in Agda16/06 19:43
ccasincopumpkin: so my guess is there is no agda term of type proof.  but maybe I'm missing something?16/06 19:43
copumpkinccasin: oh, in his case? I dunno :P16/06 19:43
copumpkinbut I'm sure that for some functions it can be proven16/06 19:43
xplateven if i prove extensional equality it buys me essentially nothing16/06 19:44
ccasinyeah, sure - I just think the general problem is a parametricity result16/06 19:44
copumpkinxplat: I simplified the Functor module a bit yesterday, not sure if I committed that16/06 19:45
xplatcopumpkin: did you merge port into master?16/06 19:45
copumpkinyeah16/06 19:45
copumpkinand added some other stuff16/06 19:45
copumpkinEverything now typechecks with everything uncommented16/06 19:45
copumpkinxplat: but I added a more sane refl to that horrible heterogeneous morphism equality thing16/06 19:46
copumpkinand used that in various places16/06 19:46
copumpkinI'm thinking of moving that heterogeneous morphism equality out of functor16/06 19:46
copumpkinsince it's conceivable that something else might want it (although I hope not)16/06 19:46
xplathm, after making some changes on port i have a feeling this merge will be 'fun'16/06 19:46
copumpkinwhat'd you do?16/06 19:47
copumpkin:P16/06 19:47
xplatadded a Categories.Lift for lifting categories, functors, and natural transformations16/06 19:47
xplatand a Categories.Power.Functorial16/06 19:48
copumpkinah :o16/06 19:48
copumpkinyou're coming to hac phi, right?16/06 19:48
xplatthat's the plan16/06 19:54
xplati'm glad to see they provide appropriate food even for metallivores16/06 19:54
djahandarie...they do?16/06 19:55
xplatlook at the example on the registration page :)16/06 19:55
copumpkinmetallivores :o16/06 20:04
xplatdon't look so shocked, they eat metal, not babies16/06 20:07
Saizanmetals are people too16/06 20:08
copumpkin:)16/06 20:11
xplatjust don't leave your sentient telepathic sword lying around16/06 20:15
xplatbut they don't usually allow swords in these kind of things anyway, so problem solved16/06 20:16
copumpkinso dolio's giving an agda tutorial at work tomorrow!16/06 20:18
copumpkinxplat: if you don't feel like doing the merge, I can merge your new changes in16/06 22:17
xplatcopumpkin: oh, i managed to do it by stashing my changes and reapplying on the main branch16/06 22:20
copumpkinoh cool16/06 22:21
copumpkinwhat is your Power.Functorial thing16/06 22:21
copumpkin?16/06 22:21
copumpkinmaybe I'll just wait to read it :P16/06 22:21
copumpkinI also noticed you have a Setoids and an ISetoids16/06 22:22
xplatit contains translations between the regular Power stuff and functor-from-discrete-category16/06 22:22
copumpkinbut both seem to contain Setoids16/06 22:22
copumpkinI see16/06 22:22
xplatcopumpkin: Setoids has stdlib setoids, ISetoids is irrelevant setoids as defined in Categories.Support16/06 22:22
copumpkinyeah, but as far as I could see, ISetoids also contained stdlib setoids16/06 22:23
copumpkinunless it merged wrong or something16/06 22:23
xplatif everything compiled, then no it doesn't16/06 22:23
copumpkinhttps://github.com/copumpkin/categories/blob/master/Categories/Agda.agda#L7416/06 22:23
xplati was originally just doing stdlib setoids, but then i realized they were being used not just for reasoning about Agda code but also for some of the purposes of Set16/06 22:24
copumpkinoh, I see16/06 22:24
copumpkinyeah, they're my poor man's Set16/06 22:24
copumpkinif you can think of a better way to make one16/06 22:24
copumpkinI'd love to have that instead16/06 22:24
xplatwell, ISetoids seems to work okay for 'the thing that plain Categories are enriched over'16/06 22:25
xplat* Category·s16/06 22:25
copumpkinwhat confused me16/06 22:26
copumpkinis that I thought ISetoids could contain Setoids with irrelevant fields16/06 22:26
copumpkin*would16/06 22:26
copumpkin(as objects)16/06 22:27
copumpkinbut it has the same objects as plain Setoids16/06 22:27
xplatno, it doesn't16/06 22:27
xplatthe Setoid name in that scope is introduced by the open Categories.Support.Equivalence16/06 22:28
copumpkinoh16/06 22:28
xplatregular Setoids are shadowed16/06 22:28
copumpkinI'm just dumb16/06 22:28
copumpkinI see16/06 22:28
xplatnot even shadowed, really; Setoids opens Relation.Binary itself to get the Setoid it uses16/06 22:30
copumpkinYEAH16/06 22:30
copumpkinwhoops16/06 22:30
copumpkinyeah16/06 22:30
xplatit does make things a little obscure, i suppose, but i'm not sure what else to do there16/06 22:30
copumpkinthat's fine16/06 22:31
copumpkinI was just confused16/06 22:31
starcloudedhello everybody16/06 22:31
starcloudedthe import pragma works with modules created by me?16/06 22:36
copumpkintry it?16/06 22:37
copumpkin:P16/06 22:37
starcloudedyes it does16/06 22:42
starcloudedif apply to IO (dbList Row) _<<=_ in the lambda abstraction I can get something like (dbList Row) ?16/06 23:09
Eduard_Munteanustarclouded: you mean _>>=_ ?16/06 23:36
Eduard_MunteanuIt's just like in Haskell16/06 23:36
Eduard_MunteanuSo yeah.16/06 23:36
Eduard_Munteanu(_<<=_ is either a typo or flip cobind :) )16/06 23:37
starcloudedyes I mean _>>=_16/06 23:38
--- Day changed Fri Jun 17 2011
starcloudedthe thing is when I apply the _>>=_ function I get Row17/06 00:05
Eduard_Munteanustarclouded: can you paste?17/06 00:26
starcloudedEduard_Munteanu: http://pastebin.com/XYQwSC7217/06 01:04
Eduard_Munteanustarclouded: dbquery conn "SELECT * FROM test" [] >>= λ x →convRow {!!}17/06 01:08
Eduard_MunteanuconvRow       : (dbList SqlValue) → String17/06 01:08
starcloudedyes17/06 01:09
Eduard_MunteanuconvRow isn't a IO String as it probably should17/06 01:09
Eduard_MunteanuSo instead >>= there works on the list monad17/06 01:09
Eduard_Munteanus/isn't/doesn't produce/17/06 01:09
starcloudedI dont understand the last part17/06 01:11
Eduard_Munteanustarclouded: if you have something of type 'IO a' and pass it to bind, it unwraps it to an 'a'17/06 01:13
Eduard_MunteanuIf instead you have something of type '[a]', it unwraps it to an 'a'17/06 01:13
Eduard_MunteanuString is just [Char]17/06 01:14
Eduard_MunteanuOops17/06 01:14
Eduard_MunteanudbList, but anyway17/06 01:14
Eduard_MunteanuLemme look at the API to see what you're trying to accomplish...17/06 01:15
Eduard_Munteanustarclouded: what's convRow?17/06 01:16
starcloudedhaskell bind to convrow :: [SqlValue] -> String17/06 01:16
starcloudedconvrow = unwords . intersperse "|" . map fromSql17/06 01:16
Eduard_MunteanuOk, its type is fine. But you can't use it like that.17/06 01:17
Eduard_MunteanuThe thing to the right of >>= must produce an IO something17/06 01:17
Eduard_Munteanu:t (>>=)17/06 01:18
lambdabotforall (m :: * -> *) a b. (Monad m) => m a -> (a -> m b) -> m b17/06 01:18
Eduard_MunteanuBecause 'connect' is of type IO something and you're practically ending that code with something that's not in IO17/06 01:19
Eduard_MunteanuMaybe you want to print that string?17/06 01:19
starcloudedyes17/06 01:20
Eduard_MunteanuThen write "[...] >>= putStrLn $ convRow [...]"17/06 01:20
starcloudedI need the response dbquery that is [[SqlValue]] and pass it to convRow as [SqlValue]17/06 01:23
Eduard_MunteanuSo dbquery's type is ... -> IO [[SqlValue]] ?17/06 01:25
starcloudedyes17/06 01:25
Eduard_MunteanuThen use, e.g., concat:    >>= putStrLn \o convRow \o concat17/06 01:26
Eduard_MunteanuDepending on what you need.17/06 01:27
Eduard_MunteanuIs it   quickQuery :: IConnection conn => conn -> String -> [SqlValue] -> IO [[SqlValue]]   in HDBC?17/06 01:28
starcloudedyes17/06 01:28
starcloudedquickQuery'17/06 01:28
Eduard_MunteanuYou might want to work that part out in Haskell first, the translation should be straightforward.17/06 01:30
copumpkinxplat: I have a deep question for you17/06 03:47
copumpkinor anyone, really17/06 03:47
copumpkinI have an evil heterogeneous morphism equality17/06 03:48
copumpkinit works sort of like the usual heterogeneous equality, but its one constructor accepts a proof that the morphisms are equivalent in the underlying category, and then lets you prove the heterogeneous equality17/06 03:48
copumpkinwhat are the ramifications of making that proof it takes irrelevant?17/06 03:49
copumpkinxplat: I've cleared up Functor quite a bit17/06 04:08
copumpkinxplat: I've pushed more changes17/06 04:34
copumpkinxplat: do you get kan extensions?17/06 05:25
djahandarieI think tomorrow sounds like a good day to hack on category stuff in Agda17/06 05:56
copumpkinoh yeah?17/06 05:56
copumpkinhow was your first day of oplss?17/06 05:57
djahandarieThough that means I'll need to get Agda on my laptop...17/06 05:57
djahandarieNeat17/06 05:57
xplatcopumpkin: Kan extensions are still pretty mysterious to me17/06 11:56
xplatah, it seems that really they are just initial or final approximate inverses to precomposition of a particular functor17/06 13:38
xplat(Lan being the initial forward approximation, Ran being the final backward approximation)17/06 13:40
xplatyou know what's annoying about non-observational type theory?17/06 13:56
xplatif two open terms are equal, it doesn't mean their lambda (or pi) abstractions are equal17/06 13:57
xplatso there are actually more lambdas than there are bodies for them to have17/06 13:57
xplat(not even counting functions not given by abstraction)17/06 13:58
xplatthe only reason this doesn't completely break the system to begin with is that lambda is not a function17/06 13:59
copumpkinI thought functions were equal if their bodies were equal17/06 14:19
augurcopumpkin: how meta-linguistic of you17/06 14:19
copumpkin:P17/06 14:23
copumpkinxplat: anyway, I added left kan extensions17/06 14:23
copumpkinI might do some yoneda tonight17/06 15:05
copumpkinit's about that time17/06 15:05
xplat@tell copumpkin lambdas are definitionally equal iff their bodies are definitionally equal.  closed terms are propositionally equal iff they are definitionally equal.  so closed lambdas are propositionally equal iff their bodies are definitionally equal.  however, the bodies are open, hence propositionally equal iff they have the same substitution instances in the free variable.  so bodies are propositionally equal iff the functions are pointwise equal.17/06 15:23
lambdabotConsider it noted.17/06 15:23
* copumpkin pokes xplat17/06 16:46
lambdabotcopumpkin: You have 1 new message. '/msg lambdabot @messages' to read it.17/06 16:46
guerrillaso, where can i read about these "syntax" declarations in Agda? just noticed them in a post to the ML17/06 17:59
Saizanin one of the release notes17/06 18:26
guerrillafound it17/06 18:26
guerrillado you know if its just sugar for more of what the mixfix paper describes? or is it more?17/06 18:26
guerrillai imagine it "just" updates parser cominator rules or something equivalent17/06 18:27
xplatguerrilla: there are basically two things it does17/06 19:23
xplat1) lets you rearrange syntactic order of arguments to not match their order in the telescope17/06 19:24
xplat2) lets you create syntax that binds variables17/06 19:25
xplatlook at the syntax declarations in e.g. Data.Product for the latter17/06 19:25
copumpkinxplat: in this definition: http://snapplr.com/mhzt17/06 19:32
copumpkinoh nevermind17/06 19:34
copumpkinxplat: remember that category presheaves thing I was making?17/06 19:36
copumpkincategory _of_ presheaves17/06 19:37
djahandarieHow are you defining it?17/06 19:40
djahandarieAs a functor category [C^op , Set] ?17/06 19:44
xplatcopumpkin: i remember that17/06 19:59
copumpkinyeah17/06 20:31
copumpkinI was wondering what universe the Set should live in17/06 20:31
copumpkinalthough I think I know17/06 20:32
copumpkinI also have a feeling that my hom functors are destined to always be yellow, the way I wrote them17/06 21:01
copumpkinunless you provide implicits17/06 21:01
copumpkinI had somehow convinced myself that wasn't the case, but now I'm not convinced17/06 21:01
xplat:(17/06 21:02
xplatthere's not much use in implicits that must always be provided17/06 21:02
copumpkinyeah17/06 21:02
copumpkinI was wondering if there were any cases in which they could be inferred17/06 21:02
copumpkinI'm thinking of making a module-ish version17/06 21:03
copumpkinwhere you open the module to fix the "implicit"17/06 21:03
copumpkinand then some de-modulified ones17/06 21:03
xplati rant into that with my Lift stuff that i wrote; Agda is really bad at inferring a level variable that only appears in a lub expression17/06 21:03
copumpkinunderstandably!17/06 21:03
copumpkinit doesn't seem like it'd have a single solution17/06 21:04
xplatmaybe it is understandable, i haven't worked out the details enough to know17/06 21:04
copumpkinwell17/06 21:04
copumpkinif I say 6 = 5 lub x17/06 21:05
xplatit probably doesn't have a unique solution, but does it have a 'unique enough' one?17/06 21:05
copumpkinthen x can only be 617/06 21:05
copumpkinbut 6 = 6 lub x17/06 21:05
copumpkinthen x can be 0-617/06 21:05
copumpkinI'm sure it could be unique enough, but it seems tricky to make a system that doesn't care about unique solutions17/06 21:05
xplatanyway there is usually enough information for a unique solution, it just doesn't flow the right places17/06 21:06
copumpkinI think I'll do the module approach17/06 21:07
xplatbtw it turns out that my 'Power' stuff is pretty similar to the operation in http://ncatlab.org/nlab/show/power17/06 21:08
starcloudedhello everybody17/06 21:20
copumpkinxplat: neat17/06 21:21
starcloudedI have List String how can I cast it to List (Colist Char)?17/06 21:51
Eduard_Munteanustarclouded: isn't there some toCostring?17/06 21:53
starcloudedyes it is17/06 21:54
Eduard_MunteanuDon't you want Colist Char? You said List (Colist Char)17/06 21:55
starcloudedthis is what I am trying to do I map { } listString, inside the brackets has to be String -> Colist Char, but when I wirte toCostring does not redefine17/06 21:58
Eduard_MunteanuI'm not sure I understand your problem.17/06 22:01
Eduard_MunteanuAnyway, listString must be of type List String.17/06 22:01
xplatif you type C-c C-. with toCostring in there, what does it say for the Goal and for what you have?17/06 22:02
starcloudedthis is shown .Data.Colist.Colist Char != Colist Char of type Set when checking that the expression map toCostring qr has type dbList (Colist Char)17/06 22:08
copumpkinxplat: I've been rearranging stuff a bit, not sure if you've looked recently17/06 22:15
copumpkinthe homs are getting moved around a bit too now17/06 22:15
xplatstarclouded: looks like you might have two kinds of colists in play?17/06 22:18
starcloudedI think so cause I have to redefine the List in my program cause when I try to use the COMPILED prama inside the orginal list definition it thew an error17/06 22:37
xplatoh, then you may need to write your own toCostring17/06 22:43
xplatthe COMPILED stuff really should just disappear level parameters, but it does not seem to17/06 22:44
xplatwell, hm, maybe it can't do that if haskell calls back into Agda17/06 22:46
Eduard_MunteanuTry defining dbList : Set -> Set    dbList = List {0}17/06 22:53
Eduard_MunteanuHrm, though I think it needs to be an actual datatype.17/06 22:55
Eduard_MunteanuAnyway I suppose you could define your own dbList -> List conversion, then use toCostring17/06 22:55
copumpkinEmbed : ∀ {o ℓ e} → (C : Category o ℓ e) → Functor C (Presheaves C)17/06 23:37
copumpkindoes that seem reasonable?17/06 23:37
copumpkinI've implemented it17/06 23:37
copumpkindo you have a better name for it?17/06 23:38
--- Day changed Sat Jun 18 2011
xplathm, i always considered Yoneda the root of Yoneda embedding18/06 00:09
Guest87456James18/06 00:12
Guest87456Oops.18/06 00:12
copumpkinxplat: ?18/06 01:11
copumpkinxplat: you mean it's named wrong, or the definition is wrong?18/06 01:33
copumpkinI guess they're different sides of the same thing :)18/06 01:34
john___Hi, I need to make a parser combinator in agda18/06 13:29
john___how i can do it18/06 13:30
starcloudedhello everybody18/06 14:02
Mtem{alForathi18/06 20:31
Mtem{alForatـــــــــــــــ♥♥ـــــــــــــــ♥♥♥♥ـــــــــــــــ♥♥♥ــــــــــ♥♥♥♥♥‏18/06 20:31
Mtem{alForatsee my18/06 20:32
Eduard_MunteanuHi, we love you too, but what's the meaning of that?18/06 20:32
Mtem{alForatthis arabic18/06 20:33
Mtem{alForatsory18/06 20:34
Mtem{alForatspik arabic18/06 20:34
Eduard_MunteanuOh, I saw underscores and hearts :)18/06 20:34
Eduard_MunteanuNo, I don't.18/06 20:34
Mtem{alForatYuo name god18/06 20:35
guerrillawhat...18/06 20:37
Mtem{alForatthank yuo18/06 20:39
Mtem{alForatsory18/06 20:39
Mtem{alForatbattery lo18/06 20:40
Mtem{alForatI going18/06 20:41
Mtem{alForatgood bay18/06 20:42
Mtem{alForatـــــــــــــــ♥♥♥♥♥♥ـــــــــــــــ♥♥♥♥♥♥♥‏18/06 20:42
Mtem{alForatمرحبا18/06 20:43
Mtem{alForathi18/06 20:44
Eduard_MunteanuErm, you should try to speak English, I'm not sure anybody here speaks Arabic.18/06 20:44
Mtem{alForatok18/06 20:45
Mtem{alForatyou from country18/06 20:47
Mtem{alForatWhat18/06 20:48
dylukescopumpkin: You around?18/06 23:54
--- Day changed Sun Jun 19 2011
dylukescopumpkin: oy...19/06 00:05
dylukeshow do I evaluate arbitrary expressions?19/06 00:05
augurC-c C-n19/06 00:05
dylukessometimes that just results in a type though19/06 00:06
dylukesnot the actual… constructors. Say for example with natural numbers.19/06 00:06
augurwhat19/06 00:06
dylukeslet me try to find an example19/06 00:07
dylukesOh, one other useful thing to know...19/06 00:08
dylukessay here I have this19/06 00:08
dylukeshttp://hpaste.org/4796119/06 00:08
dylukesis there any way to have it (in the output) use my shorthand definitions? Say, supply rewrite rules or something of that nature?19/06 00:09
augur%_%19/06 00:09
augurno19/06 00:10
augurnot that i know of19/06 00:10
dylukesit's natural numbers19/06 00:10
augurbut thats not what you asked for before19/06 00:10
dylukesnothing complex heh.19/06 00:10
auguryes i can see that its naturals19/06 00:10
augurbut its in hanzi!19/06 00:10
dylukesactually it's in japanese...19/06 00:11
dylukesbut I wouldn't be surprised if the ideographs match19/06 00:11
augurwell they had better, for the most part19/06 00:12
dylukesuh oh19/06 00:13
dylukes8 - 3 is not 4...19/06 00:13
dylukesMy definition of - must be wrong19/06 00:14
dylukes>_>19/06 00:14
* Eduard_Munteanu sees ladder, spider web, spider web : Set :P19/06 00:14
dylukesand 8 - 0 is not 7 :D19/06 00:15
dylukesEduard_Munteanu: I see self, sort of thing, number19/06 00:16
augurs s s s s s s s 0 - s s s 0 = s s s s s s s 0 - s s 0 = s s s s s s 0 - s 0 = s s s s s 0 - 0 = s s s s s 019/06 00:16
auguryour definition works19/06 00:16
Eduard_MunteanuHow exactly does one go about reading those characters on a computer screen?19/06 00:18
augurEduard_Munteanu: ?19/06 00:18
Eduard_MunteanuThey look way too small given the details involved.19/06 00:18
augurwhat19/06 00:19
Eduard_MunteanuEven if I zoom in the browser they still look small compared to latin script.19/06 00:19
augurthey look fine to me19/06 00:19
Eduard_Munteanufor example 数19/06 00:20
Eduard_MunteanuCan you make out the details?19/06 00:20
Eduard_MunteanuStuff like 六is fine, but the other ones seem hard to make out.19/06 00:22
Saizan@tell dylukes you could make it use arabic numerals if you provided BUILTIN declarations, look at stdlib's Data.Nat for the details19/06 00:22
lambdabotConsider it noted.19/06 00:22
augurEduard_Munteanu: i can make out everything but the top right radical19/06 00:25
SaizanEduard_Munteanu: i suspect most people won't look/need the precise details to read it anyway19/06 00:25
dylukesaugur: Yeah I hadn't recompiled it.19/06 00:26
lambdabotdylukes: You have 1 new message. '/msg lambdabot @messages' to read it.19/06 00:26
dylukesThat's why :P19/06 00:26
dylukesSaizan: So, is there any way to make it use my own number system?19/06 00:27
Eduard_MunteanuI guess so. I'm not sure, maybe the char count is lower in Japanese, but there are lots of characters in Chinese at least.19/06 00:27
Saizandylukes: no19/06 00:27
dylukesWhat if I feel like using the japanese number system for some arbitrary reason.19/06 00:27
Saizanyou'd have to patch the pretty printer :)19/06 00:27
Eduard_Munteanudylukes: make a 'show' for your numbers19/06 00:28
Eduard_MunteanuAnd read the output as a string.19/06 00:28
dylukesEduard_Munteanu: That works in Agda o.0?19/06 00:29
dylukeswait, I'd need a built-in for strings too...19/06 00:29
dylukesI don't know how to use them19/06 00:29
Eduard_MunteanuYou might want to get the stdlib and look around.19/06 00:30
Eduard_MunteanuWhy wouldn't it work?19/06 00:30
dylukesIs the std lib not in the default agda package?19/06 00:30
Eduard_MunteanuYou'd just C-c C-n showJPNum mynumber19/06 00:30
Eduard_MunteanuNo.19/06 00:30
dylukesgreat. I'm on dialup19/06 00:31
Eduard_Munteanuhttp://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary19/06 00:31
Eduard_MunteanuOuch.19/06 00:31
dylukes^^19/06 00:33
dylukesSo, how will I have to download/install it?19/06 00:33
dylukesOh, so before,19/06 00:33
dylukesI tried defining Ints and Nats19/06 00:33
Eduard_MunteanuYou just unpack it somewhere and set the paths in Emacs.19/06 00:34
dylukesand I had Ints as a small wrapper around Nats and a Sign...19/06 00:34
dylukesbut then I wanted overloaded _+_19/06 00:34
dylukesso, my solution I came up with19/06 00:34
dylukesafter spending 10 hours on it without internet TT_TT19/06 00:34
dylukeswas to have a data type Number where19/06 00:34
dylukesnat : Number19/06 00:34
dylukesint: Number19/06 00:34
dylukesthen19/06 00:34
dylukesdecode : Number -> Set19/06 00:35
dylukesdecode nat = Nat19/06 00:35
dylukesdecode int = Int19/06 00:35
dylukesthen had a Number implicit argument to _+_ ...19/06 00:35
dylukesand applied decode to each of the arguments19/06 00:35
dylukes_+_ : {Number a} -> decode a -> decode a -> decode a19/06 00:35
Saizancongratulations, you just re-invented "universes" :)19/06 00:35
dylukes{nat} _ + _...19/06 00:35
dylukesis there a better way to do this?19/06 00:36
dylukesuniverses....?19/06 00:36
Eduard_MunteanuIn fact they're like typeclasses but closed.19/06 00:36
dylukes(I'd google but that'd take 20 minutes)19/06 00:36
dylukesI'm basically wondering if Agda has type classes?19/06 00:36
dylukesclosed?...19/06 00:36
Eduard_MunteanuIn latest darcs, yeah, sortof.19/06 00:36
Saizanyour Number type is also called an universe19/06 00:36
dylukesAs in, you can't add items to them you mean?19/06 00:36
dylukesthat sounds sketchy.19/06 00:37
dylukesSaizan: explain?19/06 00:37
Eduard_MunteanuThey're closed in the sense you can't add new instances19/06 00:37
Eduard_MunteanuYou have to edit the original definition to do so.19/06 00:37
dylukesIt seemed to me to be more a "hackish mapping of nullary type constructors as tags to types"19/06 00:37
dylukesmmk, got it.19/06 00:37
Saizandylukes: there's nothing much to explain, it's sort of a design pattern for overloading, but as Eduard_Munteanu points out the problem is that you can't add new "instances" without modifying the universe type, Number in this case19/06 00:38
dylukesmm.19/06 00:38
Eduard_MunteanuThe non-canonical implicits (or what are they called these days?) are more like typeclasses.19/06 00:38
Saizandylukes: the darcs version of agda has something much more like typeclasses instead19/06 00:38
dylukesnon-canonincal implicits?...19/06 00:38
dylukesI have Agda 2.2.1019/06 00:39
dylukesam I too far out of date?19/06 00:39
Saizanthat's the latest released version, but no released version has themù19/06 00:39
Eduard_MunteanuThey aren't in any release so far.19/06 00:39
dylukesI see theres a Agda.TypeChecking.UniversePolymorphism module in there too19/06 00:40
dylukesis there some sort of sugar or special library support?19/06 00:40
dylukes(in 2.2.10)19/06 00:40
SaizanUniversePolymorphism is unrelated19/06 00:40
Saizanit's another notion of Universe19/06 00:40
dylukesmmk19/06 00:40
Eduard_MunteanuThey're like {} (but spelled {{}}), except Agda will look in the scope for a matching definition of the "thing", and will pick that up if it's unique.19/06 00:40
Eduard_MunteanuIt's not like regular passing of implicits, hence non-canonical.19/06 00:41
dylukesExplain?19/06 00:41
dylukesor, example would be good.19/06 00:41
dylukesAlso, I'm wondering if theres a way to do something like… say I have19/06 00:41
Eduard_MunteanuThere's one in the stdlib19/06 00:41
dylukesint Nat Sign19/06 00:41
dylukesand I do19/06 00:41
dylukes(int n1 s2) + (int n2 s2)19/06 00:42
dylukesthat doesn't work...19/06 00:42
dylukesis there any way ,in the pattern match, to assert you want to match where two things are equal?19/06 00:42
dylukesI guess that's asking too much...19/06 00:42
dylukesI could define the equality myself and use with?...19/06 00:42
Saizanyou could say _+_ : {A : Set} {{add : A -> A -> A}} -> A -> A -> A; _+_ {_} {{add}} = add19/06 00:42
dylukesthe reason I ask is I'd like to match the sign being equivalent, and then use it in the match.19/06 00:42
dylukeser, use it in the result expression19/06 00:43
dylukes._.19/06 00:43
Eduard_Munteanuhttp://code.haskell.org/Agda/doc/release-notes/2-2-12.txt19/06 00:43
Saizanthen define addNat : Nat -> Nat -> Nat; addInt : Int -> Int -> Int; and then call + on Nat's or Int's and the add argument would get filled in by addNat or addInt depending on the type19/06 00:44
Eduard_MunteanuBasically instances are records you define in the global scope.19/06 00:44
dylukesSaizan: er… wait how is it "picking up" on addNat and addInt?19/06 00:44
dylukesdo they have to have a unique type?19/06 00:44
Saizandylukes: they just need to be in scope and uniquely match the type of add in the particular context19/06 00:46
dylukescould you paste an example usage of that?19/06 00:46
Saizanone would usually define a record type to distinguish different binary operations19/06 00:46
Eduard_Munteanudylukes: look in the release notes above ^19/06 00:46
Eduard_Munteanu* Instance arguments.19/06 00:46
dylukesah its a new feature thing19/06 00:47
dylukesI'll hold off on 2.2.12 for now19/06 00:47
dylukesI have plenty to work with/learn in 2.2.10 >_>19/06 00:47
Eduard_MunteanuAlso here: http://code.haskell.org/Agda/examples/instance-arguments/19/06 00:48
dylukesshould I download 2.2.12 do you think?19/06 00:49
Eduard_MunteanuThere's no 2.2.12, just latest darcs19/06 00:50
Eduard_MunteanuI run latest darcs Agda & stdlib, it's ok.19/06 00:50
Saizandylukes: for your question about equality of signs, you're right, you have to define the comparison function yourself and then use with19/06 00:50
Eduard_MunteanuHrm, I should revisit my automated Haskell binding generator idea.19/06 01:06
augurhow should i render lagda files19/06 03:10
starclouded1Verde campeon19/06 03:12
augurwhat19/06 03:12
starclouded1sorry19/06 03:12
auguralso, is it possible to define type-level Fix? i couldve sworn it was but im getting a strict positivity error19/06 03:13
auguralso can someone point me to something that explains why strict positivity is something people like?19/06 03:26
auguralso also is there a standard include for lagda to get all the pretty coloring and fonts?19/06 03:30
Saizanyou can't define a Fix : (F : Set -> Set) -> Set, because there's no guarantee F will be strictly positive19/06 03:46
Saizanhttp://code.haskell.org/~Saizan/UCodes.agda <- here's something that works19/06 03:48
Saizan(Desc might not cover all the functors you are interested in though)19/06 03:49
Saizanstrict positivity is important because it guarantees consistency19/06 03:51
auguri tried using conors flag that turns off strict positivity checking19/06 04:01
augurbut i get a file end error with that o.O19/06 04:01
Eduard_MunteanuI wonder, does it lack of strict positivity imply there are terms which don't have a closed form?19/06 04:02
Eduard_Munteanus/it//19/06 04:03
augurwhats a closed form exactly19/06 04:04
Eduard_MunteanuSomething that's finite when spelled out.19/06 04:05
augurahh19/06 04:06
Eduard_Munteanue.g. 'fix succ' isn't19/06 04:06
augurEduard_Munteanu: sure but in the type domain type fixed points are ofcourse not finite because they're infinite disjunctions but ..19/06 04:08
xplatEduard_Munteanu: once you get used to hanzi/kanji it becomes much easier to read them.  your brain fills in the details the pixels leave out.19/06 04:10
Eduard_MunteanuI remember somebody posting that Warrior exercise in #haskell, and you can't really encode that in Agda because it's not strictly positive. In order to write a member of Warrior you'd need another one and so on.19/06 04:10
Eduard_Munteanuxplat: ah, I was wondering about that. Mainly because I saw webpages written in Japanese, and the layout was odd (big spacing, large characters and so on). So I thought that might be the reason.19/06 04:11
xplatEduard_Munteanu: they do need to be a little bit bigger than latin letters, but not as much as you'd think at first19/06 04:17
augurso regardling the lagda questions, anyone?19/06 04:18
xplati think some of the spacing stuff is more a cultural coincidence, different design sense19/06 04:18
xplatbut then again it might be connected in a more roundabout way19/06 04:19
xplataugur: sorry, i haven't even looked at lagda yet19/06 04:20
augursokay :p19/06 04:20
xplati think a wall of kanji might look a bit more intimidating and be easier to get lost in than a wall of english text since there are no spaces between words19/06 04:22
xplatso in that sense it might be better to use smaller paragraphs and more space between them19/06 04:22
augurspaces are a fairly recently invention in the realm of alphabetic writing.19/06 04:23
augurancient greek and roman texts used no spaces19/06 04:23
auguroccassionally the romans would use interpuncts, especially later19/06 04:24
xplatyet another reason i'm glad to have modern technology19/06 04:24
xplatimagine computing with roman numerals and no spaces19/06 04:24
Eduard_Munteanuaugur: maybe Pandoc?19/06 04:25
augurim not sure if anyones really done any studies on relative comprehension speeds and reliability19/06 04:25
augurthere might be tho19/06 04:25
augurEduard_Munteanu: pandoc?19/06 04:25
auguror for the rendering19/06 04:25
xplatwell, forget comprehending your own code, try getting the computer to do it19/06 04:26
auguri take it theres nothing i can do from within aquamacs?19/06 04:26
augurxplat: no i mean reading comprehension for normal text19/06 04:26
Eduard_Munteanusay   http://flygdynamikern.blogspot.com/2009/03/blogging-with-pandoc-literate-haskell.html19/06 04:26
Eduard_MunteanuI'm not sure what you meant by rendering, though. I assumed you wanted to get a PDF or whatever from the .lagda file19/06 04:26
auguryeah19/06 04:27
xplataugur: i don't find spaceless english text that bad for straight reading even though english spelling is not designed for that and i'm not used to it.  for scanning and when you lose concentration though it seems terrible.19/06 04:28
auguri mean, texshop works fine but theres no agdamode so its a pain to have to open it in texshop then render19/06 04:28
xplatof course, you might not want to go by me, since i am a freak of nature who can read latin text upside down and in mirrors at about half normal speed and do cryptograms in my head19/06 04:28
augur;)19/06 04:29
xplatlooks like tmux is what i was looking for as a replacement for screen19/06 04:36
augurcopumpkin: surely you know about lagda19/06 07:19
augursurely surely!19/06 07:19
copumpkinwhat about it?19/06 07:20
copumpkinI've never written any .lagda files19/06 07:20
auguroh19/06 07:20
augur:(19/06 07:20
augurso you wouldnt know whether or not theres a standard import i could use or anything19/06 07:20
john___Hello19/06 07:23
copumpkinaugur: it's just another format for source code?19/06 07:23
copumpkinwhat do you mean imports19/06 07:23
augurcopumpkin: syntax highlighting stuff mostly19/06 07:23
augurbut also the stuff to hide inessential code, and the stuff to inline code without it being actual code19/06 07:23
john___Anyone knows where are the functor laws definied in the standar library?19/06 07:24
john___thanks19/06 07:24
augurjohn___: probably in category19/06 07:24
augurhttp://www.cse.chalmers.se/~nad/listings/lib-0.5/Category.Functor.html#119/06 07:25
augurwell, there are no laws there i guess19/06 07:25
augurmaybe theres no proper CT stuff like that19/06 07:25
augurcopumpkin should know, surely!19/06 07:26
john___copumpkin : any ideas?19/06 07:27
copumpkinthere isn't proper CT stuff in the std lib19/06 07:28
copumpkinit's a slightly fancier version of haskell CT19/06 07:28
john___ok, thanks19/06 07:28
john___can you give any reference at all?19/06 07:30
auguroh man19/06 07:31
auguri need to get some sleep19/06 07:31
augurnight19/06 07:31
copumpkinjohn___: you can find all the functor laws in the categories library19/06 07:35
copumpkinhttps://github.com/copumpkin/categories19/06 07:35
augurwoo okay19/06 20:25
augurit seems i have made some progress with lagda19/06 20:25
Eduard_Munteanuaugur: how did you go about rendering it?19/06 20:29
* Eduard_Munteanu might want to do this some time...19/06 20:30
augurim just using the same renderer i'd otherwise be using19/06 20:30
augurblah19/06 20:48
auguri dont like the current lagda formatting that comes with lhs2tex19/06 20:48
augureverything is in math sansserif19/06 20:48
augurok thats fixable. good good19/06 20:54
--- Day changed Mon Jun 20 2011
augurwhats a good structure for a brief agda tutorial for a paper that uses agda extensively but isnt designed for an agda audience20/06 00:25
augurbrief as in order of introducing syntax, etc.20/06 00:25
xplatwhat programming languages ARE they familiar with?20/06 01:01
Eduard_MunteanuI didn't have much trouble reading through Conor's paper on Epigram without actually knowing the language beforehand.20/06 01:09
Eduard_MunteanuI suspect familiarity with lambda calculus, type theory and a vague idea about dependent types should be enough.20/06 01:10
augurxplat: almost certainly none :)20/06 01:20
Eduard_MunteanuPfft... linguists. :P20/06 01:22
augurEduard_Munteanu: tell me about it20/06 03:59
augurbut thats part of what this paper is attempting to address20/06 03:59
auguranyone know why \Sigma isnt rendering in lagda??20/06 04:30
augurusing lhs2tex i mean20/06 04:30
augurshould i use ?s or {! !} or { }n when showing holes in an lagda file, do you think?20/06 06:05
augurif they'll be used to show the process of incremental construction?20/06 06:06
kosmikusaugur: back now, if you have any more questions ...20/06 07:09
augurhey you20/06 07:09
augurkosmikus: whats for breakfast? :D20/06 07:10
kosmikusjust some muesli20/06 07:13
augurmuesli can be pretty good20/06 07:28
augurkosmikus: do you know how to turn off latex math operator spacing?20/06 07:52
augur- is showing up as a binop with the normal spacing and this is problematic20/06 07:53
kosmikusaugur: not by default20/06 07:56
augurk20/06 07:56
kosmikusaugur: so you've probably changed the formatting of identifiers20/06 07:57
augura bit!20/06 07:57
augurim using conors style20/06 07:58
augurwhich i should probably ok with him first e.e20/06 07:58
kosmikusso what are you using for variables?20/06 07:59
augurpurple mathnormal20/06 08:00
kosmikusyou probably want text, not math20/06 08:00
kosmikusat least if you're using -s in variable names20/06 08:00
auguroh?20/06 08:01
kosmikuswell, foo-bar in math will render as foo - bar. I can't do anything about it. foo-bar in text will render as foo-bar.20/06 08:03
augurtrue true20/06 08:03
augurok20/06 08:03
guerrillathis is for latex? can't you just do \- or someting20/06 08:03
augurthank you :)20/06 08:03
kosmikusyes, I could reformat all occurrences of - to something else on the lhs2TeX side, but it's unclear to me what the general default should be.20/06 08:04
kosmikusgenerally, text seems to work fine for me.20/06 08:04
kosmikusmost "math" in identifiers is done via unicode anyway, and that works in LaTeX text mode, still.20/06 08:05
augurwhoa wait20/06 08:05
auguryou're andres loh?20/06 08:06
kosmikusyes20/06 08:06
guerrillaapparently not, \mbox{-} is the correct way20/06 08:06
augurawesome. you saved me the trouble of emailing you!20/06 08:06
augurlol20/06 08:06
kosmikusaugur: and you are?20/06 08:06
augurnoone important :D20/06 08:06
augurand noone you'd know20/06 08:06
kosmikusunfair :)20/06 08:06
guerrillawow, famous people in #agda :P20/06 08:06
guerrilla:)20/06 08:07
augurhttp://www.ling.umd.edu/people/students/ darryl mcadams20/06 08:07
augurhttp://www.ling.umd.edu/people/person/darryl-mcadams/20/06 08:07
augurhey look at that20/06 08:07
augura direct link20/06 08:07
augurok heres a question for you, sir20/06 08:08
kosmikusok nice :)20/06 08:08
kosmikusguerrilla: well, pigworker is on #agda ... certainly significantly more famous than I am :)20/06 08:09
guerrillaoh what.. hahaha i didnt know that was conor20/06 08:10
kosmikus:)20/06 08:10
auguractually, nevermind, i see the answer is apparent.20/06 08:10
augurwait whoa hello20/06 08:10
augurconor is here?20/06 08:10
augurpigworker: can i totally steal your color scheme20/06 08:10
guerrillai've never seen him talk tho..20/06 08:11
auguri never saw him come in20/06 08:11
auguri know you can guarantee a response if you tweet @pigworker20/06 08:12
augurgod what a twitter addict. get a life you nerd!20/06 08:12
guerrillaoh yeah.. cool. well i don't do anything so advanced to warrent his attention at this point :)20/06 08:12
augurkosmikus: what font setup are you using for agda normally? is it all mathsf or is it text and a sans font?20/06 08:13
kosmikusaugur: I'm pretty sure Conor will actually be grateful if more people start using his color scheme.20/06 08:13
kosmikusaugur: here's an paper using Agda I've written, as an example: http://people.cs.uu.nl/andres/gdiff-wgp.pdf20/06 08:15
kosmikuss/an/a/20/06 08:15
augurer.. example of? :P20/06 08:15
kosmikusaugur: you've been asking of my preferred layout.20/06 08:17
augurno no i just meant what font do you use for agda in agda.fmt20/06 08:18
kosmikusaugur: so I thought that better than just describing it, I'd show you an example.20/06 08:18
augurwithout any customizations20/06 08:18
auguris it mathbf or something else?20/06 08:18
kosmikustextsf20/06 08:19
auguraha!20/06 08:19
augurkosmikus: ah, heres an important question. why does [] not work properly in %format?20/06 08:22
auguralso, \Sigma and \lambda render as S and l, btw.20/06 08:24
kosmikusaugur: [] is treated as two tokens even in Agda mode, which is probably wrong, but not so easy to fix. you can only give formatting directives for single tokens.20/06 08:26
auguraha ok.20/06 08:26
kosmikusaugur: \Sigma and \lambda should expand to \textSigma and \textlambda, and render as whatever you've defined these, I think.20/06 08:27
augurhmm ok20/06 08:27
kosmikusaugur: there's a package textgreek.sty that defines all greek characters properly. I should probably make agda.fmt depend on it.20/06 08:27
augurnifty. i shall include textgreek.sty immediately!20/06 08:28
augurhmm. well, im using textgreek but i still have to use a %format.20/06 08:33
kosmikusthat's strange. I think it just works for me.20/06 08:36
augurhm. ah well. its nothing major.20/06 08:37
kosmikusall of agda.fmt is a bit ad-hoc.20/06 08:38
kosmikusI made it as a proof of concept originally.20/06 08:38
augurin other directions, do you know anything about lagda mode20/06 08:38
kosmikusand then never got around to properly redoing it.20/06 08:38
auguri'd be happy to help properize it!20/06 08:39
kosmikus:)20/06 08:39
kosmikuslhs2tex is on github. you can send patches ... I'll look at them ... eventually :)20/06 08:39
augur:p20/06 08:40
augurkosmikus: in organizing your tex files, do you prefer to keep all your %formats at the top, or to you distribute them around where the definitions are?20/06 08:47
kosmikusaugur: I usually move them to a separate file, and %include it.20/06 08:52
auguraha!20/06 08:52
augurhmm20/06 09:04
augur\textit in %format gives me a weird error20/06 09:04
augurit gives me a font warning then an undefined control sequence error20/06 09:06
augurspecifically http://hpaste.org/4801120/06 09:06
pigworkeraugur: the use of my colour scheme (which goes back to 2000) requires no permission, but I am certainly pleased to see it20/06 09:13
augurhooray!20/06 09:14
augurpigworker: also, you remind me of rory williams. just fyi.20/06 09:14
pigworkernow that's a new one on me20/06 09:20
augurrory, from doctor who20/06 09:22
pigworkerI have a passing acquaintance with Doctor Who...20/06 09:25
auguroh man, its great. rorys totally badass20/06 09:26
pigworkerand he had great specs in one ep I remember20/06 09:27
augurpossibly!20/06 09:27
auguris demorgan's law constructive?20/06 10:44
augurhmm. kosmikus, does \savecolumns work in specs?20/06 11:10
auguror in agda in general20/06 11:10
kosmikusyes20/06 11:38
augurhm.20/06 11:38
auguri cant seem to get it to work.20/06 11:39
kosmikusminimal example on hpaste?20/06 11:39
augureh. its not that important. ill annoy you some other time :p20/06 11:39
kosmikuswell, it should be simple20/06 11:41
kosmikusaugur: this works, for example: http://hpaste.org/4801220/06 11:45
augurhmm20/06 11:45
auguroh i see. i guess i was doing it wrong.20/06 11:45
augurthe the real question is why i cant seem to use whitespace to align things20/06 11:46
augurwhich from what i saw should work20/06 11:46
augurbut if i do   foo : A\n    -> X   the -> isnt aligned properly20/06 11:47
kosmikusI don't understand the question.20/06 11:47
kosmikusah20/06 11:47
augurit should be under the : but it always shows up a fixed distance from the left20/06 11:47
kosmikusif there's only a single space before :, it won't work20/06 11:47
kosmikusaugur: have you read any documentation? :)20/06 11:48
augursome! :p20/06 11:48
augurbut is this for \savecolumns or in general?20/06 11:48
kosmikusgeneral20/06 11:48
augurhmm20/06 11:48
augurok ill check the docs for this.20/06 11:48
kosmikusit's simple20/06 11:48
augurno dont tell me20/06 11:48
augurif its in the docs ill find it20/06 11:49
kosmikusif you want things aligned, start them at the same column and precede them with at least two spaces20/06 11:49
kosmikusdo  foo  :  A20/06 11:49
kosmikuser20/06 11:49
kosmikusthat wen't wrong20/06 11:49
kosmikuslike this:20/06 11:51
kosmikusdo  foo  :   A ->  X20/06 11:51
kosmikusgrr20/06 11:51
kosmikussomehow, pasting doesn't work as expected20/06 11:51
augurill check the docs :P20/06 11:51
kosmikusyou'll figure it out20/06 11:51
augur:)20/06 11:52
auguris there a list of quail completions i can lookup?20/06 12:25
augurer.. i can lookup a symbol in20/06 12:25
pigworkeraugur: re demorgan 3 out of 4 variants are constructive, but "not (A and B) => (not A) or (not B)" magics up one bit from nothing!20/06 12:43
augurthats what i figured. the motivation for linear logic seems a bit clearer now20/06 12:44
augursince this seems very much like the "you get one of these but you dont know which" notion of disjunction20/06 12:44
augurwhat is that, par?20/06 12:44
auguror maybe its \oplus.. who knows20/06 12:45
--- Log closed Mon Jun 20 18:39:35 2011
--- Log opened Mon Jun 20 19:00:00 2011
-!- Irssi: #agda: Total of 49 nicks [0 ops, 0 halfops, 0 voices, 49 normal]20/06 19:00
-!- Irssi: Join to #agda was synced in 145 secs20/06 19:02
augurcopumpkin: http://wellnowwhat.net/linguistics/AlgebraicSyntax.pdf20/06 19:11
augurPREPARE FOR TEXT20/06 19:11
augur19 pages and im only about halfway into the paper. @_@20/06 19:12
augurmuch of the text is actually just introductory stuff20/06 19:13
auguri would skip to algebraic derivationality20/06 19:13
augursection 420/06 19:13
Eduard_MunteanuNice. The typesetting looks good.20/06 19:15
* Saizan wonders if a stable and a darcs agda installations can coexist peacefully20/06 19:21
augur:)20/06 19:21
Eduard_MunteanuSaizan: you can probably arrange to have different cabal prefixes20/06 19:23
Eduard_Munteanu(not exactly coexisting, but close)20/06 19:23
Eduard_Munteanu(cabal and ghc prefixes, probably)20/06 19:24
xplatcabal-dev for that maybe?20/06 19:46
xplatdon't know how well cabal-dev works with binaries, and you'd need to do something about emacs too20/06 19:46
Saizanyeah, emacs is what worries me, i guess i'll just have to edit the config files in a few places when i want to switch20/06 20:50
dylukesI'm having an obnoxious bug trying to cabal install agda 2.10.11 and the std lib from head.20/06 21:45
dylukesPasting...20/06 21:45
dylukeshttps://gist.github.com/103654020/06 21:46
dylukesI'm on OS X 10.7, x86_6420/06 21:46
copumpkinthat'll teach you to be an early adopter of OS X20/06 21:46
copumpkin;)20/06 21:46
copumpkinnot sure anyone's looked much at making ghc work on 10.7 yet20/06 21:46
dylukes>_>20/06 21:46
copumpkinyou should talk to dankna20/06 21:47
dylukesIt's worked perfectly fine otherwise.20/06 21:47
copumpkinhmm, dunno20/06 21:47
dylukesHah, dankna always has my problems too ^^20/06 21:47
dylukesI fixed the LLVM issue btw, just not elegantly.20/06 21:47
dylukesI removed the check for llvm-c entirely.20/06 21:47
copumpkin:o20/06 21:47
dylukesBut the only problem with that is,20/06 21:47
dylukesyou need to make sure when you build llvm you build it with --shared-lib20/06 21:47
dylukes(even if you do, cabal won't find it/link it...)20/06 21:48
dylukes(so have to remove the check)20/06 21:48
dylukesanyways, it works (ish)20/06 21:48
dylukesOn a different note.20/06 21:49
dylukesCould someone explain dot patterns and views to me ._.20/06 21:49
dylukesfor instance, as used in an equals proof/function20/06 21:49
dylukesor in the case of finding the parity of a number.20/06 21:49
dylukes.(2 * k + 1)20/06 21:50
dylukesetc20/06 21:50
Saizanpattern matching on something can give you additional information on what its indexes are20/06 21:55
Saizandot patterns make that info visibile in the source20/06 21:56
dylukesdo you have some sort of… canonical example20/06 21:57
dylukessomething simple and explicative?20/06 21:57
Saizanthe simplest indexed datatype is propositional equality20/06 21:59
Saizandata _==_ (A : Set) : A -> A -> Set where refl : {x : A} -> x == x20/06 21:59
dylukesThat makes some measure of sense.20/06 22:00
dylukesI mean, I get that.20/06 22:00
Saizansuppose that you want to show that it's symmetric:20/06 22:00
dylukesalright...20/06 22:00
Saizansym : {A : Set} -> (x y : A) -> x == y -> y == x20/06 22:00
copumpkinI like the half-indexed _==_20/06 22:01
copumpkindata _==_ {A : Set} (x : A) : A -> Set where20/06 22:01
copumpkinrefl : x == x20/06 22:01
Saizansym x y eq = ?20/06 22:01
Saizandylukes: so, we are in a situation like "sym x y eq = ?" where eq : x == y and ? : y == x20/06 22:01
dylukesone moment >_<20/06 22:02
Saizan"?" stand for some code we have to fill in20/06 22:02
dylukesright, I get goals somewhat… though emacs is a bitch and keeps interpreting C-c C-SPC as C-c C-@20/06 22:03
dylukes>_>20/06 22:03
dylukesand your refl isn't working for me… one moment20/06 22:03
Saizanmy _==_ you mean?20/06 22:04
dylukesyeah...20/06 22:04
dylukesone second20/06 22:04
Saizanah, sorry20/06 22:04
dylukesI had20/06 22:04
dylukesdata _≡_ {a : Level}{A : Set a}(x : A) : A → Set where20/06 22:04
dylukes  refl : x ≡ x20/06 22:04
dylukesin another file.20/06 22:04
Saizandata _==_ {A : Set} : A -> A -> Set where refl : {x : A} -> x == x <- A should be implicit20/06 22:04
Saizanyeah, that works too20/06 22:04
dylukesAnyhow, it doesn't like your implifix.20/06 22:04
dylukesalright so20/06 22:05
dylukessym x y eq = { }020/06 22:05
Saizannow, we want to make use of the fact that x == y, so we want to pattern match on eq20/06 22:05
dylukesalright...20/06 22:06
Saizan"sym x y refl = ?" doesn't work though, because x and y still appear unrelated20/06 22:06
dylukesmmk20/06 22:06
Saizan"sym x .x refl = ?" will20/06 22:06
dylukesSee, it seems to be that the dot is using to assert that those x's are the same… but somehow it's not...20/06 22:07
dylukesI'm confused by it TT_TT;20/06 22:07
Saizanthe dot is not actually pattern matching, it's just exploiting the info you get from pattern matching on refl20/06 22:08
Saizanit's not comparing x and y at runtime20/06 22:08
copumpkindylukes: the dot means that some other pattern element is forcing them to be the same20/06 22:09
dylukeshm20/06 22:09
dylukesso whats the full definition of sym?20/06 22:09
Saizansym x .x refl = refl20/06 22:09
dylukesit just says20/06 22:09
dylukesFailed to infer the value of dotted pattern20/06 22:09
dylukeswhen checking that the pattern .x has type A20/06 22:09
dylukeshm20/06 22:09
copumpkinyou probably don't have a refl in scope?20/06 22:10
dylukesso… what is the definition of the . there20/06 22:10
dylukesI do now, I fixed it20/06 22:10
copumpkinthat should work then20/06 22:10
Saizandid you put a type signature for sym?20/06 22:10
dylukesyep, it works now.20/06 22:10
dylukesSo, what is the . asserting then?20/06 22:10
Saizanthat the second argument is the same as the first20/06 22:11
dylukes"the same"20/06 22:11
dylukesaccording to who?20/06 22:11
Saizanaccording to agda20/06 22:11
dylukesI mean, we just defined equivalence here… it's not inbuilt… it must be some type checker thing.20/06 22:11
Saizanyeah, but the way we've defined it ends up exploiting the typechecker notion of equality20/06 22:12
dylukesso… the type signature of sum asserts x and y are both members of the same data type.20/06 22:12
dylukesand I guess that x == y and y == x are valid.20/06 22:12
dylukesand x and y must be the same for == to work I guess?20/06 22:13
dylukesI'm just used to the "if you do something wrong -> error" mentality20/06 22:13
dylukesnot the "if you do something wrong it just doesn't work"20/06 22:13
Saizanyou type too fast :\20/06 22:13
dylukes…in short, I don't quite get it ^^;20/06 22:13
Saizananyhow, the types "x == y" and "y == x" are valid just by knowing that x and y have the same type20/06 22:14
Saizani.e. it's perfectly fine to say (3 == 4), it's quite harder to provide a term of type (3 == 4)20/06 22:15
dylukes:\20/06 22:15
dylukesstill somewhat confused.20/06 22:15
dylukesI think the whole proof mentality really hasn't sunk in quite yet ^^;20/06 22:15
copumpkindylukes: have you come across the empty type?20/06 22:15
dylukesnope.20/06 22:15
copumpkindata Empty : Set where20/06 22:15
copumpkinwrite that in20/06 22:15
copumpkinit'll typecheck20/06 22:16
dylukessure.20/06 22:16
copumpkinyou'll never  be able to provide a value of it20/06 22:16
dylukesright20/06 22:16
copumpkinnow, what if someone asks for20/06 22:16
copumpkinEither Empty Bool20/06 22:16
copumpkinwhat can you give them20/06 22:16
dylukesahhh mkk20/06 22:16
dylukesRight true20/06 22:16
dylukesis perfectly fine20/06 22:17
dylukesyou just can't give them Left ...20/06 22:17
copumpkinand Right False20/06 22:17
copumpkinyeah20/06 22:17
copumpkinso there are only two inhabitants of that type20/06 22:17
copumpkinhow about20/06 22:17
copumpkin(Empty, Bool) (haskell notation)20/06 22:17
dylukesYou can't provide a value of that type.20/06 22:17
dylukesIt's A -> B -> A x B20/06 22:17
dylukesI guess.20/06 22:18
dylukesokay, so the only possible inhabitants of the _==_ type you can provide, are those constructed via refl, which is of type x == x20/06 22:19
dylukesso the type checker can figure out in sym that since you're using x == y -> y == x, x and y cannot be different?20/06 22:19
dylukes…but then where does the dot come in :\20/06 22:19
Saizanthe typechecker just looks at the type of refl.20/06 22:20
Saizanit knows eq : x == y from the type signature, and refl : a == a from the definition of _==_20/06 22:20
dylukesI have20/06 22:21
dylukessym : {A : Set} -> (x y : A) -> x == y -> y == x20/06 22:21
dylukessym x .x refl = refl20/06 22:21
dylukescorrect right?20/06 22:21
Saizanyes20/06 22:21
dylukesI'm noticing more often than not, the point of writing a function in Agda is not to run it :\20/06 22:21
dylukesjust to make it actually exist/work20/06 22:21
Saizanthe proofs are like that :)20/06 22:21
dylukeslike20/06 22:22
dylukessym : {A : Set} -> (x y : A) -> x == y -> y == x20/06 22:22
dylukesisn't really doing anything useful :\20/06 22:22
dylukesexcept saying given two values of a type A,20/06 22:22
dylukesand x == y20/06 22:22
dylukesthen y == x20/06 22:22
dylukesis that correct?...20/06 22:22
Saizananyhow, to typecheck that code it has to unify x == y with a == a (where a is a fresh variable here), so it concludes that x and y must be the same, and the dot serves just to display the result of this unification in the source20/06 22:22
dylukesunification means?20/06 22:22
Saizandylukes: in this case: find a mapping from 'a' to some term such that the two are equal20/06 22:23
dylukesokay, this might come off as pedantry/ignorance20/06 22:23
dylukesbut what's the formal definition of term here.20/06 22:24
dylukesterm/value/type/data type/etc20/06 22:24
Saizanby "the two" i mean "x == y"  and "a == a"20/06 22:24
dylukesah I see...20/06 22:25
dylukesI guess if you were to take20/06 22:25
dylukessym x .x refl = refl20/06 22:25
dylukesand substitute in the types to see if they match the type signature of sum… yeah20/06 22:25
Saizansym, you mean?20/06 22:25
dylukesyeah, autocorrect20/06 22:25
dylukesso, . is just indicating that what you put there should be the result of typechecking?20/06 22:27
dylukeslike "dear type checker, if this isn't the type you figure out, throw an exception"20/06 22:27
Saizanexcept that it's not a type, but yeah20/06 22:28
dylukeser… right20/06 22:28
dylukesthe type/value distinction gets a bit blurry sometime >_<20/06 22:29
copumpkinall types are values20/06 22:29
copumpkinbut not all values are types20/06 22:29
copumpkinwell, there's one type that isn't a value20/06 22:29
Saizanmost of the time i'd just say expression or term20/06 22:29
Saizanvalue might mean something in WHNF in some contexts20/06 22:30
dylukesconfused >_<20/06 22:30
dylukesso, do you have another example?20/06 22:31
dylukesor maybe ,help me understand this one...20/06 22:31
dylukesokay20/06 22:31
dylukessay the nat parity example...20/06 22:31
Saizanpaste?20/06 22:32
dylukesI am one moment20/06 22:32
dylukestyping out Nat quickly20/06 22:32
dylukesI wish I had std lib working >_>20/06 22:32
dylukesokay20/06 22:33
dylukesYou know the agda tutorial pdf?20/06 22:33
dylukesOn page 22 of 4120/06 22:33
dylukesdata Parity : Nat -> Set where20/06 22:33
dylukeseven : (k : Nat) -> Parity (k * 2)