I’ve made a GHC proposal: https://github.com/ghc-proposals/ghc-proposals/pull/521
One thing that has been annoying me for a long time in Haskell, is the inconsistency in defining
associated type instances.
import Data.Kind (Type)
import Data.Functor.Identity (Identity)
-- example type class
class C (a :: Type) where
type F a :: Type
-- this is legal
instance C (Maybe a) where
type F _ = () -- equivalent to `type F (Maybe a) = ()`
instance C (Identity a) where
type F (Identity a) = a
-- Not legal: `type F (Identity b) = b`
-- We have to use the same names, so `a` is in some sense "in-scope".
-- It gets even weirder:
class D (a :: Type) where
type G :: a
instance D (Maybe a) where
type G = (Nothing :: Maybe a)
{-
Not legal: `type G = (Nothing :: Maybe b)`
Error:
• Type indexes must match class instance head
Expected: G @(Maybe a)
Actual: G @(Maybe b)
• In the type instance declaration for ‘G’
In the instance declaration for ‘D (Maybe a)’
|
24 | type G = (Nothing :: Maybe b)
-}
a is obviously in-scope in some way. The user’s guide justifies this by saying it’s “implicitly bound”, but this doesn’t seem consistent with the following:
instance C [a] where
type F [a] = a
-- NOT LEGAL: `type F _ = a`
-- Even though `a` is "in-scope" in some sense, thus prohibiting
-- the above example, we still need to have it on the LHS.
This small inconsistency doesn’t seem that important, but repeating the instance head for no reason seems odd to me, especially when it’s allowed some times.
It would for example simplify the following:
instance (t ~ Applicative.WrappedArrow a' b' c') => Rewrapped (Applicative.WrappedArrow a b c) t
instance Wrapped (Applicative.WrappedArrow a b c) where
type Unwrapped (Applicative.WrappedArrow a b c) = a b c
_Wrapped' = iso Applicative.unwrapArrow Applicative.WrapArrow
into
instance (t ~ Applicative.WrappedArrow a' b' c') => Rewrapped (Applicative.WrappedArrow a b c) t
instance Wrapped (Applicative.WrappedArrow a b c) where
type Unwrapped _ = a b c
_Wrapped' = iso Applicative.unwrapArrow Applicative.WrapArrow
(from lens 5.1)
In general, associated type families have a lot of odd behaviour, and this is just one of them.
The fact that they’re not real members of the class stings in a lot of ways.
As John Ericson pointed out, it’s also hard to imagine any scenario where you wouldn’t want the associated type family parameterised with all of the class parameters, and only the class parameters. All uses of associated type families can seemingly still be done with this restriction.
That way you could have the following (IMO more logical) syntax, proposed by John Ericson:
class C a b where
type F :: Type
instance C (Identity a) (Identity b) where
type F = (a, b)
This kind of change is much bigger though, and I’m not sure how realistic it is.
There’s also the fact that Dependent Haskell might be happening, in which case it might just become:
class C a b where
f :: Type
instance C (Identity a) (Identity b) where
f = Pair a b -- punning is obviously very ambiguous here
Perhaps a step between is still nice though, and in that case, it might still be a backward-compatible change actually.
The following is currently illegal:
class C (a :: Type) where
type F :: Type
For any class with parameters, this syntax is currently disallowed, so it could be used here, albeit it would mean there would be two very different styles of declaring associated type families.
In the zero-parameter case, the two interpretations mean the same thing, so it would be fully backward-compatible, i.e. an associated type family with an explicit arity of zero would be implicitly parameterised by all of the class parameters (which might also be zero).
I’m not sure which approach is best, and how much change to the Haskell language is acceptable.
One thing to note is that the syntax proposed by John Ericson is exactly the syntax that Rust uses.
Thoughts?