Strange existential type

Question

http://www.iai.uni-bonn.de/~jv/mpc08.pdf - in this article I can not understand the following announcement:

instance TreeLike CTree where ... abs :: CTree a -> Tree a improve :: (forall m. TreeLike m => ma) -> Tree a improve m = abs m 

• what difference (forall m. TreeLike m => ma) brings (I thought TreeLike m => ma would be enough here)

• why does it allow abs here if m in ma can be any TreeLike, not just CTree?

Answer 1

This is a rank-2 type, not an existential type. What this type means, the argument for improve must be polymorphic. You cannot pass a value of type Ctree a (for example) to improve . It cannot be specific in the type constructor at all. It must explicitly be polymorphic in the type constructor with the constraint that the type constructor implements the Treelike class.

For your second question, this allows you to implement improve select the type that is required for the m it wants - this is the choice of implementation, and it is hidden from the caller in the type system. In this case, the implementation is performed to select Ctree for m . This is completely normal. The trick is that the caller improve cannot use this information anywhere.

This has the practical effect that a value cannot be constructed using type details — instead, it must use the functions of the Treelike class to construct it. But the implementation allows you to select a specific type for the job, allowing it to internally use the details of the view.

Answer 2

Could m be "any TreeLike" depending on your perspective.

From the point of view of the improve implementation, true - m can be any TreeLike , so it chooses the convenient one and uses abs .

From the point of view of the argument m - that is, the perspective of what improve applies to a certain argument, something that is more likely to have the opposite: m should actually be able to be any TreeLike , not the one we choose.

Compare this to the type of numeric literals - something like (5 :: forall a. Num a => a) means that this is any Num instance that we want it to be, but if the function expects an argument of type (forall a. Num a => a) , he wants something that could be any instance of Num that he selects. Therefore, we could give it polymorphic 5 , but not, say, Integer 5.

In many ways, you can think of polymorphic types, which means that a function takes a type as an additional argument that tells it which specific type we want to use for each type variable. Therefore, to see the difference between (forall m. TreeLike m => ma) -> Tree a and forall m. TreeLike m => ma -> Tree a forall m. TreeLike m => ma -> Tree a , you can read them as something like (M -> M a) -> Tree a vs. M -> M a -> Tree a .