Am Mi., 4. Nov. 2020 um 19:37 Uhr schrieb <xxxxxx@mailc.net>:
>
> 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?

This second implementation just demonstrates that the programmer
mustn't rely on that `assume` halts execution (or signals an error).
In a debug setting, a Scheme implementation is highly encouraged to
catch any failed assumption and report that. In an optimizing mode,
however, an implementation may assume that assumption *is* true and
backward propagate the implicit knowledge through the control-flow
graph.

> 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?

(car 0) is only a hack to have something like GCC's
__builtin_unreachable. In a particular implementation, it should be
replaced by something more specific that guides the control-flow
optimization (by telling that this point will never be reached).