CODEWITHSUNDEEP
haskell
Vanson Samuel
Vanson Samuel

Reputation: 2089

When is forall not for all

In the program below test₁ will not compile but test₂ will. The reason seems to be because of the forall s. in withModulus₁. It seems that the s is a different type for each and every call to withModulus₁ because of the forall s.. Why is that the case?

{-# LANGUAGE 
    GADTs
  , KindSignatures
  , RankNTypes
  , TupleSections
  , ViewPatterns #-}

module Main where

import Data.Reflection

newtype Modulus :: * -> * -> * where
  Modulus :: a -> Modulus s a
  deriving (Eq, Show)

newtype M :: * -> * -> * where
  M :: a -> M s a
  deriving (Eq, Show)

add :: Integral a => Modulus s a -> M s a -> M s a -> M s a
add (Modulus m) (M a) (M b) = M (mod (a + b) m)

mul :: Integral a => Modulus s a -> M s a -> M s a -> M s a
mul (Modulus m) (M a) (M b) = M (mod (a * b) m)

unM :: M s a -> a
unM (M a) = a

withModulus₁ :: a -> (forall s. Modulus s a -> w) -> w
withModulus₁ m k = k (Modulus m)

withModulus₂ :: a -> (Modulus s a -> w) -> w
withModulus₂ m k = k (Modulus m)

test₁ = withModulus₁ 89 (\m ->
          withModulus₁ 7 (\m' ->
            let
              a = M 131
              b = M 127
            in
              unM $ add m' (mul m a a) (mul m b b)))

test₂ = withModulus₂ 89 (\m ->
          withModulus₂ 7 (\m' ->
            let
              a = M 131
              b = M 127
            in
              unM $ add m' (mul m a a) (mul m b b)))

Here is the error message:

Modulus.hs:41:29: error:
    • Couldn't match type ‘s’ with ‘s1’
      ‘s’ is a rigid type variable bound by
        a type expected by the context:
          forall s. Modulus s Integer -> Integer
        at app/Modulus.hs:(35,9)-(41,52)
      ‘s1’ is a rigid type variable bound by
        a type expected by the context:
          forall s1. Modulus s1 Integer -> Integer
        at app/Modulus.hs:(36,11)-(41,51)
      Expected type: M s1 Integer
        Actual type: M s Integer
    • In the second argument of ‘add’, namely ‘(mul m a a)’
      In the second argument of ‘($)’, namely
        ‘add m' (mul m a a) (mul m b b)’
      In the expression: unM $ add m' (mul m a a) (mul m b b)
    • Relevant bindings include
        m' :: Modulus s1 Integer (bound at app/Modulus.hs:36:28)
        m :: Modulus s Integer (bound at app/Modulus.hs:35:27)
   |
41 |               unM $ add m' (mul m a a) (mul m b b)))
   |                             ^^^^^^^^^

Upvotes: 2

Views: 151

Answers (1)

chi
chi

Reputation: 116164

Briefly put, a function

foo :: forall s . T s -> U s

lets its caller to choose what the type s is. Indeed, it works on all types s. By comparison,

bar :: (forall s . T s) -> U

requires that its caller provides an argument x :: forall s. T s, i.e. a polymorphic value that will work on all types s. This means that bar will choose what the type s will be.

For instance,

foo :: forall a. a -> [a]
foo x = [x,x,x]

is obvious. Instead,

bar :: (forall a. a->a) -> Bool
bar x = x 12 > length (x "hello")

is more subtle. Here, bar first uses x choosing a ~ Int for x 12, and then uses x again choosing a ~ String for x "hello".

Another example:

bar2 :: Int -> (forall a. a->a) -> Bool
bar2 n x | n > 10    = x 12 > 5
         | otherwise = length (x "hello") > 7

Here a is chosen to be Int or String depending on n > 10.

Your own type

withModulus₁ :: a -> (forall s. Modulus s a -> w) -> w

states that withModulus₁ must be allowed to choose s to any type it wishes. When calling this as

withModulus₁ arg (\m -> ...)

m will have type Modulus s0 a where a was chosen by the caller, while s was chosen by withModulus₁ itself. It is required that ... must be compatible with any choice withModulus₁ may take.

What if we nest calls?

withModulus₁ arg (\m1 -> ...
   withModulus₁ arg (\m2 -> ...)
   ...
     )

Now, m1 :: Modulus s0 a as before. Further m2 :: Modulus s1 a where s1 is chosen by the innermost call to withModulus₁.

The crucial point, here, is that there is no guarantee that s0 is chosen to be the same as s1. Each call might make a different choice: see e.g. bar2 above which indeed does so.

Hence, the compiler can not assume that s0 and s1 are equal. Hence, if we call a function that requires their equality, like add, we get a type error, since this would constrain the freedom of choice of s by the two withModulus₁ calls.

Upvotes: 5

Related Questions