[catnaroek]

> Whenever one introduces a typeclass constraint to a function, one can only assume that the function exhibits uniform behavior up to the differences introduced by different instances of the typeclass.

Of course.

> Would you say that the fact that "instance Ord Word" and "instance Ord Int" are non-isomorphic is a problem? After all, the types themselves are isomorphic!

It's already bad enough, but at least the existence of non-uniform behavior is evident in a type signature containing type class constraints. OTOH, type families are sneaky, because they don't look any different from normal type constructors or synonyms.

[wyager]

>OTOH, type families are sneaky, because they don't look any different from normal type constructors or synonyms.

That is fair.

I think we're on the same page at this point. You have made me realize that ML-style modules are useful in ways I did not realize before, so thanks for that.

Question: How would you feel if the tradition was to do something like

insert :: Ord a f => a -> Set f a -> Set f a

That is, "f" is some type that indicates a particular ordering among "a"s. Then, "Set"s are parametrized over both "f" and "a", and one cannot accidentally mix up Sets that use a different Ord instance.

Here's a quick example:

https://gist.github.com/wyager/a021f7e5d9f23643bc90a9866b5c0...

[catnaroek]

Seems a lot more cumbersome than the direct ML solution:

    signature ORD =
    sig
      type t
      val <= : t * t -> t
    end
    
    functor RedBlackSet (E : ORD) :> SET =
    struct
      type elem = E.t
      
      datatype set
        = Empty
        | Red of set * elem * set
        | Black of set * elem * set
      
      (* ... *)
    end
    
    structure Foo = RedBlackSet (Int)
    structure Bar = RedBlackSet (Backwards (Int))
    
    (* Foo.set and Bar.set are different abstract types! *)

[wyager]

That is more elegant! But do you think they're functionally more or less equivalent?

[catnaroek]

Assuming you don't mind plumbing value-level proxies all over the place, it's indeed functionally equivalent.