La verificación de programa de corrección utilizando fantasma de tipos de Haskell

Question

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

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

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

• surgiendo de una pila vacía
• multiplicando dobles con int multiplicación

Pensé que podría declarar, por ejemplo:

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

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

Es posible hacer esto de esta manera?Y sería simple/conveniente/la pena?

Answer 1

Vea las "Técnicas de Chris Okasaki para incorporar idiomas postfix en Haskell": http://www.eecs.usma.edu/webs/people/okasaki/pubs.html#hw02

También esto:

{-# 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

-}

Dado que su pila varía en el tipo, no puede empacarla en una mónada estatal regular (aunque puede empacarla en una monada parametrizada, pero esa es una historia diferente) pero aparte de eso, esto debería ser sencillo, agradable y estáticamente verificado .

Answer 2

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 el tamaño de la pila en su tipo. Por ejemplo, las siguientes dos firmas indican que binOp, dado el código que funciona en dos registros y deja el tamaño de la pila como es, crea un código que saca dos argumentos de la pila y empuja el resultado. compileExpr usos binOp y otras construcciones para crear código que evalúa una expresión y la empuja encima 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 solo una cosa de prueba de concepto que lo he subido, solo lo he subido a Github hace un momento para mostrarle, así que no espere encontrar nada genial en él.

Answer 3

Simple y conveniente?Yo estoy seguro.

Me gustaría empezar con la descripción del problema.La tarea es ir desde un informal en una especificación que está más cerca de lo que tenemos en Haskell (tipos).

Hay dos problemas aquí:cumplimiento de tipo basada en invariantes en el idioma de entrada (expresiones aritméticas?) y asegurarse de que el origen de la expresión del lenguaje compilado en una pila de la máquina de programa realmente está haciendo lo que queremos.

La primera puede ser fácilmente abordado el uso de GADTs:usted necesita simplemente índice de expresiones por sus tipos (por ejemplo, Expr es a las expresiones que se evalúa como un valor de tipo a).

La segunda, no estoy tan seguro acerca de.Usted puede, por supuesto, el índice de listas por tipo de nivel de naturales (utilizando GADTs, por ejemplo).Tipos de ciertas funciones sobre listas (como la cabeza y la cola), a continuación, convertirse en lo suficientemente precisos que nos pueden hacer total.Es una pila de la pila de la máquina homogéneo (es decir, contiene sólo números enteros o solo duplica o ...)?

Otras propiedades pueden ser codificados (y forzada), pero ir por esta ruta puede requerir un esfuerzo considerable por parte del programador.

Answer 4

Creo que esto debería ser posible sin problemas, pero te encuentras con problemas cada vez que intentas hacer algo en un bucle. De lo que necesitas cosas tan divertidas como números naturales de nivel de tipo. Considere una función como esta:

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

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

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