haskell - El caso de la restricción que desaparece: Curiosidades de un tipo de rango superior

types type-constraints

Question

Todos los experimentos descritos a continuación se realizaron con GHC 8.0.1.

Esta pregunta es un seguimiento de RankNTypes con alias de tipo confusión . El problema allí se reducía a los tipos de funciones como esta ...

{-# LANGUAGE RankNTypes #-}

sleight1 :: a -> (Num a => [a]) -> a
sleight1 x (y:_) = x + y

... que son rechazados por el verificador de tipo ...

ThinAir.hs:4:13: error:
    * No instance for (Num a) arising from a pattern
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            sleight1 :: a -> (Num a => [a]) -> a
    * In the pattern: y : _
      In an equation for `sleight1'': sleight1 x (y : _) = x + y

... porque la restricción de rango superior Num a no se puede mover fuera del tipo del segundo argumento (como sería posible si tuviéramos a -> a -> (Num a => [a]) lugar). Siendo así, terminamos tratando de agregar una restricción de rango superior a una variable que ya está cuantificada en todo el proceso, es decir:

sleight1 :: forall a. a -> (Num a => [a]) -> a

Con esta recapitulación hecha, podríamos intentar simplificar un poco el ejemplo. Reemplazemos (+) con algo que no requiera Num , y desacoplamos el tipo del argumento problemático del del resultado:

sleight2 :: a -> (Num b => b) -> a
sleight2 x y = const x y

Esto no funciona como antes (excepto por un ligero cambio en el mensaje de error):

ThinAir.hs:7:24: error:
    * No instance for (Num b) arising from a use of `y''
      Possible fix:
        add (Num b) to the context of
          the type signature for:
            sleight2 :: a -> (Num b => b) -> a
    * In the second argument of `const'', namely `y''
      In the expression: const x y
      In an equation for `sleight2'': sleight2 x y = const x y
Failed, modules loaded: none.

Sin embargo, usar const aquí aquí es quizás innecesario, por lo que podríamos intentar escribir la implementación nosotros mismos:

sleight3 :: a -> (Num b => b) -> a
sleight3 x y = x

Sorprendentemente, esto realmente funciona!

Prelude> :r
[1 of 1] Compiling Main             ( ThinAir.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t sleight3
sleight3 :: a -> (Num b => b) -> a
*Main> sleight3 1 2
1

Aún más extraño, no parece haber una restricción Num real en el segundo argumento:

*Main> sleight3 1 "wat"
1

No estoy muy seguro de cómo hacer eso inteligible. Quizás podríamos decir que, al igual que podemos hacer malabares undefined siempre que nunca lo evaluemos, una restricción insatisfiable se puede mantener en un tipo muy bien siempre y cuando no se use para la unificación en ningún lado en el lado derecho. Sin embargo, esto se siente como una analogía bastante débil, especialmente dado que la falta de rigor, como solemos entender, es una noción que incluye valores y no tipos. Además, eso no nos deja más cerca de comprender cómo en el mundo String unifica con Num b => b , suponiendo que realmente ocurra algo así, algo de lo que no estoy seguro. Entonces, ¿qué es una descripción precisa de lo que está sucediendo cuando una restricción aparentemente desaparece de esta manera?

Answer 1

Oh, se pone aún más raro:

Prelude> sleight3 1 ("wat"+"man")
1
Prelude Data.Void> sleight3 1 (37 :: Void)
1

Ver, hay una restricción Num real en ese argumento. Solo, porque (como ya comentó chi) la b está en una posición covariante, esta no es una restricción que debe proporcionar al llamar a sleight3 . Más bien, puedes elegir cualquier tipo b , y sea lo que sea, ¡ sleight3 proporcionará una instancia sleight3 para ello!

Bueno, claramente eso es falso. sleight3 no puede proporcionar una instancia sleight3 para las cadenas, y definitivamente no para Void . Pero en realidad tampoco es necesario porque, como usted dijo, el argumento por el cual se aplicaría esa restricción nunca se evalúa. Recuerde que un valor polimórfico restringido es esencialmente una función de un argumento de diccionario. sleight3 simplemente promete proporcionar dicho diccionario antes de que realmente pueda usar y , pero luego no usa y de ninguna manera, así que está bien.

Es básicamente lo mismo que con una función como esta:

defiant :: (Void -> Int) -> String
defiant f = "Haha"

De nuevo, la función de argumento claramente no puede producir un Int porque no existe un valor de Void con el que evaluarla. ¡Pero esto tampoco es necesario, porque f es simplemente ignorado!

Por el contrario, sleight2 xy = const xy hace un poco de uso de y : el segundo argumento de const es solo un tipo de rango 0, por lo que el compilador debe resolver los diccionarios necesarios en ese momento. Incluso si, en última instancia, const también tira la basura, todavía "fuerza" lo suficiente de este valor para que sea evidente que no está bien escrito.