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?
You've tried to build an existential type
meaning “whoever uses a value
v
of typeOneOfTwo a
can be sure that there is some concrete type constructorh
, which is an instance ofThings
, such thatv
has typeh a
”. But that's not what the type you wrote means; that is a universal typemeaning that for all type constructors
h
that the user ofv
might think of,v
has typeh a
. I.e. the single valuev
has in general multiple different types!That means you can actually write
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 differenth
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:
which makes it conceptually possible to have something like (this code doesn't work)
To actually get that functionality, you need to put the case distinction into the class instances, like