Add [force e] strict-normalization combinator (eigentrust pitfall #11)

racket/prologos/driver.rkt

@@ -232,6 +232,7 @@
     [(expr-pair a b) (or (contains-unsupported-qtt? a) (contains-unsupported-qtt? b))]
     [(expr-fst e) (contains-unsupported-qtt? e)]
     [(expr-snd e) (contains-unsupported-qtt? e)]
+    [(expr-force e) (contains-unsupported-qtt? e)]
     [(expr-ann e t) (or (contains-unsupported-qtt? e) (contains-unsupported-qtt? t))]
     [(expr-suc e) (contains-unsupported-qtt? e)]
     [(expr-natrec m b s t) (or (contains-unsupported-qtt? m) (contains-unsupported-qtt? b)
@@ -346,6 +347,7 @@
      (expr-pair (rewrite-spec a) (rewrite-spec b))]
     [(expr-fst x) (expr-fst (rewrite-spec x))]
     [(expr-snd x) (expr-snd (rewrite-spec x))]
+    [(expr-force x) (expr-force (rewrite-spec x))]
     [(expr-ann x t) (expr-ann (rewrite-spec x) (rewrite-spec t))]
     [(expr-suc x) (expr-suc (rewrite-spec x))]
     [(expr-natrec m b s t)

racket/prologos/effect-ordering.rkt

@@ -68,6 +68,7 @@
        [(expr-pair fst snd) (append (fv-expr fst) (fv-expr snd))]
        [(expr-fst e) (fv-expr e)]
        [(expr-snd e) (fv-expr e)]
+       [(expr-force e) (fv-expr e)]
        [(expr-ann term _type) (fv-expr term)]
        [(expr-suc pred) (fv-expr pred)]
 

racket/prologos/elaborator.rkt

@@ -1022,6 +1022,11 @@
      (let ([e1 (elaborate e env depth)])
        (if (prologos-error? e1) e1 (expr-snd e1)))]
 
+    ;; Force (strict normalization)
+    [(surf-force e loc)
+     (let ([e1 (elaborate e env depth)])
+       (if (prologos-error? e1) e1 (expr-force e1)))]
+
     ;; Annotation: (the T e) -> ann(elab-e, elab-T)
     [(surf-ann type term loc)
      (let ([t (elaborate type env depth)]

racket/prologos/macros.rkt

@@ -8853,6 +8853,8 @@
      (surf-fst (expand-expression e) loc)]
     [(surf-snd e loc)
      (surf-snd (expand-expression e) loc)]
+    [(surf-force e loc)
+     (surf-force (expand-expression e) loc)]
     [(surf-suc e loc)
      (surf-suc (expand-expression e) loc)]
     [(surf-pi binder body loc)

racket/prologos/parser.rkt

@@ -932,6 +932,12 @@
             (let ([e (parse-datum (car args))])
               (if (prologos-error? e) e (surf-snd e loc))))]
 
+       ;; (force e) — strict normalization combinator
+       [(force)
+        (or (check-arity 'force args 1 loc)
+            (let ([e (parse-datum (car args))])
+              (if (prologos-error? e) e (surf-force e loc))))]
+
        ;; (boolrec motive true-case false-case target)
        ;; Constant motive shorthand: if motive is not (fn ...) or (the ...),
        ;; treat it as a constant return type and wrap:

racket/prologos/pnet-serialize.rkt

@@ -196,6 +196,7 @@
   ;; --- One-arg ---
   (reg1! expr-bvar 0) (reg1! expr-fvar 'x) (reg1! expr-suc (expr-zero))
   (reg1! expr-nat-val 0) (reg1! expr-fst (expr-unit)) (reg1! expr-snd (expr-unit))
+  (reg1! expr-force (expr-unit))
   (reg1! expr-Type (lzero)) (reg1! expr-typed-hole (expr-Nat))
   (reg1! expr-int 0) (reg1! expr-rat 1/2)
   (reg1! expr-char #\a) (reg1! expr-string "")

racket/prologos/pretty-print.rkt

@@ -184,6 +184,9 @@
     [(expr-fst e1) (format "[fst ~a]" (pp-expr e1 names))]
     [(expr-snd e1) (format "[snd ~a]" (pp-expr e1 names))]
 
+    ;; Force (strict normalization)
+    [(expr-force e1) (format "[force ~a]" (pp-expr e1 names))]
+
     ;; Annotation
     [(expr-ann term type)
      (format "[the ~a ~a]" (pp-expr type names) (pp-expr term names))]
@@ -914,6 +917,7 @@
     [(expr-pair e1 e2) (or (uses-bvar0? e1) (uses-bvar0? e2))]
     [(expr-fst e1) (uses-bvar0? e1)]
     [(expr-snd e1) (uses-bvar0? e1)]
+    [(expr-force e1) (uses-bvar0? e1)]
     [(expr-ann term type) (or (uses-bvar0? term) (uses-bvar0? type))]
     [(expr-Eq t e1 e2) (or (uses-bvar0? t) (uses-bvar0? e1) (uses-bvar0? e2))]
     [(expr-boolrec m tc fc t) (or (uses-bvar0? m) (uses-bvar0? tc) (uses-bvar0? fc) (uses-bvar0? t))]

racket/prologos/qtt.rkt

@@ -329,6 +329,14 @@
             [_ (tu-error)])]
          [_ (tu-error)]))]
 
+    ;; ---- force (strict normalization) ----
+    ;; [force e] is QTT-transparent: same type and same usage as e.
+    ;; The body is evaluated exactly once (whnf reduces force(e) to
+    ;; nf(e) and erases the wrapper), so usage equals the inner usage.
+    ;; This preserves linearity for linear (m1) values: a force around
+    ;; a linear value still consumes it exactly once.
+    [(expr-force e1) (inferQ ctx e1)]
+
     ;; ---- natrec ----
     ;; Usage = U_target + U_base + U_step (motive is type-level)
     [(expr-natrec mot base step target)

racket/prologos/reduction.rkt

@@ -1415,6 +1415,13 @@
     [(expr-fst (expr-pair e1 _)) (whnf e1)]
     [(expr-snd (expr-pair _ e2)) (whnf e2)]
 
+    ;; Force: [force e] — fully normalize e (deep, not just WHNF) and return
+    ;; the NF as a WHNF term. The force wrapper itself is eliminated. Breaks
+    ;; lazy-argument chains in deep iteration whose intermediate terms differ
+    ;; bit-for-bit (e.g., a per-iterate Posit32 update), where re-reduction
+    ;; would otherwise be O(k^2) in the iteration count.
+    [(expr-force e1) (nf e1)]
+
     ;; Iota reduction for natrec — native nat-val (Idris 2 model)
     [(expr-natrec _ base _ (expr-nat-val n)) #:when (= n 0) (whnf base)]
     [(expr-natrec mot base step (expr-nat-val n)) #:when (> n 0)
@@ -3243,6 +3250,9 @@
     ;; Projection that didn't reduce (neutral)
     [(expr-fst e1) (expr-fst (nf e1))]
     [(expr-snd e1) (expr-snd (nf e1))]
+    ;; Force should normally be eliminated by whnf, but in stuck-NF
+    ;; positions we recurse into the argument to ensure NF.
+    [(expr-force e1) (nf e1)]
 
     ;; Annotation erasure (shouldn't usually appear in WHNF, but handle it)
     [(expr-ann e1 _) (nf e1)]

racket/prologos/substitution.rkt

@@ -66,6 +66,7 @@
      (expr-pair (shift delta cutoff e1) (shift delta cutoff e2))]
     [(expr-fst e1) (expr-fst (shift delta cutoff e1))]
     [(expr-snd e1) (expr-snd (shift delta cutoff e1))]
+    [(expr-force e1) (expr-force (shift delta cutoff e1))]
     [(expr-ann e1 e2)
      (expr-ann (shift delta cutoff e1) (shift delta cutoff e2))]
     [(expr-Eq t e1 e2)
@@ -525,6 +526,7 @@
      (expr-pair (subst k s e1) (subst k s e2))]
     [(expr-fst e1) (expr-fst (subst k s e1))]
     [(expr-snd e1) (expr-snd (subst k s e1))]
+    [(expr-force e1) (expr-force (subst k s e1))]
     [(expr-ann e1 e2)
      (expr-ann (subst k s e1) (subst k s e2))]
     [(expr-Eq t e1 e2)

racket/prologos/surface-syntax.rkt

@@ -44,6 +44,7 @@
  (struct-out surf-pair)
  (struct-out surf-fst)
  (struct-out surf-snd)
+ (struct-out surf-force)
  (struct-out surf-ann)
  (struct-out surf-refl)
  (struct-out surf-eq)
@@ -461,6 +462,11 @@
 (struct surf-fst (expr srcloc) #:transparent)
 (struct surf-snd (expr srcloc) #:transparent)
 
+;; Force: [force e] — strict normalization combinator (surface form).
+;; Type identity, runtime forces full NF of the argument before
+;; returning. Lets users break lazy-argument chains in deep iteration.
+(struct surf-force (expr srcloc) #:transparent)
+
 ;; Type annotation: (the T e)
 (struct surf-ann (type term srcloc) #:transparent)
 

racket/prologos/syntax.rkt

@@ -40,6 +40,7 @@
  (struct-out expr-pair)
  (struct-out expr-fst)
  (struct-out expr-snd)
+ (struct-out expr-force)
  (struct-out expr-refl)
  (struct-out expr-ann)
  (struct-out expr-natrec)
@@ -332,6 +333,14 @@
 (struct expr-fst (expr) #:transparent)
 (struct expr-snd (expr) #:transparent)
 
+;; Force: [force e] — strict normalization combinator. Operationally,
+;; whnf(force(e)) = nf(e). Typing and QTT usage are identity (force is
+;; transparent for the type system; runtime is the only behavioral
+;; change). Useful for breaking lazy-argument chains in deep iteration
+;; whose intermediate terms differ bit-for-bit (e.g., a per-iterate
+;; Posit32 update).
+(struct expr-force (expr) #:transparent)
+
 ;; Equality introduction
 (struct expr-refl () #:transparent)
 
@@ -1048,7 +1057,7 @@
   (or (expr-bvar? x) (expr-fvar? x)
       (expr-zero? x) (expr-suc? x) (expr-nat-val? x)
       (expr-lam? x) (expr-app? x)
-      (expr-pair? x) (expr-fst? x) (expr-snd? x)
+      (expr-pair? x) (expr-fst? x) (expr-snd? x) (expr-force? x)
       (expr-refl? x) (expr-ann? x)
       (expr-natrec? x) (expr-J? x)
       (expr-Type? x) (expr-Nat? x)