5 ms·

Maybe and Monad are not types - Maybe is a type constructor and Monad is a type class.

philh 5y ago
As I said, I think that's a reasonable but nonstandard way to define the word "type" but it doesn't make much difference - type theory concerns itself with them, whatever they're called. But to support my "nonstandard" claim: * https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/type-type https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compil... mentions "Types (possibly of higher kind); e.g. [Int], Maybe" * https://limperg.de/ghc-extensions/#polykinds https://limperg.de/ghc-extensions/#polykinds talks about "types of different kinds", using Int and Monad as examples. * https://en.wikipedia.org/wiki/Kind_%28type_theory%29 https://en.wikipedia.org/wiki/Kind_%28type_theory%29 says "the type [] (list) is a type constructor". It uses the terms "data type" and "proper type" for what I think you simply want to call "type". It's also possible usage is just inconsistent on the subject. (Evidence for this: that second link calls constraints "type-like things", when they're just types according to me.) But my sense is that usually, people engaging seriously with type theory or advanced Haskell would call Maybe and Monad types. (You're of course right that Maybe is a type constructor and Monad is a typeclass, but that doesn't mean they aren't also types.)
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-...

As I said, I think that's a reasonable but nonstandard way to define the word "type" but it doesn't make much difference - type theory concerns itself with them, whatever they're called. But to support my "nonstandard" claim: * https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/type-type https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compil... mentions "Types (possibly of higher kind); e.g. [Int], Maybe" * https://limperg.de/ghc-extensions/#polykinds https://limperg.de/ghc-extensions/#polykinds talks about "types of different kinds", using Int and Monad as examples. * https://en.wikipedia.org/wiki/Kind_%28type_theory%29 https://en.wikipedia.org/wiki/Kind_%28type_theory%29 says "the type [] (list) is a type constructor". It uses the terms "data type" and "proper type" for what I think you simply want to call "type". It's also possible usage is just inconsistent on the subject. (Evidence for this: that second link calls constraints "type-like things", when they're just types according to me.) But my sense is that usually, people engaging seriously with type theory or advanced Haskell would call Maybe and Monad types. (You're of course right that Maybe is a type constructor and Monad is a typeclass, but that doesn't mean they aren't also types.)

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