Estructura de datos en evolución

Question

Estoy tratando de escribir un compilador para un lenguaje tipo C en Haskell. El compilador progresa transformando un AST. La primera pasada analiza la entrada para crear la AST, vinculando un nudo con la tabla de símbolos para permitir que los símbolos se localicen antes de que se hayan definido sin la necesidad de referencias directas.

El AST contiene información sobre tipos y expresiones, y puede haber conexiones entre ellos; p.ej. sizeof(T) es una expresión que depende de un tipo T, y T[e] es un tipo de matriz que depende de una expresión constante e.

Tipos y expresiones están representados por los tipos de datos Haskell así:

data Type = TypeInt Id 
      | TypePointer Id Type -- target type 
      | TypeArray Id Type Expr -- elt type, elt count 
      | TypeStruct Id [(String, Type)] -- [(field name, field type)] 
      | TypeOf Id Expr 
      | TypeDef Id Type 

data Expr = ExprInt Int -- literal int 
      | ExprVar Var -- variable 
      | ExprSizeof Type 
      | ExprUnop Unop Expr 
      | ExprBinop Binop Expr Expr 
      | ExprField Bool Expr String -- Bool gives true=>s.field, false=>p->field 

Dónde Unop incluye operadores como dirección-de (&), y eliminar la referencia (*), y Binop incluye operadores como más (+) y tiempos (*), etc ...

Tenga en cuenta que a cada tipo se le asigna un único Id. Esto se usa para construir un gráfico de dependencia de tipo para detectar ciclos que conducen a tipos infinitos. Una vez que estamos seguros de que no hay ciclos en el tipo de gráfico, es seguro aplicar funciones recursivas sobre ellos sin entrar en un ciclo infinito.

El siguiente paso es determinar el tamaño de cada tipo, asignar desplazamientos a campos de estructura y reemplazar ExprField con aritmética de puntero. De este modo, se puede determinar el tipo de expresiones, y eliminar ExprSizeof s, ExprField s, TypeDef s, y TypeOf s de la gráfica tipo, por lo que nuestros tipos y expresiones han evolucionado, y ahora mira de la misma familia:

data Type' = TypeInt Id 
      | TypePointer Id Type' 
      | TypeArray Id Type' Int -- constant expression has been eval'd 
      | TypeStruct Id [(String, Int, Type')] -- field offset has been determined 

data Expr' = ExprInt Type' Int 
      | ExprVar Type' Var 
      | ExprUnop Type' Unop Expr' 
      | ExprBinop Type' Binop Expr' Expr' 

Tenga en cuenta que hemos eliminado algunos de los constructores de datos y hemos cambiado ligeramente algunos de los otros. En particular, Type' ya no contiene ningún Expr', y cada Expr' ha determinado que es Type'.

Así que, finalmente, la pregunta: ¿es mejor crear dos tipos de datos casi idénticos o tratar de unificarlos en un solo tipo de datos?

Al mantener dos tipos de datos separados, se hace explícito que ciertos constructores ya no pueden aparecer. Sin embargo, la función que realiza el plegado constante para evaluar expresiones constantes tendrá Tipo:

foldConstants :: Expr -> Either String Expr' 

Pero esto significa que no podemos realizar el plegado constante después con Expr' s (imaginar algún pase que manipula un Expr', y quiere doblar cualquier expresión constante emergente). Necesitaríamos otra aplicación:

foldConstants' :: Expr' -> Either String Expr' 

Por otro lado, manteniendo un solo tipo resolvería el problema de constantes, pero volvería a prevenir el tipo corrector de hacer cumplir invariantes estáticas.

Además, ¿qué ponemos en los campos desconocidos (como desplazamientos de campo, tamaños de matriz y tipos de expresión) durante la primera pasada? Podríamos tapar los agujeros con undefined, o error "*hole*", pero eso se siente como un desastre esperando a suceder (como NULL punteros que ni siquiera puedes verificar).Podríamos cambiar los campos desconocidos en Maybe s, y tapar los agujeros con Nothing (como NULL punteros que podemos verificar), pero sería molesto en pases posteriores tener que seguir extrayendo valores de Maybe s que siempre van ser Just s.

Answer 1

Espero que alguien con más experiencia tenga una respuesta más pulida, probada en batalla y lista, pero esta es mi oportunidad.

Usted puede tener su pastel y comer parte de ella también un costo relativamente bajo con GADTs:

{-# LANGUAGE GADTs #-} 

data P0 -- phase zero 
data P1 -- phase one 

data Type p where 
    TypeInt  :: Id -> Type p 
    TypePointer :: Id -> Type p -> Type p    -- target type 
    TypeArray :: Id -> Type p -> Expr p -> Type p -- elt type, elt count 
    TypeStruct :: Id -> [(String, Type p)] -> Type p -- [(field name, field type)] 
    TypeOf  :: Id -> Expr P0 -> Type P0 
    TypeDef  :: Id -> Type P0 -> Type P0 

data Expr p where 
    ExprInt  :: Int -> Expr p      -- literal int 
    ExprVar  :: Var -> Expr p      -- variable 
    ExprSizeof :: Type P0 -> Expr P0 
    ExprUnop :: Unop -> Expr p -> Expr p 
    ExprBinop :: Binop -> Expr p -> Expr p -> Expr p 
    ExprField :: Bool -> Expr P0 -> String -> Expr P0 -- Bool gives true=>s.field, false=>p->field 

Aquí las cosas que hemos cambiado son:

• Los tipos de datos utilizan ahora GADT sintaxis. Esto significa que los constructores se declaran utilizando sus firmas de tipo. data Foo = Bar Int Char se convierte en data Foo where Bar :: Int -> Char -> Foo (aparte de la sintaxis, los dos son completamente equivalentes).

• Hemos añadido un tipo variable tanto a Type como a Expr. Esta es una de las denominadas variables de tipo fantasma: no hay datos reales almacenados que sean de tipo p, solo se utiliza para aplicar invariantes en el sistema de tipos.

• Hemos declarado los tipos ficticios para representar las fases antes y después de la transformación: fase cero y fase uno. (En un sistema más elaborado con múltiples fases, potencialmente podríamos usar números de nivel de tipo para denotarlos).)

• GADTs nos permite almacenar invariantes de nivel de tipo en la estructura de datos. Aquí tenemos dos de ellos. El primero es que las posiciones recursivas deben ser de la misma fase que la estructura que las contiene. Por ejemplo, mirando TypePointer :: Id -> Type p -> Type p, pase un Type p al constructor TypePointer y obtenga un Type p como resultado, y esos p s deben ser del mismo tipo. (Si quisiéramos permitir diferentes tipos, podríamos usar p y q.)

• El segundo es que hacemos cumplir el hecho de que algunos constructores solo pueden usarse en la primera fase. La mayoría de los constructores son polimórficos en la variable de tipo phantom p, pero algunos de ellos requieren que sea P0. Esto significa que esos constructores solo se pueden usar para construir valores del tipo Type P0 o Expr P0, no en ninguna otra fase.

GADT funcionan en dos direcciones. La primera es que si tiene una función que devuelve un Type P1 y trata de usar uno de los constructores que devuelve Type P0 para construirlo, obtendrá un error de tipo. Esto es lo que se llama "corregir por construcción": es estáticamente imposible construir una estructura inválida (siempre que pueda codificar todas las invariantes relevantes en el sistema de tipos). La otra cara de la moneda es que si tiene un valor de Type P1, puede estar seguro de que fue construido correctamente: los constructores TypeOf y TypeDef no pueden haber sido utilizados (de hecho, el compilador se quejará si intenta hacer coincidir el patrón) en ellos), y cualquier posición recursiva también debe ser de la fase P1. Básicamente, cuando construyes una GADT, almacenas evidencia de que las restricciones de tipo están satisfechas, y cuando coincides con el patrón, recuperas esa evidencia y puedes aprovecharla.

Esa fue la parte fácil. Desafortunadamente, tenemos algunas diferencias entre los dos tipos más allá de qué constructores están permitidos: algunos de los argumentos de constructor son diferentes entre las fases, y algunos solo están presentes en la fase posterior a la transformación. Nuevamente podemos usar GADT para codificar esto, pero no es tan barato y elegante. Una solución sería duplicar todos los constructores que son diferentes, y tener uno para P0 y P1. Pero la duplicación no es agradable. Podemos tratar de hacerlo más preciso:

-- a couple of helper types 
-- here I take advantage of the fact that of the things only present in one phase, 
-- they're always present in P1 and not P0, and not vice versa 
data MaybeP p a where 
    NothingP :: MaybeP P0 a 
    JustP :: a -> MaybeP P1 a 

data EitherP p a b where 
    LeftP :: a -> EitherP P0 a b 
    RightP :: b -> EitherP P1 a b 

data Type p where 
    TypeInt  :: Id -> Type p 
    TypePointer :: Id -> Type p -> Type p 
    TypeArray :: Id -> Type p -> EitherP p (Expr p) Int -> Type p 
    TypeStruct :: Id -> [(String, MaybeP p Int, Type p)] -> Type p 
    TypeOf  :: Id -> Expr P0 -> Type P0 
    TypeDef  :: Id -> Type P0 -> Type P0 

-- for brevity 
type MaybeType p = MaybeP p (Type p) 

data Expr p where 
    ExprInt  :: MaybeType p -> Int -> Expr p 
    ExprVar  :: MaybeType p -> Var -> Expr p 
    ExprSizeof :: Type P0 -> Expr P0 
    ExprUnop :: MaybeType p -> Unop -> Expr p -> Expr p 
    ExprBinop :: MaybeType p -> Binop -> Expr p -> Expr p -> Expr p 
    ExprField :: Bool -> Expr P0 -> String -> Expr P0 

aquí con algunos tipos de ayuda que hemos forzadas el hecho de que algunos argumentos de constructor sólo pueden estar presentes en la fase uno (MaybeP) y algunos son diferentes entre los dos fases (EitherP). Si bien esto nos hace completamente seguros, se siente un poco ad-hoc y todavía tenemos que envolver cosas dentro y fuera de los MaybeP sy EitherP s todo el tiempo. No sé si hay una mejor solución en ese sentido. Sin embargo, la seguridad de tipo completo es algo: podríamos escribir fromJustP :: MaybeP P1 a -> a y asegurarnos de que sea completamente segura.

Actualización: Una alternativa es utilizar TypeFamilies:

data Proxy a = Proxy 

class Phase p where 
    type MaybeP p a 
    type EitherP p a b 
    maybeP :: Proxy p -> MaybeP p a -> Maybe a 
    eitherP :: Proxy p -> EitherP p a b -> Either a b 
    phase :: Proxy p 
    phase = Proxy 

instance Phase P0 where 
    type MaybeP P0 a =() 
    type EitherP P0 a b = a 
    maybeP _ _ = Nothing 
    eitherP _ a = Left a 

instance Phase P1 where 
    type MaybeP P1 a = a 
    type EitherP P1 a b = b 
    maybeP _ a = Just a 
    eitherP _ a = Right a 

El único cambio a Expr y Type relativa a la versión anterior es que los constructores necesita tener un añadido Phase p restricción, por ejemplo, ExprInt :: Phase p => MaybeType p -> Int -> Expr p.

Aquí, si el tipo de p en un Type o Expr se conoce, puede estáticamente saber si el MaybeP s serán () o el tipo dado y cuál de los tipos de los EitherP s son, y se pueden utilizar directamente como que escriba sin desenvolver explícitamente. Cuando se desconoce p, puede usar maybeP y eitherP de la clase Phase para averiguar cuáles son. (Los argumentos Proxy son necesarios, porque de lo contrario el compilador no podría decir a qué fase se refería). Esto es análogo a la versión GADT donde, si se conoce p, puede estar seguro de qué contiene MaybeP y EitherP, mientras que de lo contrario, debe coincidir con las dos posibilidades. Esta solución tampoco es perfecta en el sentido de que los argumentos 'faltantes' se convierten en () en lugar de desaparecer por completo.

La construcción de Expr sy Type s también parece ser muy similar entre las dos versiones: si el valor que está construyendo tiene algo específico de fase, debe especificar esa fase en su tipo. El problema parece venir cuando se quiere escribir una función polimórfica en p pero aún se están manejando partes específicas de la fase. Con GADTs esto es sencillo:

asdf :: MaybeP p a -> MaybeP p a 
asdf NothingP = NothingP 
asdf (JustP a) = JustP a 

Tenga en cuenta que si sólo había escrito asdf _ = NothingP el compilador habría quejado, porque el tipo de la salida no se garantiza que sea la misma que la de entrada. Mediante la coincidencia de patrones podemos averiguar qué tipo fue la entrada y devolver un resultado del mismo tipo.

Con la versión TypeFamilies, sin embargo, esto es mucho más difícil. Simplemente usando maybeP y el resultante Maybe no puede probar nada al compilador sobre los tipos. Usted puede obtener una parte del camino que hay por, en lugar de tener maybeP y eitherP retorno Maybe y Either, haciéndolos Deconstructor funciones como maybe y either que también marcan la igualdad de tipo:

maybeP :: Proxy p -> (p ~ P0 => r) -> (p ~ P1 => a -> r) -> MaybeP p a -> r 
eitherP :: Proxy p -> (p ~ P0 => a -> r) -> (p ~ P1 => b -> r) -> EitherP p a b -> r 

(en cuenta que necesitamos Rank2Types . para esto, y también se nota que estos son esencialmente las versiones transformadas por el CPS de las versiones de GADT MaybeP y EitherP)

Entonces podemos escribir:

asdf :: Phase p => MaybeP p a -> MaybeP p a 
asdf a = maybeP phase() id a 

Pero eso todavía no es suficiente, porque GHC dice:

data.hs:116:29: 
Could not deduce (MaybeP p a ~ MaybeP p0 a0) 
from the context (Phase p) 
    bound by the type signature for 
       asdf :: Phase p => MaybeP p a -> MaybeP p a 
    at data.hs:116:1-29 
NB: `MaybeP' is a type function, and may not be injective 
In the fourth argument of `maybeP', namely `a' 
In the expression: maybeP phase() id a 
In an equation for `asdf': asdf a = maybeP phase() id a 

tal vez se podría resolver este tipo con una firma en alguna parte, pero en ese momento parece que molesta más de lo que vale. Entonces, dependiendo de más información de otra persona, recomendaré usar la versión GADT, que es la más simple y más robusta, a costa de un pequeño ruido sintáctico.

Update de nuevo: El problema aquí es que debido a MaybeP p a es una función de tipo y no hay otra información que pasar, GHC no tiene manera de saber lo que p y a debe ser. Si paso en un Proxy p y lo uso en lugar de phase que resuelve p, pero a aún se desconoce.

Answer 2

No existe una solución ideal para este problema, ya que cada uno tiene diferentes ventajas y desventajas.

Personalmente, utilizaría un solo tipo de datos "árbol" y agregaría constructores de datos separados para las cosas que necesitan diferenciarse. Es decir:

data Type 
    = ... 
    | TypeArray Id Type Expr 
    | TypeResolvedArray Id Type Int 
    | ... 

Esto tiene la ventaja de que puede ejecutar la misma fase varias veces en el mismo árbol, como usted dice, pero el razonamiento es más profundo que eso: Digamos que va a implementar un elemento de sintaxis que genera más AST (algo así como include o un tipo de plantilla de C++, y puede depender de exprs constantes como su TypeArray, por lo que no puede evaluarlo en la primera iteración). Con el enfoque de tipo de datos unificado, puede insertar el nuevo AST en su árbol existente, y no solo puede ejecutar las mismas fases que antes en ese árbol directamente, sino que obtendrá el almacenamiento en caché de forma gratuita, es decir, si el nuevo AST hace referencia a un array utilizando sizeof(typeof(myarr)) o algo así, no tiene que volver a determinar el tamaño constante de myarr, porque su tipo ya es TypeResolvedArray desde su fase de resolución anterior.

Puede usar una representación diferente cuando haya pasado todas sus fases de compilación, y es hora de interpretar el código (o algo); entonces está seguro del hecho de que ya no serán necesarios más cambios AST, y una representación más racionalizada podría ser una buena idea.

Por cierto, debe usar Data.Word.Word en lugar de Data.Int.Int para tamaños de matriz. Es un error tan común en C usar int s para indexar matrices, mientras que los punteros C en realidad no están firmados. No cometas este error en tu idioma, a menos que realmente quieras admitir matrices con tamaños negativos.