Why is Idris 2 so much faster than Idris 1?

> Totality is orthogonal to dependent types. You can absolutely have non-total programs at the type level: Rust has such programs today in fact!

Absolutely, the talk I linked to gets at this to some extent. In rust, partiality causes type checking to fail. You could use it on purpose!

> You can have an infinite loop in a total language like Agda or Idris: coinduction is the mechanism.

For sure, but the totality checker is appeased by sized-types, or at least that's how I know to do it in Agda. I've heard it can be done without them, but I'm not familiar with the approach. This is what I intended w/r/t structural recursion.

> This doesn't make a whole lot of sense to me.

This is because, as the authors state, to type check the program is to evaluate it, so before it can run you have proof that it is correct.

By opting out I'm more talking about the converse, to opt in when you need it. Kind of the opposite of Idris's %partial directive.

> You can be total over IO, and effects do not imply non-totality either.

That's fair, you're right. This is poorly stated.

Scheme isn't used to replace Haskell. Idris 1 is written in Haskell and compiled by default to C (it comes with a Javascript backend too and it has an API for making others). Idris 2 is written in Idris 2 and compiles to Scheme so far (Chez by default, there is also support for Racket and Gambit), it's not tied to scheme but there is no pluggable backend functionality yet.

So Scheme is replacing C, and Idris is replacing Haskell. The goal was self-hosting by writing the compiler in Idris. Chez Scheme is a nice compilation target because it's performant and Scheme is a sugared lambda calculus that goes well together with FP languages.

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 constructors (types that depend on types; something akin to C++ template types like `vector` but not like `std::sort`), and dependent types (types that depend on values; but definitely not restricted like `std::array`; something more like MacroC or `enable_if`).

There's not a lot of good analogies for this stuff in commonly used programming languages because the big languages are really basic (not simple!) compared to the advanced stuff the programming language theorists have gotten up to.

Rust Generics are Parametric Polymorphism - you must pre-declare the allowed operations on the Type Parameters via Trait Bounds (essentially Haskell Typeclass constraints), and the Generic will fail to compile if you try to perform any other operations in the body (even if the Generic is never instantiated).

In C++ you can do any syntactically valid thing with the Type Parameter in a Template body, and it isn't type-checked until you attempt to instantiate it.

The usual answer for such a question about X2 and X1 is that X1 was really slow. It is usually correct, with the proviso that X2 might still be really slow, only less so.

With most computer artifacts, it is hard to tell, prima facie, that they are slow, until somebody makes a faster one. Then the original comes to be recognized as slow (although somebody will still insist it's not that slow). The faster one might still be slow, but that fact remains unknown.

The fact is that almost everything is slow, in the sense that somebody smarter, more experienced, and more diligent could make it faster, often by doing things that the person who wrote the slow version would have found distasteful.