On Fri, May 1, 2015 at 12:48 AM, Keean Schupke <[email protected]> wrote: > On 30 Apr 2015 23:08, "Matt Oliveri" <[email protected]> wrote: ... >> >>> and the fast-union would require all sets >> >>> to have the same type. >> >> >> >> No it wouldn't. It needs the two sets it was passed to have the same >> >> element type and ordering, and it needs to have access to the >> >> comparator for that ordering. >> > >> On Thu, Apr 30, 2015 at 5:39 PM, Raoul Duke <[email protected]> wrote: >> > It makes sense to me that we are better off splitting out as many >> > types/interfaces as possible. >> > >> > e.g. Set+{Ascending,Descending,Random >> SetAscending, SetDescending, >> > SetRandom. >> >> Then how do you define fast union generically? No, I think the order >> really wants to be a parameter of the Set family. > > I want the order to be a _type_ parameter of the set type.
Well an ordering is not a type. Aside from that, we suddenly seem to agree. This is not what you seemed to be saying before. But from your code, it seems like you're trying to do something else. > You define fast union genetically by only defining instances where the order > is the same, and using phantom types, so: On Fri, May 1, 2015 at 12:58 AM, Keean Schupke <[email protected]> wrote: > On 1 May 2015 05:48, "Keean Schupke" <[email protected]> wrote: > >> data Set order element = S order [element] "order" and "element" are types? >> data Ord o = O o { >> cmp :: x -> y -> Bool >> } > > Except this needed to be a type class: > > class Ord x where > cmp :: x -> a -> a -> Bool Neither of these seem to be giving cmp the right type. >> data AscendingNumeric = AN Oh this is the phantom type? I think I see where you're going. >> oan = O AN { >> cmp _ = < >> } > > instance Ord AN where > cmp = > Yeah, so I think your Ord was supposed to have two parameters: the phantom type labeling the order, and the element type. "cmp" should take two of the element type: class Ord o x where cmp :: x -> x -> bool instance Ord AN int where cmp = (>) And I don't think a Set needs to hold an element of the phantom type: data Set order element = S :: [element] -> Set order element Of course, the constructor you expose shouldn't be S. It should be something that sorts the elements (and removes duplicates), to establish the invariant that the elements are in order. >> union :: Set o e -> Set o e -> Set o e >> union (S cmp l1) (S _ l2) = ... > > union :: {Ord o} -> Set o e -> Set o e -> Set o e > union (S o l1) (S _ l2) = ... (cmp o) x y ... union :: {Ord o e} -> Set o e -> Set o e -> Set o e union (S l1) (S l2) = ... cmp x y ... >> set1 = S oan [1, 3, 5] > set1 = S AN [1, 3, 5] > >> set2 = S oan [2, 4, 6] > set2 = S AN [2, 4, 6] > >> set3 = union set1 set2 Yes, just leave off the AN, since I took away that argument. So what you seem to be doing is to use phantom types like AscendingNumeric to distinguish different orders for the same element type. You associate an Ord instance not just to an element type, but a pair of "order label" phantom type and element type. This allows you to make sets of the same element type, but ordered differently. "union" requires that the two sets have the same order label. Now here's the nitpicky problem: If you don't have coherent instances, this _still_ might not work. Some idiot could make another "instance Ord AN int", and union could receive sets ordered differently after all. This is much less likely, since people who understand the setup would know to define a new order label to make a new Ord instance, but you still have no guarantee. It seems better to me to skip right to dependent types, so the Set types can depend directly on the order the set uses. No need for typeclasses or phantom types here. To really get a guarantee, each Set should come with a (erased) proof that the elements are stored in the appropriate order. This actually enforces the invariant. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
