Как мне упростить эту функцию уровня типа, которая сравнивает символы?

У меня есть код, где мне нужна функция уровня типа, которая берет два списка пар ключ-значение, которые отсортированы по ключам и имеет каждый ключ только один раз, а затем объединяет их в один такой список (предпочитая первый список, если ключи существуют в оба списка).

После долгих проб и ошибок мне наконец-то удалось заставить работать следующее:

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

и когда спрашиваете о типе test в GHCi вы получите ожидаемое:

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

При этом используются два семейства типов, так что второе может на самом деле соответствовать шаблонам при упорядочении ключей, но это выглядит намного сложнее, чем должно быть. Есть ли способ создать аналогичную ситуацию с одной семьей?

2 ответа

Решение

Я думаю, это может быть не то, что вы хотите, но вы можете продвинуть функцию для семейства закрытого типа, используя 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 [email protected]((Pair ka va):ass) [email protected]((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

Конечно, это как семья одного типа 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
Другие вопросы по тегам