Confused about this GADT

Learn
#1

Hi,everyone.
I’m a bit confused about this GADT:

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) ) ) .

How should I understand this GADT?

1 Like
#2

This GADT can be understood as nested Eithers.

  • Union [t1, t2, t3] v is equivalent to Either (t1 v) (Either (t2 v) (t3 v)).
  • The constructors UNow and UNext correspond to Left and Right.
4 Likes
#3

Thank you, i got it .
Sorry about my weak foundational knowledge . :sweat_smile:

#4

Forgive me coming back for more details.
It seems like that the **actual** constructors are:

UNow  :: t v -> Union r v -> Union (t ': r) v
UNext :: Union r v -> any v -> Union (any ': r) v

That is (assuming 'global this object' is something similar to the 'this' in c++):

  • UNow takes t v and global this object ,then return new global this object.
  • UNext takes global this object and another any v , then return new global this object.

Where can I learn about this topic, or some terminology？

#5

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).

2 Likes
#6

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.

4 Likes
#7

Thank you for providing so many details . It seems that i didn’t clear about the usage of union. Thanks a lot. :+1: :+1: :+1:

1 Like