在Haskell中使用幻像类型验证程序的正确性

Question

假设我正在使用堆栈机器的代码,它可以在整数和双精度上执行一些简单的操作(推送常量,添加,mul,dup,交换,弹出,转换类型).

现在,我正在编写的程序采用其他语言进行描述,并将其转换为此堆栈计算机的代码.我还需要计算堆栈的最大大小.

我怀疑可以使用Haskell类型检查器来消除一些错误,例如:

• 从空堆栈弹出
• 使用int乘法乘以双精度数

我以为我可以声明,例如:

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

等等.但后来我不知道如何生成代码并计算堆栈大小.

有可能这样做吗？它会简单/方便/值得吗？

Answer 1

请参阅Chris Okasaki的"在Haskell中嵌入Postfix语言的技巧":http://www.eecs.usma.edu/webs/people/okasaki/pubs.html#hw02

这个:

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

-}

由于您的堆栈类型不同,您无法将其打包成常规状态monad(虽然您可以将其打包成参数化monad,但这是一个不同的故事)但除此之外,这应该是直截了当,愉快和静态检查.

Answer 2

您可能会对此感兴趣:

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

它是一个简单的汇编程序,可以保持其类型的堆栈大小.例如,以下两个签名表明binOp,给定代码在两个寄存器上工作并按原样保留堆栈大小,创建从堆栈弹出两个参数并推送结果的代码.compileExpr使用binOp和其他构造来创建用于计算表达式并将其推送到堆栈顶部的代码.

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

请注意,这只是一个概念验证的蠢事,我现在只是将它上传到GitHub给你看,所以不要指望找到任何好的东西.