The pattern with functions like `bool`, `either`, etc

Viewed 437

I recently learned about GADTs and their notation:

E.g.

data Maybe a where
  Nothing :: Maybe a
  Just    :: a -> Maybe a

data Either a b where
  Left  :: a -> Either a b
  Right :: b -> Either a b

data Bool where
  False :: Bool
  True  :: Bool

Now I noticed a similiarity to functions like bool, and either, which is basically just like the GADT definition:

  1. taking every line as an argument
  2. replacing the actual type with the next letter of the alphabet
  3. and finally returning a function Type -> (the letter of step 2)

E.g.

maybe  :: b -> (a -> b) -> Maybe a -> b
either :: (a -> c) -> (b -> c) -> Either a b -> c
bool   :: a -> a -> Bool -> a

This also includes foldr, but I noticed that e.g. Tuple doesn't have such a function, though you could easily define it:

tuple :: (a -> b -> c) -> (a,b) -> c
tuple f (x,y) = f x y

What is this pattern? It seems to me these functions alleviate the need for pattern matching (because they give a general way for each case) and thus every function operating on the type can be defined in terms of this function.

1 Answers
Related