------------------------------------------------------------------------ -- The Agda standard library -- -- Strict combinators (i.e. that use call-by-value) ------------------------------------------------------------------------ -- The contents of this module is also accessible via the `Function` -- module. {-# OPTIONS --cubical-compatible --safe #-} module Function.Strict where open import Agda.Builtin.Equality using (_≡_) open import Function.Base using (flip) open import Level using (Level) private variable a b : Level A B : Set a infixl 0 _!|>_ _!|>′_ infixr -1 _$!_ _$!′_ ------------------------------------------------------------------------ -- Dependent combinators -- These are functions whose output has a type that depends on the -- value of the input to the function. open import Agda.Builtin.Strict public renaming ( primForce to force ; primForceLemma to force-≡ ) -- Application _$!_ : ∀ {A : Set a} {B : A → Set b} → ((x : A) → B x) → ((x : A) → B x) f $! x = force x f -- Flipped application _!|>_ : ∀ {A : Set a} {B : A → Set b} → (a : A) → (∀ a → B a) → B a _!|>_ = flip _$!_ ------------------------------------------------------------------------ -- Non-dependent combinators -- Any of the above operations for dependent functions will also work -- for non-dependent functions but sometimes Agda has difficulty -- inferring the non-dependency. Primed (′ = \prime) versions of the -- operations are therefore provided below that sometimes have better -- inference properties. seq : A → B → B seq a b = force a (λ _ → b) seq-≡ : (a : A) (b : B) → seq a b ≡ b seq-≡ a b = force-≡ a (λ _ → b) force′ : A → (A → B) → B force′ = force force′-≡ : (a : A) (f : A → B) → force′ a f ≡ f a force′-≡ = force-≡ -- Application _$!′_ : (A → B) → (A → B) _$!′_ = _$!_ -- Flipped application _!|>′_ : A → (A → B) → B _!|>′_ = _!|>_