如何简化这个比较符号的类型级函数

Question

我有一些代码，我需要一种类型级函数，该函数采用两个键值对列表，这些键值对在键上排序，每个键只有一次，然后将它们合并到一个这样的列表中(如果键存在于两个列表中，则首选第一个列表(。

经过大量的反复试验，我终于设法使以下工作：

{-# 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

当询问GHCi中的test类型时，您会得到预期的结果：

*Main> :t test
test
  :: Proxy
       '['Pair "A" Int, 'Pair "Hello" (Maybe Char), 'Pair "F" (),
         'Pair "Z" Bool]

这使用两个类型系列，以便第二个类型系列实际上可以在键的排序上进行模式匹配，但这似乎比它应该的要复杂得多。有没有办法让单一类型的家庭出现类似的情况？

Answer 1

我想这可能不是你想要的，但是您可以使用单例包中的Data.Promotion.TH将函数提升为封闭类型系列。编写这种类型函数非常方便。

{-# 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

Answer 2

当然，这里是作为单类型族Merge'和类型同义词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