Filtering of unique items from heterogeneous lists in haskell on the type level

heterogeneous-unique-lists.hs

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

import           Data.Kind    (Type)
import           GHC.TypeLits (ErrorMessage (Text), TypeError)

data HList :: [Type] -> Type where
  HNil :: HList '[]
  (:#) :: x -> HList xs -> HList (x ': xs)
infixr 5 :#

data A = A Int deriving Show
data B = B Int deriving Show
data C = C Int deriving Show

abc = A 1 :# B 2 :# C 3 :# HNil


instance Show (HList '[]) where
  show HNil = "HNil"

instance (Show x, Show (HList xs))
  => Show (HList (x ': xs)) where
  show (x :# xs) = show x ++ " :# " ++ show xs


type family Reverse' (inputList :: [Type])
                     (accumulator :: [Type])
                     :: [Type]
                     where
  Reverse' '[] accumulator = accumulator
  Reverse' (i ': is) accumulator = Reverse' is (i ': accumulator)

type Reverse a = Reverse' a '[]


class ReversedHList (inputList :: [Type])
                    (accumulator :: [Type])
                    (reversedList :: [Type])
                    where
  rev' :: HList inputList
       -> HList accumulator
       -> HList reversedList

instance ReversedHList '[] a a where
  rev' _ a = a

instance ReversedHList is (i ': as) rs
    => ReversedHList (i ': is) as rs where
    rev' (i :# is) as = rev' is (i :# as)

rev :: forall inputList.
       ReversedHList inputList '[] (Reverse inputList)
    => HList inputList
    -> HList (Reverse inputList)
rev i = rev' @inputList @'[] @(Reverse inputList) i HNil


type family Contains (inputList :: [Type]) (inputType :: Type) :: Bool where
  -- head of the list equals the input type
  Contains (x ': _) x = 'True
  -- recursion terminator: list didn't contain it
  Contains '[] _ = 'False
  -- current head does not equal the input type, so recurse to the next one
  Contains (_ ': xs) x = Contains xs x


type family If (condition :: Bool) (thenCase :: k) (elseCase :: k) :: k where
  If 'True  a _ = a
  If 'False _ b = b


type family Uniques (xs :: [Type]) :: [Type] where
  Uniques (x ': xs) = If (Contains xs x) (Uniques xs) (x ': Uniques xs)
  Uniques '[] = '[]


type family ContainsHead (listToCheckAgainst :: [Type])
                         (listToCheck :: [Type])
                         :: Bool
                         where
  ContainsHead as (b ': bs) = Contains as b
  ContainsHead _ '[] =
      TypeError ('Text "ContainsHead can't take off the head of an empty list")


class UniqueHList (inList :: [Type])
                  (accumulator :: [Type])
                  (uniqueList :: [Type])
                  (nextElementIsContainedAlready :: Bool)
                  where
  ulr' :: HList inList
       -> HList accumulator
       -> HList uniqueList

instance UniqueHList '[] uniqueList uniqueList dontCare where
  ulr' _ x = x

instance UniqueHList is (i ': as) us (ContainsHead (i ': as) is)
    => UniqueHList (i ': is) as us 'False where
    ulr' (i :# is) as =
        ulr' @is @(i ': as) @us @(ContainsHead (i ': as) is) is (i :# as)

instance UniqueHList is as us (ContainsHead as is)
    => UniqueHList (i ': is) as us 'True where
    ulr' (_ :# is) as =
        ulr' @is @as @us @(ContainsHead as is) is as

ulr :: forall inputList.
       UniqueHList inputList '[] (Uniques (Reverse inputList)) 'False
   => HList inputList
   -> HList (Uniques (Reverse inputList))
ulr x = ulr' @inputList @'[] @(Uniques (Reverse inputList)) @'False x HNil

ul :: forall inputList.
    ( ReversedHList (Uniques (Reverse inputList))
                    '[]
                    (Reverse (Uniques (Reverse inputList)))
    , UniqueHList inputList '[] (Uniques (Reverse inputList)) 'False
    )
    => HList inputList
    -> HList (Reverse (Uniques (Reverse inputList)))
ul = rev . ulr

ababca = A 1 :# B 2 :# A 3 :# B 4 :# C 5 :# A 6 :# HNil

-- $> ababca

-- $> ul ababca

{- Run this file through `ghcid -a heterogeneous-unique-lists.hs` to see
   the `-- $> ...` lines printed on the terminal. This is nice for playing
   around with the results of the intermediate functions. 

   This code was tested with GHC 8.10.7
-}