Camelia, the Perl 6 bug

IRC log for #darcs-theory, 2009-04-27

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
08:34 gal_bolle joined #darcs-theory
08:34 gal_bolle hi
09:40 Igloo Hey
09:42 gal_bolle seen my mail?
09:43 Igloo Yup. This one looks like it doesn't have scary things like <q,r> <~> <q'',r''>  :-)
09:43 gal_bolle well, they are properly enclosed in coq code
09:43 gal_bolle but they're still there
09:43 Igloo I mean the variable names
09:44 gal_bolle ok, i
09:44 gal_bolle i'm not sure what i've made simpler on this front
09:45 Igloo You don't see why <<q,r>> <~> <<r'',q''>> is easier to understand?
09:45 gal_bolle no
09:45 Igloo q and r'' are "the same patch" in the first example
09:45 gal_bolle oh yes
09:46 gal_bolle that was an embarassing typo
09:46 Igloo I wasn't sure what you actually meant, so got confused  :-)
09:46 gal_bolle coq has a tendency to auto-correct me with these things than
09:46 gal_bolle ks to using states everywhere
09:47 gal_bolle so i tend to be sloppy when it's not there to check
09:47 Igloo Grr, why do people keep spamming camp ticket #13?
09:49 * Igloo removes anonymous's ticket create/modify permissions. It's not like camp has any users anyway
09:59 gal_bolle by the way, do you know about stuff like 2-categories?
10:00 Igloo Doesn't ring a bell
10:00 gal_bolle i think there might be a way to state patch theory within a known  algebraic framework
10:07 Igloo That would certainly be nice, especially if it gave us theorems for free
11:20 tux_rocker joined #darcs-theory
12:17 gal_bolle joined #darcs-theory
12:23 Igloo gal_bolle: I have a problem
12:24 Igloo Ignoring the fact that http://hpaste.org/fastcgi/hpaste.fcgi/view?id=4244 can't be written as is, it's also not true
12:24 Igloo All I can prove is that (NameSet.Equal mid' mid'')
12:27 gal_bolle that's normal
12:27 gal_bolle that's all what holds
12:28 gal_bolle if you have built mid' and mid'' using different set operations they're not equal
12:28 gal_bolle one moment
12:28 gal_bolle did you add the assumptions that names were ordered or not?
12:29 gal_bolle if you didn't, then one can build a counter-example of your goal by building mid' and mid'' in such a way that they are not =, only NameSet.Equal
12:30 gal_bolle otherwise, you have the assumption that a `Set.Equal` b -> a = b somewhere in one of  the FSetSomethings modules
12:30 gal_bolle FsetFacts, I thin
12:30 gal_bolle k
12:31 gal_bolle damened typematrix keyboard, my return key is where my 'k' key used to be
12:31 Igloo :-)
12:32 * gal_bolle has a southern-french accent on irc: "damened"
12:32 gal_bolle cong
12:34 Igloo I don't think FSetFacts does it, unless    Add Relation t Equal ... as EqualSetoid    does it somehow
12:34 gal_bolle nope
12:34 gal_bolle this would allow you to use setoid_rewrite i believe
12:34 gal_bolle do you use a FSet or a FWeakSet?
12:35 Igloo I use FSetWeakList
12:35 gal_bolle ok, then your theorem only holds with NameSet.Equal, not with =
12:36 gal_bolle = is real equality, you can't overload it
12:36 gal_bolle and extensionality does not hold for FSetWeakLists
12:37 gal_bolle ie, you can have two sets with the same elements whose representations are not the same
12:37 Igloo Maybe I should just make names ordered. Mutter grumble abstraction.
12:37 gal_bolle if you want to mumble grumble abstraction, then just make NameSet abstract as a whole
12:37 gal_bolle make NamedPatches a functor
12:38 gal_bolle and NameSet an argument of this functor
12:38 Igloo Ah, you mean let it take any non-weak FSet?
12:39 gal_bolle and in the type of that argument, have module type NameSet: [some stuff] … Axiom extensional: forall a b, a has the same elements as b -> a = b
12:39 gal_bolle yes
12:39 Igloo Maybe I should use an ordered set for now, and do clever stuff like that later
12:39 Igloo Thanks for your advice!
12:39 gal_bolle yup
12:39 gal_bolle having an order on names is really an innocent axiom on the other hand
12:40 Igloo But it's the /principle/ of the thing  :-)
12:43 Igloo Are you sure that one of the FSet modules defines Equal => =? I can't find it
12:44 Igloo s/defines/proves/
12:45 gal_bolle maybe it's somewhere else
12:45 gal_bolle i think i saw it somewhere
12:45 Igloo I think it was in that metatheory thing you showed me
12:46 gal_bolle ah yes, probably
12:47 Igloo Yes, http://www.cis.upenn.edu/~plclub/popl0​8-tutorial/code/coqdoc/FiniteSets.html has it
12:48 Igloo But that's essentially the same as making it an axiom, isn't it?
12:49 gal_bolle yes
12:49 gal_bolle i think so
12:50 gal_bolle but why aren't you happy with an Equal in the conclusion of that theorem?
12:50 gal_bolle oh because then those NameSets creep into the types
12:50 Igloo Because it doesn't allow me to show that q' = q''
12:51 gal_bolle yes, so add the axiom
12:51 Igloo (admittedly that's not technically true, but it morally is  :-)  )
12:51 Igloo *nod*, OK, thanks again
13:22 tux_rocker joined #darcs-theory
13:48 tux_rocker_ joined #darcs-theory
14:36 gal_bolle joined #darcs-theory
16:49 arjanb joined #darcs-theory
19:26 tux_rocker joined #darcs-theory
20:51 tux_rocker joined #darcs-theory

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary