Este artículo presenta una técnica para codificar tipos existenciales en Haskell que permite que aparezcan 'desnudos' en las signaturas de tipo, sin necesidad de envolverlos en un constructor GADT ni recurrir a la transformación CPS (estilo paso de continuación). La codificación se apoya en funciones lineales que consumen un token de prueba (proof-token), garantizando un tratamiento correcto de los valores con tipo existencial.
El texto describe además una técnica complementaria, independiente de la anterior, que asegura que las funciones instancien los tipos existenciales 'ocultos' en sus resultados con el mismo tipo concreto con el que se instanció el tipo de entrada, preservando así la instanciación de las variables de tipo ocultas. Ambas técnicas recurren a unsafeCoerce, aunque el autor argumenta por qué considera seguras las coerciones, sin aportar una demostración formal.
Como caso de estudio, se implementa una variante segura del combinador óptico unsafePartsOf, de la librería lens, que opera sobre tipos con variables existenciales. El artículo parte de las limitaciones actuales de GHC 9.14, que solo admite tipos existenciales mediante tipos de rango 2 o constructores GADT, y discute por qué ciertas funciones perezosas —como un filtro o una conversión perezosa de listas a vectores— resultan imposibles de escribir con esos mecanismos. La codificación propuesta resuelve el problema, y se ilustra con la función lazyVecFromList, que convierte listas en vectores sin forzar la evaluación de la longitud.
El repositorio asociado ofrece un Codespace preconfigurado con GHC 9.12.3 y el servidor de lenguaje de Haskell, de modo que el lector puede experimentar con el código, consultar tipos al pasar el cursor y leer el artículo junto con las definiciones en archivos .hs.