Distinguish type parameters from indices

[simonpj]

Martijn van Steenbergen pointed out this program:

{-# LANGUAGE TypeFamilies #-}

module M where

-- Accepted
type family T1 f e :: *
class C1 f where
  op1 :: T1 f e -> Either e a

-- Rejected
class C2 f where
  type T2 f e :: *
  op2 :: T2 f e -> Either e a

At the moment (HEAD) the C1/T1 version is accepted but the C2/T2 declarations are rejected:

TF.hs:12:3: Not in scope: type variable `e'

I think this is just a bug.

Simon

[chak]

No, it's not a bug. The second example ought to be written:

class C2 f where
  type T2 f :: * -> *
  op2 :: T2 f e -> Either e a

The parameters of an associated family declaration must be a subset of the class parameters as documented at  http://haskell.org/haskellwiki/GHC/Type_families#Associated_family_declarations_2.

However, remember that

type family S1 a :: * -> *

and

type family S2 a b :: *

are not the same thing. S1 has one type index (and in each occurrence must be applied to at least one argument), whereas S2 has two type indices (and in each occurrence must be applied to at least two type arguments). (BTW, I'm not saying that this is the only design that's possible, but it is what we decided to be most useful at the time.)

However, the error message can certainly be improved!

[simonpj]

Oh yes, silly me. The point is that in a class instance declaration you only get to write one associated type instance declaration, so there is no point in having a type index that is not also a class index.

The syntax for distinguishing type indices from type parameters is horrible, but it's hard to think of something better.

Simon

[MartijnVanSteenbergen]

Moving the type index e to the right of the ::—turning it into a type parameter, like Manuel suggests—complicates writing certain instances. Before I could write:

type instance T2 () e = e -> Bool

But now I have to write:

instance C2 () where
  type T2 () = T2Unit

newtype T2Unit e = T2Unit (e -> Bool)

introducing a newtype whenever the type is not directly eta-reducible. In my case this defeats the purpose of writing these instances, as the goal is to derive a simpler type from a generic representation of a datatype (instances for generic building blocks), not a more complicated one (with newtypes that weren't necessary before).

Just to be clear, there isn't really a problem, because I can just leave the type family outside the class. So the actual question here is: why are [type family inside type class] and [multiple family indices for writing type lambdas] sometimes mutually exclusive?

Thanks,

Martijn.

[simonpj]

I'm getting there slowly. If you write

type family T1 f :: * -> *    -- T1 has one type index parameter
type instance T1 [f] e = e

you get the error

Tf.hs:7:0:
    Number of parameters must match family declaration; expected 1
    In the type synonym instance declaration for `T1'

Now I think Martijn is actually doing this

type family T2 f e :: *      -- T2 has two type indices, f and e
type instance T2 [f] e = e

This means that T2 gets arity 2, and has two type indices. In principle you could give another type instance that dispatches on the second parameter:

type instance T2 f Char = [f]

although I don't think Martijn intends that.

Returning to T1, could we reasonably expect to declare a type instance with two parameters like this?

type instance T1 [f] e = e

No, we could not. T1 is declared to have arity 1, so GHC ensures that it is saturated (appears applied to one argument). So it'd be fine to write the type Monad (T [f]) for exmaple. But with the above instance, T [f] is in effect a type synonym; or if you like T [f] is \e.e. So it should not appear un-saturated. So T1's arity depends on its argument. This is not good. That's the reason for the rule.

However, if we had a way to distinguish type indices from type parameters, we could say

type family T3 f !e :: *         -- The ! indicates a type parameter (not an index)
type instance T3 [f] e = e

This would say

• T3 has arity 2 and must always appear applied to two arguments
• Only f is an index, so only f can be instantiated in a type instance

Note that the indices would not necessarily be the first parameters, although they usually will be.

This would extend naturally to associated types, so you could write this, just as Martijn wishes:

class C f where
  type T4 f !e :: *

Interesting.

Simon

[MartijnVanSteenbergen]

Yes, I do intend to never use specific types for e when writing instances. In every instance it will be a 'polymorphic' e (if polymorphic is the right word here), so it behaves like argument, not an index (using Simon's terms). I'm sorry I haven't been able to make myself clear sooner. :-) The idea behind the bang solution is exactly what I have in mind.

Part of the confusion I think is that I was already expecting this to work: the problem only occurs inside type classes and instances, and the compiler knows exactly where the bangs should go, namely those indices/parameters on the left of the :: that do not appear in the type class header.

[chak]

I believe SimonPJ added this functionality a few months back. So, I am closing this ticket.