3 ms·
`Maybe a` is a type: For a start it's a discriminated union (a sum type), its set of values is: a + 1 `a` is the values in the `Just` case, and 1 is the
by louthy 5y ago
`Maybe a` is a type:
For a start it's a discriminated union (a sum type), its set of values is:
a + 1
`a` is the values in the `Just` case, and 1 is the `Nothing` case. It's obvious why they're called sum-types when you view it like this.
`Maybe a` is a type-lambda abstraction (still a type)
`Maybe Int` is a type-application, passing Int to the `Maybe a` type-lambda as an argument, to get a `Maybe Int` in return (still a type).
- lkitching 5y ago> `Maybe a` is a type-lambda abstraction (still a type) I don't know what you mean by this - lambdas are values not types. You could argue the type of the Maybe type constructor is Type -> Type but there is no Type type in Haskell so Maybe is not a 'type' in the Haskell type system in the way e.g. String is. The separation of types and values is AFAIK the defining characteristic of non-dependent type systems, which Haskell is (for now).
- philh 5y ago> I don't know what you mean by this - lambdas are values not types. I think they meant "`Maybe` is a type-lambda abstraction", meaning roughly "a type-level function", which seems true to me. I don't think they meant to say that `Maybe` is a type in the same way String is. (I'd agree it's not, though I'd still call it a type.) > there is no Type type in Haskell Incidentally there is[1], and it even has kind `Type` just like `String` does. So you can ask "what is the kind of `Maybe Type`" (it's `Type`) where you can't ask "what is the kind of `Maybe Maybe`" (`Maybe` has kind `Type -> Type` so this is a kind error). [1]: https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-Kind.html https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-...