4 ms·

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 interest

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?

Tainnor 5y ago
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).

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?

Tainnor 5y ago

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