News for hackers. Stuff that matters.
Re:Idris 2 0.6.0 is now available for the JVM by tralarpa on Monday February 27, 2023 @06:52AM (#34955360)
> 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.

Re:Idris 2 0.6.0 is now available for the JVM by pjmlp on Monday February 27, 2023 @08:32AM (#34956167)
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_Pasc...

Re:Idris 2 0.6.0 is now available for the JVM by tralarpa on Monday February 27, 2023 @09:15AM (#34956622)
My bad. In the newer edition they called it "enumerated types":

http://pascal.hansotten.com/uploads/books/Pascal_User_Manual...

I didn't realize that "scalar types" in the first edition were the same thing.

Re:Idris 2 0.6.0 is now available for the JVM by afiori on Monday February 27, 2023 @08:39AM (#34956239)
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]

[0] https://v2.ocaml.org/releases/5.0/htmlman/types.html#sss:typ...

[1][2] which typescript is

EDIT: fix typo

Re:Idris 2 0.6.0 is now available for the JVM by valenterry on Monday February 27, 2023 @10:11AM (#34957287)
It's not quite the same. You can emulate literal string types using recursive ADTs (similar lists), storing one character at the time at the typesystem.

But the ergonomics are quite different.

For example, in Scala you can do this:

    val foo: "Must be this string" = "foo" // fails to compile
In Typescript it's similar. But how would "Must be this string" look in the case of a haskell ADT?