Difference between revisions of "Bounds checking"
Jump to navigation
Jump to search
DonStewart (talk | contribs) (the non-dependently typed bounds checking example) |
Tomjaguarpaw (talk | contribs) (Deleting page that hasn't been updated for over 10 years) |
||
| Line 1: | Line 1: | ||
| − | "There is a view that in order to gain static assurances such as an array index |
||
| − | being always in range or tail being applied to a non-empty list, we must give |
||
| − | up on something significant: on data structures such as arrays (to be replaced |
||
| − | with nested tuples), on general recursion, on annotation-free programming, on |
||
| − | clarity of code, on well-supported programming languages. |
||
| − | |||
| − | That does not have to be the case. [These exampels] show non-trivial |
||
| − | examples involving native Haskell arrays, index computations, and general |
||
| − | recursion. All arrays indexing operations are statically guaranteed to be safe |
||
| − | -- and so we can safely use an efficient unsafeAt provided by GHC seemingly for |
||
| − | that purpose. The code is efficient; the static assurances cost us no run-time |
||
| − | overhead. The example uses only Haskell98 + higher-ranked types. No new type |
||
| − | classes are introduced. The safety is based on: Haskell type system, quantified |
||
| − | type variables, and a compact general-purpose trusted kernel." |
||
| − | |||
| − | [http://okmij.org/ftp/Haskell/types.html#branding Eliminating Array Bound Checking through Non-dependent types] |
||
| − | |||
| − | [[Category:Idioms]] |
||