[Felix-language] Design issue

[john s. <sk...@us...>]

I have just run into an interesting problem. 

I like pretty math operators so I've been making the TeX symbols
for set comparisons work. Stuff like \subseteq for example.

Now, at the moment you can write:

	x \in (1,2,3,4)

and it works. This is because "an array is a Set". FYI we have these
basic concepts:

	Set -- membership operator
	Container -- as set with a size operator (i.e. a finite set)

as well as Eq (equivalence relation, equality), Pord (partial order),
and Tord (total order).

I decided to do SubSet, with the nice curvy comparisons for sets from
maths: its just a Set with \subseq and \subseteq defined, the other
operators are derived. I did this:

class SubSet[c] {
   inherit Eq[c];
   virtual fun \subseteq: c * c -> bool;
   virtual fun \subset (x:c, y:c) => x \subseteq y and not x == y;
   fun \subseteqq (x:c,y:c) => x \subseteq y;

and then I realised WHOA! Hold on there!!

These arrays are subsets:

	(1,2) \subset (1,2,3,4)

Sure, but then what about this:

	(1,2) \subseteq (1,1,2)

It's a subset, and as sets, these arrays are equivalent.
But as themselves, as arrays, they're NOT equal.

On the other hand, whilst set operations for a partial order,
arrays with a total order on the element type can also form
a total order with lexicographical comparison.  And that
order is not the same as the setwise ordering!

Unfortunately, we don't have an == operator for sets, distinct
from arrays, even if we can use < and \subset distinctly to
provide two distinct orderings.

In general this is a "bug" in the idea of type classes.
In Haskell too. Ocaml functors are correct, type classes
are canonical functors and so only cover common cases.

Another example is Tord[int]. It's an ascending order.
But there is a perfectly good *descending* total order as well.
We can fix this by using

	union revint = Rev of int;

Now we've made a new type, we can define a reverse order
on it so

	Rev 1 > Rev 2

There's no performance cost (unions of one constructor are downgraded
to the constructor's argument after binding is complete).

But this is not very general .. it only applies to a single type.
[Generalised Algebraic Data types (GADTs) might help, I don't know]

However all this is suggesting the I am confusing an array with 
"an array considered as a set". And that there should be a
*conceptual* meta type "SET" and that we should have
to CAST an array to it to consider it as a set.

	x \in SET (1,2,3,4)

Note that SET is a functor from TYPE to SET, there is no actual
thing SET, it's not a data type (it's a meta type!).

The point is this:

	SET (1,2) == SET (1,1,2)
	(1,2) != (1,1,2)

I have to think what this means exactly .. especially as for some types
there may be more than one way to use that type as a model for
something else, and, because the idea doesn't just apply to a single
type, but perhaps several (eg a tree with labels on edges and nodes
of a distinct type, or, an abstract container C with a value type T).

--
john skaller
sk...@us...
http://felix-lang.org