Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Idris 2 0.6.0 is now available for the JVM

github.com

Post reply on HN
Print view View original

21–30 of 65 posts

Re: Idris 2 0.6.0 is now available for the JVM

#21

Post by frou_dh »

e3bc54b2 wrote: post #6
revskill wrote: post #4

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.

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.

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.

Re: Idris 2 0.6.0 is now available for the JVM

#22

Post by pjmlp »

zelphirkalt wrote: post #18

I am wondering what kind of implications there are for Idris 2 to run on the JVM. For example: Does it still have TCO on the JVM? What about data structures? Does it have a set of functional data structures implemented, on top of Java ones? Or is it all implemented on top of Idris 2 "primitives"?

Naturally it doesn't have TCO on JVM, at least not natively as bytecode representation for it.

The only possibility is to rewrite the code in similar way as clojure and Scala do it.

Re: Idris 2 0.6.0 is now available for the JVM

#23

Post by pjmlp »

tralarpa wrote: post #10
revskill wrote: post #4

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.

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

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

#24

Post by johnisgood »

revskill wrote: post #4

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.

I think what you are looking for is Ada.

https://learn.adacore.com/courses/intro-to-ada/chapters/stro...

https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Devel...

https://www.adaic.org/resources/add_content/standards/05rm/h...

Re: Idris 2 0.6.0 is now available for the JVM

#25

Post by afiori »

tralarpa wrote: post #10
revskill wrote: post #4

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.

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

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, type B = Array | 0 | Array and construct the type A & B = 0 | Array

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

[1][2] which typescript is

EDIT: fix typo

Re: Idris 2 0.6.0 is now available for the JVM

#26

Post by evomassiny »

freilanzer wrote: post #16
evomassiny wrote: post #8

Earlier quoted context omitted.

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

Yes, so it's just about returning a (Maybe = Just bool | Nothing). No null needed.

exaclty, whether you call it 'Nothing' or 'null' does not matter, as long as it represents a distinct type than 'true' or 'false'

Re: Idris 2 0.6.0 is now available for the JVM

#27

Post by tralarpa »

pjmlp wrote: post #23
tralarpa wrote: post #10

Earlier quoted context omitted.

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

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

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

#28

Post by avgcorrection »

evomassiny wrote: post #8
freilanzer wrote: post #5

Earlier quoted context omitted.

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.

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

That doesn’t make sense. `null | false | true` is not equivalent to `Option` or `Option`. Just like `zero | one | two` is not equivalent to `Option`.

Assuming that `true | false` is equivalent to something like `enum { true, false }`.

Re: Idris 2 0.6.0 is now available for the JVM

#29

Post by otto-edgar »

zelphirkalt wrote: post #18

I am wondering what kind of implications there are for Idris 2 to run on the JVM. For example: Does it still have TCO on the JVM? What about data structures? Does it have a set of functional data structures implemented, on top of Java ones? Or is it all implemented on top of Idris 2 "primitives"?

I think TCO and JVM are orthogonal discussions -- by the time the bytecode is generated, the TCO may have already been performed.

Re: Idris 2 0.6.0 is now available for the JVM

#30

Post by freilanzer »

evomassiny wrote: post #26
freilanzer wrote: post #16

Earlier quoted context omitted.

Yes, so it's just about returning a (Maybe = Just bool | Nothing). No null needed.

exaclty, whether you call it 'Nothing' or 'null' does not matter, as long as it represents a distinct type than 'true' or 'false'

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.
Post reply on HN