Polymorphic Types: representing multiple types using the same type synonym-CodePudding

My objective is giving two data types the same synonym. I've minimized my question to the following question:

{-# LANGUAGE KindSignatures, Rank2Types #-}

class Things (h :: * -> *) where

newtype Thing1 a = Thing1 a
newtype Thing2 a = Thing2 a

instance Things Thing1 where
instance Things Thing2 where

type OneOfTwo a = forall h. Things h => h a

foo :: OneOfTwo String -> String
foo (Thing1 name) = name
foo (Thing2 name) = name

My goal is to be able to make the type synonym oneOfTwo stand for either Thing1 and Thing2 (or even more if I want to). But when I do so, any pattern matching aside from the first one in foo will be seen as redundant:

    Pattern match is redundant
   |
15 | foo (Thing2 name) = name
   |

I'm aware that I can re-write it as the following:

newtype Thing1 a = Thing1 a
newtype Thing2 a = Thing2 a

data OneOfTwo a = One (Thing1 a)
                | Two (Thing2 a)

foo :: OneOfTwo String -> String
foo (One (Thing1 name)) = name
foo (Two (Thing2 name)) = name

But I want to avoid creating a new data type OneOfTwo.

Is there a workaround to make this happen without creating a new boxing data type?

CodePudding user response：

You've tried to build an existential type

type OneOfTwoE a = ∃ h. Things h => h a

meaning “whoever uses a value v of type OneOfTwo a can be sure that there is some concrete type constructor h, which is an instance of Things, such that v has type h a”. But that's not what the type you wrote means; that is a universal type

type OneOfTwoA a = ∀ h. Things h => h a

meaning that for all type constructors h that the user of v might think of, v has type h a. I.e. the single value v has in general multiple different types!

That means you can actually write

fooA :: OneOfTwoA String -> String
fooA v = (case v of {Thing1 name -> name})
          (case v of {Thing2 name -> name})

and both of the case matches will succeed, despite matching on different constructors! This works because in each of the case expressions, v is specialised to a different h instantiation, which is ok because the type is universal.

Haskell doesn't really have existential types. It does, as you've noted, have discriminated sum types. It also can simulated existential types with universally quantified data constructors, preferrably expressed with GADT syntax:

data OneOfTwoG a where
  OneOfTwo :: ∀ h a . Things h => h a -> OneOfTwoG a

which makes it conceptually possible to have something like (this code doesn't work)

fooG :: OneOfTwoG String -> String
fooG (OneOfTwo (Thing1 name)) = name
fooG (OneOfTwo (Thing2 name)) = name

To actually get that functionality, you need to put the case distinction into the class instances, like

class Things (h :: * -> *) where
  gname :: h a -> a

newtype Thing1 a = Thing1 a
newtype Thing2 a = Thing2 a

instance Things Thing1 where gname (Thing1 n) = n
instance Things Thing2 where gname (Thing2 n) = n
fooG :: OneOfTwoG String -> String
fooG (OneOfTwo ϑ) = gname ϑ

CodePudding user response：

At the risk of pointing out the obvious, the whole purpose of type classes is to allow you to define polymorphic functions that can be applied to multiple types, so what you're supposed to do in this situation is write:

class Things h where
  foo :: h String -> String

newtype Thing1 a = Thing1 a
newtype Thing2 a = Thing2 a

instance Things Thing1 where
  foo (Thing1 name) = name
instance Things Thing2 where
  foo (Thing2 name) = name

That is, when you want to represent multiple types with a single name, the tool you want to use is a type class, not a type synonym.