I'm fascinated by Idris, dependent types and the promise of massively expanding compile-time guarantees. The compile times mentioned in the article raise a question that I've wondered about, and would love to hear from an expert: are compile times essentially unbounded in languages like Idris? Is it possible (likely?) in practice that wrong or misguided uses of the type system could cause quadratic or exponential scaling of compile times?
Not an expert, but I've played with these languages. The short answer is yes this is possible, but it is also possible already in non-dependently typed languages to do so.
Moreover in practice it's not very common to actually evaluate your functions on large literal inputs at compile time. Indeed it's not very common to evaluate the function on a single value as such at all. Instead it is better to think of your functions as abstract rewrite rules, that allow you to substitute one side with the other. Unlike at runtime, recursive functions do not always need to recurse until their base case.
Therefore it's not actually very common to e.g. have a recursive function recurse many times at compile time. However, when it does happen, yeah your compile times can shoot up, but it's usually fairly obvious what's causing it. Even then, in absolute terms the quantity of calculations involved generally isn't astronomical, it's rather the case that the compiler is far more inefficient at executing your code at compile time than your runtime system is at executing the compiled code.
That being said, dependently typed languages on the whole do tend to have abysmal compile times, but this seems like an implementation issue rather than a fundamental limitation. Efforts like https://github.com/AndrasKovacs/smalltt/blob/master/README.m... make me hopeful this is something that can be solved.
Virtually any compiled programming language has had an infinite-loop bug in the compiler at some point or other. E.g. Java has a notoriously simplistic type system, but still had a famous case.
Typing an ML-like language is technically exponential in the length of the program, but really the way to look at it is that it's exponential in the depth of the most deeply nested block (for certain kinds of block). There's a certain symmetry with how program runtime is naturally exponential in the depth of the most deeply nested loop - and, in the same way, while deeply nested blocks are possible, they're generally bad code.
I've hit troublesome compile times in Scala a couple of times. One of them was due to a naively implemented type-level intersection operation and lead me to abandon that project (I was trying to write a compile-time dependency injection framework, so you'd have a set of types representing what you had already instantiated and a set of types representing what each service needed to instantiate itself, so you could only add a service if you already had all of its dependencies available. But it was all using linear search, since types (in Scala) are not hashable as far as I know, and even if they were, I don't know that I'm up to implementing a hashtable using type-level programming).
Yes, you can make compile times _extremely long_. They're not unbounded, as code you use in types needs to pass the _totality checker_, which proves it terminates. (The totality checker requires code to follow certain formats the checker knows how to solve for, otherwise it would solve the halting problem and therefore it could not exist)
I'm not an expert, but yes compile times can get crazy if you're not careful. In theory, the situation is no different from (ab)use of C++ templates, the Rust macro discussed here, and so on. In practice, whereas C and Rust will choke on a 100kloc function, Idris might choke on a 100-liner, depending on what you're doing. Edwin Brady is currently making steady progress on a new compiler--this time written in Idris itself--that's much faster in practice:
https://github.com/edwinb/Idris2
Compile times are already exponential in Haskell. No need to go to Idris for that. The reason is that type checking is exponential even for the simpler type systems in Haskell or OCaml. The trick is to have deeply nested sequences of `let` expressions in the right hand sides, rather than in the bodies.
But in my experience, it's possible but not likely in practice.
Some functional languages have "id id id id id id id id id..." causing exponential compile times. I know F# does, and Haskell did at one point but doesn't any more.
