This attempt at a strict foldl:
{-# TERMINATING #-}
foldl₁ : {A B : Set} → (B → A → B) → B → List A → B
foldl₁ f x [] = x
foldl₁ f x (x₁ ∷ xs) = primForce (f x x₁) (foldl₁ f) xs
normalizes correctly in holes and so forth. But it gives incorrect results when compiled, seemingly returning the result of the first function application while discarding the recursive call.
This alternate definition works correctly (and passes termination checking):
foldl₂ : {A B : Set} → (B → A → B) → B → List A → B
foldl₂ f x [] = x
foldl₂ f x (x₁ ∷ xs) = primForce (f x x₁) (λ acc → foldl₂ f acc xs)
This is with Agda 2.7.0.1 and GHC 9.6.6 (and at least some older versions).
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4