[wyager]

> I make a ML-style functor parameterized by a structure containing 15 abstract type members.

You can do this in Haskell with DataKinds (you just pass around a type of the correct kind which contains all the parameters). Admittedly, it is quite clunky at the moment. I did this to pass around CPU configuration objects for hardware synthesis a la Clash, as CPU designs are often parametrized over quite a few Nats.

> parametricity is an abstract uniformity property enjoyed by parametrically polymorphic functions

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. There is no particular reason to assume that (+) has the same behavior for Int and Word, except insofar as we have some traditional understanding of how addition should work and which laws it should respect. The same is true for type families. It is not a problem that they introduce non-uniform behavior; we can only ask that they respect some specified rules with respect to their argument and result types.

Case-analyzing types in type families is no worse than writing a typeclass instance for a concrete type. 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!

[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.