:post condition causes compiler error with recur

Question

Michael O'Keefe <michael.p.okeefe@gmail.com> posted on the mailing list an example of code that causes a compiler error only if a :post condition is added.  Here's my slightly modified version:


(defn g
  [xs acc]
  {:pre [(or (nil? xs) (sequential? xs))]
   :post [(number? %)]}
  (if (seq xs)
     (recur (next xs) (+ (first xs) acc))
     acc))


CompilerException java.lang.UnsupportedOperationException: Can only recur from tail position

The work-around is to wrap the body in a loop that simply rebinds the original args.

Answer 1

Comment made by: steveminer@gmail.com

A macro expansion shows that body is placed in a let form to capture the result for later testing with the post condition, but the recur no longer has a proper target. The work-around of using a loop form is easy once you understand what's happening but it's a surprising limitation.

Answer 2

Comment made by: steveminer@gmail.com

Use a local fn* around the body and call it with the original args so that the recur has a proper target. Update: not good enough for handling destructuring. Patch withdrawn.

Answer 3

Comment made by: michael.p.okeefe@gmail.com

Link to the original topic discussion: https://groups.google.com/d/topic/clojure/Wb1Nub6wVUw/discussion

Answer 4

Comment made by: steveminer@gmail.com

Patch withdrawn because it breaks on destructured args.

Answer 5

Comment made by: steveminer@gmail.com

While working on a patch, I came up against a related issue: Should the :pre conditions apply to every recur "call". Originally, I thought the :pre conditions should be checked just once on the initial function call and never during a recur. People on the mailing list pointed out that the recur is semantically like calling the function again so the :pre checks are part of the contract. But no one seemed to want the :post check on every recursion, so the :post would happen only at the end.

That means automatically wrapping a loop (or nested fn* call) around the body is not going to work for the :pre conditions. A fix would have to bring the :pre conditions inside the loop.

Answer 6

_Comment made by: steveminer@gmail.com_

I'm giving up on this bug.  My approach was adding too much complexity to handle an edge case.  I recommend the "loop" work-around to anyone who runs into this problem.


(defn g2
  [xs acc]
  {:pre [(or (nil? xs) (sequential? xs))]
   :post [(number? %)]}
  (loop [xs xs acc acc]
    (if (seq xs)
       (recur (next xs) (+ (first xs) acc))
       acc)))

Answer 7

Comment made by: ambrosebs

Add patch that handles rest arguments and destructuring.

Answer 8

_Comment made by: michael.p.okeefe@gmail.com_

With regard to Steve's question on interpreting :pre, to me I would expect g to act like the case g3 below which uses explicit recursion (which does work and does appear to check the :pre conditions each time and :post condition once):


(defn g3
  [xs acc]
  {:pre [(or (sequential? xs) (nil? xs)) (number? acc)]
   :post [(number? %)]}
  (if (seq xs)
    (g3 (next xs) (+ (first xs) acc))
    acc))

Answer 9

Comment made by: ambrosebs

Patch clj-1475.diff handles destructuring, preconditions and rest arguments

Answer 10

Comment made by: steveminer@gmail.com

The clj-1475.diff patch looks good to me.

Answer 11

Comment made by: alexmiller

Please don't use "patch" as a label - that is the purpose of the Patch field. There is a list of good and bad labels at http://dev.clojure.org/display/community/Creating Tickets

Answer 12

Comment made by: steveminer@gmail.com

More knowledgeable commenters might take a look at CLJ-701 just in case that's applicable to the proposed patch.

Answer 13

Comment made by: hiredman

re clj-701

it is tricky to express loop expression semantics in jvm byte code, so the compiler sort of punts, hoisting expression loops in to anonymous functions that are immediately invoked, closing over whatever is in scope that is required by the loop, this has some problems like those seen in CLJ-701, losing type data which the clojure compiler doesn't track across functions, the additional allocation of function objects (the jit may deal with that pretty well, I am not sure) etc.

where the world of clj-701 and this ticket collide is the patch on this ticket lifts the function body out as a loop expression, which without the patch in clj-701 will have the issues I listed above, but we already have those issues anywhere something that is difficult to express in bytecode as an expression (try and loop) is used as an expression, maybe it doesn't matter, or maybe clj-701 will get fixed in some way to alleviate those issues.

general musings

it seems like one feature people like from asserts is the ability to disable them in production (I have never actually seen someone do that with clojure), assert and :pre/:post have some ability to do that (it may only work at macroexpansion time, I don't recall) since the hoisting of the loop could impact performance it might be nice to have some mechanism to disable it (maybe using the same flag assert does?).

Answer 14

Reference: https://clojure.atlassian.net/browse/CLJ-1475 (reported by steveminer@gmail.com)