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

Question

假设我正在使用堆栈机的代码，它可以对整数和 double 执行一些简单的操作(推送常量、加法、乘法、重复、交换、弹出、转换类型)。

现在我正在编写的程序采用其他语言的描述并将其翻译成该堆栈机的代码。我还需要计算堆栈的最大大小。

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

• 从空堆栈中弹出
• 使用 int 乘法将 double 相乘

我想我可以声明，例如:

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

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

这样可以吗？它会简单/方便/值得吗？

Answer 1

参见 Chris Okasaki 的“在 Haskell 中嵌入后缀语言的技术”: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 中，但这是一个不同的故事)，但除此之外，这应该是简单、愉快的，并进行静态检查。