Compile-time checks is what's implied in virtually all these conversations.

Does that check run at compile time?

▲ tmtvl 4 days ago | parent [-]

If I define a function foo which takes an (Array Float (10 5)) and then define a function bar which uses the result of calling foo with an (Array String (3 3)) then SBCL will print a warning. If I don't redefine foo and call bar with such an array then a condition will be raised. It's not quite the same as, say Rust's 'thing just won't compile', but that's due to the interactive nature of Common Lisp (I believe someone called it the difference between a living language and a dead language (though the conventional meaning of living language and dead language in programming is a bit different)).

▲ chongli 4 days ago | parent [-]

Can you replace 10 5 and 3 3 with variable names and still get the warning without first calling the function?

▲ tmtvl 4 days ago | parent [-]

No. You can replace them with asterisks to mean 'any length is fine', but you can't at compile time check something that's only known at runtime (granted, you could see that it can't match if the variables are, for example, an (Integer 1 10) and an (Integer 75 100)). Something you can do with variables is:

  (defvar *example-dimension* 20)

  (deftype Example-Array (element-type minor-dimension)
    `(Array ,element-type (,*example-dimension* ,minor-dimension)))

...and then you can declare variables to be something like, say, (Example-Array Boolean 5) and have it expand to (Array Boolean (20 5)). But the type declaration needs to be of the form (Array &optional element-type dimensions) where dimensions can be any of the following:

- An asterisk, which means anything goes.

- A number, which means the array needs to have that many dimensions (so an (Array Fixnum 2) is a 2-dimensional array of fixnums).

- A list of numbers, asterisks, or a combination of the two, where an asterisk means 'this dimension can be anything' and the numbers mean exactly what you would expect.

Maybe something like that would be possible with Coalton, but I haven't played around a lot with that yet.

	▲	chongli 3 days ago \| parent [-]
		Dependent types can do this. This is information that can be known at compile time by means of a proof that the values are what they should be (or within certain bounds) through the entire call chain.