simbolos - ¿Por qué no hay variables tipográficas existencialmente cuantificadas en GHC Haskell?

pattern matching haskell

Question

Existen variables de tipo cuantificadas universalmente, y existen tipos de datos cuantificados existencialmente. Sin embargo, a pesar de que la gente da pseudocódigo de la forma exists a. Int -> a exists a. Int -> a para ayudar a explicar los conceptos a veces, no parece una extensión de compilador en la que haya un interés real. ¿Es esto simplemente un "no hay mucho valor en agregar este" tipo de cosas (porque parece valioso) para mí), o hay un problema como la indecidibilidad que lo hace realmente imposible.

EDITAR: He marcado la respuesta de Viorior como correcta porque parece que probablemente sea la razón real por la que no se incluyó. Me gustaría agregar algún comentario adicional, aunque en caso de que alguien quiera ayudar a aclarar esto más.

Tal como se solicita en los comentarios, daré un ejemplo de por qué consideraría esto útil. Supongamos que tenemos un tipo de datos de la siguiente manera:

data Person a = Person
  { age: Int
  , height: Double
  , weight: Int
  , name: a
  }

Así que elegimos parametrizar sobre a , que es una convención de nomenclatura (sé que probablemente tenga más sentido en este ejemplo hacer un ADT de NamingConvention con los constructores de datos adecuados para el nombre "paternal," first, middle, last "de los estadounidenses" nombre, nombre materno ", etc. Pero por ahora, solo sigue con esto).

Entonces, hay varias funciones que vemos que básicamente ignoran el tipo sobre el que la Persona está parametrizada. Ejemplos seria

age :: Person a -> Int
height :: Person a -> Double
weight :: Person a -> Int

Y cualquier función construida sobre estos podría ignorar el tipo a. Por ejemplo:

atRiskForDiabetes :: Person a -> Bool
atRiskForDiabetes p = age p + weight p > 200
--Clearly, I am not actually a doctor

Ahora, si tenemos una lista heterogénea de personas (de tipo [exists a. Person a] ), nos gustaría poder mapear algunas de nuestras funciones en la lista. Por supuesto, hay algunas formas inútiles de mapear:

heteroList :: [exists a. Person a]
heteroList = [Person 20 30.0 170 "Bob Jones", Person 50 32.0 140 3451115332]
extractedNames = map name heteroList

En este ejemplo, extractedNames es, por supuesto, inútil porque tiene el tipo [exists a. a] [exists a. a] . Sin embargo, si utilizamos nuestras otras funciones:

totalWeight :: [exists a. Person a] -> Int
totalWeight = sum . map age

numberAtRisk :: [exists a. Person a] -> Int
numberAtRisk = length . filter id . map atRiskForDiabetes

Ahora, tenemos algo útil que opera sobre una colección heterogénea (Y, ni siquiera involucramos las clases de tipos). Observe que pudimos reutilizar nuestras funciones existentes. El uso de un tipo de datos existencial sería el siguiente:

data SomePerson = forall a. SomePerson (Person a) --fixed, thanks viorior

Pero ahora, ¿cómo podemos usar age y atRiskForDiabetes ? Nosotros no podemos Creo que tendrías que hacer algo como esto:

someAge :: SomePerson -> Int
someAge (SomePerson p) = age p

Lo que es realmente escaso porque tienes que reescribir todos tus combinadores para un nuevo tipo. Se pone aún peor si desea hacer esto con un tipo de datos que está parametrizado sobre varias variables de tipo. Imagina esto:

somewhatHeteroPipeList :: forall a b. [exists c d. Pipe a b c d]

No explicaré esta línea de pensamiento más a fondo, pero simplemente note que reescribiría muchos combinadores para hacer algo como esto usando solo tipos de datos existenciales.

Dicho esto, espero darle un uso ligeramente convincente de que esto podría ser útil. Si no parece útil (o si el ejemplo parece demasiado artificial), no dude en hacérmelo saber. Además, como en primer lugar soy programador y no tengo formación en teoría de tipos, es un poco difícil para mí ver cómo usar el teorema de Skolem (publicado por viorior) aquí. Si alguien me pudiera mostrar cómo aplicar a la Person a ejemplo que di, estaría muy agradecido. Gracias.

Answer 1

Es innecesario.

Según el teorema de Skolem, podríamos convertir el cuantificador existencial en un cuantificador universal con tipos de rango más alto:

(∃b. F(b)) -> Int   <===>  ∀b. (F(b) -> Int)

Cada tipo de rango n + 1 cuantificado existencialmente puede codificarse como un tipo de rango n cuantificado universalmente

Answer 2

Los tipos cuantificados existencialmente están disponibles en GHC, por lo que la pregunta se basa en una suposición falsa.