Awesome! My only experience with it is from messing around with Idris, here's the relevant section in the docs - the "holes" described in the section preceding are another really cool idea. Idris is just pretty cool in general, and worth your time even if you never deploy any code
I do think it's a useful idea, but the Wiki article notes it does complicate type checking. It can slow the process, and lead to more complicated situations, including those which may be undecidable - potentially a step backwards in terms of practical benefit if you hit that case.
In general, though, I agree with you, I think moving that check to the type level is a good idea. If I append to an array, it actually, conceptually, is part of the "type" of the return value that the length of my array is greater than the original length (by exactly one). Seems useful to be able to specify that in the definition, much like it's useful to define any types at all.
I'd be curious to see if you come up with anything cool with this feature, or work out a way to approximate it with TS!
For further actions, you may consider blocking this person and/or reporting abuse
We're a place where coders share, stay up-to-date and grow their careers.
Awesome! My only experience with it is from messing around with Idris, here's the relevant section in the docs - the "holes" described in the section preceding are another really cool idea. Idris is just pretty cool in general, and worth your time even if you never deploy any code
I do think it's a useful idea, but the Wiki article notes it does complicate type checking. It can slow the process, and lead to more complicated situations, including those which may be undecidable - potentially a step backwards in terms of practical benefit if you hit that case.
In general, though, I agree with you, I think moving that check to the type level is a good idea. If I append to an array, it actually, conceptually, is part of the "type" of the return value that the length of my array is greater than the original length (by exactly one). Seems useful to be able to specify that in the definition, much like it's useful to define any types at all.
I'd be curious to see if you come up with anything cool with this feature, or work out a way to approximate it with TS!