I'm studying the type family features of Haskell, and type level computation.
It appears it's quite easy to get parametric polymorphism at the type-level using 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's 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 or :kind! Int == Int or :kind! Z == Z and :kind! (I Z (S Z)) == (I (S Z) (S (S Z))).
However I want to make type + ad-hoc polymorphic. So that it's constrained to the instances I give it. The 2 instances here, would be types of kind NatK and types of kind IntK.
I first tried making 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)
This works, as I can do :kind! (I (S Z) Z) :+ (I (S Z) Z).
However I can also do :kind! Bool :+ Bool. And this doesn't make any sense, but it allows it as a simple type constructor. I want to create a type family that doesn't allow such errant types.
At this point I'm lost. I tried type classes with a type parameter. But that didn't work.
class NumK (a :: k) (b :: k) where
type Add a b :: 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 a b)
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.
Does this have something to do with the ConstraintKinds extension, where I need to constrain the :+ or Add to some "kind class"?