haskell - herencia - Subsumos en tipos polimórficos.

polimorfismo herencia encapsulamiento abstraccion pdf

Question

En ''Inferencia de tipo práctico para tipos de rango arbitrario'' , los autores hablan de la subsunción :

Intento probar cosas en GHCi mientras leo, pero a pesar de que g k2 está hecho para revisar, no lo hago cuando trato 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

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

Answer 1

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

Puedes decirlo 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 para todos forall b. fb -> fb forall b. fb -> fb .

Entonces podemos intentarlo con éxito en el segundo ejemplo.

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

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

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 sé si podemos escribir una versión más general de u ; necesitaríamos una noción de nivel de restricción menos polimórfica para escribir algo como let s :: (a :<: b) => (a -> c) -> (b -> c); sfx = fx let s :: (a :<: b) => (a -> c) -> (b -> c); sfx = fx