7 ms·

One of most frequent usage of a type system is literal types. Haskell, Rust,... and modern programming languages fail to do it. The only exception is Typescrip

One of most frequent usage of a type system is literal types. Haskell, Rust,... and modern programming languages fail to do it. The only exception is Typescript. For example, simple way to adding a extended boolean type: type MyBoolean = null | true | false. Or type MyRange = 3 | 4 | 5 Curious.

freilanzer 4y ago
Why would I ever want to extend a type with null? That's exactly the opposite of what I want of a type system in the first place.
- evomassiny 4y ago
  the type `null | true | false` is different from `true | false`, a type checker can assert that you handle the `null` case before using a function that wants a boolean. This is how rust handles it (with the Option<T> type).
  - harperlee 4y ago
    In particular, you may want this to signify “I dont know” with NULL, just as in SQL. See the Wikipedia page for ternary logic for more info.
    - alexvoda 4y ago
      Note that 3VL (3 valued logic) is one of the more criticized aspects of SQL. 3VL is a gigantic leap of of complexity over 2VL (boolean). The number of possible operations is a lot higher and the choice of operations is not standardized. To quote wikipedia: "In two-valued logic there are 2 nullary operators (constants), 4 unary operators, 16 binary operators, 256 ternary operators" And we all agree which of those 16 is named what. "In three-valued logic there are 3 nullary operators (constants), 27 unary operators, 19683 binary operators, 7625597484987 ternary operators" There is no standard meaning of the 3'rd value and of the operations involving it. That is not to say that 3VL isn't useful. I believe the reason for the criticism of 3VL in SQL it that the system made those choices for you and those choices are not always intuitive. Therefore a null in one attribute in one relation might mean something very different from a null in another attribute in another relation. Also note that as opposed to digital signal processing (where binary and ternary refer to the number of possible values a bit/trit can have), when discussing logic arity (nullary, unary, binary, ternary, n-ary) refers to the number of arguments required by a function as opposed to the number of values the arguments can have (univalent, bivalent, trivalent, k-valent). This is confusing because the terms are used interchangeably.
  - freilanzer 4y ago
    Yes, so it's just about returning a (Maybe = Just bool | Nothing). No null needed.
    - evomassiny 4y ago
      exaclty, whether you call it 'Nothing' or 'null' does not matter, as long as it represents a distinct type than 'true' or 'false'
      - freilanzer 4y ago
        Null for me is a null pointer, and thus there's a difference. Anyway, if that's all you want than Haskell, etc. definitely handle that case.
        nerdponx 4y ago
        The word "null" means "missing value" in e.g. SQL and most data science / analytics contexts. It's unfortunately an overloaded term with two different meaning. Conflating the two things is where we get the egregious mistake of using null pointers to represent null data!
  - avgcorrection 4y ago
    That doesn’t make sense. `null | false | true` is not equivalent to `Option<bool>` or `Option<false | true>`. Just like `zero | one | two` is not equivalent to `Option<one | two>`. Assuming that `true | false` is equivalent to something like `enum { true, false }`.
    - evomassiny 4y ago
      > Just like `zero | one | two` is not equivalent to `Option<one | two>` Isn't it ? both cases represent a type than can express 3 variants
      - valenterry 4y ago
        It is equivalent in the amount of information you can encode, but not in how you can use it. Classical example is wrapping multiple times: Option<Option<one | two>>. If you have null | null | one | two, well... that just boils down to null | one | two.
      - Nullabillity 4y ago
        Those two types are indeed equivalent by themselves. The problem comes when you want to store them somewhere nullable. `zero | one | two | zero` flattens back down to `zero | one | two`, you can't distinguish between the two zero/null cases. On the other hand, `Option<Option<one | two>>` allows you to distinguish between None and Some(None). This makes union types unsound in the presence of type parameters/generics. TypeScript supports both anyway, because Hejlsberg cares more about being able to type existing JS antipatterns than about providing a sound type system.
        valenterry 4y ago
        > This makes union types unsound in the presence of type parameters/generics. I'm not sure if "unsound" is a good adjective here. There are cases where this is actually desired behaviour and the rules can definitely be "sound". For example, I might want to know what errors can appear, but not care where they come from. So `ErrorA | ErrorB` is what I want to see, not some nested structured that allows me to differentiate where ErrorA came from in case that there are multiple possible options.
e3bc54b2 4y ago
Usually this is done by means of Enumerated types. As someone who didn't get conventional CS education, Enums were bit of me-too for me, but the moment I realised they can be used to make invalid states unrepresentable, I was hooked. Sure, they can be better in java, but they cover a large enough ground, and as always, most people find that sufficient.
- frou_dh 4y ago
  What's different to typical Algebraic-Types/Sum-Types/Nü-Enums in what they showed is that it's existing values being OR'd together, not types or new type constructors. That is presumably why they are obliquely mentioning it in the comments thread of an Idris release, because Idris is known for "Dependent Types", i.e. types that depend on actual values of existing types, not just existing types.
quchen 4y ago
Isn’t it contradictory to say it’s the most frequent usage, and in the next sentence that no modern programming language does it?
- kelipso 4y ago
  No modern PL explicitly allows for it or type checks for it. Examples are enum types and null pointers, which are used everywhere. Implicit usage includes things like natural numbers (ints more than 0), ranges, values of a type following some rule, etc.
tralarpa 4y ago
> Haskell That can be done in Haskell with algebraic data types (with constructors without arguments), no? Languages that have enums: Java, Kotlin, Dart, Ada, C (not in the first version), Pascal (not in the first version), Modula-2, Visual Basic,... Pascal had subrange types since the first specification. For example "var month : 1..12;" I don't know anything about Typescript but from what I have found it seems that Typescript's literal types are similar to Pascal's subrange types, i.e., the new type is compatible to the basic type it is derived from (unlike enums in the above languages, which are completely new types). But there is no runtime check.
- pjmlp 4y ago
  I am quite sure that Pascal had enumerations since the early days. Section "6.1.1 Scalar Types", 1973 edition: https://www.standardpascal.org/The_Programming_Language_Pascal_1973.pdf https://www.standardpascal.org/The_Programming_Language_Pasc...
  - tralarpa 4y ago
    My bad. In the newer edition they called it "enumerated types": http://pascal.hansotten.com/uploads/books/Pascal_User_Manual_and_Report_Fourth_Edition.pdf http://pascal.hansotten.com/uploads/books/Pascal_User_Manual... I didn't realize that "scalar types" in the first edition were the same thing.
- afiori 4y ago
  Typescripts types are more similar to OCaml's variant types[0]; sadly my knowledge of OCaml's type system is less than a tenth of what I would like so I cannot give precise parallels, but in typescript you can have type A = 0 | null | Array<string>, type B = Array<number> | 0 | Array<string> and construct the type A & B = 0 | Array<string> In general I think that it is not possible to "just" add an type intersection operator to an Hindley–Milner type system without making it either incomplete[1] or unsound[2] In typescript this is often used with records as {a:number} & {b:string} = {a:number, b:string} [0] https://v2.ocaml.org/releases/5.0/htmlman/types.html#sss:typexpr-obj https://v2.ocaml.org/releases/5.0/htmlman/types.html#sss:typ... [1][2] which typescript is EDIT: fix typo
alpaca128 4y ago
Defining `MyType = 3 | "foo" | false` needs the language to allow arbitrary type changes of a variable, and while that's possible in JS it's generally not considered a good idea. Rust forces you to define a single enum to represent this, and then you can implement the TryFrom trait to make it directly comparable to booleans, integers etc, but without having to deal with random `undefined` values popping up everywhere. Is it less convenient? Yes, but so are seatbelts. Sometimes you need to build software where this tradeoff is worth it.
- dpratt71 4y ago
  In your example, '3 | "foo" | false' is the type of the variable. What is the argument for this being a bad idea in general? You imply it's unsafe. How?
  - alpaca128 4y ago
    > In your example, '3 | "foo" | false' is the type of the variable Depends. TypeScript would (usually) recognize 3 being a part of that union type, but it's still a normal integer that is fully compatible with other numbers. If you add 1 to it the variable is still a number but doesn't belong to this union type anymore. You could of course argue that this is just a consequence of TS being wrapped around JS, but whether the type changes between `3` and `false` or between `3` and `4`, it does change. In Rust this is not allowed, hence you cannot just do an addition between e.g. an enum variant and a number unless you explicitly implement the interface to make them compatible, in which case the addition produces a new value with - again - an immutable type. If 3, "foo" and false have different types by themselves then the language has to either allow changing the type of a variable or forbid a mix of them in one type.
    - dpratt71 4y ago
      Rust is more restrictive than it needs to be, in this case. What matters is whether it's possible to have a situation where the value of a variable or parameter is not concordant with its type in a given context and what it takes to make that happen. Of course it's possible to tell the TS type checker to sod off in a given context (cast, use the "any" type, etc.), but without doing that, I think it's hard to contrive a situation such as I described above. https://www.typescriptlang.org/play?#code/C4TwDgpgBAsiAq5oF4oGYoB8oCIBmA9gTllHgIYA2AzhANwBQDeArgHYDGwAlgW2VAAUADygAuWAiQBKBgG8GUKAHplUACYEo1YCzx4AdEYYBfJpQjAooiXESRGDUajSO8I6Y9EBqVAEY3DzogA https://www.typescriptlang.org/play?#code/C4TwDgpgBAsiAq5oF4...
pron 4y ago
Many languages have enum types and algebraic data types (Java has both now). TypeScript is a little unique in that its core type system is much more structural than nominal (even more so than Haskell) -- and that's because of its JS heritage and interop -- but structural types have significant disadvantages as well advantages. The main advantage is succinctness as well as very powerful inference. The main downside is inscrutable type errors (if two types having the same structure are considered to be the same type, the compiler has little choice but to refer only to the structure in error messages rather than the type name).
- uryga 4y ago
  > TypeScript is a little unique in that its core type system is much more structural than nominal (even more so than Haskell) I'm a bit confused by the point about Haskell here -- IME Haskell's type system is pretty strictly nominal, not a lot of structural typing there
  - pron 4y ago
    Function types are structural in Haskell.
nequo 4y ago
Your example in Haskell: —- ADTs in regular old Haskell data MyBoolean = MyNull | MyTrue | MyFalse —- Refinement types in Liquid Haskell {-@ type MyRange = {v:Int | ((v >= 3) && (v <= 5))} @-}
johnisgood 4y ago
I think what you are looking for is Ada. https://learn.adacore.com/courses/intro-to-ada/chapters/strongly_typed_language.html https://learn.adacore.com/courses/intro-to-ada/chapters/stro... https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Developer/chapters/05_Type_System.html https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Devel... https://www.adaic.org/resources/add_content/standards/05rm/html/RM-3-2-2.html https://www.adaic.org/resources/add_content/standards/05rm/h...
aranchelk 4y ago
Comment is getting some hate, but it’s somewhat interesting. This is something you can’t do in standard Haskell. You can certainly do: data MyRange = My3 | My4 | My5, then write a MyRangeToInt function. But in Haskell (AFAIK, there may be a GHC extension) you cannot say to the type checker: I want to define a new type as a subset of the inhabitants of an existing type. That seems slightly more ergonomic in some situations if you then wanted to then run other functions that work on the original type — it at least saves you the conversion step. Regarding MyBoolean, you’re now doing the previous trick, using a subset of the inhabitants of existing types, but they’re from different types and they’re being put in an untagged union, in Haskell this would be implemented with: type MyBoolean = Maybe Bool, where “Maybe” takes any type as an argument, IMO the Haskell way is a lot cleaner.
Georgelemental 4y ago
For the subcase where the literals are all members of a same overarching type (like your "MyRange" example), there has been some experimentation in this direction in Rust: https://github.com/rust-lang/rust/pull/107606 https://github.com/rust-lang/rust/pull/107606
speed_spread 4y ago
Anonymous union types? Scala has that. So did Ceylon.
ObscureScience 4y ago
Hi, what do you mean when you say that literla types are both one of the most frequent uses of a type system, while at the same time modern languages doesn't support them? Did you mean to say "most useful" rather than "most frequent"?

freilanzer 4y ago

Why would I ever want to extend a type with null? That's exactly the opposite of what I want of a type system in the first place.

evomassiny 4y ago
the type `null | true | false` is different from `true | false`, a type checker can assert that you handle the `null` case before using a function that wants a boolean. This is how rust handles it (with the Option<T> type).
- harperlee 4y ago
  In particular, you may want this to signify “I dont know” with NULL, just as in SQL. See the Wikipedia page for ternary logic for more info.
  - alexvoda 4y ago
    Note that 3VL (3 valued logic) is one of the more criticized aspects of SQL. 3VL is a gigantic leap of of complexity over 2VL (boolean). The number of possible operations is a lot higher and the choice of operations is not standardized. To quote wikipedia: "In two-valued logic there are 2 nullary operators (constants), 4 unary operators, 16 binary operators, 256 ternary operators" And we all agree which of those 16 is named what. "In three-valued logic there are 3 nullary operators (constants), 27 unary operators, 19683 binary operators, 7625597484987 ternary operators" There is no standard meaning of the 3'rd value and of the operations involving it. That is not to say that 3VL isn't useful. I believe the reason for the criticism of 3VL in SQL it that the system made those choices for you and those choices are not always intuitive. Therefore a null in one attribute in one relation might mean something very different from a null in another attribute in another relation. Also note that as opposed to digital signal processing (where binary and ternary refer to the number of possible values a bit/trit can have), when discussing logic arity (nullary, unary, binary, ternary, n-ary) refers to the number of arguments required by a function as opposed to the number of values the arguments can have (univalent, bivalent, trivalent, k-valent). This is confusing because the terms are used interchangeably.
- freilanzer 4y ago
  Yes, so it's just about returning a (Maybe = Just bool | Nothing). No null needed.
  - evomassiny 4y ago
    exaclty, whether you call it 'Nothing' or 'null' does not matter, as long as it represents a distinct type than 'true' or 'false'
    - freilanzer 4y ago
      Null for me is a null pointer, and thus there's a difference. Anyway, if that's all you want than Haskell, etc. definitely handle that case.
      - nerdponx 4y ago
        The word "null" means "missing value" in e.g. SQL and most data science / analytics contexts. It's unfortunately an overloaded term with two different meaning. Conflating the two things is where we get the egregious mistake of using null pointers to represent null data!
- avgcorrection 4y ago
  That doesn’t make sense. `null | false | true` is not equivalent to `Option<bool>` or `Option<false | true>`. Just like `zero | one | two` is not equivalent to `Option<one | two>`. Assuming that `true | false` is equivalent to something like `enum { true, false }`.
  - evomassiny 4y ago
    > Just like `zero | one | two` is not equivalent to `Option<one | two>` Isn't it ? both cases represent a type than can express 3 variants
    - valenterry 4y ago
      It is equivalent in the amount of information you can encode, but not in how you can use it. Classical example is wrapping multiple times: Option<Option<one | two>>. If you have null | null | one | two, well... that just boils down to null | one | two.
    - Nullabillity 4y ago
      Those two types are indeed equivalent by themselves. The problem comes when you want to store them somewhere nullable. `zero | one | two | zero` flattens back down to `zero | one | two`, you can't distinguish between the two zero/null cases. On the other hand, `Option<Option<one | two>>` allows you to distinguish between None and Some(None). This makes union types unsound in the presence of type parameters/generics. TypeScript supports both anyway, because Hejlsberg cares more about being able to type existing JS antipatterns than about providing a sound type system.
      - valenterry 4y ago
        > This makes union types unsound in the presence of type parameters/generics. I'm not sure if "unsound" is a good adjective here. There are cases where this is actually desired behaviour and the rules can definitely be "sound". For example, I might want to know what errors can appear, but not care where they come from. So `ErrorA | ErrorB` is what I want to see, not some nested structured that allows me to differentiate where ErrorA came from in case that there are multiple possible options.

e3bc54b2 4y ago

Usually this is done by means of Enumerated types. As someone who didn't get conventional CS education, Enums were bit of me-too for me, but the moment I realised they can be used to make invalid states unrepresentable, I was hooked. Sure, they can be better in java, but they cover a large enough ground, and as always, most people find that sufficient.

frou_dh 4y ago
What's different to typical Algebraic-Types/Sum-Types/Nü-Enums in what they showed is that it's existing values being OR'd together, not types or new type constructors. That is presumably why they are obliquely mentioning it in the comments thread of an Idris release, because Idris is known for "Dependent Types", i.e. types that depend on actual values of existing types, not just existing types.

quchen 4y ago

Isn’t it contradictory to say it’s the most frequent usage, and in the next sentence that no modern programming language does it?

kelipso 4y ago
No modern PL explicitly allows for it or type checks for it. Examples are enum types and null pointers, which are used everywhere. Implicit usage includes things like natural numbers (ints more than 0), ranges, values of a type following some rule, etc.

tralarpa 4y ago

> Haskell That can be done in Haskell with algebraic data types (with constructors without arguments), no? Languages that have enums: Java, Kotlin, Dart, Ada, C (not in the first version), Pascal (not in the first version), Modula-2, Visual Basic,... Pascal had subrange types since the first specification. For example "var month : 1..12;" I don't know anything about Typescript but from what I have found it seems that Typescript's literal types are similar to Pascal's subrange types, i.e., the new type is compatible to the basic type it is derived from (unlike enums in the above languages, which are completely new types). But there is no runtime check.

pjmlp 4y ago
I am quite sure that Pascal had enumerations since the early days. Section "6.1.1 Scalar Types", 1973 edition: https://www.standardpascal.org/The_Programming_Language_Pascal_1973.pdf https://www.standardpascal.org/The_Programming_Language_Pasc...
- tralarpa 4y ago
  My bad. In the newer edition they called it "enumerated types": http://pascal.hansotten.com/uploads/books/Pascal_User_Manual_and_Report_Fourth_Edition.pdf http://pascal.hansotten.com/uploads/books/Pascal_User_Manual... I didn't realize that "scalar types" in the first edition were the same thing.
afiori 4y ago
Typescripts types are more similar to OCaml's variant types[0]; sadly my knowledge of OCaml's type system is less than a tenth of what I would like so I cannot give precise parallels, but in typescript you can have type A = 0 | null | Array<string>, type B = Array<number> | 0 | Array<string> and construct the type A & B = 0 | Array<string> In general I think that it is not possible to "just" add an type intersection operator to an Hindley–Milner type system without making it either incomplete[1] or unsound[2] In typescript this is often used with records as {a:number} & {b:string} = {a:number, b:string} [0] https://v2.ocaml.org/releases/5.0/htmlman/types.html#sss:typexpr-obj https://v2.ocaml.org/releases/5.0/htmlman/types.html#sss:typ... [1][2] which typescript is EDIT: fix typo

alpaca128 4y ago

Defining `MyType = 3 | "foo" | false` needs the language to allow arbitrary type changes of a variable, and while that's possible in JS it's generally not considered a good idea. Rust forces you to define a single enum to represent this, and then you can implement the TryFrom trait to make it directly comparable to booleans, integers etc, but without having to deal with random `undefined` values popping up everywhere. Is it less convenient? Yes, but so are seatbelts. Sometimes you need to build software where this tradeoff is worth it.

dpratt71 4y ago
In your example, '3 | "foo" | false' is the type of the variable. What is the argument for this being a bad idea in general? You imply it's unsafe. How?
- alpaca128 4y ago
  > In your example, '3 | "foo" | false' is the type of the variable Depends. TypeScript would (usually) recognize 3 being a part of that union type, but it's still a normal integer that is fully compatible with other numbers. If you add 1 to it the variable is still a number but doesn't belong to this union type anymore. You could of course argue that this is just a consequence of TS being wrapped around JS, but whether the type changes between `3` and `false` or between `3` and `4`, it does change. In Rust this is not allowed, hence you cannot just do an addition between e.g. an enum variant and a number unless you explicitly implement the interface to make them compatible, in which case the addition produces a new value with - again - an immutable type. If 3, "foo" and false have different types by themselves then the language has to either allow changing the type of a variable or forbid a mix of them in one type.
  - dpratt71 4y ago
    Rust is more restrictive than it needs to be, in this case. What matters is whether it's possible to have a situation where the value of a variable or parameter is not concordant with its type in a given context and what it takes to make that happen. Of course it's possible to tell the TS type checker to sod off in a given context (cast, use the "any" type, etc.), but without doing that, I think it's hard to contrive a situation such as I described above. https://www.typescriptlang.org/play?#code/C4TwDgpgBAsiAq5oF4oGYoB8oCIBmA9gTllHgIYA2AzhANwBQDeArgHYDGwAlgW2VAAUADygAuWAiQBKBgG8GUKAHplUACYEo1YCzx4AdEYYBfJpQjAooiXESRGDUajSO8I6Y9EBqVAEY3DzogA https://www.typescriptlang.org/play?#code/C4TwDgpgBAsiAq5oF4...

pron 4y ago

Many languages have enum types and algebraic data types (Java has both now). TypeScript is a little unique in that its core type system is much more structural than nominal (even more so than Haskell) -- and that's because of its JS heritage and interop -- but structural types have significant disadvantages as well advantages. The main advantage is succinctness as well as very powerful inference. The main downside is inscrutable type errors (if two types having the same structure are considered to be the same type, the compiler has little choice but to refer only to the structure in error messages rather than the type name).

uryga 4y ago
> TypeScript is a little unique in that its core type system is much more structural than nominal (even more so than Haskell) I'm a bit confused by the point about Haskell here -- IME Haskell's type system is pretty strictly nominal, not a lot of structural typing there
- pron 4y ago
  Function types are structural in Haskell.

nequo 4y ago

Your example in Haskell: —- ADTs in regular old Haskell data MyBoolean = MyNull | MyTrue | MyFalse —- Refinement types in Liquid Haskell {-@ type MyRange = {v:Int | ((v >= 3) && (v <= 5))} @-}

johnisgood 4y ago

I think what you are looking for is Ada. https://learn.adacore.com/courses/intro-to-ada/chapters/strongly_typed_language.html https://learn.adacore.com/courses/intro-to-ada/chapters/stro... https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Developer/chapters/05_Type_System.html https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Devel... https://www.adaic.org/resources/add_content/standards/05rm/html/RM-3-2-2.html https://www.adaic.org/resources/add_content/standards/05rm/h...

aranchelk 4y ago

Comment is getting some hate, but it’s somewhat interesting. This is something you can’t do in standard Haskell. You can certainly do: data MyRange = My3 | My4 | My5, then write a MyRangeToInt function. But in Haskell (AFAIK, there may be a GHC extension) you cannot say to the type checker: I want to define a new type as a subset of the inhabitants of an existing type. That seems slightly more ergonomic in some situations if you then wanted to then run other functions that work on the original type — it at least saves you the conversion step. Regarding MyBoolean, you’re now doing the previous trick, using a subset of the inhabitants of existing types, but they’re from different types and they’re being put in an untagged union, in Haskell this would be implemented with: type MyBoolean = Maybe Bool, where “Maybe” takes any type as an argument, IMO the Haskell way is a lot cleaner.

Georgelemental 4y ago

For the subcase where the literals are all members of a same overarching type (like your "MyRange" example), there has been some experimentation in this direction in Rust: https://github.com/rust-lang/rust/pull/107606 https://github.com/rust-lang/rust/pull/107606

speed_spread 4y ago

Anonymous union types? Scala has that. So did Ceylon.

ObscureScience 4y ago

Hi, what do you mean when you say that literla types are both one of the most frequent uses of a type system, while at the same time modern languages doesn't support them? Did you mean to say "most useful" rather than "most frequent"?