Reputation: 584
I have some code where I need a type-level function that takes two lists of key-value pairs that are sorted on the keys and has each key only once and then merges them into one such list (preferring the first list if keys exist in both lists).
After a lot of trial-and-error I finally managed to get the following working:
{-# 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 asking for the type of test
in GHCi you get the expected:
*Main> :t test
test
:: Proxy
'['Pair "A" Int, 'Pair "Hello" (Maybe Char), 'Pair "F" (),
'Pair "Z" Bool]
This uses two type families so that the second one can actually pattern-match on the ordering of the keys, but that seems a lot more complicated than it ought to be. Is there a way to get a similar situation going with just a single type family?
Upvotes: 3
Views: 166
Reputation: 6703
I guess this may not be what you want, but you can promote a function to a closed type family using Data.Promotion.TH
in singletons package. It's very handy to write this kind of type 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
Upvotes: 2
Reputation: 89063
Sure, here it is as a single type family Merge'
and a type synonym 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
Upvotes: 2