Skip to content

Instantly share code, notes, and snippets.

@tfc
Created March 20, 2022 10:14
Show Gist options
  • Save tfc/a525ef630abe215d1ec1d3c50609a340 to your computer and use it in GitHub Desktop.
Save tfc/a525ef630abe215d1ec1d3c50609a340 to your computer and use it in GitHub Desktop.
Filtering of unique items from heterogeneous lists in haskell on the type level
{-# 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
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment