In the aftermath to a talk I gave at LeFUNK, I’d like to share the algorithm that computes a refinement type. For the sake of conciseness, This demo is untyped and unsafe, in the sense that type mismatches are incomplete pattern matches.
Preliminaries
{-# LANGUAGE DeriveFunctor,
DeriveGeneric,
PatternSynonyms,
ScopedTypeVariables,
FlexibleInstances,
PolyKinds,
TypeOperators,
TypeFamilies,
DefaultSignatures #-}
import Data.Proxy (Proxy(..))
import Data.Typeable (Typeable,TypeRep,typeRep)
import qualified GHC.Generics as Sub
A Boolean algebra of predicates
Predicates on a type t can be represented by functions t -> Bool but we need their internal algebraic structure. First, we define syntax trees of predicates, free over some generators.
infixr 3 :/\:
infixr 2 :\/:
data BoolExpr g = Generator g
| Neg (BoolExpr g)
| (BoolExpr g) :/\: (BoolExpr g)
| (BoolExpr g) :\/: (BoolExpr g)
| T
deriving (Functor)
The generators are just the enough to express predicates on sum and product types: While predicates on sum types use case analysis, every non-trivial predicate on a tuple must eventually inspect a factor.
data Generator = GCase Predicate Predicate -- use only on :+:
| GFst Predicate -- use only on :*:
| GSnd Predicate -- use only on :*:
type Predicate = BoolExpr Generator
For convenience, we define some patterns.
pattern F :: Predicate
pattern F = Neg T
pattern Case :: Predicate -> Predicate -> Predicate
pattern Case p q = Generator (GCase p q)
pattern Fst :: Predicate -> Predicate
pattern Fst p = Generator (GFst p)
pattern Snd :: Predicate -> Predicate
pattern Snd p = Generator (GSnd p)
Polynomial types
Next, we need types that the predicates can operate on. We deliberately steal names from GHC Generics, because that is what a proper implementation of this algorithm would be operating on.
infixr 3 :*:
infixr 2 :+:
data TypeStruct r = Opaque r
| U
| V
| TypeStruct r :+: TypeStruct r
| TypeStruct r :*: TypeStruct r
deriving (Show)
In this type, Opaque stands for a non-trivial type that has no visible sub-structure, with some identifying label r. The other leaves are U, the unit type, and V, the void type. In the last section we will provide a mechanism to derive the TypeStruct from the proxy of a real type.
Without the compiler to help us, the least we can do is to implement a baby type checker that tells us whether the structure of a predicate is applicable to the structure of a type.
typeCheck :: TypeStruct r -> Predicate -> Bool
typeCheck _ T = True
typeCheck t (Neg p) = typeCheck t p
typeCheck t (p :/\: q) = typeCheck t p && typeCheck t q
typeCheck t (p :\/: q) = typeCheck t p && typeCheck t q
typeCheck (x :+: y) (Case p q) = typeCheck x p && typeCheck y q
typeCheck (x :*: y) (Fst p) = typeCheck x p
typeCheck (x :*: y) (Snd p) = typeCheck y p
typeCheck _ _ = False
We see that the only predicates allowed on Opaque, unit and void types
are tautologies and falsehood, as expected: No predicate can identify sub-structure in a monolithic type.
Sub-types
Our sub-types are representationally distincts from the un-refined types.
We want to compute not only refinements, but also embeddings from the refined type into the original type. Surprisingly little is needed: Apart from the categorical identity and composition, we need the operations guaranteed by the universal properties of Cartesian product and coproduct.
infixr 3 :&:
infixr 2 :|:
infixr 8 :.:
data SmartConstructor = Id
| SmartConstructor :.: SmartConstructor -- composition
| Absurd -- use only on V
| SmartConstructor :|: SmartConstructor -- use only on :+:
| SmartConstructor :&: SmartConstructor -- use only into :*:
deriving Show
In smart constructors, :|: plays the role of the either function while :&: is function pairing as provided by Control.Arrow.(&&&).
Any language that has algebraic data types (or can emulate them via Church encoding) can implement this algebra of smart constructors.
We shall refine iteratively. Therefore, we need to be able to compose predicates (which stand for functions into Bool) with smart constructors.
compose :: Predicate -> SmartConstructor -> Predicate
compose p Id = p
compose p (f :.: g) = (compose p f) `compose` g
compose p Absurd = F
compose p (f :|: g) = Case (compose p f) (compose p g)
compose p fg@(f :&: g) = case p of
T -> T
Fst q -> compose q f
Snd q -> compose q g
Neg q -> Neg (compose q fg)
p1 :/\: p2 -> (compose p1 fg) :/\: (compose p2 fg)
p1 :\/: p2 -> (compose p1 fg) :\/: (compose p2 fg)
Equipped with this, we declare a sub-type to be a combination of sub-type structure and smart constructor. We represent opaque types by their Data.Typeable.TypeRep because that is what is readily available via proxies, in base.
data SubType = SubType (TypeStruct TypeRep) SmartConstructor
deriving (Show)
The refinement algorithm
The predicate operations Case, Fst and Snd are all Boolean homomorphisms. In particular this means we can push Boolean operations like negation through them. Together with De Morgan’s laws we can transform every predicate into a form that has negation only for the tautology T.
-- Introduces 'Neg' only in front of 'T'.
neg :: Predicate -> Predicate
neg T = F
neg F = T
neg (Neg p) = p
neg (p :/\: q) = (neg p) :\/: (neg q)
neg (p :\/: q) = (neg p) :/\: (neg q)
neg (Case p q) = Case (neg p) (neg q)
neg (Fst p) = Fst (neg p)
neg (Snd p) = Snd (neg p)
-- logically equivalent,
-- but guaranteed to contain only 'F'
-- as negation.
negationFree :: Predicate -> Predicate
negationFree (Neg p) = neg (negationFree p)
negationFree (p :/\: q) = negationFree p :/\: negationFree q
negationFree (p :\/: q) = negationFree p :\/: negationFree q
negationFree (Case p q) = Case (negationFree p) (negationFree q)
negationFree (Fst p) = Fst (negationFree p)
negationFree (Snd q) = Snd (negationFree q)
negationFree p = p
For predicates on types with no sub-structure, we further must be able to decide whether a predicate is a tautology.
tautology :: Predicate -> Bool
tautology T = True
tautology (Neg p) = not (tautology p)
tautology (p :/\: q) = tautology p && tautology q
tautology (p :\/: q) = tautology p || tautology q
Here is the refinement algorithm for negation-free predicates.
refine' :: TypeStruct TypeRep -> Predicate -> SubType
refine' t T = SubType t Id
refine' t F = SubType V Absurd
refine' V _ = SubType V Id
refine' U p = if tautology p then SubType U Id else SubType V Absurd
refine' t@(Opaque _) p = if tautology p then SubType t Id else SubType V Absurd
refine' t (p :/\: q) = let
SubType x f = refine' t p
SubType y g = refine' x (q `compose` f)
in SubType y (f :.: g)
refine' t (p :\/: q) = let
SubType tp f = refine' t p
SubType tq g = refine' t q
in SubType (tp :+: tq) (f :|: g)
refine' (t1 :*: t2) (Fst p) = let
SubType t1p f = refine' t1 p
in SubType (t1p :*: t2) (f :&: Id)
refine' (t1 :*: t2) (Snd p) = let
SubType t2p f = refine' t2 p
in SubType (t1 :*: t2p) (Id :&: f)
refine' (t1 :+: t2) (Case p q) = let
SubType t1p f = refine' t1 p
SubType t2q g = refine' t2 q
in SubType (t1p :+: t2q) (f :|: g)
The complete refinement algorithm first makes the predicate negation-free
and then employs the above variant.
refine t = refine' t . negationFree
Limitations
The embedding SmartConstructor will be have infinite structure if the predicate has infinite structure. This is the case every time a predicate must look arbitrarily deep into the (infinite) TypeStruct tree. typeCheck diverges for such predicates. While refine is still productive for such predicates, the resultung SmartConstructor can have infinitely many brances of :|: and the sub-type infinitely many branches of :+:, that is, an infinite number of constructors. Very inconvenient, at best.
Comparison to theorem provers
Liquid Haskell has no problems expressing the predicates we can encode in Predicate. Likewise, a dependently typed language such as Lean can express the sub-types computed with the algorithm outlined above. However, with the help of @thielema we did some quick experiments and could not convice either system to divulge the sub-type itself or the smart constructor function without guidance.
In contrast, our algorithm requires no user intervention whatsoever.
Computing the type structure
This part is optional and only provides a convenient (but brittle) way to derive a TypeStruct for any given monomorphic Haskell type. We have at least three mechanisms in GHC to probe the internal structure of a type:
- The
TypeRepprovided byData.Typeable, - the
reifyfunction provided by Template Haskell, - the
Reptype derived by GHC Generics.
The TypeRep can tell us what parameter types are given to a type constructor, but we do not immediately learn whether the parameters are used in a sum or product. Template Haskell has the DataD type that lists all constructors, while the indivdual Con has several ways of being product-like.
Template Haskell is dependent on the internals of GHC, though.
Relative to that, Generics offer a stable interface and heavily rely on binary sums and products to represent types. We therefore focus on Generics as the preferred provider of sub-structure.
class StructuralRep (rep :: k -> *) where
subStructure :: proxy rep -> TypeStruct TypeRep
genericStructure :: forall t rep proxy.
(Sub.Generic t, Sub.Rep t ~ rep, StructuralRep rep)
=> proxy t -> TypeStruct TypeRep
genericStructure _ = subStructure (Proxy :: Proxy rep)
instance StructuralRep Sub.U1 where
subStructure _ = U
instance StructuralRep Sub.V1 where
subStructure _ = V
instance forall i m rep. StructuralRep rep => StructuralRep (Sub.M1 i m rep) where
subStructure _ = subStructure (Proxy :: Proxy rep)
instance forall f g. (StructuralRep f, StructuralRep g) => StructuralRep (f Sub.:+: g) where
subStructure _ = subStructure (Proxy :: Proxy f) :+: subStructure (Proxy :: Proxy g)
instance forall f g. (StructuralRep f, StructuralRep g) => StructuralRep (f Sub.:*: g) where
subStructure _ = subStructure (Proxy :: Proxy f) :*: subStructure (Proxy :: Proxy g)
instance forall c. Structural c => StructuralRep (Sub.K1 Sub.R c) where
subStructure _ = tyStructure (Proxy :: Proxy c)
Notice that we choose to ignore all meta-information that Generics provides about a type. Furthermore, recursive types will have a TypeStruct tree that is infinitely deep, something that the real Generics cleverly avoids via their Rec0 and Rec1 types.
Above we have used the class Stuctural which we define as follows.
class Structural t where
tyStructure :: proxy t -> TypeStruct TypeRep
default tyStructure ::
(Sub.Generic t, Sub.Rep t ~ rep, StructuralRep rep)
=> proxy t -> TypeStruct TypeRep
tyStructure = genericStructure
instance {-# OVERLAPPABLE #-} forall opaque. Typeable opaque => Structural opaque where
tyStructure p = Opaque (typeRep p)
It is of course a bad idea to have a match-all instance and a default implementation at the same time, but we can thereby obtain a TypeStruct without effort: If we have a Generic Rep for a type, say T, we can declare
instance Structural T where
while for other types the overlappable instance takes over.