I don’t know what @hgarrood meant when he said that Purescript’s type constructors are injective.
I mean, sure, injectivity means for any x and y: (f x = f y) → (x = y). Eg. This would mean that (Maybe x = Maybe y) → (x = y).
He told that type families invalidate this reasoning, why do they do so?
Why do you want type constructors to be injective?
The problem seem to be related to most general common unifier.
Lets say we were trying to determine whether the following equation is satisfiable, and we decide to compute the most general common unifier:
f x w = f (g y) z
To solve it, we must have injectivity. The rule allows us to move into the next step:
x = (g y) ∧ (f` w) = (f` z)
The (f’) in the expression is the ‘f’ function with one parameter filled in.
Now we can further move on.
x = (g y) ∧ w = z
Now we have equations that have a variable on another side of a term. We have found the most general common unifier. Ok, Injectivity is required so you can do this.
Anything else?
Type families are arbitrary equations mapping types to other types. I don’t remember the exact syntax, but something like:
type family F a where
F Int = String
F String = String
F a = a
If you assumed injectivity, you could prove that Int ~ String. I think GHC supports injective type families, which are essentially functional dependencies on the type family.