Idris 2 0.6.0 is now available for the JVM
1–10 of 65 posts
Re: Idris 2 0.6.0 is now available for the JVM
#2Idris 2 is a purely functional programming language with first class types. This repository provides Idris 2 compiler targeting JVM bytecode so that Idris 2 compiler and Idris 2 programs can run on the JVM
Re: Idris 2 0.6.0 is now available for the JVM
#3It would be nice if this linked to the README rather than a dump of the commit log, which makes it hard to know what's new or interesting in this release. It would be double nice if the readme talked about JVM language interop or performance, as that's presumably the main selling points of running Idris on the JVM.
Re: Idris 2 0.6.0 is now available for the JVM
#4One 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.
Re: Idris 2 0.6.0 is now available for the JVM
#5One 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.
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.
Re: Idris 2 0.6.0 is now available for the JVM
#6One 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.
Re: Idris 2 0.6.0 is now available for the JVM
#7One 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.
Isn’t it contradictory to say it’s the most frequent usage, and in the next sentence that no modern programming language does it?
Re: Idris 2 0.6.0 is now available for the JVM
#8One 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.
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).
Re: Idris 2 0.6.0 is now available for the JVM
#9How does it interop with the existing Java libraries?
Re: Idris 2 0.6.0 is now available for the JVM
#10One 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 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.