codepad
[
create a new paste
]
login
|
about
Language:
C
C++
D
Haskell
Lua
OCaml
PHP
Perl
Plain Text
Python
Ruby
Scheme
Tcl
staload _ = "prelude/DATS/array.dats" fun getitem{n,m:nat}(arr : array(int, n) , length : int(n), index : int m) : int = (* This is an ML-style comment, which is similar to C-style comments except that they can be nested arbitrarily (* like this *) The first thing we do is declare compile-time variables that the dependent types refer to, the natural numbers n and m. These refer to the size of the list, and the index, respectively. {n,m:nat} is the same as {n,m:int | n >= 0 && m >= 0} Arguably we should be saying this as {n,m:nat | n > m >= 0}, but perhaps that's getting ahead of ourselves. Besides, the array type already does that. a value is of type array(X, Y) if its contents are of type X, and it is of length Y array(int, nat(n)) says: the array has some non-negative length, and only contains integers length: nat(n) says: length is a natural number value n, which is the same as the length of the array Because the types have been declared this way, the code will fail to typecheck (at compile time) if these relations are not true. The compiler's job is to verify, everywhere this function is called, that the value passed for the length parameter is the same as the allocated size of the list. If the compiler can't prove this, then the program fails to typecheck. in short, we know at _compile time_ a value "n" which is the length of the array and we know, at _run time_, a value "length", which is also the length of the array. The compiler guarantees to us that length == n, and moreover it is aware of this fact itself, so that if we check things against length, it knows that it can do the same checks against n. This means that we can inspect the value "index" to make sure it will not go out of bounds, and when we do that, we also satisfy the compiler that we have done so. *) (* The compiler would complain if there was ever a value for which this was not true, and we forgot to check it *) if index < length then arr[index] else ~1 (* -1, error *) (* erm ...*) implement main () = let (* def main(): *) val A = array $arrsz{int}(2, 1, ~20, 900, 123, 2, 12) (* A = [2, 1, -20, 900, 123, 2, 12] *) in ( printf("%d\n", @(getitem(A, 7, 0))) (* print "%d\n" % (getitem(A, 7, 0),) *) ) end
Private
[
?
]
Run code
Submit