Automatic detection of domain for dependent type function in Idris
|Added at||2016-12-25 16:12|
Idris language tutorial has simple and understandable example of the idea of Dependent Types: http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#first-class-types
Here is the code:
I decided to spend more time on this example. What bothers me in
Of course, I understand, this is not possible in general case. Such compiler tricks require my function
So I started with next implementation: I just made
Well, it doesn't really solve my problem because I still need to call this function in the next way:
But I read in tutorial about
And it works for lists!
But doesn't work for single value :(
Can someone explain is it actually possible to achieve my goal in such injective function usages currently? I watched this short video about proving something is injective: https://www.youtube.com/watch?v=7Ml8u7DFgAk
But I don't understand how I can use such proofs in my example. If this is not possible what is the best way to write such functions?