Sure, I wasn't doubting that you can prove anything in Idris or Coq or ... – same as you can write every program in any Turing complete language (not 100% strictly true because of non-functional requirements, but you get what I mean).
But in terms of practical developments, these "restrictions" can matter. Especially when you have specific maintenance concerns. And I'm talking more about programming than theorem proving (Idris is, after all, more geared towards the former than the latter unlike e.g. Coq or Lean).
I've had a problem in the back of my head for a while and I knew it would probably be a bit cumbersome to do in Haskell (although maybe with some advanced extensions it's possible?). I thought that dependent types might solve that problem but I yet don't see a way how I could do that, at least in Idris (possibly I'm missing out on some very obvious way). I think I'd really need subtyping to make it work in a non-cumbersome way. (Or else, possibly some code generation for the boilerplate part.)
That’s interesting. I have never heard of a problem that could be solved in a sub-typed language but not in a Dependently Typed language. I am honestly interested. Perhaps give an example?
It's not that you can't solve it, obviously. It's about the elegance of the approach.
The context is a mathematical problem solver. Mathematical terms form hierarchies (possibly not a single one), and certain operations only make sense for certain types of terms (e.g. inverting a matrix), while others apply to all terms (e.g. simplifying an expression). I want to be able to verify this at compile time and at the same time, the function signatures should be "easy" enough that operations can be composed through operators (i.e. manually passing proof terms probably wouldn't work as well).
In a language like Haskell, I could probably use wrapper types, e.g.
data Matrix = ...
data Integral = ...
...
data Term = MatrixT Matrix | IntegralT Integral | ...
but that's cumbersome especially if you have lots of types of terms.
I'm thinking that in Idris, maybe I could do something like:
data TermType = MatrixT Nat Nat a | IntegralT | ...
data Term : TermType -> Type where
Matrix : Vect n (Vect m a) -> Term (MatrixT n m a)
Integral : Term -> Term Integral T
which would probably allow me to specifically write functions that only work on matrices (or on square matrices) etc., but it still only gives me one level of hierarchy... in case I find out that I need to group some terms together for a particular operation, I would probably be out of luck.
This is all based on work that I previously did, but where all these checks did unfortunately not happen at compile time, so every operation needed to have explicit runtime type checks (this was in a language with subtyping though).
But in terms of practical developments, these "restrictions" can matter. Especially when you have specific maintenance concerns. And I'm talking more about programming than theorem proving (Idris is, after all, more geared towards the former than the latter unlike e.g. Coq or Lean).
I've had a problem in the back of my head for a while and I knew it would probably be a bit cumbersome to do in Haskell (although maybe with some advanced extensions it's possible?). I thought that dependent types might solve that problem but I yet don't see a way how I could do that, at least in Idris (possibly I'm missing out on some very obvious way). I think I'd really need subtyping to make it work in a non-cumbersome way. (Or else, possibly some code generation for the boilerplate part.)