On: A convenient untruth: Array notation in C is a lie

[kibwen]

A language doesn't need dependent types to make fixed-size arrays of differing size count as incompatible types. Rust does this, for example:

  // error: expected an array with a fixed size of 5 
  // elements, found one with 7 elements
  let x: [i32; 5] = [1,2,3,4,5,6,7];

[pasquinelli → kibwen]

i don't know rust, but i read a bit about fixed size arrays in it and the fact that 32 is the largest fixed size array makes me suspicious that it works like a pair. you can do this without depending on a value, because the length is encoded in the type.

like, you can have a type (a, b), and b can, of course, be of type (a, b), b again having type (a, b), and so on. then you always carry around the length encoded in the type, and it can be checked like above.

ghc has a limit on tuple sizes, and haskell makes no type distinction between [a] based on the number of elements in it, and it isn't dependently typed.

but again i don't know rust.

[kibwen → pasquinelli]

  > i read a bit about fixed size arrays in it and the fact 
  > that 32 is the largest fixed size array

This is exceptionally mistaken, where did you read it? Arrays in Rust top out at the maximum value of a platform-sized pointer, which is either 2^32 or 2^64 depending on platform.

[pasquinelli → kibwen]

"Arrays of sizes from 0 to 32 (inclusive) implement the following traits if the element type allows it:

Clone (only if T: Copy) Debug IntoIterator (implemented for &[T; N] and &mut [T; N]) PartialEq, PartialOrd, Eq, Ord Hash AsRef, AsMut Borrow, BorrowMut Default This limitation on the size N exists because Rust does not yet support code that is generic over the size of an array type. [Foo; 3] and [Bar; 3] are instances of same generic type [T; 3], but [Foo; 3] and [Foo; 5] are entirely different types. As a stopgap, trait implementations are statically generated up to size 32."

from the rust docs. https://doc.rust-lang.org/std/primitive.array.html

i sort of leapt to the conclusion that these traits couldn't be implemented because generically because the type system requires them to be implemented for each size of N, and they provide the first 32 as a nicety. the similarity to the situation with tuples in haskell, (http://stackoverflow.com/questions/2978389/haskell-tuple-siz...), and the fact that rust doesn't have dependent types and so a type couldn't depend on a value, and i just kind of guessed at a possible reason.

[kibwen → pasquinelli]

Ah I see, yes the explanation there is correct. The types exist up to ginormous sizes, but the standard library only implements certain convenience traits for certain sizes (though using newtypes, you can implement those traits yourself for any array size you want). The specific feature we're lacking is type-level numerals, which is on the way towards but not anywhere close to a dependent type system AIUI.