data Union (r :: [ * -> * ]) v where
UNow :: t v -> Union (t ': r) v
UNext :: Union r v -> Union (any ': r) v
Especially for the value constructor UNext , it seems to add something like ‘t’ to the list r ,but there is no such parameter as ‘t v’ in UNow .
So, the expected list seems like : UNext ( t1 v1, UNext ( t2 v2, UNow(t3 v3) ) ) ,
while the list in the code seems like : UNext ( UNext ( UNow( t1 v1) ) ) .
The types of the constructors are exactly those listed in the program:
UNow :: t v -> Union (t ': r) v
UNext :: Union r v -> Union (any ': r) v
Maybe you’re confusing GADT syntax with record syntax? Record syntax does give the actual selectors different types than those that are written in the program (it adds the record itself as argument).
A concrete example would probably be useful… Here’s one:
myMaybe :: Union (Maybe ': IO ': '[]) Int
myMaybe = UNow (Just 5)
myIO :: Union (Maybe ': IO ': '[]) Int
myIO = UNext (UNow (do putStrLn "Hello, World!"; return 5))
In this way the type Union [Maybe, IO] Int is a union of Maybe Int and IO Int. It could be either of the two, and the UNext and UNow constructors indicate which one you are using.
We could look in more detail at how the constructors are used in this example. In myMaybe we use only UNow which is instantiated as follows (I’ve aligned the general type below it):
UNow :: Maybe Int -> Union (Maybe ': (IO ': [])) Int
UNow :: t v -> Union (t ': r ) v
So we’re using UNow to create a union where Maybe is the leftmost member of the union and we basically ignore the IO that comes after it.
In myIO we use UNow and UNext instantiated like this:
UNow :: IO Int -> Union (IO ': []) Int
UNow :: t v -> Union (t ': r ) v
UNext :: Union (IO ': []) Int -> Union (Maybe ': (IO ': [])) Int
UNext :: Union r v -> Union (any ': r ) v
So here we’re first using UNow to build a union with only IO in it, and then using UNext to say that Maybe is also in the union but we do nothing with that Maybe.
As @int-index said, this is very similar to Either where you could write myMaybe and myIO like this:
myMaybe' :: Either (Maybe Int) (IO Int)
myMaybe' = Left (Just 5)
myIO' :: Either (Maybe Int) (IO Int)
myIO' = Right (do putStrLn "Hello, World!"; return 5)
But that only works for unions of exactly two types, while the Union type you showed works for any number of types.