Case Intersection

case_intersection.hs

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

main :: IO ()
main = putStrLn "hello"

data Attr = A | B | C | D | E
data MyData (c :: [Attr]) = MyData { getMyData :: Int }

data NothingX = NothingX
data JustX a = JustX a

reAttr :: MyData xs -> MyData ys
reAttr (MyData a) = MyData a

caseMaybe :: Maybe a -> (NothingX -> b, JustX a -> b) -> b
caseMaybe m (caseNothing, caseJust) = case m of
  Just a  -> caseJust (JustX a)
  Nothing -> caseNothing NothingX

caseMaybeIntersection :: Maybe a -> (NothingX -> MyData xs, JustX a -> MyData ys) -> MyData (Intersection xs ys)
caseMaybeIntersection m (caseNothing, caseJust) = case m of
  Just a  -> reAttr $ caseJust (JustX a)
  Nothing -> reAttr $ caseNothing NothingX

type family Intersection (xs :: [k]) (ys :: [k]) :: [k] where
  Intersection '[] ys = '[]
  Intersection (x ': xs) ys = IntersectionHelp (Elem x ys) x xs ys

type family IntersectionHelp (b :: Bool) (x :: k) (xs :: [k]) (ys :: [k]) :: [k] where
  IntersectionHelp 'True x xs ys = x ': Intersection xs ys
  IntersectionHelp 'False x xs ys = Intersection xs ys

type family Elem (x :: k) (xs :: [k]) :: Bool where
  Elem x '[] = 'False
  Elem x (x ': xs) = 'True
  Elem x (y ': xs) = Elem x xs

------------------------------------------
-- Examples
------------------------------------------

numA :: Int
numA = caseMaybe Nothing
  ( \NothingX -> 6
  , \(JustX n) -> n + 2
  )

attrA :: MyData '[ 'A, 'C, 'D]
attrA = MyData 55

attrB :: MyData '[ 'B, 'A, 'D]
attrB = MyData 23

-- type sig for attrC can be omitted because it's inferrable
attrC :: MyData '[ 'A, 'D]
attrC = caseMaybeIntersection (Just "ignored")
  (\NothingX -> attrA, \(JustX _) -> attrB)