4 ms·

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 'jus

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?

pwm 5y ago
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).
- earleybird 5y ago
  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))
  - pwm 5y ago
    > 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
- dllthomas 5y ago
  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.
Twisol 5y ago
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.

pwm 5y ago

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

earleybird 5y ago
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))
- pwm 5y ago
  > 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
dllthomas 5y ago
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.

Twisol 5y ago

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.