How can I simplify this level function that compares characters?
I have some code where I need a type level function that takes two lists of key-value pairs that are sorted by keys, and each has only one key, and then concatenates them into one such list (preferring the first list if keys exist in both lists).
After a lot of trial and error, I was finally able to get the following:
{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
import Data.Proxy
import GHC.TypeLits
data KVPair s a = Pair s a
type family Merge (as :: [KVPair Symbol *]) (bs :: [KVPair Symbol *]) :: [KVPair Symbol *] where
Merge '[] bs = bs
Merge as '[] = as
Merge ((Pair k1 a) : as) ((Pair k2 b) : bs) = Merge' (CmpSymbol k1 k2) ((Pair k1 a) : as) ((Pair k2 b) : bs)
type family Merge' (ord :: Ordering) (as :: [k]) (bs :: [k]) :: [k] where
Merge' LT (a : as) (b : bs) = a : Merge as (b : bs)
Merge' EQ (a : as) (b : bs) = a : Merge as bs
Merge' GT (a : as) (b : bs) = b : Merge (a : as) bs
test :: Proxy (Merge [Pair "A" Int, Pair "Hello" (Maybe Char), Pair "Z" Bool] [Pair "Hello" String, Pair "F" ()])
test = Proxy
and when you query the type test
in GHCi, you get the expected:
*Main> :t test
test
:: Proxy
'['Pair "A" Int, 'Pair "Hello" (Maybe Char), 'Pair "F" (),
'Pair "Z" Bool]
In this case, two types of families are used, so the second may actually match the pattern when ordering the keys, but this seems a lot more complicated than it should be. Is there a way to get a similar situation with a single type family?
source to share
I think it might not be what you want, but you can promote the function of the closed family types using Data.Promotion.TH
in singletons . It is very convenient to write these types of functions.
{-# LANGUAGE DataKinds, FlexibleContexts, GADTs, PolyKinds, ScopedTypeVariables,
TemplateHaskell, TypeFamilies, UndecidableInstances #-}
import Data.Proxy
import Data.Promotion.TH
import Data.Singletons.Prelude
promote [d|
data KVPair k v = Pair k v
merge :: Ord k => [KVPair k a] -> [KVPair k a] -> [KVPair k a]
merge [] bs = bs
merge as [] = as
merge as@((Pair ka va):ass) bs@((Pair kb vb):bss) =
case compare ka kb of
LT -> (Pair ka va):merge ass bs
EQ -> (Pair ka va):merge ass bss
GT -> (Pair kb vb):merge as bss
|]
test :: Proxy (Merge [Pair "A" Int, Pair "Hello" (Maybe Char), Pair "Z" Bool] [Pair "Hello" String, Pair "F" ()])
test = Proxy
source to share
Of course, here it is like a family of the same type Merge'
and a synonym for type Merge
:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Merge where
import Data.Proxy
import GHC.TypeLits
type family Merge' (mord :: Maybe Ordering) (as :: [(Symbol,*)]) (bs :: [(Symbol,*)]) :: [(Symbol,*)] where
Merge' 'Nothing '[] bs = bs
Merge' 'Nothing as '[] = as
Merge' 'Nothing (('(k1, a)) : at) (('(k2, b)) : bt) = Merge' ('Just (CmpSymbol k1 k2)) (('(k1, a)) : at) (('(k2, b)) : bt)
Merge' ('Just 'LT) (a : as) (b : bs) = a : Merge' 'Nothing as (b : bs)
Merge' ('Just 'EQ) (a : as) (b : bs) = a : Merge' 'Nothing as bs
Merge' ('Just 'GT) (a : as) (b : bs) = b : Merge' 'Nothing (a : as) bs
type Merge as bs = Merge' 'Nothing as bs
test :: Proxy (Merge ['("A", Int), '("Hello", Maybe Char), '("Z", Bool)] ['("Hello", String), '("F", ())])
test = Proxy
source to share