haskell - online - Estructura de datos en evolución.

haskell online (2)

Esperemos que alguien con más experiencia tenga una respuesta más pulida, probada en la batalla y lista, pero aquí está mi oportunidad.

Puede tener su pastel y comer parte de él también a 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 ahora usan la sintaxis GADT. Esto significa que los constructores se declaran usando sus firmas de tipo. data Foo = Bar Int Char convierte en data Foo where Bar :: Int -> Char -> Foo (aparte de la sintaxis, los dos son completamente equivalentes).
Hemos agregado una variable de tipo a Type y Expr . Esta es una llamada variable de tipo fantasma: no hay datos reales almacenados que sean de tipo p , se usa solo para imponer invariantes en el sistema de tipos.
Hemos declarado 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, podríamos usar números de nivel de tipo para indicarlos).
Los GADT nos permiten almacenar invariantes a nivel de tipo en la estructura de datos. Aquí tenemos dos de ellos. La primera 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 , pasa un Type p al constructor TypePointer y obtiene un Type p como resultado, y esas p s deben ser del mismo tipo. (Si quisiéramos permitir diferentes tipos, podríamos usar p y q ).
La segunda es que aplicamos 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 fantasma p , pero algunos de ellos requieren que sea P0 . Esto significa que esos constructores solo se pueden utilizar para construir valores de tipo Type P0 o Expr P0 , no en ninguna otra fase.

Los GADTs trabajan 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 un Type P0 para construirlo, obtendrá un error de tipo. Esto es lo que se llama "correcto por construcción": es estáticamente imposible construir una estructura no válida (siempre que pueda codificar todos los invariantes relevantes en el sistema de tipos). La otra cara de esto es que si tiene un valor de Type P1 , puede estar seguro de que se construyó correctamente: los constructores TypeOf y TypeDef no se pueden usar (de hecho, el compilador se quejará si intenta hacer un patrón coinciden en ellos), y cualquier posición recursiva también debe ser de la fase P1 . Esencialmente, cuando construyes un GADT almacenas evidencia de que las restricciones de tipo están satisfechas, y cuando haces un patrón de coincidencia en ellas, recuperas esa evidencia y puedes aprovecharla.

Esa fue la parte fácil. Desafortunadamente, tenemos algunas diferencias entre los dos tipos más allá de los constructores permitidos: algunos de los argumentos de los constructores son diferentes entre las fases, y algunos solo están presentes en la fase posterior a la transformación. Podemos usar GADTs de nuevo para codificar esto, pero no es tan económico 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 intentar hacerlo más fino:

-- 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, hemos aplicado el hecho de que algunos argumentos de constructor solo pueden estar presentes en la fase uno ( MaybeP ) y algunos son diferentes entre las dos fases ( EitherP ). Si bien esto nos hace completamente seguros para el tipo, parece un poco ad-hoc y todavía tenemos que envolver las cosas dentro y fuera de los MaybeP y los EitherP todo el tiempo. No sé si hay una mejor solución al respecto. Sin embargo, el tipo completo de seguridad es algo: podríamos escribir desde fromJustP :: MaybeP P1 a -> a y estar seguros de que es completamente seguro.

Actualización: una alternativa es usar 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 en Expr y Type relativo en la versión anterior es que los constructores necesitan tener una restricción de Phase p agregada, por ejemplo, ExprInt :: Phase p => MaybeType p -> Int -> Expr p .

Aquí, si se conoce el tipo de p en un Type o Expr , puede saber estáticamente si el MaybeP s será () o el tipo dado y cuál de los tipos son los EitherP s, y puede usarlos directamente como ese tipo sin explícito desenvolver Cuando p es desconocido, puede usar maybeP y eitherP de la clase Phase para averiguar cuáles son. (Los argumentos de Proxy son necesarios, porque de lo contrario el compilador no tendría ninguna manera de decir a qué fase te refieres). Esto es análogo a la versión de GADT donde, si se conoce p , puedes estar seguro de qué contienen MaybeP y EitherP , mientras que de lo contrario tienes que ajustar el patrón de ambas posibilidades. Esta solución tampoco es perfecta en el sentido de que los argumentos "faltantes" se convierten en () lugar de desaparecer por completo.

La construcción de Expr s y Type s también parece ser bastante similar entre las dos versiones: si el valor que está construyendo tiene algo de fase específica, debe especificar esa fase en su tipo. El problema parece surgir cuando se desea escribir una función polimórfica en p pero aún manejar 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 simplemente hubiera escrito asdf _ = NothingP el compilador se habría quejado, porque no se garantizaría que el tipo de salida sea el mismo que la entrada. Mediante la coincidencia de patrones podemos averiguar qué tipo de entrada fue y devolver un resultado del mismo tipo.

Sin embargo, con la versión de TypeFamilies , esto es mucho más difícil. Simplemente utilizando maybeP y el resultado. Maybe no pueda demostrar nada al compilador sobre los tipos. Puede obtener una parte del camino allí, en lugar de tener maybeP y eitherP retornar Maybe y Either , convirtiéndolos en funciones deconstructor y maybe que también hace disponible una igualdad de tipos:

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

(Tenga en cuenta que necesitamos Rank2Types para esto, y también tenga en cuenta que estas son esencialmente las versiones transformadas por CPS de las versiones MaybeP de MaybeP y EitherP ).

Entonces podemos escribir:

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

Pero eso 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 podrías resolver esto con una firma de tipo en algún lugar, pero en ese momento parece más molesto de lo que vale. Por lo tanto, en espera de más información de otra persona, recomendaré usar la versión GADT, ya que es la más sencilla y robusta, a costa de un poco de ruido sintáctico.

Actualice nuevamente: el problema aquí fue que debido a que MaybeP pa es una función de tipo y no hay otra información a la que acudir, GHC no tiene forma de saber qué p y a debería ser. Si paso un Proxy p y lo uso en lugar de la phase que resuelve p , pero aún se desconoce.

Estoy tratando de escribir un compilador para un lenguaje tipo C en Haskell. El compilador avanza transformando un AST. La primera pasada analiza la entrada para crear el AST, atando 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; por ejemplo, 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 .

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

Donde Unop incluye operadores como address-of ( & ), y dereference ( * ), y Binop incluye operadores como más ( + ), y tiempos ( * ), etc.

Tenga en cuenta que a cada tipo se le asigna una Id única. Esto se utiliza 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 gráfico de tipo, es seguro aplicar funciones recursivas sobre ellos sin entrar en un bucle infinito.

El siguiente paso es determinar el tamaño de cada tipo, asignar desplazamientos a los campos de estructura y reemplazar ExprField con aritmética de punteros. Al hacerlo, podemos determinar el tipo de expresiones y eliminar ExprSizeof s, ExprField s, TypeDef s, y TypeOf s de la gráfica de tipos, por lo que nuestros tipos y expresiones han evolucionado, y ahora se parecen más a esto:

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 constructores. En particular, el Type'' ya no contiene ningún Expr'' , y cada Expr'' ha determinado su Type'' .

Entonces, finalmente, la pregunta: ¿es mejor crear dos conjuntos de tipos de datos casi idénticos o intentar unificarlos en un solo tipo de datos?

Mantener dos tipos de datos separados hace que sea 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 más adelante con los de Expr'' (imagine algún pase que manipule un Expr'' , y quiera plegar cualquier expresión constante emergida). Necesitaríamos otra implementación:

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

Por otro lado, mantener un solo tipo resolvería el problema de plegado constante, pero evitaría que el verificador de tipos impusiera invariantes estáticos.

Además, ¿qué colocamos en los campos desconocidos (como las compensaciones de campo, los tamaños de matriz y los 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 punteros NULL que no se pueden verificar). Podríamos cambiar los campos desconocidos en Maybe s, y tapar los agujeros con Nothing (como los punteros NULL que podemos verificar), pero sería molesto que en los pases subsiguientes tuviéramos que seguir extrayendo valores de Maybe s que siempre van a ser. Just s.

No hay una solución ideal para este problema, ya que cada uno tiene diferentes pros y contras.

Personalmente utilizaría un único tipo de datos "árbol" y agregaría constructores de datos separados para cosas que necesitan ser diferenciadas. 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 dice, pero el razonamiento es más profundo que eso: digamos que está implementando un elemento de sintaxis que genera más AST (algo como include o un C ++ tipo de acuerdo de plantilla, y puede depender de exprs constantes como su TypeArray para que no pueda evaluarlo en la primera iteración). Con el enfoque de tipo de datos unificado, puede simplemente insertar el nuevo AST en su árbol existente, y no solo puede ejecutar las mismas fases que antes en ese árbol directamente, sino que también obtendrá el almacenamiento en caché de forma gratuita, es decir, si el nuevo AST hace referencia a un Para usar la matriz usando sizeof(typeof(myarr)) o algo así, no tiene que determinar el tamaño constante de myarr nuevo, porque su tipo ya es un TypeResolvedArray de su fase de resolución anterior.

Podría usar una representación diferente cuando haya pasado todas las fases de compilación, y es hora de interpretar el código (o algo); entonces está seguro de que no será necesario realizar más cambios en la AST, y una representación más racional podría ser una buena idea.

Por cierto, debería usar Data.Word.Word lugar de Data.Int.Int para los 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. Por favor, no cometa este error en su idioma, a menos que realmente quiera admitir matrices con tamaños negativos.