Geek Answers Handbook

For all restrictions

How to write a forall constraint, for example, for some families of types F and G :

 forall x y. G (F xy) ~ (x, y)

Is it possible to use the Edward A. Kmett Constraints package? And if it were a small example? I guess I need to use forall .

+6
source share
1 answer

Yes, this is possible with constraints . Be careful though! I believe that the equality you state is unlikely to have sufficient generality for constraints if the types of families are nontrivial. Consider, in particular, whether a type family is successful when x and y are stuck type families

 type family X where {} type family Y where {}

In addition, I see that your specific search constraint does not have any free variables. Hope this is just an example; an actual closed restriction like this is unlikely to be useful.

The main type family in Data.Constraint.Forall is Forall . This particular example can be handled a little more conveniently with ForallT , but it is most important to understand how to use Forall .

Typically, Forall p means forall x . px forall x . px . This does not sound very general, but in fact it is if you build up your p step by step. You are looking for

 forall x y. G (F xy) ~ (x, y)

Start by defining the class that expresses the relation you are looking for.

 class G (F xy) ~ (x, y) => C xy instance G (F xy) ~ (x, y) => C xy

Now you can go step by step by defining

 class Forall (C x) => D x instance Forall (C x) => D x

(which you can read as D x = forall y . C xy )

and then using Forall D (i.e. forall x . D x ) to express your restriction. You will need to use inst to get Dict (D x) and get Dict (C xy) again.

+6
source

More articles:


All Articles