-- Descend to classify the specimens
class Functor f where
fmap :: (a -> b) -> f a -> f b
The most elementary of the type-monsters. A gentle giant drifting through the shallows, it lifts ordinary functions into structured worlds. Its tendrils of fmap reach into any container, transforming contents without disturbing the vessel.
class Functor f => Applicative f where
pure :: a -> f a
(<*>) :: f (a -> b) -> f a -> f b
A more evolved form of the Functor, the Applicative can carry functions within its body. Its radial symmetry of <*> operators allows it to combine multiple effectful computations in parallel, weaving them together like a bioluminescent coral colony.
class (Functor t, Foldable t) => Traversable t where
traverse :: Applicative f => (a -> f b) -> t a -> f (t b)
This migratory species moves through structures element by element, carrying effects in its wake. Unlike its cousin fmap, the Traversable can reshape its container through the journey itself, turning structures inside-out as it swims.
class Applicative m => Monad m where
(>>=) :: m a -> (a -> m b) -> m b
return :: a -> m a
The serpentine Bindworm chains computations through the murky depths. Each segment of its body is a >>= operator, passing the result of one computation into the jaws of the next. Its twin eyes are return — the only way in or out of its monadic coils.
newtype State s a = State { runState :: s -> (a, s) }
A creature that carries its environment coiled within itself. The Stateful Lurker remembers everything, its internal state threading silently through each computation. To observe it is to change it: get and put are the only handles into its sealed world.
newtype Reader r a = Reader { runReader :: r -> a }
This passive observer absorbs its environment without ever altering it. The Reader floats motionless, letting configuration data flow through its translucent body. It asks the world a question and computes its answer from the response, pure and unperturbed.
data Expr a where
Lit :: Int -> Expr Int
Add :: Expr Int -> Expr Int -> Expr Int
If :: Expr Bool -> Expr a -> Expr a -> Expr a
A polymorphic predator that reshapes its own type at each branch. GADTs encode invariants in their very spine, each constructor a different species masquerading under one name. To pattern-match is to unlock forbidden knowledge about the type variable.
type family Eval (a :: *) :: * where
Eval Int = Int
Eval [a] = [Eval a]
Eval (a -> b) = Eval a -> Eval b
Computation at the type level: this creature exists before runtime, resolving its form during compilation. The TypeFamily rewrites the fabric of the type system itself, its branching patterns mirroring a recursive descent through the kind hierarchy.
data Showable = forall a. Show a => MkShowable a
The most elusive specimen: it hides its true type behind an existential quantifier. You know it exists, you can observe its behavior through a typeclass interface, but its concrete form remains forever sealed inside its opaque shell. Information enters but never escapes.
class Category cat where
id :: cat a a
(.) :: cat b c -> cat a b -> cat a c
At the bottom of the trench, where abstraction meets its limit, swims the Category itself. Not a container, not a computation — a structure of pure composition. Its body is the morphism, its skeleton the identity law, its movement the associative chain of arrows flowing through the darkness.
newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b }
The deepest creature in the trench: an entity that encodes the entirety of a functor's behavior in a single universal property. The Yoneda Lemma given flesh. To know all its morphisms is to know the creature itself. It grants fmap for free, dissolving the boundary between structure and transformation.
The type system is not a cage. It is a language for describing the shapes of thought. Each constraint is a gift; each type, a proof that the impossible has been excluded. In the abyss, where the monsters grow complex beyond comprehension, we find not chaos but a deeper order — a grammar of computation that speaks in the voice of pure mathematics.