refined-subtype

This package solves the following problem. We start with a data type X, e.g. a large record. The specification of the busieness logic imposes some properties on the type, which we model as a predicate p :: X -> Bool. Hence we are interested in only those elements x that satisfy p. Packages such as refined solve this by attaching the predicate to the type X, but the run-time representation stays the same.

In contrast, this package computes a type Y and a morphism f :: Y -> X such that p x if and only if there exists some y :: Y with x = f y. If the predicate p is devoid of logical disjunctions, then the function f is actually an embedding.

Predicate transformers

In order for the problem to be feasible, we must make the internal structure of the predicate available for static analysis. Hence we restrict the type X -> Bool to a well-behaved subset, a GADT named Predicate.

Internally, the function f is represented as a predicate transformer. The category of predicate transformers is isomorphic to the category of Stone spaces. Only for a Stone space X we can recover the embedding f :: Y -> X from its predicate transformer representation.

The type of sub-types

Since only the type of X is statically known, but the predicate p is a run-time value, the refined type Y can not be known at compile-time. We must therefore wrap the embedding f in an existential type.

The machinery of Data.Dynamic and Type.Reflection enables us to

1. extract a type representation from an existentially quantified sub-type embedding,
2. execute the embedding with a detour through the Dynamic type.

Refinable types

The refinement of X by p is not computed on the type X itself but on its Generic representation. The class of refinable types contains singletons, constants and is closed under products and sums.

Hence for a Generic type X, usually the empty declaration

instance Refinable X where

suffices. For types that are neither Generic nor Stone spaces, such as the integers or function spaces, the set of analyzable predicates is sparse and the default implementation

instance Refinable X where
    refine = refineDeMorgan

is sufficient.