Subsunción en tipos polimórficos

Question

Subsunción en tipos polimórficos

En 'Practical type inference for arbitrary-rank types' , los autores hablan de subsunción :

3.3 Subsunción

Trato de probar las cosas en GHCi mientras leo, pero aunque g k2 está destinado a revisar, no lo hace cuando intento con GHC 7.8.3:

λ> :set -XRankNTypes
λ> let g :: ((forall b. [b] -> [b]) -> Int) -> Int; g = undefined
λ> let k1 :: (forall a. a -> a) -> Int; k1 = undefined
λ> let k2 :: ([Int] -> [Int]) -> Int; k2 = undefined
λ> :t g k1

<interactive>:1:3: Warning:
    Couldn't match type ‘a’ with ‘[a]’
      ‘a’ is a rigid type variable bound by
          the type forall a1. a1 -> a1 at <interactive>:1:3
    Expected type: (forall b. [b] -> [b]) -> Int
      Actual type: (forall a. a -> a) -> Int
    In the first argument of ‘g’, namely ‘k1’
    In the expression: g k1
g k1 :: Int
λ> :t g k2

<interactive>:1:3: Warning:
    Couldn't match type ‘[Int] -> [Int]’ with ‘forall b. [b] -> [b]’
    Expected type: (forall b. [b] -> [b]) -> Int
      Actual type: ([Int] -> [Int]) -> Int
    In the first argument of ‘g’, namely ‘k2’
    In the expression: g k2
g k2 :: Int

Realmente no he llegado al punto en el que entiendo el papel, todavía, pero aún así, me preocupa que he malinterpretado algo. En caso de que este tipo de comprobación? ¿Están equivocados mis tipos de Haskell?

31

types haskell ml

Author: beta, 2014-11-07

Source

1 answers

score 17 · Accepted Answer

El typechecker no sabe cuándo aplicar la regla de subsunción.

Se puede decir cuando con la siguiente función.

Prelude> let u :: ((f a -> f a) -> c) -> ((forall b. f b -> f b) -> c); u f n = f n

Esto dice, dada una función de una transformación para un tipo específico, podemos hacer una función de una transformación natural forall b. f b -> f b.

Luego podemos probarlo con éxito en el segundo ejemplo.

Prelude> :t g (u k2)
g (u k2) :: Int

El primer ejemplo ahora da un error más informativo también.

Prelude> :t g (u k1)
    Couldn't match type `forall a. a -> a' with `[a0] -> [a0]'
    Expected type: ([a0] -> [a0]) -> Int
      Actual type: (forall a. a -> a) -> Int
    In the first argument of `u', namely `k1'
    In the first argument of `g', namely `(u k1)'

No se si podemos escribir un más versión general de u; necesitaríamos una noción a nivel de restricción de menos polimórfico para escribir algo como let s :: (a :<: b) => (a -> c) -> (b -> c); s f x = f x