Paul Visschers
Paul Visschers

Reputation: 584

How do I simplify this type-level function that compares symbols?

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

Answers (2)

snak
snak

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

rampion
rampion

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

Related Questions