Skip to content

2015 001 Correction to ListPair

John Reppy edited this page Aug 3, 2015 · 7 revisions

Proposal 2015-001

Correction to the ListPair module

Author: John Reppy
Last revised: August 3, 2015
Status: proposed


There is a problem with the way that the current Basis Library specification describes some of the ListPair operations with respect to the precedence of the UnequalLengths exception. For example, consider the expression

    ListPair.appEq (fn _ => raise Fail "fail") ([], [1])

The Basis Library specification states that it is equivalent to

   List.app (fn _ => raise Fail "fail") (ListPair.zipEq ([], [1])

but a direct (and efficient) implementation of ListPair.app will raise the Fail exception in the first expression, whereas the second expression raises the UnequalLengths exception.

I propose that the Basis Library Specification be amended by adding the qualification "assuming that 'f' is pure and terminates" to the statements of equivalence.


History

  • [2015-08-03] Proposed