# 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](https://hackage.haskell.org/package/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.