Is there a way to concatenate type-level literals from two type-level lists?

[coderfromhere]

subj, I'm looking for a way to compose variants from two different definitions. Is there something similar to https://stackoverflow.com/questions/59495874/creating-a-completely-dependent-concatenation ?

[cdepillabout]

I don't think there is a type-level concat function for two type-level lists in world-peace.

What are you trying to do with it? What sort of function are you trying to write with it?

[coderfromhere]

I'm using it as part of servamt-checked-exceptions and I'm looking for way to define and extend a common authentication alias like type AuthenticatedEnv extended = Envelope ('[TokenErr, FormatErr, DecryptErr] ??? extended) where ??? would allow me to compose extended error types with authentication-specific ones.

[cdepillabout]

Ah, I see. You want something like a union or monoid append operator for type-level sets?

So '[TokenErr, FormatErr, DecryptErr] '<> '[TokenErr, RequestErr] would be '[TokenErr, FormatErr, DecryptErr, RequestErr]?

[coderfromhere]

yes, precisely

[cdepillabout]

It is relatively straight-forward to write a Union type-family: https://hackage.haskell.org/package/type-list-0.5.0.0/docs/Data-Type-List.html#t:Union.

I'm guessing that at the value level you want to write something like:

let foo = undefined :: OpenUnion '[Int, Char]
    bar = undefined :: OpenUnion '[Char, Double]
in foo `union` bar :: OpenUnion '[Int, Char, Double]

The problem with this is that in addition to a Union type-family, you'll also need a type-class implementing this union or monoid append operation. You'll have to figure out what sort of semantics it should have. For instance, in the above example, when the sum-type foo is a Char, and bar is a Char, what should be the value of foo `union` bar? Should the Char value in bar be thrown away? Or foo? Or combine them somehow?

You might want to look at the following part of the world-peace codebase for some ideas about how to write this function:

world-peace/src/Data/WorldPeace/Union.hs

Lines 417 to 610 in ceb2549

	-- | This type family removes a type from a type-level list.
	--
	-- This is used to compute the type of the returned 'Union' in 'unionRemove'.
	--
	-- ==== __Examples__
	--
	-- >>> Refl :: Remove Double '[Double, String] :~: '[String]
	-- Refl
	--
	-- If the list contains multiple of the type, then they are all removed.
	--
	-- >>> Refl :: Remove Double '[Char, Double, String, Double] :~: '[Char, String]
	-- Refl
	--
	-- If the list is empty, then nothing is removed.
	--
	-- >>> Refl :: Remove Double '[] :~: '[]
	-- Refl
	type family Remove (a :: k) (as :: [k]) :: [k] where
	Remove a '[] = '[]
	Remove a (a ': xs) = Remove a xs
	Remove a (b ': xs) = b ': Remove a xs
	-- | This is used internally to figure out which instance to pick for the
	-- 'ElemRemove\'' type class.
	--
	-- This is needed to work around overlapping instances.
	--
	-- >>> Refl :: RemoveCase Double '[Double, String] :~: 'CaseFirstSame
	-- Refl
	--
	-- >>> Refl :: RemoveCase Double '[Char, Double, Double] :~: 'CaseFirstDiff
	-- Refl
	--
	-- >>> Refl :: RemoveCase Double '[] :~: 'CaseEmpty
	-- Refl
	type family RemoveCase (a :: k) (as :: [k]) :: Cases where
	RemoveCase a '[] = 'CaseEmpty
	RemoveCase a (a ': xs) = 'CaseFirstSame
	RemoveCase a (b ': xs) = 'CaseFirstDiff
	-- | This type alias is a 'Constraint' that is used when working with
	-- functions like 'unionRemove' or 'unionHandle'.
	--
	-- 'ElemRemove' gives you a way to specific types from a 'Union'.
	--
	-- Note that @'ElemRemove' a as@ doesn't force @a@ to be in @as@. We are able
	-- to use 'unionRemove' to try to pull out a 'String' from a
	-- @'Union' 'Identity' \'['Double']@ (even though there is no way this 'Union'
	-- could contain a 'String'):
	--
	-- >>> let u = This (Identity 3.5) :: Union Identity '[Double]
	-- >>> unionRemove u :: Either (Union Identity '[Double]) (Identity String)
	-- Left (Identity 3.5)
	--
	-- When writing your own functions using 'unionRemove', in order to make sure
	-- the @a@ is in @as@, you should combine 'ElemRemove' with 'IsMember'.
	--
	-- 'ElemRemove' uses some tricks to work correctly, so the underlying 'ElemRemove\''typeclass
	-- is not exported.
	type ElemRemove a as = ElemRemove' a as (RemoveCase a as)
	-- | This function allows you to try to remove individual types from a 'Union'.
	--
	-- This can be used to handle only certain types in a 'Union', instead of
	-- having to handle all of them at the same time.
	--
	-- ==== __Examples__
	--
	-- Handling a type in a 'Union':
	--
	-- >>> let u = This (Identity "hello") :: Union Identity '[String, Double]
	-- >>> unionRemove u :: Either (Union Identity '[Double]) (Identity String)
	-- Right (Identity "hello")
	--
	-- Failing to handle a type in a 'Union':
	--
	-- >>> let u = That (This (Identity 3.5)) :: Union Identity '[String, Double]
	-- >>> unionRemove u :: Either (Union Identity '[Double]) (Identity String)
	-- Left (Identity 3.5)
	--
	-- Note that if you have a 'Union' with multiple of the same type, they will
	-- all be handled at the same time:
	--
	-- >>> let u = That (This (Identity 3.5)) :: Union Identity '[String, Double, Char, Double]
	-- >>> unionRemove u :: Either (Union Identity '[String, Char]) (Identity Double)
	-- Right (Identity 3.5)
	unionRemove
	:: forall a as f
	. ElemRemove a as
	=> Union f as
	-> Either (Union f (Remove a as)) (f a)
	unionRemove = unionRemove' (Proxy @(RemoveCase a as))
	{-# INLINE unionRemove #-}
	-- | This is used as a promoted data type to give a tag to the three different
	-- instances of 'ElemRemove\''. These also correspond to the three different
	-- cases of 'Remove' and 'RemoveCase'.
	data Cases = CaseEmpty | CaseFirstSame | CaseFirstDiff
	-- | This is an internal typeclass used for removing elements from a 'Union'.
	--
	-- The most surprising thing about this is the last argument, @caseMatch@.
	-- This is used to stop GHC from seeing overlapping instances:
	--
	-- https://kseo.github.io/posts/2017-02-05-avoid-overlapping-instances-with-closed-type-families.html
	--
	-- Each of the instances of this correspond to one case in 'Remove' and
	-- 'RemoveCase'.
	class ElemRemove' (a :: k) (as :: [k]) (caseMatch :: Cases) where
	unionRemove' :: Proxy caseMatch -> Union f as -> Either (Union f (Remove a as)) (f a)
	instance ElemRemove' a '[] 'CaseEmpty where
	unionRemove'
	:: Proxy 'CaseEmpty -> Union f '[] -> Either (Union f '[]) (f a)
	unionRemove' _ u = absurdUnion u
	{-# INLINE unionRemove' #-}
	instance
	( ElemRemove' a xs (RemoveCase a xs)
	) =>
	ElemRemove' a (a ': xs) 'CaseFirstSame where
	unionRemove'
	:: forall f
	. Proxy 'CaseFirstSame
	-> Union f (a ': xs)
	-> Either (Union f (Remove a xs)) (f a)
	unionRemove' _ (This a) = Right a
	unionRemove' _ (That u) = unionRemove' (Proxy @(RemoveCase a xs)) u
	instance
	( ElemRemove' a xs (RemoveCase a xs)
	, -- We need to specify this equality because GHC doesn't realize it will
	-- always work out this way. We know that for this case, @a@ and @b@
	-- will always be different (because of how the 'RemoveCase' type family
	-- works and the fact that there is already another instance that handles
	-- the case when @a@ and @b@ are the same type).
	--
	-- However, GHC doesn't realize this, so we have to specify it.
	Remove a (b ': xs) ~ (b ': Remove a xs)
	) =>
	ElemRemove' a (b ': xs) 'CaseFirstDiff where
	unionRemove'
	:: forall f
	. Proxy 'CaseFirstDiff
	-> Union f (b ': xs)
	-> Either (Union f (b ': Remove a xs)) (f a)
	unionRemove' _ (This b) = Left (This b)
	unionRemove' _ (That u) =
	case unionRemove' (Proxy @(RemoveCase a xs)) u of
	Right fa -> Right fa
	Left u2 -> Left (That u2)
	-- | Handle a single case on a 'Union'. This is similar to 'union' but lets
	-- you handle any case within the 'Union'.
	--
	-- ==== __Examples__
	--
	-- Handling the first item in a 'Union'.
	--
	-- >>> let u = This 3.5 :: Union Identity '[Double, Int]
	-- >>> let printDouble = print :: Identity Double -> IO ()
	-- >>> let printUnion = print :: Union Identity '[Int] -> IO ()
	-- >>> unionHandle printUnion printDouble u
	-- Identity 3.5
	--
	-- Handling a middle item in a 'Union'.
	--
	-- >>> let u2 = That (This 3.5) :: Union Identity '[Char, Double, Int]
	-- >>> let printUnion = print :: Union Identity '[Char, Int] -> IO ()
	-- >>> unionHandle printUnion printDouble u2
	-- Identity 3.5
	--
	-- If you have duplicates in your 'Union', they will both get handled with
	-- a single call to 'unionHandle'.
	--
	-- >>> let u3 = That (This 3.5) :: Union Identity '[Double, Double, Int]
	-- >>> let printUnion = print :: Union Identity '[Int] -> IO ()
	-- >>> unionHandle printUnion printDouble u3
	-- Identity 3.5
	--
	-- Use 'absurdUnion' to handle an empty 'Union'.
	--
	-- >>> let u4 = This 3.5 :: Union Identity '[Double]
	-- >>> unionHandle (absurdUnion :: Union Identity '[] -> IO ()) printDouble u4
	-- Identity 3.5
	unionHandle
	:: ElemRemove a as
	=> (Union f (Remove a as) -> b)
	-> (f a -> b)
	-> Union f as
	-> b
	unionHandle unionHandler aHandler u =
	either unionHandler aHandler $ unionRemove u