On 26/03/2015, at 5:30 AM, Martin DeMello wrote:
>>> I believe this is where you went wrong - a set isn't a container with
>>> a membership operator, it's a container with a membership operator and
>>> the property that all elements are distinct.
>>
>> How would you specify that property?
>
> You can't without dependent types, certainly. (I'm not even sure you
> can *with* dependent types; I know very little about them). In actual
> code you could always maintain the invariant by simply removing
> duplicates on all set-modifying operations.
I think you're missing the point.
class Set[C,T] { virtual fun \in : T * C -> bool; }
defines a Set as a data type with a member operator.
Now, an array, even with duplicate values stored,
can satisfy the axiom, because there's no requirement
about duplication of elements in an array.
Note there's also no requirement for an equality operator,
and no size. This is not your usual mathematical set.
I actually defined a Container as a Set with a length operator.
Consider a regexp: RE2 "(a|b)*abb". That's a set, using the obvious
rule that a string that matches the regexp is in the set.
Consider also:
class MultiSet[C,T] { virtual fun count: T * C -> int; }
I hope it's clear there is a natural transform from MultiSet to Set
using
fun non-zero (x:int) => x != 0;
Now also consider this:
instance[T,N] Set[T^N,T] { fun \in (x:T, a:T^N) => x not-in a; }
That's a perfectly good model of a set too. It's an infinite set,
in this model:
assert 1 \in (2,3);
That really is the crux of the problem. An array can be used in an
infinite number of ways as a set. You could even use
9 in (1,2,3)
given by the fact 9 is the square of 3. It's a design fault in the whole
concept of type classes.
The problem is seen to be serious if you then pick one, and then
you inherit Set into a more constrained class and that constraint
can't be met. For example, and this is *the* example at hand,
if you have Eq for equality and Set as above, and you then want
a subset relation, SetOrd, you're screwed, because array equality
and set equality required for SetOrd aren't compatible.
One can certainly DEFINE an array equality that works for sets,
by ignoring duplicates. So we're back to the original point:
TYPE CLASSES DO NOT WORK
We can actually fix the problem, just use
union[T,N] ArrayAsSet_t = ArrayAsSet of T^N;
instance[T,N] Set[ArrayAsSet_t[T,N],T] { ... }
Note that:
////////////////////
open class Streamable[ContainerType, ValueType] {
virtual fun iterator : ContainerType -> 1 -> opt[ValueType];
// check if a streamable x is a subset of a set y.
fun \subseteq[T with Set[T,ValueType]] (x:ContainerType, y:T) =
{
for v in x do
if not (v \in y) goto bad;
done
return true;
bad:>
return false;
}
}
//////////////////////
works fine and is in the library. There's just no way to use THAT
subseteq operator to define an instance of SetOrd[C1, C2] because
it requires a third type (the ValueType], whereas the set comparisons
don't need that.
Ocaml functors just work better because you have to supply a whole
package as an argument, that is, the functor accepts the type
parameters AND the instance functions. With type classes you can
only define one function for each list of type arguments.
So for example you can make array-as-set in 10 different ways
by giving 10 different functions for the membership operator.
--
john skaller
skal...@users.sourceforge.net
http://felix-lang.org
------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the
conversation now. http://goparallel.sourceforge.net/
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
