Puzzled at SRFI-145 noosphere@xxxxxx (04 Nov 2020 18:36 UTC)
Re: Puzzled at SRFI-145 Marc Nieper-Wißkirchen (04 Nov 2020 18:51 UTC)

Puzzled at SRFI-145 noosphere@xxxxxx 04 Nov 2020 18:36 UTC

This question was originally posted to:  https://old.reddit.com/r/scheme/comments/jo0u7i/puzzled_at_srfi145/

I'm relatively new to scheme, so please pardon me if my questions seem naive.

I've been looking at possibly porting SRFI-145 but have run in to a number of issues.

The most glaring one is with the second implementation listed in the SRFI:

(define-library (srfi 145)
  (export assume)
  (import (scheme base))
  (begin
    (define-syntax assume
      (syntax-rules ()
        ((assume obj . _) obj)))))

The SRFI states:

"The reason why this is a faithful implementation is that whenever (assume #f) is invoked, it is an error anyway, so that implementations are allowed to fail catastrophically (in the words of the R7RS), including that they simply return #f."

This may be true, but it seems to make the assume completely useless, because a violated assumption won't halt execution. Moreover, using this implementation would leave the user with a false sense of security, if they thought the assumption would guarantee a halt of execution if it was violated.

For example:

(define (do-if-times-match time1 time2)
  (assume (equal? time1 time2))
  (print "This should only be printed if time1 and time2 are the same"))

(do-if-times-match 'day 'night)
;; => "This should only be printed if time1 and time2 are the same"

You could, of course manually check the return value of assume to make sure it's not #f before proceeding, but if you're going to be your own checks then why are you even using assume in the first place?

The next problem I ran in to was with the first implementation:

(define-library (srfi 145)
  (export assume)
  (import (scheme base))
  (begin
    (define-syntax assume
      (syntax-rules ()
        ((assume expression message ...)
         (or expression
             (fatal-error "invalid assumption" (quote expression) (list message ...))))
        ((assume . _)
         (syntax-error "invalid assume syntax"))))
  (cond-expand
    (debug
     (begin
       (define fatal-error error)))
    (else
     (begin
       (define (fatal-error message . objs)
         (car 0)))))))

The error caused by (car 0) is misleading, as it tells the user nothing about why assumption failed in the first place, and makes it seem like it failed due to the (car 0) itself, while that was just an artificial construct placed there to cause an error and make "the whole code path leading to the invocation of that assume invalid."

If instead of (car 0) the implementer used some other way of signaling an error, I'm not sure why using assume would be any better than using assert.

What am I missing?