¿Qué significa "existir" en el sistema de tipo Haskell?

exists forall

Question

Estoy luchando por comprender la palabra clave exists en relación con el sistema de tipo Haskell. Hasta donde yo sé, no existe tal palabra clave en Haskell por defecto, pero:

• Hay extensions que los agregan, en declaraciones como estos data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a) data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a)
• He visto un artículo sobre ellos, y (si no recuerdo mal) afirmó que exists palabra clave que no es necesaria para el sistema de tipos, ya que se puede generalizar mediante forall

Pero ni siquiera puedo entender lo que significa el medio.

Cuando digo, por forall a . a -> Int forall a . a -> Int , significa (a mi entender, el incorrecto, supongo) "para cada (tipo) a , hay una función de un tipo a -> Int ":

myF1 :: forall a . a -> Int
myF1 _ = 123
-- okay, that function (`a -> Int`) does exist for any `a`
-- because we have just defined it

Cuando digo que exists a . a -> Int exists a . a -> Int , ¿qué puede significar? "Hay al menos un tipo a para el cual hay una función de tipo a -> Int "? ¿Por qué uno escribiría una declaración como esa? ¿Cuál es el propósito? ¿Semántica? Comportamiento del compilador?

myF2 :: exists a . a -> Int
myF2 _ = 123
-- okay, there is at least one type `a` for which there is such function
-- because, in fact, we have just defined it for any type
-- and there is at least one type...
-- so these two lines are equivalent to the two lines above

Tenga en cuenta que no está destinado a ser un código real que pueda compilar, solo un ejemplo de lo que estoy imaginando y luego escucho acerca de estos cuantificadores.

PD. No soy exactamente un novato total en Haskell (tal vez como un alumno de segundo grado), pero mis fundamentos matemáticos de estas cosas faltan.

Answer 1

Cuando digo, por favor a. a -> Int, significa (a mi entender, el incorrecto, supongo) "para cada (tipo) a, hay una función de un tipo a -> Int":

Cerca, pero no del todo. Significa "para cada tipo a, se puede considerar que esta función tiene el tipo a -> Int". Por lo tanto, se puede especializar a cualquier tipo de elección de la persona que llama.

En el caso "existe", tenemos: "hay un tipo (específico, pero desconocido) a tal que esta función tiene el tipo a -> Int". Entonces debe ser un tipo específico, pero el que llama no sabe qué.

Tenga en cuenta que esto significa que este tipo particular ( exists a. a -> Int ) no es tan interesante: no hay una forma útil de llamar a esa función excepto para pasar un valor "inferior" como undefined o let x = x in x . Una firma más útil podría exists a. Foo a => Int -> a exists a. Foo a => Int -> a . Dice que la función devuelve un tipo específico a , pero no se llega a saber qué tipo. Pero usted sabe que es una instancia de Foo , por lo que puede hacer algo útil con ella a pesar de no saber su tipo "verdadero".

Answer 2

Significa precisamente que "existe un tipo a para el cual puedo proporcionar valores de los siguientes tipos en mi constructor". Tenga en cuenta que esto es diferente de decir "el valor de a es Int en mi constructor"; en el último caso, sé cuál es el tipo, y podría usar mi propia función que toma Int s como argumentos para hacer algo más con los valores en el tipo de datos.

Por lo tanto, desde la perspectiva pragmática, los tipos existenciales le permiten ocultar el tipo subyacente en una estructura de datos , lo que obliga al programador a usar solo las operaciones que ha definido en él. Representa la encapsulación.

Es por esta razón que el siguiente tipo no es muy útil:

data Useless = exists s. Useless s

Porque no hay nada que pueda hacer con el valor (no del todo cierto, podría seq ); No sé nada sobre su tipo.

Answer 3

Un uso de tipos existenciales con el que me he encontrado es con mi código para mediar en un juego de Clue .

Mi código de mediación actúa como un distribuidor. No importa cuáles sean los tipos de jugadores, lo único que importa es que todos los jugadores implementen los ganchos que se dan en la clase de tipo Player .

class Player p m where
  -- deal them in to a particular game
  dealIn :: TotalPlayers -> PlayerPosition -> [Card] -> StateT p m ()

  -- let them know what another player does
  notify :: Event -> StateT p m ()

  -- ask them to make a suggestion
  suggest :: StateT p m (Maybe Scenario)

  -- ask them to make an accusation
  accuse :: StateT p m (Maybe Scenario)

  -- ask them to reveal a card to invalidate a suggestion
  reveal :: (PlayerPosition, Scenario) -> StateT p m Card

Ahora, el crupier podría mantener una lista de jugadores del tipo Player pm => [p] , pero eso restringiría que todos los jugadores sean del mismo tipo.

Eso es demasiado constrictivo. ¿Qué pasa si quiero tener diferentes tipos de jugadores, cada uno implementado de manera diferente, y ejecutarlos uno contra el otro?

Así que uso ExistentialTypes para crear un contenedor para jugadores:

-- wrapper for storing a player within a given monad
data WpPlayer m = forall p. Player p m => WpPlayer p

Ahora puedo mantener fácilmente una lista heterogénea de jugadores. El distribuidor todavía puede interactuar fácilmente con los jugadores usando la interfaz especificada por la clase de tipo Player .

Considere el tipo de constructor WpPlayer .

    WpPlayer :: forall p. Player p m  => p -> WpPlayer m

Aparte del forraje en el frente, este es un haskell bastante estándar. Para todos los tipos p que satisfacen el contrato Player pm , el constructor WpPlayer asigna un valor de tipo p a un valor de tipo WpPlayer m .

La parte interesante viene con un deconstructor:

    unWpPlayer (WpPlayer p) = p

¿Cuál es el tipo de unWpPlayer ? ¿Esto funciona?

    unWpPlayer :: forall p. Player p m => WpPlayer m -> p

No en realidad no. Un grupo de diferentes tipos p podría satisfacer el contrato de Player pm con un tipo particular m . Y le dimos al constructor WpPlayer un tipo particular p, por lo que debería devolver ese mismo tipo. Entonces no podemos usar forall .

Todo lo que realmente podemos decir es que existe algún tipo p, que satisface el contrato de Player pm con el tipo m .

    unWpPlayer :: exists p. Player p m => WpPlayer m -> p

Answer 4

UHC implementa la palabra clave exists. Aquí hay un ejemplo de su documentación

x2 :: exists a . (a, a -> Int)
x2 = (3 :: Int, id)

xapp :: (exists b . (b,b -> a)) -> a
xapp (v,f) = f v

x2app = xapp x2

Y otro:

mkx :: Bool -> exists a . (a, a -> Int)
mkx b = if b then x2 else (''a'',ord)

y1 = mkx True -- y1 :: (C_3_225_0_0,C_3_225_0_0 -> Int)
y2 = mkx False -- y2 :: (C_3_245_0_0,C_3_245_0_0 -> Int)

mixy = let (v1,f1) = y1
            (v2,f2) = y2
       in f1 v2

"mixy causa un error de tipo. Sin embargo, podemos usar y1 e y2 perfectamente bien:"

main :: IO ()
main = do putStrLn (show (xapp y1))
          putStrLn (show (xapp y2))

ezyang también blogueó bien sobre esto: http://blog.ezyang.com/2010/10/existential-type-curry/