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

51–60 of 65 posts

Re: Idris 2 0.6.0 is now available for the JVM

#51

Post by kelipso »

quchen wrote: post #7
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.

Isn’t it contradictory to say it’s the most frequent usage, and in the next sentence that no modern programming language does it?

No modern PL explicitly allows for it or type checks for it. Examples are enum types and null pointers, which are used everywhere. Implicit usage includes things like natural numbers (ints more than 0), ranges, values of a type following some rule, etc.

Re: Idris 2 0.6.0 is now available for the JVM

#53

Post by avgcorrection »

mixedCase wrote: post #49
avgcorrection wrote: post #47

Earlier quoted context omitted.

No. There is an isomorphism between them, but they aren’t equivalent since for one you will have to match on the `Option` first in order to see whether it is `None` or `Some(Next)` and then inspect `Next` (if `Some(…)`). Same reason that `Nothing | Pointer` is not equivalent to `Option `. And it makes a huge practical difference, since the first type allows for “nothing-pointer dereference” while the second one does…

> And it makes a huge practical difference, since the first type allows for “nothing-pointer dereference” That's not how strict TypeScript works. If you have a nullable you'll need to prove to the compiler first that it is not currently null before dereferencing.

Here’s what I originally replied to:

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

If the variant `null` here is handled specially in general in TS then yeah, I was wrong. However, I was mostly replying to the part about “this is how Rust handles it”.

Re: Idris 2 0.6.0 is now available for the JVM

#54

Post by saghm »

exabrial wrote: post #52

Never seen this language before, but I can say I _really_ like the syntax. Just looking at it it's pretty easy to figure out what they were trying to do.

Have you used Haskell before? It seems almost identical syntactically at a glance, so I'm curious if that's what you mean by "what they were trying to do" or if it's your first time seeing syntax like this at all.

Re: Idris 2 0.6.0 is now available for the JVM

#55

Post by speed_spread »

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.

Anonymous union types? Scala has that. So did Ceylon.

Re: Idris 2 0.6.0 is now available for the JVM

#56

Post by ObscureScience »

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.

Hi, what do you mean when you say that literla types are both one of the most frequent uses of a type system, while at the same time modern languages doesn't support them?

Did you mean to say "most useful" rather than "most frequent"?

Re: Idris 2 0.6.0 is now available for the JVM

#57

Post by ObscureScience »

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…

I did not catch from you comment if you knew, but "sound" and "unsound" are specific concepts in type theory, and they are binary properties. A system either is or is not sound.

Re: Idris 2 0.6.0 is now available for the JVM

#58

Post by valenterry »

ObscureScience wrote: post #57
valenterry wrote: post #43

Earlier quoted context omitted.

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

I did not catch from you comment if you knew, but "sound" and "unsound" are specific concepts in type theory, and they are binary properties. A system either is or is not sound.

Yeah I know that.

So: > This makes union types unsound in the presence of type parameters/generics.

Sounds a bit strange to me. Why would union types + type parameters be generally unsafe? I doubt that that's true.

Re: Idris 2 0.6.0 is now available for the JVM

#59

Post by alpaca128 »

dpratt71 wrote: post #19
alpaca128 wrote: post #12

Earlier quoted context omitted.

Defining `MyType = 3 | "foo" | false` needs the language to allow arbitrary type changes of a variable, and while that's possible in JS it's generally not considered a good idea. Rust forces you to define a single enum to represent this, and then you can implement the TryFrom trait to make it directly comparable to booleans, integers etc, but without having to deal with random `undefined` values popping up everywhere…

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 whether the type changes between `3` and `false` or between `3` and `4`, it does change.

In Rust this is not allowed, hence you cannot just do an addition between e.g. an enum variant and a number unless you explicitly implement the interface to make them compatible, in which case the addition produces a new value with - again - an immutable type.

If 3, "foo" and false have different types by themselves then the language has to either allow changing the type of a variable or forbid a mix of them in one type.

Re: Idris 2 0.6.0 is now available for the JVM

#60

Post by mmhelloworld »

fidgewidge wrote: post #3

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

Hello, I am the author of Idris JVM. Thank you for your feedback. I will update the README to include a link for JVM interop. For now, 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 also show constructor calls ``, instance methods `.lock` and static methods `getThreadData`.
Post reply on HN