A refinement type can be understood as a type X together with a predicate p :: X -> Bool. The refined type consists of all elements of X that satisfy the predicate. There are several tools in Haskell to work with refinement types. Among them are refined, rerefined and Liquid Haskell.
What I am looking for are tools or literature about encoding a refinement type as an ordinary type, where possible, as part of a code generator, thus following the make illegal values unrepresentable paradigm. There is the functional pearl ghosts of departed proofs but I feel that approach also does not go beyond the refinement type approach, since the run-time representation remains the same.
Problem scope:
We begin with a polynomial type X, built using sums and products and a few base types, no recursion. Thus it can have a Generic instance. Further there is a predicate p :: X -> Bool and we are interested in encoding the subset of X that satisfies the predicate as a new, smaller type. We also assume that we have access to the structure of the predicate as an AST, e.g. the logical connectives and the patterns used to define it.
Example 1:
data X = X {foo :: Maybe Int, bar :: Maybe Bool}
p :: X -> Bool
p (X (Just _) Nothing) = True
p (X Nothing (Just _)) = True
p _ = False
We are looking for a type Y and a function t :: Y -> X such that the diagram
p
X ------> Bool
^ ^
| t | const True
| |
Y ------> ()
const ()
is a weak pullback. Here weak means that t is not required to be injective. In case of the example above, there is such a type (even a proper pullback):
type Y = Either Int Bool
t :: Y -> X
t = either
(\i -> X (Just i) Nothing)
(\b -> X Nothing (Just b))
The above example is special because the predicate mentions only constructor patterns or their predicate counterparts, like isNothing and isJust.
Example 2:
type X = Integer
p :: X -> Bool
p = even
This time the predicate mentions values of X, not only patterns. Nevertheless a refinement is possible:
type Y = Integer
t :: Y -> X
t = (2*)
This works because the predicate even can be āsolvedā: even x holds if any only if x = (2*) y for some y.
In general though, we can not expect this to work in a language without dependent types when p can contain arbitrary code. In particular, negations: There is no type of strings that do not begin with 'A', although it is definable as a refinement type.
Why even the first example is problematic: Consider a further refinement:
q :: X -> Bool
q x = p x && r x
Since we already have the sub-type inclusion t :: Either Int Bool -> X that handles the p part, we are now dealing with two new predicates
r.t.Left :: Int -> Bool
r.t.Right :: Bool -> Bool
which, if we carry out the above procedure mechanically, results in combinatorial explosion. I would be grateful for pointers to literature that solves this problem efficiently, avoiding combinatorial explosion when possible.