Explicit ForAll

Juan Pablo Yamamoto
jpyamamoto[at]ciencias.unam.mx
Lógica Computacional II. Semestre 2025-1.

Polimorfismo en tipos

Haskell está construido sobre el fundamento del Sistema F.

• Bajo la correspondencia "proposiciones como tipos" tenemos lógica de Segundo Orden.
• Polimorfismo sobre tipos.

ExplicitForAll

En Haskell, el cuantificador universal tiende a estar oculto, pero ímplicito.

id :: a -> a
id x = x

:t id

id :: forall a. a -> a

fst :: (a, b) -> a
fst (x, _) = x

:t fst

fst :: forall a b. (a, b) -> a

Pero también podemos pedirle al compilador que nos permita escribir explícitamente los cuantificadores:

{-# LANGUAGE ExplicitForAll #-}

id' :: forall a . a -> a
id' x = x

:t id'

id' :: forall a. a -> a

fst' :: forall a b . (a, b) -> a
fst' (x, _) = x

:t fst'

fst' :: forall a b. (a, b) -> a

ScopedTypeVariables

Debido a que en general no damos todos los tipos de todos los términos de un programa, puede resultar difícil para Haskell inferir correctamente el tipificado correcto en todos los casos. De hecho, es demostrable que en los sistemas al estilo Church, la inferencia de tipos es no decidible.

Debido a ello, hay problemas al tipificar fragmentos como el siguiente:

import Data.List

weirdList :: Ord a => [a] -> [(a, a)]
weirdList xs = zip sortedList nubbedList
    where sortedList :: [a]
          sortedList = sort xs
          nubbedList :: [a]
          nubbedList = nub xs

<interactive>:6:28: error:
    • Couldn't match type ‘a1’ with ‘a’
      Expected: [a1]
        Actual: [a]
      ‘a1’ is a rigid type variable bound by
        the type signature for:
          nubbedList :: forall a1. [a1]
        at <interactive>:5:11-27
      ‘a’ is a rigid type variable bound by
        the type signature for:
          weirdList :: forall a. Ord a => [a] -> [(a, a)]
        at <interactive>:1:1-37
    • In the first argument of ‘nub’, namely ‘xs’
      In the expression: nub xs
      In an equation for ‘nubbedList’: nubbedList = nub xs
    • Relevant bindings include
        nubbedList :: [a1] (bound at <interactive>:6:11)
        xs :: [a] (bound at <interactive>:2:11)
        weirdList :: [a] -> [(a, a)] (bound at <interactive>:2:1)
<interactive>:4:29: error:
    • Couldn't match type ‘a1’ with ‘a’
      Expected: [a1]
        Actual: [a]
      ‘a1’ is a rigid type variable bound by
        the type signature for:
          sortedList :: forall a1. [a1]
        at <interactive>:3:11-27
      ‘a’ is a rigid type variable bound by
        the type signature for:
          weirdList :: forall a. Ord a => [a] -> [(a, a)]
        at <interactive>:1:1-37
    • In the first argument of ‘sort’, namely ‘xs’
      In the expression: sort xs
      In an equation for ‘sortedList’: sortedList = sort xs
    • Relevant bindings include
        sortedList :: [a1] (bound at <interactive>:4:11)
        xs :: [a] (bound at <interactive>:2:11)
        weirdList :: [a] -> [(a, a)] (bound at <interactive>:2:1)

{-# LANGUAGE ScopedTypeVariables #-}

weirdList :: forall a . Ord a => [a] -> [(a, a)]
weirdList xs = zip sortedList nubbedList
    where sortedList :: [a]
          sortedList = sort xs
          nubbedList :: [a]
          nubbedList = nub xs

LiberalTypeSynonyms

En algunas ocasiones, puede resultar de utilidad expandir las definiciones de los alias de tipos, previo a realizar el análisis estático.

type Foo a = a -> a -> Bool
 
-- (forall b . b -> b) -> (forall b . b -> b) -> Bool
f :: Foo (forall b . b -> b)
f _ _ = True

<interactive>:2:6: error:
    • Illegal polymorphic type: forall b. b -> b
    • In the type signature: f :: Foo (forall b. b -> b)

{-# LANGUAGE LiberalTypeSynonyms #-}

type DropTwoBool a = a -> a -> Bool
 
ignore :: DropTwoBool (forall b. b->b)
ignore _ _ = True

:t ignore

ignore :: DropTwoBool (forall b. b -> b)

RankNTypes

Anteriormente hicimos trampa. Haskell por defecto activa esta extensión.

¿Qué sucede si la desactivamos?

{-# LANGUAGE NoRankNTypes #-}

f :: (forall b . b -> b) -> (forall b . b -> b) -> Bool
f _ _ = True

<interactive>:1:6: error:
    • Illegal polymorphic type: forall b. b -> b
    • In the type signature: f :: (forall b. b -> b) -> (forall b. b -> b) -> Bool

Entendemos el rank de un tipo como:

• Si el tipo no tiene variables de tipo, es rank 0.
• Si el tipo tiene cuantificación universal, pero los cuantificadores nunca están a la izquierda de una flecha, son rango 1.
• Si el tipo tiene un cuantificador de rank n a la izquierda de una flecha, es de rank n+1.

{-# LANGUAGE RankNTypes #-}

transformAnyType :: (forall a. a -> a) -> b -> b
transformAnyType f x = f x

Eta reduce

Found:

transformAnyType f x = f x

Why Not:

transformAnyType f = f

printAnyTransf :: (forall a. Show a => a -> a) -> String -> Int -> String
printAnyTransf g prefix suffix = g prefix ++ show (g suffix)

printAnyTransf id "key" 10

"key10"

ImpredicativeTypes

f :: [forall a. a -> a]
f = [id]

<interactive>:1:6: error:
    • Illegal polymorphic type: forall a. a -> a
    • In the type signature: f :: [forall a. a -> a]

g :: Maybe (forall a . a -> a)
g = Just id

<interactive>:1:6: error:
    • Illegal polymorphic type: forall a. a -> a
    • In the type signature: g :: Maybe (forall a. a -> a)

{-# LANGUAGE ImpredicativeTypes #-}

f :: [forall a. a -> a]
f = [id]

g :: Maybe (forall a . a -> a)
g = Just id

{-# LANGUAGE NoImpredicativeTypes #-}

h :: forall a . Maybe (a -> a)
h = Just id