Skip to content

Archive Survey Haskell

Jump to bottom
enumeratio edited this page Sep 29, 2026 · 1 revision

Survey — Haskell ecosystem (typeclasses as a capability model)

Carried over from the earlier enumeratio. Written against the old Postgres base_trait/base_category registries, which are gone, but the capability ladder it argues for (Universe → Finite → rankable → graded → sampleable) is exactly the shape @enumeratio/structures and the Plausible capability model now build in compute-engine terms — see Structures and Speculative Plausible. Read the steal/avoid verdicts against those, not against the retired registries.

One of the ecosystem surveys (../spikes.md → Ecosystem surveys). Feeds base_trait / base_category and the enumeration-capability traits (../backlog.md #8). Cross-checks Haskell against the (still unwritten) Sage / Rust / Lean surveys for a convergent capability vocabulary — the Sage/Rust/Lean columns here are drawn from those systems directly (the brief's "your knowledge"), to be reconciled when those docs land.

TL;DR

  • Steal: the capability ladder — Universe (lazily enumerable) → Finite (has cardinality) → rankable (unrank) → graded (size-stratified) → sampleable (uniform random). It's the shape backlog #8 is reaching for, and it lands cleanly as base_trait rows closed over implies. Steal feat's Finite { fCard, fIndex } as the canonical (cardinality, unrank) bundle, size-stratified enumeration (feat [Finite] / LeanCheck tiers :: a) as the model for graded, and feat's uniform (sample a bounded prefix) as the answer to #8's infinite/unknown-count case.
  • Avoid: the Num monolith (a god-class you can't join without paying for everything) and baking cost into a capability's identity. Don't chase higher-kinded / Functor-style machinery — it's elegant and it doesn't map to a concrete-carrier data catalog.
  • Validated: enumeratio's capability-as-data (base_trait rows + implies closure) is exactly what Haskell had to bolt on with ConstraintKinds/Dict. We get for free — and can re-slice as a view — what Haskell bakes into base at compile time and pays for at every migration (AMP/FTP).

1. Capability vs representation: class vs instance

Haskell's core separation is typeclass = capability, instance = a representation claiming it:

class Eq a where (==) :: a -> a -> Bool     -- capability: "can be compared"
instance Eq Bool where ...                  -- Bool is one representation that has it

The class is an interface over an abstract type; an instance binds it to a concrete type. A function constrains what it needs (sort :: Ord a => [a] -> [a]) and stays blind to representation. This is the same split enumeratio draws between a capability a collection HAS (base_trait) and the carrier/collection that realizes it.

Entailment is a DAG. Superclass constraints declare that one capability presupposes another:

class Eq a       => Ord a         -- can-order  ⇒ can-equate
class Num a      => Fractional a  -- has-division ⇒ is-a-Num
class Universe a => Finite a      -- is-finite  ⇒ is-enumerable

This is base_trait.implies / Rust supertraits / Sage supercategories — the realizer comment already names the parallel. One refinement enumeratio has over Haskell: Haskell has a single edge type (superclass), and uses one class to mean both "capability" (Foldable = can fold) and "algebraic structure with laws" (Monoid = is a monoid). enumeratio splits that into three typed edges — base_trait.implies (capability ⇒ capability), base_category.parents (structure ⇒ super- structure), base_category.requires (structure ⇒ its axiom-traits). Keep that finer typing; it's the thing Sage half-has and Haskell lacks.

Constraints as first-class values. ConstraintKinds promotes a constraint to the Constraint kind, and the constraints package reifies it as data: Dict :: p => Dict p captures a dictionary; (:-) :: Constraint -> Constraint -> Type is entailment as a value you can pass and compose. This is Haskell straining to make its class system into data. enumeratio already lives on the other side of that line — a trait is a row, implies is a column, the closure is a recursive view. The takeaway isn't a feature to build; it's a validation: keep deriving assignments from the registries and closing over implies (as base_collection_trait does) rather than hand-wiring — the data form is the whole advantage.

Laziness → infinite enumeration. universe :: [a] and [1..] are lazy: an enumeration can be infinite and still a value, consumed prefix-by-prefix. Crucially, finiteness is a separate capability you assert only when the list ends (Finite subclass), and cardinality lives on Finite, not on Universe. You can enumerate without being able to count. That is precisely enumeratio's unbounded flag → finite trait, and precisely the support-function taxonomy #8 wants: the enumeration is always available; counting and random access are additional, declarable capabilities.

2. The numeric hierarchy — a cautionary tale

Num a is base's numeric root, and it's the community's standard example of a god-class: to be Num you must supply (+), (*), abs, signum, fromInteger, negate all at once, with Eq/Show historically dragged in as superclasses. There is no way to be additive-only, or a semiring, or a ring-without-signum. The hierarchy is "convenient but not principled": no stated laws (associativity is assumed, never declared), superfluous superclasses, and too coarse to express real algebra.

The fixes — numeric-prelude (Algebra.Additive → Ring → Field …), Kmett's algebra, numhask, the semirings package — all do the same thing: shatter the monolith into fine-grained, composable classes with mathematical names, so you claim exactly the structure you have. (PureScript rebased its Prelude on Semiring for this reason.)

Two lessons land on enumeratio:

  • Fine-grained beats monolithic (the algebra/operations lattice, design/ structure lattice magma→field, already leans this way). Don't grow a "fully enumerable" mega-trait; keep the rungs separate and let implies compose them.
  • Retrofit is the real cost. The Applicative-Monad and Foldable-Traversable Proposals (AMP/FTP) took years because Haskell's superclass DAG is compiled into base and every instance breaks when it moves. enumeratio's implies closure is a view over rows — re-slicing the hierarchy is a query, not an ecosystem migration. That asymmetry is the strongest argument for keeping the capability graph data-driven (per the registry-is-data-driven principle), never hardcoded in engine code.

3. Enumeration & countability capabilities (the meat for #8)

Haskell has several independent takes on "enumerate a type," and their union is a clean capability ladder.

Enum (base). toEnum :: Int -> a / fromEnum :: a -> Int / enumFrom :: a -> [a]. A weak, partial rank/unrank plus lazy successor-enumeration — but lawless and Int-bounded, so not a serious model. Its lesson is only that succ/toEnum (next/unrank) are recognized as distinct capabilities.

universe package — the countability split, stated as two classes:

class Universe a where universe :: [a]              -- "recursively enumerable" (may be infinite)
class Universe a => Finite a where
  universeF   :: [a]
  cardinality :: Tagged a Natural                   -- "the enumeration eventually ends"

Universe = can list them lazily; Finite = and the list ends, with a known count. The superclass edge is the implies. This is the cleanest statement of enumeratio's unbounded → finite distinction anywhere in the survey set.

feat (testing-feat) — the closest analog to enumeratio's engine. It represents an enumeration as a size-indexed sequence of finite, indexable parts:

data Finite a   = Finite { fCard :: Index, fIndex :: Index -> a }   -- Index = Integer
data Enumerate a = Enumerate { ... :: [Finite a] }                  -- one Finite per SIZE (constructor count)

Finite's two fields are enumeratio's (cardinality, unrank) pair — fCard is cardinality, fIndex :: Index -> a is unrank. Enumerate as a list of Finite parts, one per size is exactly grading: partition the enumeration into finite, independently-counted, independently-indexable strata. The algebra is closed under sum/product/bijection — i.e. you build a composite carrier's enumeration from its factors' enumerations, and a bijection transports one enumeration onto another (this is enumeratio's order-isomorphic sibling collections; see §6). Test.Feat.Access adds index (global unrank across parts) and uniform :: Enumerate a -> Int -> Gen a — uniform random selection from a bounded prefix, which is the exact answer to #8's "define the infinite / unknown-count behaviour (sample a bounded prefix)."

LeanCheck — same grading idea, minimal surface: tiers :: a, a (possibly infinite) list of finite sublists of same-and-increasing size. tiers :: a is a graded enumeration. Confirms the shape is convergent, not a feat quirk.

QuickCheck Arbitrary / feat uniform — the sampleable rung: arbitrary :: Gen a. Note the split QuickCheck vs SmallCheck/feat/LeanCheck makes explicit — random sampling and exhaustive enumeration are different capabilities over the same set, and feat derives both from one Enumerate (uniform = draw an index in [0, card), unrank). That is verbatim #8's plan: "draw a uniform rank in [0, cardinality) and unrank."

4. Number / combinatorics libraries (quick)

  • arithmoi — efficient number theory. The relevant design point is the UniqueFactorisation typeclass (factorise, isPrime, factorBack): factorization modeled as a capability, and factorBack (recompose from prime powers) is its inverse — a capability + its inverse map, i.e. a bijection between an integer and its prime-exponent vector. Direct grist for the number-theory-gradings carrier (naturals-as-prime-exponent-vector) and for modeling factorization as a base_map with an inverse.
  • combinat — generate/count/manipulate partitions, compositions, permutations, Young tableaux, lattice paths, trees. The nearest ecosystem to enumeratio's actual objects. Not a capability-model reference (it's concrete generators, à la Sage's constructors), but a coverage checklist and a source of counting formulas (e.g. tableaux via the hook-length formula) if we port more collections.

5. What DOESN'T map (deliberately skip)

  • Higher-kinded classes (Functor/Applicative/Monad/Foldable/Traversable f) — capabilities of a type constructor parameterized over its element type. Beautiful, and irrelevant to a catalog of concrete-carrier collections: a collection isn't parametric over an element type the way [] is. The one honest touch-point is Foldable/Traversable ≈ "iterate the elements," which we already have as the enumeration capability — no HKT needed.
  • Global instance coherence — Haskell allows one instance per (class, type), forbidding orphans. enumeratio deliberately wants the opposite: many structures on one carrier (the sibling-collection pattern, §6). Don't import the coherence constraint; do borrow the mechanism Haskell uses to work around it — the newtype (§6).
  • Reifying constraints as a feature — §1: we already have it as rows; there's nothing to build.

6. Newtype-per-instance = sibling-collection-per-structure

Haskell's answer to "one carrier, several structures" is the newtype: Sum/Product/Min/Max are distinct Monoid instances over the same underlying number; Down a reverses an Ord. Same bits, different declared structure, kept distinct because coherence forbids two instances on the raw type.

This is enumeratio's one-collection-one-carrier, siblings-borrow-order-via-order-iso rule (see the one-collection-one-carrier / one-identity-many-roles design notes) stated in a second vocabulary. It's worth citing in the maps/bijections doc: an alternate order is a sibling collection (a newtype), not a config flag, for the same reason Haskell uses a newtype — the structure travels with the (re)named type, and the bijection between them is feat's enumeration-transport. Convergent design, independently arrived at.

7. Convergent capability vocabulary

Reconciling Haskell against Rust / Sage / Lean-mathlib (the latter three from direct knowledge, pending their surveys):

concept Haskell Rust Sage Lean / mathlib4 enumeratio
capability typeclass trait category (methods live on it) class (typeclass) base_trait
representation instance (a type) impl (a type) Parent / Element instance / structure carrier / collection
entailment superclass => supertrait : supercategory extends / superclass implies (+ parents)
axioms / laws convention only doc convention declared axioms proved (proof fields) base_category.requires + oracle/golden tests
lazily enumerable Universe ([a]) Iterator (next) EnumeratedSets Countable enumerable (elements SRF)
next and prev — DoubleEndedIterator next/previous — bidirectional (next/prev)
finite + counted Finite (cardinality) ExactSizeIterator::len FiniteEnumeratedSets Fintype (card, elems) finite + cardinality
rank / unrank feat fIndex :: Index→a — unrank / rank Encodable (encode/decode), Denumerable (ℕ≃α) unrank(ordered_<coll>), checkable rank
graded (by size) feat [Finite]; LeanCheck tiers::a — graded graded / GradedRing base_grade / graded
uniform random feat uniform; QuickCheck Arbitrary rand distributions random_element — random_element (#8)
reified capability ConstraintKinds Dict/:- dyn Trait objects a category is an object typeclass is a term rows (already reified)

Two divergences worth remembering: laws get progressively harder guarantees left-to-right (Haskell comments them → Rust documents → Sage declares → Lean proves); enumeratio sits between Sage and Lean — it declares axioms (base_category.requires) and tests them (oracle/golden), which is stronger than Haskell and cheaper than proof. And Lean's ladder is the sharpest: Countable (∃ injection to ℕ) → Encodable (explicit encode/decode = rank/unrank) → Denumerable (ℕ ≃ α, a total unrank bijection) → Fintype (finite, with card). That four-rung split is the reference target for #8's taxonomy; Haskell's Universe/Finite + feat's fIndex cover the same rungs with running code.

The enumeration-capability ladder (the #8 deliverable)

Each rung is a base_trait; implies points from richer to the capabilities it's built on. A collection carries the highest rung its ranking supports, and the closure fills in the rest.

  1. enumerable — a lazy elements() stream; no count, no O(1) access. (Haskell Universe, Rust Iterator, Sage EnumeratedSets, Lean Countable.) The floor; every collection has it.
  2. bidirectional — next and prev on the ranking. (Rust DoubleEndedIterator, Sage next/previous.)
  3. counted — cardinality is known (finite). (Haskell Finite, Rust ExactSizeIterator, Sage FiniteEnumeratedSets, Lean Fintype.) ⇒ enumerable. (This is today's finite trait; counted names the capability — "you may call cardinality" — vs the property "the set is finite," which is the same edge here.)
  4. rankable — unrank(rank) → element (and rank where order-isomorphically checkable). (feat fIndex, Lean Encodable/Denumerable, Sage unrank/rank.) ⇒ enumerable; ⇒ counted for a finite carrier.
  5. graded — the enumeration splits into finite, independently counted+indexed size-strata. (feat [Finite], LeanCheck tiers.) ⇒ counted per stratum. (Already base_grade / graded.)
  6. sampleable — uniform random_element. (feat uniform, QuickCheck Arbitrary, Sage random_element.) ⇒ rankable + counted (draw rank ∈ [0, cardinality), unrank); for an unbounded carrier, degrade to a bounded-prefix sample or refuse — feat's uniform is the bounded-prefix precedent.

8. Map onto enumeratio — recommendations

Steal

  • Adopt the ladder in §7 as base_trait rows (enumerable, bidirectional, counted, rankable, graded, sampleable) with implies edges, derived from each ranking's support functions the way base_collection_trait already derives finite/graded/has_stats. This is backlog #8's "declare each collection's enumeration capability," and it drops into the existing view machinery unchanged.
  • Name the (cardinality, unrank) bundle after feat's Finite. counted + rankable traveling together is the Finite { fCard, fIndex } record; treat them as the pair that a random-access ranking provides, and let sampleable imply both.
  • uniform = bounded-prefix sampling for the infinite/unknown-count case in #8. Finite+known → uniform over [0, cardinality); unbounded → sample a bounded prefix (document the prefix as the support), matching feat.
  • graded = size-stratified [Finite]. Reconfirms base_grade: a grade axis partitions the enumeration into finite strata, each independently counted and unrankable — the feat/LeanCheck shape. No change, but the framing sharpens the "grading is a partition of the enumeration" story.
  • arithmoi's factorise/factorBack as the template for factorization-as-capability-plus-inverse-map — feeds the number-theory-gradings carrier and modeling factorization as a base_map with an inverse.
  • Cite the newtype ↔ sibling-collection parallel (§6) in the maps/bijections doc — it's independent corroboration that alternate structures on one carrier should be named siblings, not flags.

Avoid

  • No god-trait. The Num lesson: don't fuse the ladder into one "enumerable" mega-capability. Keep the rungs separate and compose via implies (already the house style — this just says stay the course).
  • Keep cost out of the capability's identity. #8 wants an asymptotic cost / size heuristic; Haskell (and Sage) encode what capability exists, never how cheap. The closest anyone comes is Rust's ExactSizeIterator (its existence asserts O(1) len). Recommendation: a base_trait says the capability exists; a separate, orthogonal cost/tier annotation (the existing aggregate/filterable/groupable tiering) says how cheap. Don't mint rankable_o1 vs rankable_scan traits — annotate cost on the assignment, keep the capability id clean.
  • Skip HKT and instance-coherence. §5 — no Functor-style machinery, and don't import the one-instance-per-type rule that the sibling-collection pattern is specifically designed to sidestep.

Validated (no action, worth stating)

  • Capability-as-data (base_trait rows + implies view) is what Haskell reaches for ConstraintKinds/Dict to fake, and what makes AMP/FTP-style re-slicing a query here instead of a multi-year ecosystem migration. The data-driven registry isn't just convenient — it's the structural advantage over a compiled class hierarchy.
  • The trait (HAS) / category (IS, with requires axioms) split is finer than Haskell's single overloaded "class," and closer to the Sage picture. Keep the three typed edges.

Sources

Home

Project

Design: every design page, settled, speculative and archived

Clone this wiki locally