Verificando la corrección del programa usando tipos fantasma en Haskell

Question

Supongamos que estoy trabajando con el código de una máquina de pila, que puede hacer algunas operaciones simples (empujar constante, agregar, mul, dup, swap, pop, convertir tipos) en entradas y dobles .

Ahora el programa que estoy escribiendo toma una descripción en otro idioma y lo traduce en código para esta máquina de pila. También necesito calcular el tamaño máximo de la pila.

Sospecho que es posible utilizar el tipo Haskell corrector para eliminar algunos errores, por ejemplo:

• haciendo estallar de una pila vacía
• multiplicador de dobles utilizando int multiplicación

pensé que yo podría declarar, por ejemplo:

dup :: Stack (a :%: b) -> Stack (a :%: b :%: b) 
int2double :: Stack (a :%: SInt) -> Stack (a :%: SDouble) 

y así sucesivamente. Pero entonces no sé cómo generar el código y calcular el tamaño de la pila.

¿Es posible hacerlo así? ¿Y sería simple/conveniente/vale la pena?

Answer 1

Ver Chris Okasaki de "Técnicas para la Incorporación de Postfix Idiomas en Haskell": http://www.eecs.usma.edu/webs/people/okasaki/pubs.html#hw02

Además, este:

{-# LANGUAGE TypeOperators #-} 
module Stacks where 

data a :* b = a :* b deriving Show 
data NilStack = NilStack deriving Show 

infixr 1 :* 

class Stack a where 
    stackSize :: a -> Int 

instance Stack b => Stack (a :* b) where 
    stackSize (_ :* x) = 1 + stackSize x 

instance Stack NilStack where 
    stackSize _ = 0 

push :: Stack b => a -> b -> a :* b 
push = (:*) 

pop :: Stack b => a :* b -> (a,b) 
pop (x :* y) = (x,y) 

dup :: Stack b => a :* b -> a :* a :* b 
dup (x :* y) = x :* x :* y 

liftBiOp :: Stack rest => (a -> b -> c) -> a :* b :* rest -> c :* rest 
liftBiOp f (x :* y :* rest) = push (f x y) rest 

add :: (Stack rest, Num a) => a :* a :* rest -> a :* rest 
add = liftBiOp (+) 

{- 
demo: 

*Stacks> stackSize $ dup (1 :* NilStack) 
2 

*Stacks> add $ dup (1 :* NilStack) 
2 :* NilStack 

-} 

Desde su pila varía en tipo, no se puede empaquetar en un estado normal mónada (aunque puedes empacarla en una mónada parametrizada, pero esa es una historia diferente), pero aparte de eso, esto debería ser directo, agradable y estático.

Answer 2

Creo que esto debería ser posible sin problemas, pero se tropieza con problemas cada vez que intenta hacer algo en un ciclo. Entonces necesitas cosas tan divertidas como los números naturales a nivel de tipo. Considere una función como esta:

popN :: Int -> Stack (?????) 

Pero si no necesita tales cosas, puede hacer lo que quiera. Por cierto, los bucles solo funcionan si la cantidad de elementos es la misma antes y después, de lo contrario no se compilará. (Tipo A-la infinito).

Puede intentar solucionar esto usando clases-tipo, pero supongo que para lo que intenta hacer es mejor usar un lenguaje con tipos dependientes.

Answer 3

Esto puede ser de interés para usted:

https://github.com/gergoerdi/arrow-stack-compiler/blob/master/StackCompiler.hs

Es un ensamblador simple que mantiene tamaño de la pila en su tipo. P.ej. las dos firmas siguientes indican que binOp, dado el código que funciona en dos registros y deja el tamaño de la pila como está, crea un código que saca dos argumentos de la pila y empuja el resultado. compileExpr usa binOp y otras construcciones para crear código que evalúa una expresión y la empuja hacia la parte superior de la pila.

binOp :: (Register -> Register -> Machine n n) -> Machine (S (S n)) (S n) 
compileExpr :: Expr -> Machine n (S n) 

Tenga en cuenta que esto es sólo una prueba de concepto-haciendo el tonto-en torno cosa, sólo he subido a GitHub ahora a mostrar, así que no espere encontrar algo grande en ella.

Answer 4

¿Simple y conveniente? No estoy seguro.

Comenzaré con la descripción del problema. La tarea es pasar de una informal a una especificación que esté más cerca de lo que tenemos en Haskell (tipos).

Aquí hay dos problemas: imponer invariantes basados ​​en el tipo en el idioma de entrada (expresiones aritméticas?) Y asegurarse de que la expresión del lenguaje de origen compilada en un programa de máquina de pila realmente está haciendo lo que queremos.

La primera se puede abordar fácilmente usando GADT: simplemente necesita indizar expresiones por sus tipos (por ejemplo, Expr a es para expresiones que evalúan a un valor de tipo a).

El segundo, no tan seguro. Por supuesto, puede indexar las listas por tipos de nivel natural (utilizando GADT, por ejemplo). Los tipos de ciertas funciones en las listas (como la cabeza y la cola) se vuelven lo suficientemente precisas para que podamos hacerlas totales. ¿Es homogénea una pila de su máquina de pila (es decir, contiene solo enteros o solo dobles o ...)?

Otras propiedades pueden codificarse (y aplicarse) también, pero seguir esta ruta puede requerir un esfuerzo considerable por parte del programador.