Extract: Data.Quant

[danmatichuk]

Overview

Data.Quant is a container type that allows for writing code and types that implicitly generalize over existential and universal quantification. For example:

data ColorK = RedK | BlueK

data Bucket (tp :: ColorK) = Bucket { bucketSize :: Int }

Now for types that contain Bucket there are multiple cases to consider:

data MixedBuckets = SomeBuckets [Some Bucket] -- heterogeneous collection
data SameColorBuckets (tp :: ColorK) = SameColorBuckets [Bucket tp] -- homogenous collection
data BothColorBuckets = BothColorBuckets [(Bucket RedK, Bucket BlueK)] -- universal/total collection

The Quant (f :: k -> Type) (tp :: QuantK k) datatype instead allows for all three of the above types to be effectively defined at once.

data BucketCollection (qc :: QuantK ColorK) = BucketCollection [Quant Bucket qc]

type MixedBuckets = BucketCollection ExistsK
type SameColorBuckets (c :: ColorK) = BucketCollection (OneK tp)
type BothColorBuckets = BucketCollection AllK

Functions that operate on a universally-quantified BucketCollection are then type-compatible with all of the above cases.

e.g.:

bucketContainerSize :: BucketContainer (tp :: QuantK ColorK) -> Int
bucketContainerSize (BucketContainer bs) =
  foldr (\x y -> TFC.foldrFC (\(Bucket sz) sz' -> sz + sz') y x) 0 bs

History

The Data.Quant module is a generalization of Pate.PatchPair, which was implemented as a solution for writing code that is agnostic of whether or not it is executing in a single-sided context (i.e. analyzing either the original or patched program as part of handling a control flow divergence) or the typical two-sided context (i.e. proving equivalence between an original and patched CFAR).

Originally the decision was made to not distinguish these cases at the type level, and instead rely on runtime checks to validate PatchPair usage (i.e. you can view the Original content for a single-sided "Original" PatchPair or a two-sided PatchPair, but not a "Patched" PatchPair, etc).

All of the types containing PatchPairs are therefore effectively existentially quantified over which case they fall into. This is suitable for most uses, but becomes cumbersome when trying to write anything that handles specific cases. For example, the function that merges two single-sided GraphNodes together just looks like GraphNode -> GraphNode -> Maybe GraphNode.

As a workaround, some types were duplicated to create single-sided variants, with a type parameter indicating which side (Original or Patched) they belonged to. The merge function then changes into something like: SingleGraphNode Original -> SingleGraphNode Patched -> GraphNode. The weakness of this approach is that it requires duplicating types and corresponding duplicate interface functions.

The Quant datatype allows for functions and types to be written that implicitly generalize over the above. The QuantK type constructor adds AllK and ExistsK cases to a type. We can then instead write one type definition, and each case as a specialization of that type:

Example

data Block (bin :: WhichBinary) = ...

data GraphNode  = GraphNode { blocks :: PatchPair Block }
data SingleGraphNode bin = SingleGraphNode { singleBlocks :: Block bin }
data TwoSidedGraphNode = TwoSidedGraphNode { originalBlock :: Block Original, patchedBlock :: Block Patched}

Becomes:

data Block (bin :: WhichBinary) = ...

data GraphNodeGen (qbin :: QuantK WhichBinary) = GraphNodeGen { blocks :: Quant Block qbin }

type GraphNode = GraphNodeGen ExistsK
type SingleGraphNode bin = GraphNodeGen (OneK bin)
type TwoSidedGraphNode = GraphNodeGen AllK

Now the function blocks :: GraphNodeGen qbin -> Quant Block qbin applies to all 3 types. If we re-define PatchPair as follows:

type PatchPair f = Quant f ExistsK`

Then we recover the original type signature for blocks when specialized to ExistsK, i.e:

blocks :: GraphNode -> PatchPair Block