Define instances on open sum

Learn
1

I have an open sum data type defined as

class Member a (as :: [Type])

instance {-# OVERLAPPING #-} Member a (a ': as)

instance Member a as => Member a (a0 ': as)

data OneOf (as :: [Type]) where
  OneOf :: Member a as => a -> OneOf as

I’d like to define a Show instance on OneOf as if all the as have a Show instance.

I tried like this

type family All (c :: Type -> Constraint) (ts :: [Type]) :: Constraint where
  All c '[] = ()
  All c (t ': ts) = (c t, All c ts)

instance All Show as => Show (OneOf as) where
  show (OneOf x) = show x

but this fails with

Could not deduce (Show a) arising from a use of ‘show’

I guess this is because when searching for the instance, All Show as and Member are not really talking to each other. Is this intuition correct?

Is there a way to make this (or something similar) actually work?

2

Can you add a method to Member?

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind

type family OpTuple r as where
  OpTuple _ '[] = ()
  OpTuple r (a ': as) = (a -> r, OpTuple r as)

class Member a (as :: [Type]) where
  match :: OpTuple r as -> a -> r

instance {-# OVERLAPPING #-} Member a (a ': as) where
  match (f, _) a = f a

instance Member a as => Member a (a0 ': as) where
  match (_, fs) a = match @a @as fs a

data OneOf (as :: [Type]) where
  OneOf :: Member a as => a -> OneOf as


instance ShowOpTuple as => Show (OneOf as) where
  show (OneOf a) = match @_ @as (showOpTuple @as) a

class ShowOpTuple (as :: [Type]) where
  showOpTuple :: OpTuple String as

instance ShowOpTuple '[] where
  showOpTuple = ()

instance (Show a, ShowOpTuple as) => ShowOpTuple (a ': as) where
  showOpTuple = (show, showOpTuple @as)


x :: OneOf [String, Int, Bool, Char, ()]
x = OneOf True

main = print x
3

Thanks! I can modify Member as I see fit, so for his specific case this could work.

I’d like it to be more generic, though, and having something which work with every possible constraint on variants of OneOf

4

Ah, then perhaps you would enjoy this variation.

class All c (as :: [Type]) where
  polyOpTuple :: (forall a. c a => a -> b) -> OpTuple b as

instance All c '[] where
  polyOpTuple _ = ()

instance (c a, All c as) => All c (a ': as) where
  polyOpTuple f = (f, polyOpTuple @c @as f)

polyMatch :: forall c as a b. (All c as, Member a as) => (forall a'. c a' => a' -> b) -> a -> b
polyMatch f = match @_ @as (polyOpTuple @c @as f)

-- This is the only bit that needs repeating for
-- each new operation.
instance All Show as => Show (OneOf as) where
  show (OneOf a) = polyMatch @Show @as show a
5

I think I’d do it like this:

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}

import Data.Kind

data SMember a as where
  Here :: SMember a (a : as)
  There :: SMember a as -> SMember a (b : as)

class Member a as where
  smember :: SMember a as

instance {-# OVERLAPPING #-} Member a (a : as) where
  smember = Here

instance Member a as => Member a (b : as) where
  smember = There smember

data OneOf as where
  OneOf :: Member a as => a -> OneOf as

type All :: (Type -> Constraint) -> [Type] -> Constraint
type family All c as where
  All c '[] = ()
  All c (a : as) = (c a, All c as)

instance forall as. All Show as => Show (OneOf as) where
  show (OneOf x) = go (smember @_ @as) x where
    go :: All Show bs => SMember b bs -> b -> String
    go Here x = show x
    go (There i) x = go i x
2 Likes
6

that is lovely! Thanks!