refined-extras-0.1.0.0: Increased functionality for refined types.
Safe HaskellNone
LanguageHaskell2010

Refined.Extras.Polymorphism.Internal

Description

Internal module for predicate polymorphism. These are all used to implement the Implies type family in Refined.Extras.Polymorphism.

Since: 0.1.0.0

Synopsis

Documentation

type family ImpliesCNF q p :: Bool where ... Source #

ImpliesCNF q p determines if q implies p, i.e., returns True iff whenever q is true, then p is also true. We assume q and p are in conjunctive normal form.

Since: 0.1.0.0

Equations

ImpliesCNF q p = ImpliesCNFHelper (PropEquals q p) q p 

type family ImpliesCNFHelper (propEq :: Bool) q p :: Bool where ... Source #

Helper for ImpliesCNF.

Once again split the (equals) condition check from the recursive call so that we do not do any extra work due to strictness.

Since: 0.1.0.0

Equations

ImpliesCNFHelper 'True _1 _2 = 'True 
ImpliesCNFHelper _1 p p = 'True 
ImpliesCNFHelper _1 (q && r) p = ImpliesCNF q p || ImpliesCNF r p 
ImpliesCNFHelper _1 (q || r) p = ImpliesCNF q p && ImpliesCNF r p 
ImpliesCNFHelper _1 _2 _3 = 'False 

type family ToCNF p where ... Source #

Transforms a predicate expression into conjunctive normal form. This should be total for propositions (obviously other Types will get "stuck"), but a proof of termination would be nice.

Since: 0.1.0.0

Equations

ToCNF p = ToCNFHelper (IsCNF p) p 

type family ToCNFHelper (cond :: Bool) p where ... Source #

Helper for ToCNF. We split up the condition check and reduction step because type families are not guaranteed to be evaluated lazily. In particular, the obvious implementation:

B.If (IsCNF p) p (ToCNF (Reduce p))

creates an infinite loop. See: https://gitlab.haskell.org/ghc/ghc/-/issues/18965

Since: 0.1.0.0

Equations

ToCNFHelper 'True p = p 
ToCNFHelper 'False p = ToCNF (Reduce p) 

type family IsCNF p :: Bool where ... Source #

Returns true if the formula is in conjunctive normal form. See https://en.wikipedia.org/wiki/Conjunctive_normal_form.

Since: 0.1.0.0

Equations

IsCNF (Not (And _1 _2)) = 'False 
IsCNF (Not (Or _1 _2)) = 'False 
IsCNF (Not (Xor _1 _2)) = 'False 
IsCNF (Not (Not _1)) = 'False 
IsCNF (Not _1) = 'True 
IsCNF (Or (And _1 _2) _3) = 'False 
IsCNF (Or _1 (And _2 _3)) = 'False 
IsCNF (Or p q) = IsCNF p && IsCNF q 
IsCNF (Xor _1 _2) = 'False 
IsCNF (And p q) = IsCNF p && IsCNF q 
IsCNF _1 = 'True 

type family Reduce p where ... Source #

Reduces towards conjunctive normal form. The result is not guaranteed to be in CNF, i.e., Reduce may need to be applied repeatedly.

Since: 0.1.0.0

Equations

Reduce (Xor p q) = (p || q) && (Not p || Not q) 
Reduce (Not (Not p)) = p 
Reduce (Not (p || q)) = Not p && Not q 
Reduce (Not (p && q)) = Not p || Not q 
Reduce (Not p) = Not (Reduce p) 
Reduce (Or (p && q) r) = (p || r) && (q || r) 
Reduce (Or r (p && q)) = (r || p) && (r || q) 
Reduce (p || q) = Reduce p || Reduce q 
Reduce (p && q) = Reduce p && Reduce q 
Reduce p = p 

type family PropEquals p q :: Bool where ... Source #

Equals that ignores order (e.g. (A && B) == (B && A)). Equality is syntactic, not semantic. For instance,

(A && B) && C /= A && (B && C).

Examples

Expand
>>> :kind! PropEquals (A && (B && C)) ((A && B) && C)
PropEquals (A && (B && C)) ((A && B) && C) :: Bool
= False

>>> :kind! PropEquals (And (A || B) (Not B)) (And (A || B) (Not B))
PropEquals (And (A || B) (Not B)) (And (A || B) (Not B)) :: Bool
= True

>>> :kind! PropEquals (And A B) (And B B)
PropEquals (And A B) (And B B) :: Bool
= False

>>> :kind! PropEquals (Not (And A B)) (Not (And B A))
PropEquals (Not (And A B)) (Not (And B A)) :: Bool
= True

Since: 0.1.0.0

Equations

PropEquals p p = 'True 
PropEquals (Not p) (Not q) = PropEquals p q 
PropEquals (And p q) (And r s) = (PropEquals p r && PropEquals q s) || (PropEquals p s && PropEquals q r) 
PropEquals (Or p q) (Or r s) = (PropEquals p r && PropEquals q s) || (PropEquals p s && PropEquals q r) 
PropEquals (Xor p q) (Xor r s) = (PropEquals p r && PropEquals q s) || (PropEquals p s && PropEquals q r) 
PropEquals _1 _2 = 'False