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.