Hacker News Reader

Comment by earleybird | Hacker News Reader

In these discussions about ADTs, often I see Maybe and Either identified as an ADT rather than an ADT constructor. Am I just missing something other folks 'just know'? If so, what's the intuition I should be looking for?

View on HN

For any type `a`, `Maybe a` is a type. We say "Maybe" in the same sense we say "List" -- it's obviously a list of some type `a`, but if what we're saying doesn't depend on any particular choice of `a`, then by abuse of language, we don't bother saying it.

On the other hand, `Just` and `Nothing` are constructors, or variants, for values of type `Maybe a`. You can think of them as almost like static factories (as in `Optional.empty()` and `Optional.of(val)` in Java), except that algebraic constructors are invertible: you can match on a value to determine whether it was constructed with `Just` or `Nothing`, and what the arguments to the constructor were.

It's just semantics.

    data Bool = False | True
    data Maybe a = Nothing | Just a

Bool is a nullary type constructor or simply type. False and True are nullary data constructors or simply constants. Maybe is an unary type constructor taking one parameter to construct a fully saturated type (eg. Maybe Int), but calling it a "Maybe type" is ok, no crazy ambiguity. Nothing is a constant and Just is an unary data constructor taking one parameter to construct fully saturated data (eg. Just 1).

And in the context of Haskell, non-nullary type constructors are still types. They don't happen to be the types of any values, but they can still parameterize types, be constrained by type equality (eg. a ~ Maybe), etc.

So in essence I could think of types as functions (possibly nullary) from types to types?

Bool = sum(False, True)

Maybe = λ a . sum(Nothing, Just(a))

> So in essence I could think of types as functions (possibly nullary) from types to types?

Type constructors, yes. In Haskell the type of type constructors are called kinds:

    λ> :kind Bool
    Bool :: Type
    λ> :kind Maybe
    Maybe :: Type -> Type
    λ> :kind Maybe Int
    Maybe Int :: Type
    λ> :kind Either
    Either :: Type -> Type -> Type
    λ> :kind Eq
    Eq :: Type -> Constraint
    λ> :kind Functor
    Functor :: (Type -> Type) -> Constraint

Reply on news.ycombinator.com