Difference between revisions of "Bounds checking"

From HaskellWiki
Jump to: navigation, search
(Deleting page that hasn't been updated for over 10 years)
m (Reverted edits by Tomjaguarpaw (talk) to last revision by DonStewart)
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]]

Revision as of 15:19, 6 February 2021

"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."

Eliminating Array Bound Checking through Non-dependent types