# Refine polynomial types

**URL:** <https://discourse.haskell.org/t/refine-polynomial-types/14779>\
**Category:** Show and Tell\
**Created:** [October 1, 2026, 10:06pm UTC](https://discourse.haskell.org/t/refine-polynomial-types/14779 "2026-10-01T22:06:16Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![olf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/olf/32/3813_2.png) [@olf](https://discourse.haskell.org/u/olf)\
**Post date:** [October 1, 2026, 10:06pm UTC](https://discourse.haskell.org/t/refine-polynomial-types/14779/1 "2026-10-01T22:06:16Z")

</div>

In the aftermath to a talk I gave at [LeFUNK](https://discourse.haskell.org/t/lefunk-2026-leipzig-workshop-on-functional-programming/14296), I’d like to share the algorithm that computes a refinement type. For the sake of conciseness, This demo is untyped and unsafe, in the sense that type mismatches are incomplete pattern matches.

## Preliminaries

```haskell
{-# LANGUAGE DeriveFunctor,
        DeriveGeneric, 
        PatternSynonyms, 
        ScopedTypeVariables, 
        FlexibleInstances, 
        PolyKinds, 
        TypeOperators,
        TypeFamilies,
        DefaultSignatures #-}
import Data.Proxy (Proxy(..))
import Data.Typeable (Typeable,TypeRep,typeRep)
import qualified GHC.Generics as Sub

```

# A Boolean algebra of predicates

Predicates on a type `t` can be represented by functions `t -> Bool` but we need their internal algebraic structure. First, we define syntax trees of predicates, free over some generators.

```haskell
infixr 3 :/\:
infixr 2 :\/:
data BoolExpr g = Generator g
        | Neg (BoolExpr g) 
        | (BoolExpr g) :/\: (BoolExpr g)
        | (BoolExpr g) :\/: (BoolExpr g)
        | T
        deriving (Functor)

```

The generators are just the enough to express predicates on sum and product types: While predicates on sum types use case analysis, every non-trivial predicate on a tuple must eventually inspect a factor.

```haskell
data Generator = GCase Predicate Predicate -- use only on :+: 
        | GFst Predicate -- use only on :*:
        | GSnd Predicate -- use only on :*:

type Predicate = BoolExpr Generator       

```

For convenience, we define some patterns.

```haskell
pattern F :: Predicate
pattern F = Neg T

pattern Case :: Predicate -> Predicate -> Predicate
pattern Case p q = Generator (GCase p q)

pattern Fst :: Predicate -> Predicate
pattern Fst p = Generator (GFst p)

pattern Snd :: Predicate -> Predicate
pattern Snd p = Generator (GSnd p)

```

# Polynomial types

Next, we need types that the predicates can operate on. We deliberately steal names from GHC Generics, because that is what a proper implementation of this algorithm would be operating on.

```haskell
infixr 3 :*:
infixr 2 :+:
data TypeStruct r = Opaque r
        | U 
        | V
        | TypeStruct r :+: TypeStruct r
        | TypeStruct r :*: TypeStruct r
        deriving (Show)

```

In this type, `Opaque` stands for a non-trivial type that has no visible sub-structure, with some identifying label `r`. The other leaves are `U`, the unit type, and `V`, the void type. In the last section we will provide a mechanism to derive the `TypeStruct` from the proxy of a real type.

Without the compiler to help us, the least we can do is to implement a baby type checker that tells us whether the structure of a predicate is applicable to the structure of a type.

```haskell
typeCheck :: TypeStruct r -> Predicate -> Bool
typeCheck _ T = True
typeCheck t (Neg p) = typeCheck t p
typeCheck t (p :/\: q) = typeCheck t p && typeCheck t q
typeCheck t (p :\/: q) = typeCheck t p && typeCheck t q
typeCheck (x :+: y) (Case p q) = typeCheck x p && typeCheck y q
typeCheck (x :*: y) (Fst p) = typeCheck x p
typeCheck (x :*: y) (Snd p) = typeCheck y p
typeCheck _ _ = False

```

We see that the only predicates allowed on `Opaque`, unit and void types  
are tautologies and falsehood, as expected: No predicate can identify sub-structure in a monolithic type.

# Sub-types

Our sub-types are representationally distincts from the un-refined types.  
We want to compute not only refinements, but also embeddings from the refined type into the original type. Surprisingly little is needed: Apart from the categorical identity and composition, we need the operations guaranteed by the universal properties of Cartesian product and coproduct.

```haskell
infixr 3 :&:
infixr 2 :|:
infixr 8 :.:
data SmartConstructor = Id
        | SmartConstructor :.: SmartConstructor -- composition
        | Absurd -- use only on V
        | SmartConstructor :|: SmartConstructor -- use only on :+:
        | SmartConstructor :&: SmartConstructor -- use only into :*:
        deriving Show

```

In smart constructors, `:|:` plays the role of the `either` function while `:&:` is function pairing as provided by `Control.Arrow.(&&&)`.  
Any language that has algebraic data types (or can emulate them via Church encoding) can implement this algebra of smart constructors.

We shall refine iteratively. Therefore, we need to be able to compose predicates (which stand for functions into `Bool`) with smart constructors.

```haskell
compose :: Predicate -> SmartConstructor -> Predicate
compose p Id = p
compose p (f :.: g) = (compose p f) `compose` g
compose p Absurd = F
compose p (f :|: g) = Case (compose p f) (compose p g)
compose p fg@(f :&: g) = case p of
      T -> T
      Fst q -> compose q f
      Snd q -> compose q g
      Neg q -> Neg (compose q fg)
      p1 :/\: p2 -> (compose p1 fg) :/\: (compose p2 fg)
      p1 :\/: p2 -> (compose p1 fg) :\/: (compose p2 fg)

```

Equipped with this, we declare a sub-type to be a combination of sub-type structure and smart constructor. We represent opaque types by their `Data.Typeable.TypeRep` because that is what is readily available via proxies, in base.

```haskell
data SubType = SubType (TypeStruct TypeRep) SmartConstructor
	deriving (Show)

```

# The refinement algorithm

The predicate operations `Case`, `Fst` and `Snd` are all Boolean homomorphisms. In particular this means we can push Boolean operations like negation through them. Together with De Morgan’s laws we can transform every predicate into a form that has negation only for the tautology `T`.

```haskell
-- Introduces 'Neg' only in front of 'T'. 
neg :: Predicate -> Predicate
neg T = F
neg F = T
neg (Neg p) = p
neg (p :/\: q) = (neg p) :\/: (neg q)
neg (p :\/: q) = (neg p) :/\: (neg q)
neg (Case p q) = Case (neg p) (neg q)
neg (Fst p) = Fst (neg p)
neg (Snd p) = Snd (neg p)

-- logically equivalent, 
-- but guaranteed to contain only 'F' 
-- as negation.
negationFree :: Predicate -> Predicate
negationFree (Neg p) = neg (negationFree p)
negationFree (p :/\: q) = negationFree p :/\: negationFree q
negationFree (p :\/: q) = negationFree p :\/: negationFree q
negationFree (Case p q) = Case (negationFree p) (negationFree q)
negationFree (Fst p) = Fst (negationFree p)
negationFree (Snd q) = Snd (negationFree q) 
negationFree p = p

```

For predicates on types with no sub-structure, we further must be able to decide whether a predicate is a tautology.

```haskell
tautology :: Predicate -> Bool
tautology T = True
tautology (Neg p) = not (tautology p)
tautology (p :/\: q) = tautology p && tautology q
tautology (p :\/: q) = tautology p || tautology q

```

Here is the refinement algorithm for negation-free predicates.

```haskell
refine' :: TypeStruct TypeRep -> Predicate -> SubType
refine' t T = SubType t Id
refine' t F = SubType V Absurd
refine' V _ = SubType V Id
refine' U p = if tautology p then SubType U Id else SubType V Absurd
refine' t@(Opaque _) p = if tautology p then SubType t Id else SubType V Absurd
refine' t (p :/\: q) = let
      SubType x f = refine' t p
      SubType y g = refine' x (q `compose` f)
      in SubType y (f :.: g)
refine' t (p :\/: q) = let
      SubType tp f = refine' t p
      SubType tq g = refine' t q
      in SubType (tp :+: tq) (f :|: g)
refine' (t1 :*: t2) (Fst p) = let
      SubType t1p f = refine' t1 p
      in SubType (t1p :*: t2) (f :&: Id)
refine' (t1 :*: t2) (Snd p) = let
      SubType t2p f = refine' t2 p
      in SubType (t1 :*: t2p) (Id :&: f)
refine' (t1 :+: t2) (Case p q) = let
      SubType t1p f = refine' t1 p
      SubType t2q g = refine' t2 q
      in SubType (t1p :+: t2q) (f :|: g)

```

The complete refinement algorithm first makes the predicate negation-free  
and then employs the above variant.

```haskell
refine t = refine' t . negationFree

```

# Limitations

The embedding `SmartConstructor` will be have infinite structure if the predicate has infinite structure. This is the case every time a predicate must look arbitrarily deep into the (infinite) `TypeStruct` tree. `typeCheck` diverges for such predicates. While `refine` is still productive for such predicates, the resultung `SmartConstructor` can have infinitely many brances of `:|:` and the sub-type infinitely many branches of `:+:`, that is, an infinite number of constructors. Very inconvenient, at best.

# Comparison to theorem provers

[Liquid Haskell](https://wiki.haskell.org/Liquid_Haskell) has no problems expressing the predicates we can encode in `Predicate`. Likewise, a dependently typed language such as [Lean](https://lean-lang.org/) can express the sub-types computed with the algorithm outlined above. However, with the help of @thielema we did some quick experiments and could not convice either system to divulge the sub-type itself or the smart constructor function without guidance.  
In contrast, our algorithm requires no user intervention whatsoever.

# Computing the type structure

This part is optional and only provides a convenient (but brittle) way to derive a `TypeStruct` for any given monomorphic Haskell type. We have at least three mechanisms in GHC to probe the internal structure of a type:

1. The `TypeRep` provided by `Data.Typeable`,
2. the `reify` function provided by Template Haskell,
3. the `Rep` type derived by GHC Generics.

The `TypeRep` can tell us what parameter types are given to a type constructor, but we do not immediately learn whether the parameters are used in a sum or product. Template Haskell has the `DataD` type that lists all constructors, while the indivdual `Con` has several ways of being product-like.  
Template Haskell is dependent on the internals of GHC, though.  
Relative to that, Generics offer a stable interface and heavily rely on binary sums and products to represent types. We therefore focus on Generics as the preferred provider of sub-structure.

```haskell
class StructuralRep (rep :: k -> *) where
        subStructure :: proxy rep -> TypeStruct TypeRep

genericStructure :: forall t rep proxy. 
  (Sub.Generic t, Sub.Rep t ~ rep, StructuralRep rep) 
   => proxy t -> TypeStruct TypeRep
genericStructure _ = subStructure (Proxy :: Proxy rep)

instance StructuralRep Sub.U1 where
        subStructure _ = U

instance StructuralRep Sub.V1 where
        subStructure _ = V

instance forall i m rep. StructuralRep rep => StructuralRep (Sub.M1 i m rep) where
        subStructure _ = subStructure (Proxy :: Proxy rep)

instance forall f g. (StructuralRep f, StructuralRep g) => StructuralRep (f Sub.:+: g) where
        subStructure _ = subStructure (Proxy :: Proxy f) :+: subStructure (Proxy :: Proxy g)

instance forall f g. (StructuralRep f, StructuralRep g) => StructuralRep (f Sub.:*: g) where
        subStructure _ = subStructure (Proxy :: Proxy f) :*: subStructure (Proxy :: Proxy g)

instance forall c. Structural c => StructuralRep (Sub.K1 Sub.R c) where
        subStructure _ = tyStructure (Proxy :: Proxy c)

```

Notice that we choose to ignore all meta-information that Generics provides about a type. Furthermore, recursive types will have a `TypeStruct` tree that is infinitely deep, something that the real Generics cleverly avoids via their `Rec0` and `Rec1` types.

Above we have used the class `Stuctural` which we define as follows.

```haskell
class Structural t where
        tyStructure :: proxy t -> TypeStruct TypeRep
        default tyStructure :: 
			(Sub.Generic t, Sub.Rep t ~ rep, StructuralRep rep) 
				=> proxy t -> TypeStruct TypeRep
        tyStructure = genericStructure

instance {-# OVERLAPPABLE #-} forall opaque. Typeable opaque => Structural opaque where
        tyStructure p = Opaque (typeRep p)

```

It is of course a bad idea to have a match-all instance and a default implementation at the same time, but we can thereby obtain a `TypeStruct` without effort: If we have a Generic `Rep` for a type, say T, we can declare

```haskell
instance Structural T where

```

while for other types the overlappable instance takes over.

---

<div class="post-metadata">

**Author:** ![olf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/olf/32/3813_2.png) [@olf](https://discourse.haskell.org/u/olf)\
**Post date:** [October 2, 2026, 5:59am UTC](https://discourse.haskell.org/t/refine-polynomial-types/14779/2 "2026-10-02T05:59:25Z")

</div>

Ultimately, this is a SAT solver in disguise. Indeed, the assumptions

- non-void terminals of the type structure tree are `U` or `Opaque` types (irreducible),
- the predicate has finite structure (is [uniformly continuous](https://en.wikipedia.org/wiki/Uniform_continuity))

reduce the sub-typing problem to the question: Which of the finitely many irreducible sub-types that the predicate touches are to keep and which are to be deleted? Thus the type structure and the predicate structure together determine a propositional formula over finitely many variables.

In more generality, the Boolean algebra of predicates over any type is a propositional logical theory. Sub-typing by a predicate asks for the largest quotient of the theory in which the predicate is a tautology.  
Notice that [Stone duality](https://en.wikipedia.org/wiki/Stone's_representation_theorem_for_Boolean_algebras) is at work here: sub-objects and quotients are dual, products are dual to co-products. `Fst` and `Snd` for the predicates on products play the role of `Left` and `Right`, while `Case` for predicates on sums is a tuple constuctor like `(,)`.

Apparently, so far we were unable to teach Liquid Haskell and Lean about Stone duality, since both should be capable of eating plain SAT problems for breakfast. Any ideas on how to formalize the assumptions in e.g. Liquid Haskell?

Recursive predicates break the nice correspondence of Stone duality: The predicate algebra makes no distinction between finite and infinite inputs. Consequently, predicates that diverge on infinite inputs (e.g. existential quantification) have no correspondence in the dual world and can not be handled properly by this framework.

---

<div class="post-metadata">

**Author:** ![LeventErkok](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/leventerkok/32/5716_2.png) [@LeventErkok](https://discourse.haskell.org/u/LeventErkok)\
**Post date:** [October 2, 2026, 5:32pm UTC](https://discourse.haskell.org/t/refine-polynomial-types/14779/3 "2026-10-02T17:32:37Z")

</div>

Curious about your comment “This is a SAT solver in disguise.” So far as I can see your predicates do not allow variables, so everything is a constant expression; correct?

I’m not sure what a SAT solver without any variables around really means.

In that regard your `tautology` function is really `eval`, isn’t it? (If you had variables, it would be incorrect to code `tautology` like that.)

---

<div class="post-metadata">

**Author:** ![jwaldmann](https://avatars.discourse-cdn.com/v4/letter/j/977dab/32.png) [@jwaldmann](https://discourse.haskell.org/u/jwaldmann)\
**Post date:** [October 2, 2026, 6:31pm UTC](https://discourse.haskell.org/t/refine-polynomial-types/14779/4 "2026-10-02T18:31:14Z")

</div>

> [@olf](#):
>
> … should be capable of eating plain SAT problems for breakfast

Prove it by entering, and winning, the SAT competition. For breakfast.

[https://satcompetition.github.io/](https://satcompetition.github.io/)