Simulación de la cuantificación existencial en los tipos de devolución de función

Question

A veces me surge la necesidad de devolver valores de tipo cuantitativo existencial. Esto sucede más a menudo cuando estoy trabajando con tipos fantasmas (por ejemplo, representando la profundidad de un árbol equilibrado). AFAIK GHC no tiene ningún tipo de cuantificador exists. Solo permite existentially quantified data types (directamente o usando GADT).

Para dar un ejemplo, me gustaría tener funciones como esto:

Hasta ahora, tengo 2 soluciones posibles que voy a añadir como respuesta, estaría feliz de saber si alguien sabe algo mejor o diferente.

Answer 1

La solución estándar es crear un tipo de datos cuantificado existencialmente. El resultado sería algo así como

{-# LANGUAGE ExistentialQuantification #-} 

data Exists1 = forall a . (Show a) => Exists1 a 
instance Show Exists1 where 
    showsPrec _ (Exists1 x) = shows x 

somethingPrintable1 :: Int -> Exists1 
somethingPrintable1 x = Exists1 x 

Ahora, uno puede usar libremente show (somethingPrintable 42). Exists1 no puede ser newtype, supongo que es porque es necesario pasar la implementación particular de show en un diccionario de contexto oculto.

Para los vectores con seguridad de tipos, se podría proceder de la misma manera a crear fromList1 aplicación:

{-# LANGUAGE GADTs #-} 

data Zero 
data Succ n 

data Vec a n where 
    Nil ::     Vec a Zero 
    Cons :: a -> Vec a n -> Vec a (Succ n) 

data Exists1 f where 
    Exists1 :: f a -> Exists1 f 

fromList1 :: [a] -> Exists1 (Vec a) 
fromList1 [] = Exists1 Nil 
fromList1 (x:xs) = case fromList1 xs of 
        Exists1 r -> Exists1 $ Cons x r 

Esto funciona bien, pero el principal inconveniente que veo es el constructor adicional. Cada llamada al fromList1 da como resultado una aplicación del constructor, que se deconstruye inmediatamente. Como antes, newtype no es posible para Exists1, pero supongo que sin restricciones de tipo de tipo el compilador podría permitirlo.

---

Creé otra solución basada en la clasificación-N continuaciones. No necesita el constructor adicional, pero no estoy seguro, si la aplicación de función adicional no agrega una sobrecarga similar. En el primer caso, la solución sería:

{-# LANGUAGE Rank2Types #-} 

somethingPrintable2 :: Int -> ((forall a . (Show a) => a -> r) -> r) 
somethingPrintable2 x = \c -> c x 

ahora se podría usar somethingPrintable 42 show para obtener el resultado.

Y, por el tipo de datos Vec:

{-# LANGUAGE RankNTypes, GADTs #-} 

fromList2 :: [a] -> ((forall n . Vec a n -> r) -> r) 
fromList2 [] c  = c Nil 
fromList2 (x:xs) c = fromList2 xs (c . Cons x) 

-- Or wrapped as a newtype 
-- (this is where we need RankN instead of just Rank2): 
newtype Exists3 f r = Exists3 { unexists3 :: ((forall a . f a -> r) -> r) } 

fromList3 :: [a] -> Exists3 (Vec a) r 
fromList3 []  = Exists3 (\c -> c Nil) 
fromList3 (x:xs) = Exists3 (\c -> unexists3 (fromList3 xs) (c . Cons x)) 

esto se puede hacer un poco más fácil de leer usando un par de funciones de ayuda:

-- | A helper function for creating existential values. 
exists3 :: f x -> Exists3 f r 
exists3 x = Exists3 (\c -> c x) 
{-# INLINE exists3 #-} 

-- | A helper function to mimic function application. 
(?$) :: (forall a . f a -> r) -> Exists3 f r -> r 
(?$) f x = unexists3 x f 
{-# INLINE (?$) #-} 

fromList3 :: [a] -> Exists3 (Vec a) r 
fromList3 []  = exists3 Nil 
fromList3 (x:xs) = (exists3 . Cons x) ?$ fromList3 xs 

Las principales desventajas que vemos aquí son:

1. Posible sobrecarga con la aplicación de función adicional (No sé cuánto puede el compilador optar imitar esto).
2. Código menos legible (al menos para personas no acostumbradas a las continuaciones).