Re: Injective type families

* Kim-Ee Yeoh [2014-07-10 23:40:44+0700]

On Thu, Jul 10, 2014 at 9:37 PM, Jan Stolarek wrote:

...

1. Standard injective type family (all parameters uniquely determined by the RHS): injective type family F a b c | a b c

<snip>

2. Type family injective only in some parameters (ie. only some parameters uniquely determined by the RHS): injective type family G a b c | a b

English is not my mother tongue. Perhaps you mean: 'the image under the type function is uniquely determined by the parameters on the right of the vertical bar'?

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.

As they stand, the sentences confuse which determines what.

Such confusion has a way of squirreling into official documentation.