type-generics.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
import Data.Kind
import Data.Type.Equality
import GHC.Generics
import GHC.TypeLits

-------------------------------------------------------------------------------
-- Class
-------------------------------------------------------------------------------

class (To r ~ v, From v ~ r) -- , To (From v :: Rep a x) ~ v)
    => TypeGeneric a (r :: Rep a x) (v :: a)
  where
    type To r :: a
    type From v :: Rep a x

-------------------------------------------------------------------------------
-- Iso
-------------------------------------------------------------------------------

toThenFrom
    :: forall a x (r :: Rep a x) (v :: a) pr. TypeGeneric a r v
    => pr x
    -> To (From v :: Rep a x) :~: (v :: a)
toThenFrom _ = Refl

fromThenTo
    :: forall a x (r :: Rep a x) (v :: a) pr1 pr2. TypeGeneric a r v
    => pr1 a -> pr2 (r :: Rep a x)
    -> From (To r :: a) :~: (r :: Rep a x)
fromThenTo _ _ = Refl

-------------------------------------------------------------------------------
-- List
-------------------------------------------------------------------------------

instance TypeGeneric [k] ('M1 ('L1 ('M1 'U1))) '[] where
    type To ('M1 ('L1 ('M1 'U1))) = '[]
    type From '[] = 'M1 ('L1 ('M1 'U1))

instance TypeGeneric [k] ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))) (x ': xs) where
    type To ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))) = x ': xs
    type From (x ': xs) = 'M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))

-------------------------------------------------------------------------------
-- OrdK
-------------------------------------------------------------------------------

class OrdK (k :: Type) where
  type Compare (x :: k) (y :: k) :: Ordering
  type Compare (x :: k) (y :: k) = GenComp (Rep k ()) (From x) (From y)

instance OrdK Nat where
  type Compare x y = CmpNat x y

instance OrdK Symbol where
  type Compare x y = CmpSymbol x y

instance OrdK [a] -- No implementation needed!

type family GenComp k (x :: k) (y :: k) :: Ordering where
  GenComp (M1 i c f p) ('M1 x) ('M1 y) = GenComp (f p) x y
  GenComp (K1 i c p) ('K1 x) ('K1 y) = Compare x y
  GenComp ((x :+: y) p) ('L1 m) ('L1 n) = GenComp (x p) m n
  GenComp ((x :+: y) p) ('R1 m) ('R1 n) = GenComp (y p) m n
  GenComp ((x :+: y) p) ('L1 _) ('R1 _) = 'LT
  GenComp ((x :+: y) p) ('R1 _) ('L1 _) = 'GT
  GenComp ((x :*: y) p) (x1 ':*: y1) (x2 ':*: y2) =
    PComp (GenComp (x p) x1 x2) (y p) y1 y2
  GenComp (U1 p) _ _ = 'EQ
  GenComp (V1 p) _ _ = 'EQ

type family PComp (c :: Ordering) k (x :: k) (y :: k) :: Ordering where
  PComp 'EQ k x y = GenComp k x y
  PComp x _ _ _ = x