imp-ppl-0.1.0.0: README.md

# Imp

Imprecise probabilistic programming via BDDs in Haskell.

**Imp** is a domain-specific language for discrete probabilistic programs with *Knightian uncertainty*, where some probabilities are not precisely known.
Programs compile to binary decision diagrams (BDDs) for inference via weighted model counting.

Unlike standard probabilistic programming, **Imp** computes *credal sets*.
These are convex sets of distributions that capture all possibilities consistent with the specified uncertainty,
enabling reasoning under ambiguity in settings like decision-making, planning, and robust inference.

## Key ideas

| Concept | Description |
|---------|-------------|
| **Graded Monad DSL** | Programs have type `Imp (g :: [Symbol]) a`, where `g` is a type-level set of *Knightian names* tracking sources of adversarial uncertainty. Uses `QualifiedDo` for ergonomic do-notation. |
| **BDD Compilation** | Both probabilistic flips and Knightian choices compile to BDD variables. Probabilistic variables get weights for WMC whereas Knightian variables are left free. |
| **Semiring-parametric Inference** | Inference is performed via semiring-parametric WMC enabling different inference methods based on the instantiation. |
| **Enumeration via Probabilities** | Computes the full credal set by enumerating Knightian valuations, giving exact lower and upper probabilities. |
| **Optimization via Dual Numbers** | Performs gradient ascent over the Knightian weights to search for probability bounds. |
| **Approximation via Intervals** | Uses interval arithmetic to give a sound outer approximation of interval bounds in one WMC pass. |
| **Symbolic via Polynomials** | Recovers polynomial representation of the credal set for later optimization (i.e. by a corner search). |

## Quick start

```haskell
{-# LANGUAGE DataKinds, QualifiedDo, RebindableSyntax, TypeApplications #-}
import Imp

data Ball = Red | Black | Yellow deriving (Eq, Ord, Show)

-- Ellsberg's urn: 30 red, 60 either black or yellow
ellsberg :: Imp '["split"] Ball
ellsberg = Imp.do
  isRed   <- flip (1/3)
  isBlack <- interval @"split" 0.0 1.0
  Imp.return $ if isRed then Red
               else if isBlack then Black
               else Yellow
```

### Running inference

```haskell
-- Per-value marginal bounds (exact enumeration)
marginal ellsberg
-- fromList [(Red,(0.333,0.333)),(Black,(0.0,0.667)),(Yellow,(0.0,0.667))]

-- Lower/upper probability of an event
intervalProbability ellsberg (== Red)
-- (0.333, 0.333)

intervalProbability ellsberg (\b -> b == Red || b == Yellow)
-- (0.333, 1.0)
```

Precise marginals can be calculated for programs with no Knightian uncertainty:

```haskell
fairCoin :: Imp '[] Bool
fairCoin = flip 0.5

preciseMarginal fairCoin
-- fromList [(False,0.5),(True,0.5)]
```

## Building and running

Requires GHC 9.10+ and Cabal. Add `imp-ppl` to build-depends, then `import Imp`.

```bash
# Build the library
cabal build

# Run the test suite
cabal test

# Dev tooling below (requires the `dev` flag)

# Benchmarks (each emits CSV to stdout: N,method,time_s):
cabal run -f dev bench-ellsberg  # n-way Ellsberg, N = 2..15
cabal run -f dev bench-robot     # n-step robot IMDP, N = 1..8

# Visualization tool (generates index.html with credal set plots and BDD diagrams)
cabal run -f dev viz
open index.html
```

## Modules

| Module | Description |
|--------|-------------|
| `Imp` | Single-import entry point: custom prelude, DSL combinators, and the inference API |
| `Imp.Prelude` | The standard `Prelude` minus the six names the DSL replaces |
| `Imp.DSL` | Graded monad GADT, `flip`, `knight`, `interval`, `observe`, `tag` |
| `Imp.DSL.Grade` | Type-level grade algebra: `Merge`, `Union`, `TagAll` |
| `Imp.DSL.Combinators` | Iteration combinators: `mapName`, `intervalMap`, `foldN`, `scanN`, `foldMN` |
| `Imp.Semiring` | `Semiring` class, `ProbS`, `DualS`, `IntervalS`, `PolyS` |
| `Imp.BDD` | Core BDD types |
| `Imp.BDD.Builder` | Hash-consed BDD manager, ITE/And/Or operations |
| `Imp.BDD.Compile` | Compilation from `Imp` programs to BDDs |
| `Imp.BDD.WMC` | Semiring-parametric weighted model counting |
| `Imp.Inference` | Re-exports the four inference backends |
| `Imp.Inference.Enumerate` | Exact inference by Knightian valuation enumeration |
| `Imp.Inference.Approx` | Sound outer bounds via interval WMC |
| `Imp.Inference.Optimize` | Gradient ascent via dual number WMC |
| `Imp.Inference.Symbolic` | Exact inference via polynomial WMC and corner search |
| `Imp.Examples.Basic` | Simple coin-flip programs with no Knightian uncertainty |
| `Imp.Examples.Ellsberg` | The Ellsberg paradox: 30 Red balls, 60 Black or Yellow in unknown proportion |
| `Imp.Examples.IMDP` | Interval MDP: robot navigation on a line |
| `Imp.Examples.Iteration` | Random walks with imprecise step probability |
| `Imp.Examples.Knightian` | Knightian names controlling correlation between choices |
| `Imp.Examples.MontyHall` | Monty Hall problem with imprecise host behavior |
| `Imp.Examples.Polytope` | Polytope credal sets from composed intervals |
| `Imp.Examples.TwoChild` | The imprecise two-child problem |

## GHC extensions

Users need only four pragmas plus one import:

```haskell
{-# LANGUAGE DataKinds, QualifiedDo, RebindableSyntax, TypeApplications #-}
import Imp
```

The single import provides both unqualified access (DSL combinators, `ifThenElse` for `RebindableSyntax`, and the inference API) and the `Imp.` qualifier that `QualifiedDo` desugaring uses (`Imp.do`, `Imp.return`).
`RebindableSyntax` also rebinds ordinary monadic do, so put driver code in a separate module importing `Imp.Inference` (not `Imp`, which shadows `return`, `flip`, and `fmap`), or keep one module and use `import qualified Prelude as P` with `P.do` for `IO`.

Internally, the library uses `DataKinds`, `DerivingStrategies`, `GADTs`, and `TypeFamilies` as cabal default-extensions, plus per-file `UndecidableInstances` and `AllowAmbiguousTypes` where needed.

## Main features

### Probabilistic and Knightian choices

`flip p` creates a coin flip that returns `True` with probability `p`.
`knight @"name"` creates a Knightian binary choice returning `True` with unknown probability.
`interval @"name" lo hi` is shorthand for a Bernoulli with unknown probability in `[lo, hi]`.

### Conditioning

`observe` conditions on a Boolean being `True`:

```haskell
conditioned :: Imp '["bias"] Bool
conditioned = Imp.do
  biased <- interval @"bias" 0.3 0.7
  observe biased
  Imp.return biased
```

### Tagging and iteration

`tag @"name"` scopes all Knightian choices in a subprogram under a tag, enabling reuse.
Combinators like `foldN`, `scanN`, and `foldMN` iterate over numbered tags for multi-step models:

```haskell
-- Robot taking 5 steps with interval transition probabilities
trajectory :: Imp '["step1.d", "step2.d", "step3.d", "step4.d", "step5.d"] [Position]
trajectory = scanN @5 @"step" dynamics startPos step
```

### Inference modes

| Function | Description | Complexity |
|----------|-------------|------------|
| `preciseMarginal` | Exact marginals for programs with no Knightian uncertainty | O(\|BDD\|) |
| `marginal` | Exact per-value lower/upper bounds via enumeration | O(2^k x \|BDD\|) |
| `intervalProbability` | Exact lower/upper P(event) via enumeration | O(2^k x \|BDD\|) |
| `intervalExpectation` | Exact lower/upper E[f] via enumeration | O(2^k x \|BDD\|) |
| `marginalApprox` | Sound outer approximation via interval WMC | O(\|BDD\|) |
| `intervalProbabilityApprox` | Sound outer approximation of P(event) | O(\|BDD\|) |
| `intervalExpectationApprox` | Sound outer approximation of E[f] | O(\|BDD\|) |
| `marginalSymbolic` | Exact per-value bounds via symbolic WMC | O(2^k x \|BDD\|) |
| `intervalProbabilitySymbolic` | Exact lower/upper P(event) via symbolic WMC | O(2^k x \|BDD\|) |
| `intervalExpectationSymbolic` | Exact lower/upper E[f] via symbolic WMC | O(2^k x \|BDD\|) |
| `credalVertices` | The distributions per feasible Knightian valuation | O(2^k x \|BDD\|) |
| `optimizeProbability` | Gradient-based optimization over the credal set | O(steps x k x \|BDD\|) |
| `optimizeExpectation` | Gradient-based optimization of expectations | O(steps x k x \|BDD\|) |

Where *k* = number of Knightian variables.

## Examples

See `Imp.Examples.*` for worked examples:

- **Basic:** simple coin flips
- **Ellsberg:** the classic ambiguity-aversion paradox (30 red, 60 black/yellow unknown split)
- **Knightian:** `dependent`/`independent` showing how Knightian names control correlation
- **IMDP:** robot navigation on a line with interval transition probabilities, including compositional reuse via `tag`
- **Iteration:** random walks using `intervalMap`
- **MontyHall:** Monty Hall problem with Knightian host bias
- **Polytope:** composed interval choices forming higher-dimensional credal sets
- **TwoChild:** an imprecise variant of the two-child problem, demonstrating `observe`

## Accompanying paper

The library accompanies the paper [Imprecise Probabilistic Programming, Precisely (Functional Pearl)](https://doi.org/10.1145/3828698) (to appear).
The corresponding code is tagged [`icfp2026`](https://github.com/jacklc3/imp/tree/icfp2026).
The current version differs from the paper as follows.

| Name | Change |
|------|--------|
| `compile` | Returns a tuple of BDD manager, variable weights, Knightian variable indices, and worlds as a map rather than an association list |
| `wmc`, `wmcBatch` | Take a `Weight -> (s, s)` interpretation of the probability/Knightian weights into the semiring, rather than `WMCParams`; added `wmcBatch` for `Traversable`s |
| `ProbS` | Renamed from `RealS` |
| `foldMN` | Renamed from `foldmN` |
| `preciseMarginal`, `credalVertices` | Return maps instead of association lists |
| `marginal`, `marginalApprox`, `marginalSymbolic` | Return maps of lower/upper pairs instead of lists of triples |
| `optimizeExpectation`, `optimizeProbability` | Renamed from `credalOptimize*`, take the program as the first argument, and return maps of Knightian weights rather than association lists |
| `(>>=)`, `(>>)` | Carry an `Ord` constraint, permitting intermediate grouping of worlds in `compile`, which reduces the branching factor |
| `Imp.Inference.Symbolic` | Implemented the polynomial semiring and corner search that the paper left for future work |
| Empty credal set | Now uniformly throws an error when inferring bounds |