Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why is Idris 2 so much faster than Idris 1?

type-driven.org.uk

Post reply on HN
Print view View original

71–80 of 88 posts

Re: Why is Idris 2 so much faster than Idris 1?

#71

Post by Legogris »

nilkn wrote: post #57

How practical is Idris (or Idris 2) for real-world production programming right now? It seems to be a pretty natural evolution of Haskell with dependent types built in from the ground up instead of being sort of achievable with a patchwork of language extensions. Moreover, making laziness optional is a big deal for real-world industrial applications. (Note that even the author of this post indicates at the end signif…

My experience is from 2015 but from a language-perspective the only things I personally saw lacking for prime-time use would be performance and the compiler/type-checker not always giving accurate error messages - but overall, nothing considerable when comparing to Haskell. I don't know how much those areas have been improving since. Overall I was very excited about Idris and found the syntax a lot more approachable than Haskell.

If the meager library of third-party and community packages is an important factor or not depends a lot on the domain.

I really wish some powerful corp would pick up Idris and put contributions and/or funding to it.

Re: Why is Idris 2 so much faster than Idris 1?

#72

Post by dejj »

icen wrote: post #70
dejj wrote: post #69

Earlier quoted context omitted.

> pass types as parameters to be altered during execution Wouldn't that be at odds with static typing?

Dependent types let you do this. The type system ensures that you have all the types known at every point, and everything is sewn up before runtime - even though you don't know which type you will actually get ahead of time. Types are values, and types can depend on values - so if your protocol tells you you should be getting a string, a string shows up in the type signature.

> you don't know which type you will actually get ahead of time

Sounds like it's statically kinded, and dynamically typed. Or is it a place between kinds and types at which Idris operates?

Re: Why is Idris 2 so much faster than Idris 1?

#73

Post by ImprobableTruth »

dejj wrote: post #72
icen wrote: post #70

Earlier quoted context omitted.

Dependent types let you do this. The type system ensures that you have all the types known at every point, and everything is sewn up before runtime - even though you don't know which type you will actually get ahead of time. Types are values, and types can depend on values - so if your protocol tells you you should be getting a string, a string shows up in the type signature.

> you don't know which type you will actually get ahead of time Sounds like it's statically kinded, and dynamically typed. Or is it a place between kinds and types at which Idris operates?

It's just standard dependent types. Types don't (necessarily) get erased, but all the type checking itself is done at compile time.

I don't think it makes sense to think of it as specifically "statically kinded", since kinds (which are just types higher on the universe hierarchy) can also be present at runtime.

Re: Why is Idris 2 so much faster than Idris 1?

#74

Post by afiori »

dejj wrote: post #72
icen wrote: post #70

Earlier quoted context omitted.

Dependent types let you do this. The type system ensures that you have all the types known at every point, and everything is sewn up before runtime - even though you don't know which type you will actually get ahead of time. Types are values, and types can depend on values - so if your protocol tells you you should be getting a string, a string shows up in the type signature.

> you don't know which type you will actually get ahead of time Sounds like it's statically kinded, and dynamically typed. Or is it a place between kinds and types at which Idris operates?

The terminology is nearing its limit when talking about these kind of things.

I believe that static typing here means that there is no need for runtime dynamics type checks (outside of things like dynamic dispatch as with haskell typeclasses).

That is you can have a body of code where a variable can assume multiple incompatible types, but you always know that it will be the right one.

I would say it is a change in paradigm. Similarly to how rust' borrow checker and lifetimes change the paradigm of manual vs GC memory management

Re: Why is Idris 2 so much faster than Idris 1?

#75

Post by tluyben2 »

thechao wrote: post #46
PunksATawnyFill wrote: post #43

What is Idris? Critical info missing.

Your question is fair, and it's unfair you're being downvoted. Idris is a dependently typed programming language. If you imagine a "cube" of fundamental language features, on one corner is "the simply typed lambda calculus" which you can think of as old-school C. Along each of three edges we add a fundamental language feature: parametric polymorphism (values that depend on their type; think 'C# generics'), type const…

> Your question is fair, and it's unfair you're being downvoted.

I agree partly; I didn't downvote but I think in this case the downvotes are not that weird; it's quite well known what Idris is in HN circles, but that's not the point; the article has links that tell you (pointing to idris-lang) and google idris edwin brady (which is on top of the article) will get you more than you want to know most likely but at least enough to know what it is. So it is the absolute bare minimum to open an article and pop in; 'what is this?' if it's not in the first line of an article which I think is not great. A little bit more I do expect from this place; like clicking on the article, immediately recognising it as a language (that's clear within seconds of scrolling the article I would say) and then maybe come back with 'what is dependently typed?' or something. But going from opening the article to hitting wikipedia explaining dependently typed languages is ... well, not much more work than doing nothing and just popping 'huh?' in here imho.

Edit: actually, just google 'idris2' and you have in the first line exactly what, who, why etc.

Re: Why is Idris 2 so much faster than Idris 1?

#76

Post by icen »

dejj wrote: post #72
icen wrote: post #70

Earlier quoted context omitted.

Dependent types let you do this. The type system ensures that you have all the types known at every point, and everything is sewn up before runtime - even though you don't know which type you will actually get ahead of time. Types are values, and types can depend on values - so if your protocol tells you you should be getting a string, a string shows up in the type signature.

> you don't know which type you will actually get ahead of time Sounds like it's statically kinded, and dynamically typed. Or is it a place between kinds and types at which Idris operates?

It is more that you can have values like `payload : if byte[TYPE_OFFSET] == TYPE_INT then Int else String`.

You are required to disambiguate the type before anything useful can be done. What has happened is that you have types being passed around by functions and evaluations which reflect dynamic behaviour at runtime - but there is a type statically known at all times for each part of the program.

Re: Why is Idris 2 so much faster than Idris 1?

#77

Post by icen »

ImprobableTruth wrote: post #73
dejj wrote: post #72

Earlier quoted context omitted.

> you don't know which type you will actually get ahead of time Sounds like it's statically kinded, and dynamically typed. Or is it a place between kinds and types at which Idris operates?

It's just standard dependent types. Types don't (necessarily) get erased, but all the type checking itself is done at compile time. I don't think it makes sense to think of it as specifically "statically kinded", since kinds (which are just types higher on the universe hierarchy) can also be present at runtime.

Indeed - the Type/Kind hierarchy is unified when you write a dependently typed system. In simply typed lambda calculus, you have a system of values, types, and kinds, which are required to make sense of the structure. In dependent types, you have values, and types, which are also values.

Re: Why is Idris 2 so much faster than Idris 1?

#78

Post by lmm »

icen wrote: post #70
dejj wrote: post #69

Earlier quoted context omitted.

> pass types as parameters to be altered during execution Wouldn't that be at odds with static typing?

Dependent types let you do this. The type system ensures that you have all the types known at every point, and everything is sewn up before runtime - even though you don't know which type you will actually get ahead of time. Types are values, and types can depend on values - so if your protocol tells you you should be getting a string, a string shows up in the type signature.

Types are not "altered". Types can be parameters. You can have a function that takes a type and returns something else (another type, or even another value). But nothing is changing.

Re: Why is Idris 2 so much faster than Idris 1?

#79

Post by lmm »

nikivi wrote: post #2

What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?

You might like to read https://serokell.io/blog/why-dependent-haskell , which describes a roadmap for making dependent types practical in Haskell.

Useful steps on the road: singleton types (needed to make it easy to represent basic values as types), higher-kinded types (needed to implement functions at the type level), kind polymorphism (needed to be able to reuse the same functions at the type and the value level). Rust is I think getting the first, is gradually implementing little subsets of the second, and is nowhere near the third.

The other thing you need to worry about is how dependent types interact with existing language features. In particular, if not implemented carefully then they may break type inference, and I imagine Rust's lifetime inference might have similar issues.

Re: Why is Idris 2 so much faster than Idris 1?

#80

Post by icen »

dejj wrote: post #72
icen wrote: post #70

Earlier quoted context omitted.

Dependent types let you do this. The type system ensures that you have all the types known at every point, and everything is sewn up before runtime - even though you don't know which type you will actually get ahead of time. Types are values, and types can depend on values - so if your protocol tells you you should be getting a string, a string shows up in the type signature.

> you don't know which type you will actually get ahead of time Sounds like it's statically kinded, and dynamically typed. Or is it a place between kinds and types at which Idris operates?

As the workhorse example, consider the length-indexed Vector:

    data Vec : Nat -> Type -> Type
Each Vec has its length in its type. You get a type error if you try the following:

    f : Vec 3 Int -> Int
    f [1, 2, 3, 4] -- error: wanted a Vec 3 Int, found a Vec 4 Int
and with that, consider the following program:

    import Data.Vect
    
    readInts : (n : Nat) -> IO (Vect n Int)
    readInts 0 = pure []
    readInts (S n) = do
      x
The above program doesn't know what the type of `ints` is in the do-block precisely. It has a length specified by the user! But we can reason about its length - and the type system would ensure that its length is propagated and handled properly everywhere we try to use it.
Post reply on HN