Hale.Base — Haskell base for Lean 4

API Reference: Hale.Base

Re-exports all Base sub-modules.

Design Philosophy (Concurrency)

All concurrency primitives are promise-based, not OS-thread-based. Blocking operations return BaseIO (Task a) rather than suspending an OS thread. This enables scaling to millions of concurrent “threads” on Lean’s task-pool scheduler.

Cancellation is cooperative: killThread sets a CancellationToken rather than throwing an asynchronous exception. CPU-bound threads that never check the token will not be interrupted.

Foundational

• Void — Data.Void
• Function — Data.Function
• Newtype — Data.Monoid / Data.Semigroup

Core Abstractions

• Bifunctor — Data.Bifunctor
• Contravariant — Data.Functor.Contravariant
• Const — Data.Functor.Const
• Identity — Data.Functor.Identity
• Compose — Data.Functor.Compose
• Category — Control.Category

Data Structures

• NonEmpty — Data.List.NonEmpty
• Either — Data.Either
• Ord — Data.Ord
• Tuple — Data.Tuple + Prelude

Traversals

• Foldable — Data.Foldable
• Traversable — Data.Traversable

Numeric Types

• Ratio — Data.Ratio
• Complex — Data.Complex
• Fixed — Data.Fixed

Advanced Abstractions

• Arrow — Control.Arrow

Concurrency

• Concurrent — Control.Concurrent
• MVar — Control.Concurrent.MVar
• Chan — Control.Concurrent.Chan
• QSem — Control.Concurrent.QSem
• QSemN — Control.Concurrent.QSemN