some kind classes

kindclass.hs

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

-- (some examples at the bottom)

import Data.Kind (Constraint, Type)
import GHC.TypeLits (Nat, type (+), type (*))
import Prelude hiding (Monoid, Semigroup)

--               v- this looks innocent, but remember, `k` can actually be any kind!
class Semigroup (k :: Type) where
  -- instead of ordinary class functions, we define type-level functions
  type (a :: k) <> (b :: k) :: k

class Semigroup k => Monoid (k :: Type) where
  type Mappend (a :: k) (b :: k) :: k
  type Mappend a b = a <> b
  type Mempty :: k

-- These will be handy later

type family Fold (ts :: [m]) :: m where
  Fold '[] = Mempty
  Fold (t ': ts) = Mappend t (Fold ts)

type family Map (f :: a -> b) (as :: [a]) :: [b] where
  Map _ '[] = '[]
  Map f (a ': as) = (f a ': Map f as)

type FoldMap f xs = Fold (Map f xs)

--------------------------------------------------------------------------------
-- * Constraints

instance Semigroup Constraint where
  type a <> b = (a, b)

instance Monoid Constraint where
  type Mempty = ()

type All c xs = FoldMap c xs

--------------------------------------------------------------------------------
-- * (+, 0)

data Add = Add Nat

type family UnAdd n where
  UnAdd ('Add n) = n

instance Semigroup Add where
  type ('Add a) <> ('Add b) = 'Add (a + b)

instance Monoid Add where
  type Mempty = 'Add 0

--------------------------------------------------------------------------------
-- * (*, 1)

data Mult = Mult Nat

type family UnMult n where
  UnMult ('Mult n) = n

instance Semigroup Mult where
  type ('Mult a) <> ('Mult b) = 'Mult (a * b)

instance Monoid Mult where
  type Mempty = 'Mult 1

--------------------------------------------------------------------------------
-- * Some examples

f :: Fold (Map Show '[a, b]) => a -> b -> String
f a b = show a ++ ", " ++ show b

type Sum xs = UnAdd (Fold (Map 'Add xs))

-- *Main> :kind! Sum '[1,2,3,4,5]
-- Sum '[1,2,3,4,5] :: Nat
-- = 15

type Prod xs = UnMult (Fold (Map 'Mult xs))
-- *Main> :kind! Prod '[1,2,3,4,5]
-- Prod '[1,2,3,4,5] :: Nat
-- = 120