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

61–65 of 65 posts

Re: Idris 2 0.6.0 is now available for the JVM

#61

Post by mmhelloworld »

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"?

In the JVM backend, recursive calls are eliminated with loop. There is an option to enable trampoline for functions but I am currently working on replacing mutual recursion with loops so with that the trampoline option might be removed. As for data structures, there are Idris data structures like `List`, `SortedSet`, `SortedMap` etc. but only Idris `List` currently implements Java `List` interface.

Re: Idris 2 0.6.0 is now available for the JVM

#62

Post by mmhelloworld »

ghostwriter wrote: post #9

How does it interop with the existing Java libraries?

This file https://github.com/mmhelloworld/idris-jvm/blob/main/libs/bas... demonstrates how the interop looks like currently. The `%foreign` directive takes an FFI descriptor to talk to the respective backends. Here you can see few scheme and JVM descriptors starting with "scheme:" and "jvm:" respectively. The JVM descriptors there show constructor calls ``, instance methods `.lock` and static methods `getThreadData`.

Re: Idris 2 0.6.0 is now available for the JVM

#63

Post by trenchgun »

valenterry wrote: post #43
Nullabillity wrote: post #38

Earlier quoted context omitted.

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

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

Sound type system is not one of the design goals of TypeScript

https://effectivetypescript.com/2021/05/06/unsoundness/

Re: Idris 2 0.6.0 is now available for the JVM

#64

Post by pron »

uryga wrote: post #14
pron wrote: post #13

Earlier quoted context omitted.

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…

> 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

Function types are structural in Haskell.

Re: Idris 2 0.6.0 is now available for the JVM

#65

Post by dpratt71 »

alpaca128 wrote: post #59
dpratt71 wrote: post #19

Earlier quoted context omitted.

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?

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

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

Post reply on HN