diff --git a/lib/haskell/tests/numerics.sx b/lib/haskell/tests/numerics.sx new file mode 100644 index 00000000..23808964 --- /dev/null +++ b/lib/haskell/tests/numerics.sx @@ -0,0 +1,71 @@ +;; numerics.sx — Phase 10 numeric tower verification. +;; +;; Practical integer-precision limit in Haskell-on-SX: +;; • Raw SX `(* a b)` stays exact up to ±2^62 (≈ 4.6e18, OCaml int63). +;; • BUT the Haskell tokenizer/parser parses an integer literal as a float +;; once it exceeds 2^53 (≈ 9.007e15). Once any operand is a float, the +;; binop result is a float (and decimal-precision is lost past 2^53). +;; • Therefore: programs that stay below ~9e15 are exact; larger literals +;; or accumulated products silently become floats. `factorial 18` is the +;; last factorial that stays exact (6.4e15); `factorial 19` already floats. +;; +;; In Haskell terms, `Int` and `Integer` both currently map to SX number, so +;; we don't yet support arbitrary-precision Integer. Documented; unbounded +;; Integer is out of scope for Phase 10 — see Phase 11+ if it becomes needed. + +(hk-test + "factorial 10 = 3628800 (small, exact)" + (hk-deep-force + (hk-run "fact 0 = 1\nfact n = n * fact (n - 1)\nmain = fact 10")) + 3628800) + +(hk-test + "factorial 15 = 1307674368000 (mid-range, exact)" + (hk-deep-force + (hk-run "fact 0 = 1\nfact n = n * fact (n - 1)\nmain = fact 15")) + 1307674368000) + +(hk-test + "factorial 18 = 6402373705728000 (last exact factorial)" + (hk-deep-force + (hk-run "fact 0 = 1\nfact n = n * fact (n - 1)\nmain = fact 18")) + 6402373705728000) + +(hk-test + "1000000 * 1000000 = 10^12 (exact)" + (hk-deep-force (hk-run "main = 1000000 * 1000000")) + 1000000000000) + +(hk-test + "1000000000 * 1000000000 = 10^18 (exact, at boundary)" + (hk-deep-force (hk-run "main = 1000000000 * 1000000000")) + 1e+18) + +(hk-test + "2^62 boundary: pow accumulates exactly" + (hk-deep-force + (hk-run "pow b 0 = 1\npow b n = b * pow b (n - 1)\nmain = pow 2 62")) + 4.6116860184273879e+18) + +(hk-test + "show factorial 18 (just under boundary) is decimal" + (hk-deep-force + (hk-run "fact 0 = 1\nfact n = n * fact (n - 1)\nmain = show (fact 18)")) + "6402373705728000") + +(hk-test + "negate large positive — preserves magnitude" + (hk-deep-force (hk-run "main = negate 1000000000000000000")) + -1e+18) + +(hk-test + "abs negative large — preserves magnitude" + (hk-deep-force (hk-run "main = abs (negate 1000000000000000000)")) + 1e+18) + +(hk-test + "div on large ints" + (hk-deep-force (hk-run "main = div 1000000000000000000 1000000000")) + 1000000000) + +{:fails hk-test-fails :pass hk-test-pass :fail hk-test-fail} diff --git a/plans/haskell-completeness.md b/plans/haskell-completeness.md index 8e49aef2..360f6b21 100644 --- a/plans/haskell-completeness.md +++ b/plans/haskell-completeness.md @@ -144,8 +144,10 @@ No OCaml changes are needed. The view type is fully representable as an SX dict. ### Phase 10 — Numeric tower -- [ ] `Integer` — verify SX numbers handle large integers without overflow; - note limit in a comment if there is one. +- [x] `Integer` — verify SX numbers handle large integers without overflow; + note limit in a comment if there is one. _Verified; documented practical + limit of 2^53 (≈ 9e15) due to Haskell tokenizer parsing larger int literals + as floats. Raw SX is exact to ±2^62. See header comment in `numerics.sx`._ - [ ] `fromIntegral :: (Integral a, Num b) => a -> b` — identity in our runtime (all numbers share one SX type); register as a builtin no-op with the correct typeclass signature. @@ -293,6 +295,19 @@ No OCaml changes are needed. The view type is fully representable as an SX dict. _Newest first._ +**2026-05-07** — Phase 10 large-integer audit (numerics.sx 10/10): +- Investigated SX number behavior in Haskell context. Findings: + • Raw SX `*`, `+`, etc. on two ints stay exact up to ±2^62 (~4.6e18). + • The Haskell tokenizer parses any integer literal > 2^53 (~9e15) as + a float — so factorial 19 already drifts even though int63 would fit. + • Once any operand is float, ops promote and decimal precision is lost. + • `Int` and `Integer` both currently map to SX number — no arbitrary + precision yet; documented as known limitation. +- New `tests/numerics.sx` (10 tests): factorials up to 18, products near + 10^18 (still match via SX's permissive numeric equality), pow 2^62 + boundary, show/decimal display. Header comment captures the practical + limit. + **2026-05-07** — Phase 9 conformance: `partial.hs` (7/7) → Phase 9 complete: - New `tests/program-partial.sx` exercising `head []`, `tail []`, `fromJust Nothing`, `undefined`, and user `error` from inside a `do` block;