How to create a "kind class" in Haskell, or ad-hoc polymorphism at the type-level using type families

Question

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"?

Arboreal

Answer 1

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

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 a b)

type family AddIntK (a :: IntK) (b :: IntK) where
  AddIntK (I a b) (I a' b') = I (AddNatK a a') (AddNatK b b')

type instance Add (a :: NatK) (b :: NatK) = AddNatK a b
type instance Add (a :: IntK) (b :: IntK) = AddIntK a b

If we want multiple type-level and term-level methods grouped together, we can write kind classes using 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 a b = AddNatK a b

instance NumKind ('KProxy :: KProxy IntK) where
  type Add a b = AddIntK a b

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

From GHC 8.0, KProxy becomes unnecessary since kinds and types will be treated the exact 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 a b = AddNatK a b

instance NumKind IntK where
  type Add a b = AddIntK a b 

Osculum

Thanks! This is pretty cool, but could you expand on what exactly makes it work? That is, why does it work? For both your open+closed solution, KProxy solution, and the TypeInType solution. – Arboreal

Oh but i just tested your first solution, and it still allows :kind! Add Bool Bool resulting in Add Bool Bool :: *. I was hoping for this to become a type error, instead of being accepted!? – Arboreal

Also your second solution also allows Add Bool Bool. It doesn't show up as a type error. – Arboreal

That's unavoidable. If we have a well-kinded type family application, and there isn't a matching case for the arguments, we get a stuck application, instead of a pattern error as in runtime. A stuck application cannot be used for anything (with an esoteric exception) so this behavior is safe. – Impedance

So, your solution of defining a single poly-kinded closed type family is also safe, it's just not extensible/modular. – Impedance

Ok I guess the behaviour is not possible/not desirable? – Arboreal

It's a valid alternative to the current behavior, perhaps desirable, but definitely not possible currently. – Impedance

@AndrásKovács, that's not the only esoteric exception. The same constraints package also defines a (nullary) class that can't have any instances using class Any => Bottom where no :: Dict a. Since Any is a stuck type family (used here at kind Constraint!) there is no way to satisfy it, and thus no way whatsoever to write even a bogus instance of Bottom. I'm not sure just why that's important, if it is, but it's there. – Sunburst

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 have no idea if what you ask is achievable.

The best approximation I got is making Add Bool Bool kind-check, but generate an unsolvable constraint, so that if we ever use it we'll get an error anyway. Perhaps this could be enough for your purposes (?).

class Fail a where

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

Hollyanne