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

11–20 of 65 posts

Re: Idris 2 0.6.0 is now available for the JVM

#11

Post by harperlee »

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

In particular, you may want this to signify “I dont know” with NULL, just as in SQL. See the Wikipedia page for ternary logic for more info.

Re: Idris 2 0.6.0 is now available for the JVM

#12

Post by alpaca128 »

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.

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.

Is it less convenient? Yes, but so are seatbelts. Sometimes you need to build software where this tradeoff is worth it.

Re: Idris 2 0.6.0 is now available for the JVM

#13

Post by pron »

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.

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 inscrutable type errors (if two types having the same structure are considered to be the same type, the compiler has little choice but to refer only to the structure in error messages rather than the type name).

Re: Idris 2 0.6.0 is now available for the JVM

#14

Post by uryga »

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

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

Re: Idris 2 0.6.0 is now available for the JVM

#15

Post by nequo »

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.

Your example in Haskell:

  —- ADTs in regular old Haskell
  data MyBoolean = MyNull | MyTrue | MyFalse

  —- Refinement types in Liquid Haskell
  {-@ type MyRange = {v:Int | ((v >= 3) && (v

Re: Idris 2 0.6.0 is now available for the JVM

#16

Post by freilanzer »

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

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

Re: Idris 2 0.6.0 is now available for the JVM

#18

Post by zelphirkalt »

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

Re: Idris 2 0.6.0 is now available for the JVM

#19

Post by dpratt71 »

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

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?

Re: Idris 2 0.6.0 is now available for the JVM

#20

Post by zarzavat »

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

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…

TypeScript lets you fit your types to your data, whatever that data is. If your data includes mixed types, then you can represent those. If I have a JSON array that mixes numbers and strings then I can write (number|string)[].

Most other statically typed languages force you to fit your data to your types. Many statically typed languages simply degenerate into dynamic typing when trying to consume external data, e.g. by representing JSON as an enumeration of every possible JSON value type.

Post reply on HN