[Haskell-cafe] Injective type families for GHC - syntax proposals

[flicky frans]

2014-09-18 21:38 GMT+04:00, Brent Yorgey <byorgey at gmail.com>:
> On Thu, Sep 18, 2014 at 11:02 AM, flicky frans <flickyfrans at gmail.com>
> wrote:
>
>>    Plus a b :: (result :: Nat)
>>
>> That looks quite unintuitive to me, since `result' reads like a
>> variable of type Nat.
>
>
> But isn't that exactly what it is supposed to be?

At least (Plus a b :: Nat) /= (Plus a b :: (result :: Nat)), since a
variable of type Nat is not the type of Plus a b. In (a :: (b :: c))
`a' is a variable, `b' is a type, `c' is a kind (in System F, of
course)

But yes, I made a mistake, `result' should be a variable. Maybe this?

  type family Plus a b = r :: * | r a -> b, r b -> a where