How to Use `anyOfType` to Get All Possible Implementations in Curry-Howard Regardless of Information Loss

The anyOfType macro returns a Seq containing every possible implementation of a given type, including high information-loss solutions that the standard ofType macro would discard.

The curryhoward library implements the Curry-Howard correspondence to automatically generate Scala code from type signatures. While the standard ofType macro returns only the "best" implementation with minimal information loss, the anyOfType macro allows you to retrieve all inhabiting terms regardless of their information-loss score.

Understanding the anyOfType Macro

anyOfType is a compile-time macro that asks the Curry-Howard theorem prover to enumerate every inequivalent term that inhabits a given type. Unlike ofType, which returns a single implementation with the lowest information-loss score, or allOfType, which returns all implementations sharing the best (lowest) score, anyOfType bypasses score-based filtering entirely.

Key distinction:

• ofType[T]: Returns one implementation (lowest score).
• allOfType[T]: Returns all implementations with the lowest score only.
• anyOfType[T]: Returns all implementations regardless of score.

How anyOfType Works Under the Hood

The macro operates through three distinct layers that progressively transform your type signature into a sequence of executable implementations.

The Public API Layer

The user-facing method is defined in [src/main/scala/io/chymyst/ch/package.scala](https://github.com/chymyst/curryhoward/blob/master/src/main/scala/io/chymyst/ch/package.scala#L52-L58):

def anyOfType[U](values: Any*): Seq[U] = macro anyOfTypeImplWithValues[U]

This facade accepts a type parameter U and a variadic sequence of values, then delegates to the macro implementation.

Macro Implementation and Proof Enumeration

The macro implementation resides in [src/main/scala/io/chymyst/ch/Macros.scala](https://github.com/chymyst/curryhoward/blob/master/src/main/scala/io/chymyst/ch/Macros.scala#L415-L424) within anyOfTypeImplWithValues:

def anyOfTypeImplWithValues(c: Context)(values: c.Expr[Any]*)(implicit tt: c.WeakTypeTag[U]): c.Expr[Seq[U]] = {
  inhabitAllInternal(c)(values, returnAllProofTerms = true)
}

This method builds a TypeExpr for U, incorporates any supplied values, and forwards to inhabitAllInternal with the critical flag returnAllProofTerms = true.

Theorem Prover Integration

Inside [src/main/scala/io/chymyst/ch/Macros.scala](https://github.com/chymyst/curryhoward/blob/master/src/main/scala/io/chymyst/ch/Macros.scala#L75-L89), inhabitAllInternal invokes TheoremProver.findProofs, which returns two collections:

val (lowestScoreTerms, allTerms) = TheoremProver.findProofs(typeStructure)

• lowestScoreTerms: Implementations with minimal information loss.
• allTerms: Every inhabiting term discovered by the prover, each carrying its own informationLossScore.

Because returnAllProofTerms is true, the macro selects allTerms, converts each TermExpr into executable Scala code, and constructs the final Seq[U].

Practical Code Examples

Enumerating All Flatten Implementations for Pairs

When working with nested tuples, anyOfType reveals every possible way to flatten the structure, including implementations that discard information:

type Pair[A] = (A, A)

// Generate all 16 possible implementations of Pair[Pair[A]] => Pair[A]
val flattenings = anyOfType[Pair[Pair[Int]] => Pair[Int]]()

println(s"Found ${flattenings.length} implementations")  // Output: 16

// Inspect the lambda terms to see the information-loss characteristics
flattenings.foreach { f =>
  println(f.lambdaTerm.prettyPrint)
}

Sample output (from the test suite in [TermExprSpec.scala](https://github.com/chymyst/curryhoward/blob/master/src/test/scala/io/chymyst/ch/unit/TermExprSpec.scala#L78-L88)):

a ⇒ a._2
a ⇒ a._1
a ⇒ Tuple2(a._1._1, a._2._2)
a ⇒ Tuple2(a._2._2, a._2._2)

Each line represents a distinct implementation, including those that project single elements (high information loss) and those that combine elements structurally.

Exhaustive Generation of Option Transformations

For Option types, anyOfType generates every possible function that matches the type signature, revealing both identity and constant functions:

def optOpt[A] = anyOfType[Option[Option[A]] => Option[Option[A]]]()

println(s"Number of implementations: ${optOpt[Int].size}")  // Output: 4

optOpt[Int].foreach { f =>
  println(f.lambdaTerm.prettyPrint)
}

Source: This pattern appears in [TermExprSpec.scala](https://github.com/chymyst/curryhoward/blob/master/src/test/scala/io/chymyst/ch/unit/TermExprSpec.scala#L85) demonstrating exhaustive enumeration of Option transformations.

Incorporating User-Supplied Values

You can provide existing values as hints to the prover, which anyOfType will treat as potential building blocks while still returning all possible implementations:

val increment = (x: Int) => x + 1

// The macro may reuse `increment` or synthesize other functions
val allIncrementers = anyOfType[Int => Int](increment)

// Execute each implementation to see behavior
allIncrementers.foreach(f => println(f(10)))

Implementation detail: The macro receives the supplied increment via the values: Any* parameter in anyOfTypeImplWithValues (lines 415-424 in [Macros.scala](https://github.com/chymyst/curryhoward/blob/master/src/main/scala/io/chymyst/ch/Macros.scala#L415-L424)), treating it as a candidate term during proof search.

Key Source Files and Implementation Details

File	Purpose	Key Lines
src/main/scala/io/chymyst/ch/package.scala	Public API exposing anyOfType	52-58
src/main/scala/io/chymyst/ch/Macros.scala	Macro implementation and proof selection	415-424 (entry point), 75-89 (selection logic)
src/main/scala/io/chymyst/ch/TheoremProver.scala	Core proof search returning both filtered and complete term sets	findProofs method (returns (lowestScoreTerms, allTerms))
src/test/scala/io/chymyst/ch/unit/TermExprSpec.scala	Concrete usage examples and assertions	78-88

Summary

• anyOfType is a macro in the curryhoward library that enumerates every possible implementation of a given type signature, bypassing the standard filtering by information-loss score.
• The macro sets returnAllProofTerms = true in inhabitAllInternal (lines 75-89 of Macros.scala), forcing the selection of allTerms over lowestScoreTerms returned by the theorem prover.
• You receive a Seq[U] containing every inhabiting term, including high information-loss variants that discard data or return constants.
• The macro accepts user-supplied values as hints via the values: Any* parameter, integrating them into the proof search while still returning the complete set of solutions.

Frequently Asked Questions

What is the difference between anyOfType and allOfType?

allOfType returns only the implementations that share the lowest information-loss score, giving you all "optimal" solutions. anyOfType returns every implementation the prover can construct, including those with higher information-loss scores that may discard information or produce constant results.

How does anyOfType handle information loss scores?

The macro explicitly ignores the information-loss score by passing returnAllProofTerms = true to inhabitAllInternal. This flag instructs the system to select the allTerms collection from the theorem prover's output rather than filtering for lowestScoreTerms, ensuring no implementation is discarded based on its score.

Can I use anyOfType with user-provided values?

Yes. The macro accepts a variadic values: Any* parameter that allows you to supply existing functions or values as potential building blocks. The prover treats these as candidate terms during proof search, but still returns the complete set of all possible implementations, not just those utilizing your supplied values.

What types of implementations can anyOfType generate?

anyOfType can generate any inhabiting term for the requested type signature, including identity functions, projections, constant functions, and complex combinations. For example, when requesting Pair[Pair[A]] => Pair[A], it returns 16 distinct implementations ranging from standard monadic flatten operations to degenerate projections that discard three-quarters of the input data.

{
  "mcpServers": {
    "instagit": {
      "command": "npx",
      "args": ["-y", "instagit@latest"]
    }
  }
}