¿Los tipos de datos algebraicos de haskell regulares son equivalentes a las gramáticas libres de contexto? ¿Qué pasa con GADTS?

programming-languages formal-languages

Question

La sintaxis para los tipos de datos algebraicos es muy similar a la sintaxis de Backus-Naur Form , que se usa para describir gramáticas sin contexto. Eso me hizo pensar, si pensamos en el comprobador de tipos de Haskell como un analizador para un idioma, representado como un tipo de datos algebraico (constructores de tipo nularry que representan los símbolos terminales, por ejemplo), es el conjunto de todos los idiomas aceptados igual que el conjunto de lenguajes libres de contexto? Además, con esta interpretación, ¿qué conjunto de lenguajes formales pueden aceptar los GADT?

Answer 1

En primer lugar, los tipos de datos no siempre describen un conjunto de cadenas (es decir, un idioma). Es decir, mientras que un tipo de lista lo hace, un tipo de árbol no. Uno podría contrarrestar que podríamos "aplanar" los árboles en listas y pensar en eso como su idioma. Sin embargo, ¿qué pasa con los tipos de datos como

data F = F Int (Int -> Int)

o peor

data R = R (R -> Int)

?

Los tipos de polinomios (tipos sin -> adentro) describen aproximadamente los árboles, que se pueden aplanar (visitar en orden), así que vamos a usarlos como ejemplo.

Como ha observado, escribir un CFG como un tipo (polinomial) es fácil, ya que puede explotar la recursión

data A = A1 Int A | A2 Int B
data B = B1 Int B Char | B2

arriba A expresa { Int^m Char^n | m>n } { Int^m Char^n | m>n } .

Los GADT van mucho más allá de los lenguajes libres de contexto.

data Z
data S n 

data ListN a n where
  L1 :: ListN a Z
  L2 :: a -> ListN a n -> ListN a (S n)

data A
data B
data C

data ABC where
   ABC :: ListN A n -> ListN B n -> ListN C n -> ABC

arriba ABC expresa el lenguaje (aplanado) A^n B^n C^n , que no está libre de contexto.

No tienes restricciones con los GADT, ya que es fácil codificar la aritmética con ellos. Es decir, puedes construir un Plus abc tipo Plus abc que no esté vacío si c=a+b con Peano naturals. También puede construir un tipo Halt nm que no esté vacío si la máquina de Turing m detiene en la entrada m . Entonces, puedes construir un lenguaje

{ A^n B^m proof | n halts on m , and proof proves it }

que es recursivo (y no en una clase más simple, aproximadamente).

En este momento, no sé si se pueden describir lenguajes recursivamente enumerables (computablemente enumerables) en GADTs. Incluso en el ejemplo del problema de detención, tengo que incluir el término "prueba" dentro de GADT para que funcione.

De manera intuitiva, si tiene una cadena de longitud n y desea compararla con una GADT, puede compilar todos los términos de profundidad n GADT, aplanarlos y luego compararlos con la cadena. Esto debería probar que tal lenguaje es siempre recursivo. Sin embargo, los tipos existenciales hacen que este enfoque de construcción de árboles sea bastante complicado, por lo que no tengo una respuesta definitiva en este momento.