Difference between revisions of "Bounds checking"

From HaskellWiki
Jump to: navigation, search
m (Reverted edits by Tomjaguarpaw (talk) to last revision by DonStewart)
m (Could use some more content...)
 
Line 5: Line 5:
 
clarity of code, on well-supported programming languages.  
 
clarity of code, on well-supported programming languages.  
  
That does not have to be the case. [These exampels] show non-trivial
+
That does not have to be the case. [These examples] show non-trivial
 
examples involving native Haskell arrays, index computations, and general
 
examples involving native Haskell arrays, index computations, and general
 
recursion. All arrays indexing operations are statically guaranteed to be safe
 
recursion. All arrays indexing operations are statically guaranteed to be safe
Line 17: Line 17:
  
 
[[Category:Idioms]]
 
[[Category:Idioms]]
 +
[[Category:Pages under construction]]

Latest revision as of 01:33, 26 April 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 examples] 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