3 ms·

> At the end of the day, you just end up having to code for both the case where the list matches the size requirements of the code you want to call and the case

> At the end of the day, you just end up having to code for both the case where the list matches the size requirements of the code you want to call and the case where it doesn't. I don't follow. If your list is not the right size, your program doesn't compile, period. If it does, you're not using a dependently typed language. Am I missing something?

clhodapp 11y ago
I think you are. I think you are missing the possibility to write a total function of type `List[Int] => Option[List[Int]] @@ MinSize[_5]` (I'm still writing Scala-ish types because that's where I feel comfortable). This gets you into a world where you can deal with your previously-unsized `List` as a sized `List` (either you can map over your `Option` or you can fold the `Some` and `None` cases together by providing some default).
pathsjs 11y ago
It depends on the language. For instance in Scala you can simulate collections of fixed size as in https://github.com/milessabin/shapeless/blob/master/core/src/main/scala/shapeless/sized.scala https://github.com/milessabin/shapeless/blob/master/core/src... Then, at runtime, you can cast an unsized list to a sized list giving - say - a function List[A] => Option[Sized[List[A], N5]] that will fail if the list is not of size 5. From then on you can go on letting the compiler keep track of lengths. Of course, this does not work at all if you have no clue what size your input will have
- clhodapp 11y ago
  I believe that you don't need to know what size your input will have. Rather, you need to know what size the thing you will be calling will need, right?
lomnakkus 11y ago
Yes, you're missing this, I think: When you call a function which takes, say, a list-5, all you need to do is to prove to the compiler that you've checked that the list is indeed of length 5 before you pass it along. The key insight here is that the check may be performed at compile time or runtime as long as the compiler can see that you've performed the check. It can do this e.g. in pattern match clauses. For example in code like case inputList of [a,b,c,d,e] -> branch-A otherwise -> branch-B Idris will automatically have proof that inputList is length 5 in branch-A. Which means you'd be free to call any function which expects list-of-length-5 in branch-A without further ceremony. This will not be the case for branch-B. (And if you think about it... if you didn't allow for runtime checks to satisfy such proof obligations there would essentially no way for any dependently programs to depend on any runtime values at all.) Aside: Another thing which I think has been missed in this entire discussion is that you don't have to actually use List-of-size-N as your type. If you don't actually care about the size of the list in the code you're writing, you're also allowed to just use List-of-any-finite-size as your data type. (Of course this could cause a certain amount of friction if the standard library is all based on List-of-size-N, but it shouldn't be too bad in e.g. Idris.)

clhodapp 11y ago

I think you are. I think you are missing the possibility to write a total function of type `List[Int] => Option[List[Int]] @@ MinSize[_5]` (I'm still writing Scala-ish types because that's where I feel comfortable). This gets you into a world where you can deal with your previously-unsized `List` as a sized `List` (either you can map over your `Option` or you can fold the `Some` and `None` cases together by providing some default).

pathsjs 11y ago

It depends on the language. For instance in Scala you can simulate collections of fixed size as in https://github.com/milessabin/shapeless/blob/master/core/src/main/scala/shapeless/sized.scala https://github.com/milessabin/shapeless/blob/master/core/src... Then, at runtime, you can cast an unsized list to a sized list giving - say - a function List[A] => Option[Sized[List[A], N5]] that will fail if the list is not of size 5. From then on you can go on letting the compiler keep track of lengths. Of course, this does not work at all if you have no clue what size your input will have

clhodapp 11y ago
I believe that you don't need to know what size your input will have. Rather, you need to know what size the thing you will be calling will need, right?

lomnakkus 11y ago

Yes, you're missing this, I think: When you call a function which takes, say, a list-5, all you need to do is to prove to the compiler that you've checked that the list is indeed of length 5 before you pass it along. The key insight here is that the check may be performed at compile time or runtime as long as the compiler can see that you've performed the check. It can do this e.g. in pattern match clauses. For example in code like case inputList of [a,b,c,d,e] -> branch-A otherwise -> branch-B Idris will automatically have proof that inputList is length 5 in branch-A. Which means you'd be free to call any function which expects list-of-length-5 in branch-A without further ceremony. This will not be the case for branch-B. (And if you think about it... if you didn't allow for runtime checks to satisfy such proof obligations there would essentially no way for any dependently programs to depend on any runtime values at all.) Aside: Another thing which I think has been missed in this entire discussion is that you don't have to actually use List-of-size-N as your type. If you don't actually care about the size of the list in the code you're writing, you're also allowed to just use List-of-any-finite-size as your data type. (Of course this could cause a certain amount of friction if the standard library is all based on List-of-size-N, but it shouldn't be too bad in e.g. Idris.)