¿Cómo constituye esto un error de tipo rígido Haskell?

Question

Esto funciona:

data Wrapped a = Wrapped a 

alpha :: IO s -> IO() 
alpha x = do 
    rv <- wrapit x 
    return() 
    where  
     wrapit :: IO s -> IO (Wrapped s) 
     wrapit x' = do 
      a <- x' 
      return (Wrapped a) 

Esto no es así:

data Wrapped a = Wrapped a 

alpha :: IO s -> IO() 
alpha x = do 
    rv <- wrapit 
    return() 
    where  
     wrapit :: IO (Wrapped s) 
     wrapit = do 
      a <- x 
      return (Wrapped a) 

¿Por qué?

Answer 1

Esto se debe a la forma en que las variables de tipo se determinan y cuantifican en Haskell estándar. Puede tomar la segunda versión de trabajo de esta manera:

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-} 

module RigidProblem where 

data Wrapped a = Wrapped a 

alpha :: forall s. IO s -> IO()             
alpha x = do 
    rv <- wrapit 
    return() 
    where  
     wrapit :: IO (Wrapped s) 
     wrapit = do 
      a <- x 
      return (Wrapped a) 

Hay dos cambios: los RankNTypes y extensiones de lenguaje ScopedTypeVariables están habilitados y se añade el forall s explícita en la firma tipo de alpha. La primera de las dos extensiones es lo que nos permite introducir el forall s explícito, lo que lleva el s dentro del cuerpo de alpha, mientras que el segundo hace que la firma en wrapit no sea tomada por el motor de inferencia tipo para contener un implícito forall s - en su lugar, el s en esa firma se toma para nombrar una variable de tipo que debe estar dentro del alcance y se identifica con ella.

La situación actual por defecto en Haskell, si he entendido bien, es que todas las variables de tipo rígido (es decir variables de tipo que ocurren en las firmas de tipos previstas explícitamente por el programador) están implícitamente cuantificados y no scoped léxico, por lo que hay no hay forma de referirse a una variable de tipo rígida desde un ámbito externo en una firma explícita provista en un ámbito interno ... (Oh, molesta, estoy seguro de que alguien podría decirlo mejor que esto.) De todos modos, desde el punto de vista del comprobador de tipos ver, el s en la firma alpha y la que está en la firma wrapit son totalmente independientes y no se pueden unificar - por lo tanto, el error.

Ver de los documentos de GHC y this page de Haskell Prime wiki para obtener más información.

Actualización: Me acabo de dar cuenta de que nunca he explicado por qué funciona la primera versión. En aras de la exhaustividad: tenga en cuenta que con la primera versión, podría usar t en lugar de s en la firma wrapit y nada cambiaría. Incluso puede tomar wrapit del bloque where y convertirlo en una función separada de nivel superior. El punto clave es que es una función polimórfica, por lo que el tipo de wrapit x está determinado por el tipo de x. Ninguna relación de la variable de tipo utilizada en la primera versión wrapit de la firma utilizada en la firma alpha sería útil aquí. Con la segunda versión esto es por supuesto diferente y debe recurrir a los trucos mencionados para hacer que wrapit 's s sea lo mismo que alphas.

Answer 2

respuesta de

Michał Marczyk anterior es correcta, pero vale la pena señalar que la segunda versión funciona si se quita la firma tipo de la función wrapit:

data Wrapped a = Wrapped a 

alpha :: IO s -> IO() 
alpha x = do 
    rv <- wrapit 
    return() 
    where 
     -- No type signature here! 
     wrapit = do 
      a <- x 
      return (Wrapped a) 

Es decir, el problema no es con el código en sí mismo; es que Haskell 98 no le permite escribir una firma de tipo para la función wrapit, porque incluye una variable de tipo vinculada por su contexto (la función externa alpha) y H98 no tiene forma de expresar eso.Como dijo Michał, habilitar ScopedTypeVariables le permite hacerlo.