Injective type families

[Kim-Ee Yeoh]

On Fri, Jul 11, 2014 at 3:27 AM, Roman Cheplyaka <roma at ro-che.info> wrote:

> The result of any function is always determined by that function's
> parameters.
>
> Injectivity means that the *parameters* are determined by the result.
>
> So I think Jan's definition is correct.
>

What's correct could still be confusing. Now that you brought it up, I no
longer know what "RHS" in OP means! It could be (1) the result. Or (2) the
right of the vertical bar.

For easy reference, here are the statements in question:

* "Standard injective type family (all parameters uniquely determined by
the RHS)"

* "Type family injective only in some parameters (ie. only some parameters
uniquely determined by the RHS):"

So when you say "arguments always determine result", one has to pause and
think about what that means in the presence of multiple arguments as we
have here. Because that doesn't hold when only some arguments are applied.

Also, note the usage of the expression "uniquely determined" in OP. When a
single-argument function is injective, we say that the argument 'uniquely
determines' (as opposed to just determine) the result. But note how it
appears flipped in OP!

Finally, let's look at how the verb 'determine' is used. When defining a
type family case-by-case, one works from arguments to the result determined
by the arguments. But saying "Injectivity means that the *parameters* are
determined by the result" raises the specter of the inverse function.
Suddenly, the arrow of work gets flipped in reverse. Doesn't that only
contribute to cognitive noise?

Imprecise language not only trips up experts, it also sets up
insurmountable barriers for outsiders. We can do much better here.

-- Kim-Ee
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140711/7873033a/attachment.html>