Safe Haskell	None
Language	Haskell2010

Refined.Extras.Polymorphism

Contents

Type Families
Errors

Description

Type families for defining functions that are polymorphic over predicates.

Since: 0.1.0.0

Synopsis

type family Implies q p where ...
type (:=>) p q = Implies p q
type family ImpliesBool q p :: Bool where ...
type family ErrIfFalse (p :: ErrorMessage) (b :: Bool) where ...
type PredNotFound p q = (('Text "Desired predicate " ':<>: 'ShowType q) ':<>: 'Text " was not implied by ") ':<>: 'ShowType p

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 :: Bool 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 :: ErrorMessage) (b :: Bool) 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 :: Constraint
ErrIfFalse _1 _2 = ()

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