Safe Haskell | Safe-Infered |
---|

A data type to represent constraints in general, and a type class for constraints that are solvable.

- type Constraints m = [Constraint m]
- data Constraint m = forall c . (Show c, Substitutable c) => Constraint c (c -> m ()) (c -> m Bool)
- class (Show c, Substitutable c, Monad m) => Solvable c m where
- solveConstraint :: c -> m ()
- checkCondition :: c -> m Bool

- liftConstraint :: Solvable c m => c -> Constraint m
- liftConstraints :: Solvable c m => [c] -> Constraints m
- mapConstraint :: (forall a. m1 a -> m2 a) -> Constraint m1 -> Constraint m2
- newtype Operation m = Op_ String
- operation :: Monad m => String -> m () -> Constraint m
- data ConstraintSum f g info
- constraintSum :: (f info -> c) -> (g info -> c) -> ConstraintSum f g info -> c

# Documentation

type Constraints m = [Constraint m]Source

data Constraint m Source

forall c . (Show c, Substitutable c) => Constraint c (c -> m ()) (c -> m Bool) |

Show (Constraint m) | |

Substitutable (Constraint m) | |

Monad m => Solvable (Constraint m) m |

class (Show c, Substitutable c, Monad m) => Solvable c m whereSource

A constraint is solvable if it knows how it can be solved in a certain state (a monadic operation), if it can check afterwards whether the final state satisfies it, and when it can be shown.

solveConstraint :: c -> m ()Source

checkCondition :: c -> m BoolSource

Monad m => Solvable (Constraint m) m | |

(TypeConstraintInfo info, HasSubst m info, HasTI m info) => Solvable (EqualityConstraint info) m | |

(HasBasic m info, HasTI m info, HasSubst m info, HasQual m info, PolyTypeConstraintInfo info) => Solvable (PolymorphismConstraint info) m | |

(HasQual m info, PolyTypeConstraintInfo info) => Solvable (ExtraConstraint info) m | |

(Solvable a m, Solvable b m) => Solvable (Either a b) m | If both constraints of type |

(Solvable (f info) m, Solvable (g info) m) => Solvable (ConstraintSum f g info) m |

liftConstraint :: Solvable c m => c -> Constraint mSource

Lifting a constraint to the Constraint data type. Every instance of the Solvable type class can be lifted.

liftConstraints :: Solvable c m => [c] -> Constraints mSource

mapConstraint :: (forall a. m1 a -> m2 a) -> Constraint m1 -> Constraint m2Source

data ConstraintSum f g info Source

The data type ConstraintSum is similar to the (standard) Either data type. However, its Show instance is slightly different as the name of the constructor is not shown.

(Functor f, Functor g) => Functor (ConstraintSum f g) | |

(Show (f info), Show (g info)) => Show (ConstraintSum f g info) | |

(Substitutable (f info), Substitutable (g info)) => Substitutable (ConstraintSum f g info) | |

(Solvable (f info) m, Solvable (g info) m) => Solvable (ConstraintSum f g info) m |

constraintSum :: (f info -> c) -> (g info -> c) -> ConstraintSum f g info -> cSource

Similar to the `either`

function.