Thanks! I guess what you are describing looks - from my very limited experience with scala - as a path-dependent type. If I'm right.
I'm actually talking about C# because I'm working in it and I'd like to make some compile-time guarantees if possible. Or at least know how to assure a method that they are getting a list with at least 2 values in it, for example. It may not be worth the effort but it would be nice to know how.
I've got books on DT, idris, and another DT lang, trouble is there's no call for any of this stuff in industry so they get repeatedly pushed to the bottom of the priority stack. Sickening, innit.
I'm actually talking about C# because I'm working in it and I'd like to make some compile-time guarantees if possible. Or at least know how to assure a method that they are getting a list with at least 2 values in it, for example. It may not be worth the effort but it would be nice to know how.
I've got books on DT, idris, and another DT lang, trouble is there's no call for any of this stuff in industry so they get repeatedly pushed to the bottom of the priority stack. Sickening, innit.