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

31–40 of 65 posts

Re: Idris 2 0.6.0 is now available for the JVM

#31

Post by evomassiny »

avgcorrection wrote: post #28
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).

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

> Just like `zero | one | two` is not equivalent to `Option`

Isn't it ? both cases represent a type than can express 3 variants

Re: Idris 2 0.6.0 is now available for the JVM

#32

Post by nerdponx »

otto-edgar wrote: post #29
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.

I'm actually not sure about that. I think the Javascript compiler target also lacks full TCO. The Idris 2 compiler itself I think does not perform this optimization, because the Scheme reference backend does it already. I might be wrong about that, but I remember several active unresolved discussions on this topic in the community last year. I haven't been involved actively in it for several months, so my memory might be wrong.

Re: Idris 2 0.6.0 is now available for the JVM

#33

Post by nerdponx »

bsaul wrote: post #17

saw that idris compiled to C . How realistic is it to build a small core library in idris that would then have hooks to external components in other PL using C as a bridging layer ?

Idris 2 does compile to C, but it uses its own reference-counting garbage collector and cannot currently be used to generate libraries. I believe this limitation is true for all of the compiler targets right now, except maybe Javascript (some work was actively in progress on this when I last checked).

Re: Idris 2 0.6.0 is now available for the JVM

#34

Post by nerdponx »

freilanzer wrote: post #30
evomassiny wrote: post #26

Earlier quoted context omitted.

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.

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!

Re: Idris 2 0.6.0 is now available for the JVM

#35

Post by nerdponx »

ghostwriter wrote: post #9

How does it interop with the existing Java libraries?

I can't speak for the JVM backend specifically, but in general Idris 2 code can call arbitrary functions in the backend with the "%foreign" pragma. So hopefully that would be supported for Java, although I don't know how it would work with classes.

Re: Idris 2 0.6.0 is now available for the JVM

#36

Post by valenterry »

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…

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?

Re: Idris 2 0.6.0 is now available for the JVM

#37

Post by valenterry »

evomassiny wrote: post #31
avgcorrection wrote: post #28

Earlier quoted context omitted.

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

> Just like `zero | one | two` is not equivalent to `Option ` Isn't it ? both cases represent a type than can express 3 variants

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>. If you have null | null | one | two, well... that just boils down to null | one | two.

Re: Idris 2 0.6.0 is now available for the JVM

#38

Post by Nullabillity »

evomassiny wrote: post #31
avgcorrection wrote: post #28

Earlier quoted context omitted.

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

> Just like `zero | one | two` is not equivalent to `Option ` Isn't it ? both cases represent a type than can express 3 variants

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

Re: Idris 2 0.6.0 is now available for the JVM

#39

Post by aranchelk »

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.

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.

Re: Idris 2 0.6.0 is now available for the JVM

#40

Post by Georgelemental »

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.

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