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

Refined.Extras.Polymorphism

Description

Type families for defining functions that are polymorphic over predicates.

Since: 0.1.0.0

Synopsis

Type Families

The Implies type family lets us write functions that are polymorphic over predicates, i.e., we can define functions that require some predicate p, which can then be used by any refined term, as long as the term satisfies p . This means we can write APIs that are both safe and flexible.

type family Implies q p where ... Source #

Implies q p raises a type error if q does not logically imply p. See ImpliesBool for when q implies p.

Examples

Expand
>>> :{
  let safeDiv :: (Implies p NonZero, Integral n) => n -> Refined p n -> n
      safeDiv x d = x `div` unrefine d
      --
      -- term does not have to exactly match Refined '[NonZero] n
      d :: Refined (NonZero && Positive) Int
      d = $$(refineTH 7)
   in safeDiv 14 d
:}
2

>>> :{
  -- total wrapper over Data.Text's partial splitOn.
  let safeSplitOn :: Implies p NonEmpty => Refined p Text -> Text -> [Text]
      safeSplitOn needle haystack = unrefine needle `splitOn` haystack
      --
      splitter = $$(refineTH @NonEmpty @Text ",")
   in safeSplitOn splitter "some,text,"
:}
["some","text",""]

Since: 0.1.0.0

Equations

Implies q p = ErrIfFalse (PredNotFound q p) (ImpliesBool q p) 

type (:=>) p q = Implies p q infixr 1 Source #

Infix operator for Implies.

Examples

Expand
>>> :{
  safeDiv2 :: (p :=> NonZero, Integral n) => n -> Refined p n -> n
  safeDiv2 x d = x `div` unrefine d
:}

Since: 0.1.0.0

type family ImpliesBool q p where ... Source #

ImpliesBool q p returns 'True if q logically implies p, i.e., whenever q is true, p is also true.

NB. For a (possibly exclusive) disjunction to imply p, both clauses must individually imply p, since we cannot know which one is satisfied. That is,

\[ q_1 \vee q_2 \implies p \quad \iff \quad (q_1 \implies p) \wedge (q_2 \implies p) \]

When determining whether q implies p we are unfortunately limited by searching for syntactic, not semantic, equality. In particular,

  ((A && B) && C) /=> (A && (B && C))
  (A || (B && Not B) || C) /=> A || C

Thus it is advisable to write function constraints as simply as possible.

-- not this
foo :: Implies p (A && B) => Refined p a -> ...
-- prefer this
bar :: (Implies p A, Implies p B) => Refined p a -> ...

Of course this transformation cannot be performed universally (e.g. A || B), and we do have

  (A && B) == (B && A), (A || B) == (B || A)

for convenience.

Examples

Expand
>>> :kind! ImpliesBool (Not A) B
ImpliesBool (Not A) B :: Bool
= False

>>> :kind! ImpliesBool (Not (Not A)) A
ImpliesBool (Not (Not A)) A :: Bool
= True

>>> :kind! ImpliesBool (A || B) A
ImpliesBool (A || B) A :: Bool
= False

>>> :kind! ImpliesBool (A || (A && B)) A
ImpliesBool (A || (A && B)) A :: Bool
= True

Since: 0.1.0.0

Equations

ImpliesBool p p = 'True 
ImpliesBool q p = ImpliesCNF (ToCNF q) (ToCNF p) 

Errors

type family ErrIfFalse p b where ... Source #

Emits a TypeError when given False. The parameter type is used in the error message.

Since: 0.1.0.0

Equations

ErrIfFalse err 'False = TypeError err 
ErrIfFalse _ _ = () 

type PredNotFound p q = (('Text "Desired predicate " ':<>: 'ShowType q) ':<>: 'Text " was not implied by ") ':<>: 'ShowType p Source #

Type error for a missing, wanted predicate.

Since: 0.1.0.0