On 29 April 2015 at 22:12, Matt Oliveri <atma...@gmail.com> wrote:

> Well, not really. Mathematically speaking, sets don't have an order;
> that's an implementation issue. But whether it's nonsense or just a
> bad idea is besides the point..
>

I think this is missing the point. Sets and Ord are just an example. The
key point I was making was that the 'type' is the tag that differentiates
different orderings, so coherence is not a problem. There is only one
ordering for a given type of set, and the fast-union would require all sets
to have the same type.

In this way you can make coherence a required property and it forces you to
distinguish types, which is exactly what is required to statically
determine which ordering to use.

The point of the implicit parameter is something else. You might sensibly
define:

union : Ord a => Set a -> Set a -> Set a

and

union : (a -> a -> Bool) -> Set a -> Set a -> Set a

The idea with the implicit is that a single definition:

union : {Ord a} -> Set a -> Set a -> Set a

gives both functionalities. With no "ord" argument it behaves like the type
class version, and with the ord argument, it behaves like the explicit
comparison version (except the function needs to be wrapped in an Ord
record).

The point with the 'use' directive is that multiple imported modules may
define different instances of Ord. with the use directive the order of
imports does not affect the functionality, I import the sets I want and I
choose which Ord definition is available implicitly, it doesn't matter if
other modules define different Ord instances.


Keean,
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to