Goal forall in RankNTypes

When writing some Haskell code using hlint I hlint query to add a type signature to a function. He introduced something like this:

 {-# LANGUAGE RankNTypes #-} multipleOf :: forall a. Integral a => a -> a -> Bool multipleOf divisor n = n `mod` divisor == 0 

This language extension is new to me, but as I understand it, it is identical to the simpler one:

 multipleOf :: Integral a => a -> a -> Bool multipleOf divisor n = n `mod` divisor == 0 

Each example of the type of rank N that I read about does not seem to add anything new to the existing polymorphism, and this forall syntax does not seem to add any meaning.

What am I missing? Is there a good example of what this forall syntax does outside of what is available without extensions?

+6
source share
1 answer

You are missing the point that you can limit the scope of a variable of a quantitative type:

 modifyPair :: (Num b, Num c) => (forall a. Num a => a -> a) -> (b, c) -> (b, c) modifyPair f (b, c) = (fb, fc) 

Try writing this function without the RankNTypes extension. In particular, allowing the elements of the pair to be different types from each other.

This specific example is not very useful, but a general idea holds. You can specify that the function argument must be polymorphic.

There is an additional trick that you can perform with this snap. The canonical example comes from ST . The purpose of the ST library is to allow limited use of mutable data. That is, you can implement an algorithm that includes a true mutation and present a clean external interface. ST himself will make sure that the use is safe with the help of ingenious system tricks:

 newtype ST sa = ... -- details aren't important newtype STRef sa = ... -- details still aren't important -- a standard-ish interface to mutable data newSTRef :: ST s (STRef sa) readSTRef :: STRef sa -> ST sa writeSTRef :: STRef sa -> a -> ST s () -- the magic using RankNTypes runST :: (forall s. ST sa) -> a 

This additional variable of type s deserves attention. It is displayed in both ST and STRef . Each function that controls STRef ensures that s in ST and STRef are the same type variable. Therefore, when you get to runST , you will find that type s should not be associated with type a . s has a more limited scope than a . The end result of this is that you cannot write something like runST newSTRef . A type controller will reject it because a variable of type s would have to avoid the context in which it was defined.

So there really are some useful tricks that you can do when you can indicate that the argument of the function should be polymorphic.

+11
source

Source: https://habr.com/ru/post/984629/


All Articles