Aclaración sobre los tipos existenciales en Haskell

Estoy tratando de entender los tipos existenciales en Haskell y encontré un PDF http://www.ii.uni.wroc.pl/~dabi/courses/ZPF15/rlasocha/prezentacja.pdf

Corrija mis entendimientos a continuación que tengo hasta ahora.

• Los tipos existenciales no parecen estar interesados ​​en el tipo que contienen, pero los patrones que coinciden con ellos dicen que existe algún tipo que no sabemos de qué tipo es y hasta que usemos Typeable o Data.
• Los usamos cuando queremos Ocultar tipos (por ejemplo, para Listas heterogéneas) o realmente no sabemos cuáles son los tipos en tiempo de compilación.
• GADT's proporcionan la sintaxis clara y mejor código usando tipos existenciales proporcionando implícitos forall' s

Mis dudas

• En la página 20 del PDF anterior se menciona para el siguiente código que es imposible que una Función exija un Buffer específico. ¿Por que es esto entonces? Cuando estoy redactando una función, sé exactamente qué tipo de búfer usaré aunque no sé qué datos voy a poner en eso. ¿Qué hay de malo en tener? :: Worker MemoryBuffer IntSi realmente quieren abstraer sobre Buffer, pueden tener un tipo Sum data Buffer = MemoryBuffer | NetBuffer | RandomBuffery tener un tipo como:: Worker Buffer Int

data Worker x = forall b. Buffer b => Worker {buffer :: b, input :: x}
data MemoryBuffer = MemoryBuffer

memoryWorker = Worker MemoryBuffer (1 :: Int)
memoryWorker :: Worker Int

• Como Haskell es un lenguaje de borrado de tipo completo como C, entonces, ¿cómo sabe en tiempo de ejecución qué función llamar? ¿Es algo así como mantendremos poca información y pasaremos una enorme V-Table of Functions y en el tiempo de ejecución se resolverá desde V-Table? Si es así, ¿qué tipo de información almacenará?

Los GADT proporcionan la sintaxis clara y mejor para codificar usando Tipos Existenciales al proporcionar forall implícito

Creo que hay acuerdo general en que la sintaxis de GADT es mejor. No diría que se debe a que los GADT proporcionan foralls implícitos, sino más bien porque la sintaxis original, habilitada con la ExistentialQuantificationextensión, es potencialmente confusa / engañosa. Esa sintaxis, por supuesto, se ve así:

data SomeType = forall a. SomeType a

o con una restricción:

data SomeShowableType = forall a. Show a => SomeShowableType a

y creo que el consenso es que el uso de la palabra clave forallaquí permite que el tipo se confunda fácilmente con el tipo completamente diferente:

data AnyType = AnyType (forall a. a)    -- need RankNTypes extension

Una mejor sintaxis podría haber usado una existspalabra clave separada , por lo que escribiría:

data SomeType = SomeType (exists a. a)   -- not valid GHC syntax

La sintaxis GADT, ya sea que se use con implícito o explícito forall , es más uniforme en todos estos tipos y parece ser más fácil de entender. Incluso con un explícito forall, la siguiente definición transmite la idea de que puede tomar un valor de cualquier tipo ay ponerlo dentro de un monomorfo SomeType':

data SomeType' where
    SomeType' :: forall a. (a -> SomeType')   -- parentheses optional

y es fácil ver y comprender la diferencia entre ese tipo y:

data AnyType' where
    AnyType' :: (forall a. a) -> AnyType'

Los tipos existenciales no parecen estar interesados ​​en el tipo que contienen, pero los patrones que coinciden con ellos dicen que existe algún tipo que no sabemos de qué tipo es y hasta que usemos Typeable o Data.

Los usamos cuando queremos Ocultar tipos (por ejemplo, para Listas heterogéneas) o realmente no sabemos cuáles son los tipos en tiempo de compilación.

Supongo que no están muy lejos, aunque no es necesario usar Typeableo Datausar tipos existenciales. Creo que sería más exacto decir que un tipo existencial proporciona un "cuadro" bien escrito alrededor de un tipo no especificado. El cuadro "oculta" el tipo en cierto sentido, lo que le permite hacer una lista heterogénea de dichos cuadros, ignorando los tipos que contienen. Resulta que un existencial sin restricciones, comoSomeType' anterior, es bastante inútil, pero un tipo restringido:

data SomeShowableType' where
    SomeShowableType' :: forall a. (Show a) => a -> SomeShowableType'

le permite hacer coincidir el patrón para mirar dentro de la "caja" y hacer que las instalaciones de clase de tipo estén disponibles:

showIt :: SomeShowableType' -> String
showIt (SomeShowableType' x) = show x

Tenga en cuenta que esto funciona para cualquier clase de tipo, no solo Typeable o Data.

Con respecto a su confusión acerca de la página 20 de la presentación de diapositivas, el autor dice que es imposible que una función que requiere una existencia Worker exija una instancia Workerparticular Buffer. Puede escribir una función para crear un Workeruso de un tipo particular de Buffer, como MemoryBuffer:

class Buffer b where
  output :: String -> b -> IO ()
data Worker x = forall b. Buffer b => Worker {buffer :: b, input :: x}
data MemoryBuffer = MemoryBuffer
instance Buffer MemoryBuffer

memoryWorker = Worker MemoryBuffer (1 :: Int)
memoryWorker :: Worker Int

pero si escribe una función que toma un Workerargumento, solo puede usar las Bufferinstalaciones de clase de tipo general (por ejemplo, la funciónoutput ):

doWork :: Worker Int -> IO ()
doWork (Worker b x) = output (show x) b

No puede intentar exigir que b sea ​​un tipo particular de búfer, incluso a través de la coincidencia de patrones:

doWorkBroken :: Worker Int -> IO ()
doWorkBroken (Worker b x) = case b of
  MemoryBuffer -> error "try this"       -- type error
  _            -> error "try that"

Finalmente, la información de tiempo de ejecución sobre los tipos existenciales está disponible a través de argumentos implícitos de "diccionario" para las clases de tipos involucradas. losWorker tipo anterior, además de tener campos para el búfer y la entrada, también tiene un campo implícito invisible que apunta al Bufferdiccionario (algo así como v-table, aunque no es enorme, ya que solo contiene un puntero a la outputfunción apropiada ).

Internamente, la clase de tipo Bufferse representa como un tipo de datos con campos de función, y las instancias son "diccionarios" de este tipo:

data Buffer' b = Buffer' { output' :: String -> b -> IO () }

dBuffer_MemoryBuffer :: Buffer' MemoryBuffer
dBuffer_MemoryBuffer = Buffer' { output' = undefined }

El tipo existencial tiene un campo oculto para este diccionario:

data Worker' x = forall b. Worker' { dBuffer :: Buffer' b, buffer' :: b, input' :: x }

y una función como doWorkesa opera en Worker'valores existenciales se implementa como:

doWork' :: Worker' Int -> IO ()
doWork' (Worker' dBuf b x) = output' dBuf (show x) b

Para una clase de tipo con una sola función, el diccionario está optimizado para un nuevo tipo, por lo que en este ejemplo, el Workertipo existencial incluye un campo oculto que consiste en un puntero de función a la outputfunción para el búfer, y esa es la única información de tiempo de ejecución necesaria por doWork.

En la página 20 del PDF anterior se menciona para el siguiente código que es imposible que una Función exija un Buffer específico. ¿Por que es esto entonces?

Porque Worker, como se define, toma solo un argumento, el tipo del campo "input" (variable de tipo x). Por ejemplo, Worker Intes un tipo. La variable tipo b, en cambio, no es un parámetro de Worker, sino una especie de "variable local", por así decirlo. No se puede pasar como enWorker Int String - eso provocaría un error de tipo.

Si en su lugar definimos:

data Worker x b = Worker {buffer :: b, input :: x}

entonces Worker Int Stringfuncionaría, pero el tipo ya no es existencial; ahora también tenemos que pasar el tipo de búfer también.

Como Haskell es un lenguaje de borrado de tipo completo como C, entonces, ¿cómo sabe en tiempo de ejecución qué función llamar? ¿Es algo así como mantendremos poca información y pasaremos una enorme V-Table of Functions y en el tiempo de ejecución se resolverá desde V-Table? Si es así, ¿qué tipo de información almacenará?

Esto es más o menos correcto. En pocas palabras, cada vez que aplica el constructor Worker, GHC infiere el btipo de los argumentos de Worker, y luego busca una instanciaBuffer b . Si se encuentra eso, GHC incluye un puntero adicional a la instancia en el objeto. En su forma más simple, esto no es muy diferente del "puntero a vtable" que se agrega a cada objeto en OOP cuando las funciones virtuales están presentes.

Sin embargo, en el caso general, puede ser mucho más complejo. El compilador podría usar una representación diferente y agregar más punteros en lugar de uno solo (por ejemplo, agregar directamente los punteros a todos los métodos de instancia), si eso acelera el código. Además, a veces el compilador necesita usar varias instancias para satisfacer una restricción. Por ejemplo, si necesitamos almacenar la instancia para Eq [Int]... entonces no hay uno sino dos: uno paraInt y otro para listas, y los dos deben combinarse (en tiempo de ejecución, salvo optimizaciones).

Es difícil adivinar exactamente qué hace GHC en cada caso: eso depende de una tonelada de optimizaciones que pueden o no activarse.

Puede intentar buscar en Google la implementación "basada en el diccionario" de las clases de tipos para ver más sobre lo que está sucediendo. También puede pedirle a GHC que imprima el Core interno optimizado -ddump-simply observe los diccionarios que se están construyendo, almacenando y distribuyendo. Tengo que advertirte: Core es de nivel bastante bajo y puede ser difícil de leer al principio.