How to create a “class class” in Haskell or type-level ad-hoc polymorphism using type families

Question

I study the functions of the Haskell type family and compute the level level. It seems pretty easy to get level-level parametric polymorphism with PolyKinds :

 {-# LANGUAGE DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators, UndecidableInstances, PolyKinds, MultiParamTypeClasses, FlexibleInstances #-} data NatK = Z | S NatK data IntK = I NatK NatK infix 6 + type family (x :: NatK) + (y :: NatK) :: NatK where Z + y = y (S x) + y = S (x + y) -- here a parametrically polymorphic (==) at the type-level -- it also deals specifically with the I type of kind IntK infix 4 == type family (a :: k) == (b :: k) :: Bool where (I a1 a2) == (I b1 b2) = (a1 + b2) == (a2 + b1) a == a = True a == b = False 

I can do things like :kind! Bool == Bool :kind! Bool == Bool or :kind! Int == Int :kind! Int == Int or :kind! Z == Z :kind! Z == Z and :kind! (IZ (SZ)) == (I (SZ) (S (SZ))) :kind! (IZ (SZ)) == (I (SZ) (S (SZ))) .

However, I want to make type + ad-hoc polymorphic. So this is limited to the cases that I give them. The 2 examples here are NatK view NatK and IntK view IntK .

At first I tried to make it parametrically polymorphic:

 infix 6 :+ type family (x :: k) :+ (y :: k) :: k where Z :+ y = y (S x) :+ y = S (x :+ y) (I x1 x2) :+ (I y1 y2) = I (x1 :+ y1) (x2 :+ y2) 

It works, how can I do :kind! (I (SZ) Z) :+ (I (SZ) Z) :kind! (I (SZ) Z) :+ (I (SZ) Z) .

However, I can also do :kind! Bool :+ Bool :kind! Bool :+ Bool . And this makes no sense, but allows you to use it as a simple type constructor. I want to create a type family that does not allow such erroneous types.

At that moment I was lost. I tried class types with the type parameter. But that did not work.

 class NumK (a :: k) (b :: k) where type Add ab :: k instance NumK (Z :: NatK) (b :: NatK) where type Add Z b = b instance NumK (S a :: NatK) (b :: NatK) where type Add (S a) b = S (Add ab) instance NumK (I a1 a2 :: IntK) (I b1 b2 :: IntK) where type Add (I a1 a2) (I b1 b2) = I (Add a1 b1) (Add a2 b2) 

It still allows :kind! Add Bool Bool :kind! Add Bool Bool .

Is this ConstraintKinds extension, where do I need to limit :+ or Add some “cool class”?

Answer 1

The simplest solution is to use open-type families for ad-hoc overloads and closed-type families to implement:

 data NatK = Z | S NatK data IntK = I NatK NatK type family Add (x :: k) (y :: k) :: k type family AddNatK (a :: NatK) (b :: NatK) where AddNatK Z b = b AddNatK (S a) b = S (AddNatK ab) type family AddIntK (a :: IntK) (b :: IntK) where AddIntK (I ab) (I a' b') = I (AddNatK a a') (AddNatK b b') type instance Add (a :: NatK) (b :: NatK) = AddNatK ab type instance Add (a :: IntK) (b :: IntK) = AddIntK ab 

If we want to group several types of level and terminological level together, we can write class classes using KProxy from Data.Proxy :

 class NumKind (kproxy :: KProxy k) where type Add (a :: k) (b :: k) :: k -- possibly other methods on type or term level instance NumKind ('KProxy :: KProxy NatK) where type Add ab = AddNatK ab instance NumKind ('KProxy :: KProxy IntK) where type Add ab = AddIntK ab 

Of course, related types are the same as open type families, so we could also use open type families with a separate class for term-level methods. But I think it’s generally cleaner to have all the overloaded names in the same class.

From GHC 8.0, KProxy is no longer needed, since views and types will be handled in exactly the same way:

 {-# LANGUAGE TypeInType #-} import Data.Kind (Type) class NumKind (k :: Type) where type Add (a :: k) (b :: k) :: k instance NumKind NatK where type Add ab = AddNatK ab instance NumKind IntK where type Add ab = AddIntK ab 

Answer 2

(This should be a comment, but I need more space)

I tried something like

 class GoodK (Proxy k) => NumK (a :: k) (b :: k) where ... 

but i failed. I do not know if it is possible that you ask.

The best approximation I got is to do an Add Bool Bool kind-check, but create an unsolvable restriction, so if we ever use it, we will get an error anyway. Perhaps this may be enough for your purposes (?).

 class Fail a where instance Fail a => NumK (a :: *) (b :: *) where type Add ab = ()