5 ms·

I think this is too simplistic for real-world programming languages. For example TypeScript has the "any" and the "unknown" types. Both encompass the same set

by goto11 5y ago

I think this is too simplistic for real-world programming languages. For example TypeScript has the "any" and the "unknown" types. Both encompass the same set of values (any possible value which can be represented in the language), but the allowed operations are different. C# has something similar with "object" and "dynamic". For a static type system it makes more sense to think of a type as a set of supported operations rather than a set of values.

philh 5y ago
Or Haskell has types like `Void`, `Maybe`, and `Monad`. If you think of them as "sets of possible values", these all have no possible values. But they're very different types. You could probably define terms such that of these, only `Void` is a "type" - for example, it's the only one that you can use directly as function inputs or outputs. (i.e. you can write a function `Void -> Int` but not a function `Maybe -> Int`.) I think that would be nonstandard, but maybe reasonable to do. But then when you explain what a "type" is you've only explained a subset of what "type theorists" talk about, which includes the others.
- lkitching 5y ago
  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-...
louthy 5y ago
> For a static type system it makes more sense to think of a type as a set of supported operations rather than a set of values. It really doesn't. 'any', 'unknown', 'object', and 'dynamic' are all 'top' in type systems (the type that is the super-type of all other types), they hold the set of all values. The fact a language assigns additional semantics based on their name is just sugar over the underlying type system, the type-system can live quite happily without names. But even then, you could consider the name of a type a 'discriminating tag', like in discriminated unions. So, something like: type Top = Any a | Unknown a | Object a | Dynamic a The same type, but with different states depending on the semantics of the language.
- goto11 5y ago
  I don't know what you mean with "sugar", but the fact that several different types can represent the exact same set of possible values means that a type cannot be considered as just a set of possible values. > The same type, but with different states depending on the semantics of the language. This is just playing games with definitions. What you call "state" is a type in the type system of the programming language.

by goto11 5y ago

philh 5y ago

Or Haskell has types like `Void`, `Maybe`, and `Monad`. If you think of them as "sets of possible values", these all have no possible values. But they're very different types. You could probably define terms such that of these, only `Void` is a "type" - for example, it's the only one that you can use directly as function inputs or outputs. (i.e. you can write a function `Void -> Int` but not a function `Maybe -> Int`.) I think that would be nonstandard, but maybe reasonable to do. But then when you explain what a "type" is you've only explained a subset of what "type theorists" talk about, which includes the others.

lkitching 5y ago
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-...

louthy 5y ago

> For a static type system it makes more sense to think of a type as a set of supported operations rather than a set of values. It really doesn't. 'any', 'unknown', 'object', and 'dynamic' are all 'top' in type systems (the type that is the super-type of all other types), they hold the set of all values. The fact a language assigns additional semantics based on their name is just sugar over the underlying type system, the type-system can live quite happily without names. But even then, you could consider the name of a type a 'discriminating tag', like in discriminated unions. So, something like: type Top = Any a | Unknown a | Object a | Dynamic a The same type, but with different states depending on the semantics of the language.

goto11 5y ago
I don't know what you mean with "sugar", but the fact that several different types can represent the exact same set of possible values means that a type cannot be considered as just a set of possible values. > The same type, but with different states depending on the semantics of the language. This is just playing games with definitions. What you call "state" is a type in the type system of the programming language.