Generally, I can get a feel for ‘what sort of a thing’ some type variable is by how it’s used in a type signature.

parTraverse
:: forall f m t a b
. Parallel f m
=> Traversable t
=> (a -> m b)
-> t a
-> m (t b)

Here I read this as if you give me :

A function that takes a purescript value, and returns a value in some larger language

A traversable context containing the same sort of purescript value used by the function

Then I can return you something that relates the two.

I can see that ‘t’ must meet some constraints because it has an instance of a type class (namely ‘Traversable’).

I’m not sure what to make of ‘f m’.

‘f’ is seen only in the constraints and not the arguments or return type. This reads to me like "It doesn’t matter what ‘f’ is, just so long as there exists some ‘f’ somewhere such that ‘Parallel f m’

Whatever ‘Parallel f m’ says about ‘m’, that must be true of ‘m’ here.

Given that f doesn’t matter, couldn’t I create a new typeclass ‘Parallel2’ to read like this:

parTraverse'
:: forall m t a b
. Parallel2 m
=> Traversable t
=> (a -> m b)
-> t a
-> m (t b)

such that ‘m’ is now part of a normal constraint? Would I lose anything?

Right. Parallel f m means that conversions must exist between f and m, where f is the “parallel” version of m. Specifically, the Apply instance of f is presumably going to run each value in parallel while the Apply instance of m presumably runs in sequence.

For example, if I’m using Aff and I say f <$> a <*> b <*> c (so a, b, and c are all Aff values), then it will execute a, b, and c in sequence. It’ll start b once it finishes a, and start c once it finishes b, etc. But if I’m using ParAff (so a, b, and c are all ParAff values) then that same line would execute all three in parallel.
The Parallel type class provides these members

to convert back and forth between the “normal” version and the “parallel” version. So calling parallel on an Aff will give you a ParAff, while calling sequential on a ParAff gets you back to an Aff. The implementation of parTraverse uses these members:

parTraverse f = sequential <<< traverse (parallel <<< f)

So while you as a consumer of the parTraverse function don’t care what f is, the implementation of parTraverse needs to create and use values of type f _. There would just be no way to implement parTraverse without the compiler knowing anything about what type you were converting to and from.

So this is a case where the compiler needs to know about the type constructor f, but you don’t care about it at all. Fortunately, the compiler can also solve for type constructor f without you having to specify what it is, so it’s hopefully not too much of a hassle anyway.

You’re likely to run into similar stuff in the future - it’s not terribly uncommon in PureScript that a type class constrains that some type must exist, but you as a user don’t care at all what that type is.

The need for both f and m in the type signature/constraint here is basically a downside to using functional dependencies to encode situations this, but that’s the tool we have in PureScript.

Associated types are another approach that would enable an alternative encoding of this, where only one parameter is needed on the class. There was some discussion of which approach to take on the original issue. If I remember/understand correctly, there are things you can do with FDs that can’t be done with ATs, unless you also have type families (ATs are a step towards full type families) - but type families are not really something we’re considering adding.

I’m going to need to do some more reading on functional dependencies but is this in the ballpark?

A functional dependency on a type class narrows the domain. To have a correct (compiles) instance of a type class, you now need to be aware of all the other instances of that type class to ensure that type if (a -> b)’, then a’ uniquely identifies type ‘b’ ?

Does this mean that two libraries could be fundamentally incompatible if they both implement instances such that a functional dependency constraint fails?

This is where not allowing “orphan instances” saves us. If I defined a type class

class MyClass a b | a -> b

and elsewhere I defined a type

data MyType = MyType

there are only 2 places that I could put an instance of MyClass MyType _ without it being an orphan: in the same module as MyClass or in the same module as MyType. So to create an instance, one of those module needs to reference the other, and then the dependent module is where the instance goes. Now within that module I might write some broken code like

instance MyClass MyType Int
instance MyClass MyType String

which wouldn’t compile, but there’s no way that I could put those instances in different modules, let alone different packages without getting compile errors about orphan instances first.