使用haskell中的幻影类型验证程序正确性

Question

假设我正在使用堆栈计算机的代码，该代码可以在INT和Doubles上执行一些简单的操作（按常数，添加，MUL，DUP，STAP，POP，CONST，CONST类型）。

现在，我正在编写的程序使用其他语言进行了描述，并将其转换为该堆栈计算机的代码。我还需要计算堆栈的最大尺寸。

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

• 从一个空堆栈中弹出
• 使用int乘法繁殖双打

我以为我可以声明，例如：

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

-}

由于您的堆栈在类型上有所不同，因此您不能将其包装到常规状态单元中（尽管您可以将其包装到参数化的单元中，但这是一个不同的故事），但是除此之外，这应该是直接，愉快的，宜人的和静态检查的。

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，以向您展示，所以不要期望在其中找到任何很棒的东西。

Answer 3

简便？我不确定。

我将从问题描述开始。任务是从非正式的任务转变为更接近我们在Haskell（类型）中的规范。

这里有两个问题：在输入语言（算术表达式？）上强制执行基于类型的不变性，并确保编译为堆栈机程序中的源语言表达式实际上是在做我们想要的。

第一个可以使用GADT轻松解决：您只需要按其类型索引表达式（例如，Expr a是评估A型值的表达式）。

第二，不太确定。当然，您可以按类型级的自然列表索引列表（例如，使用GADTS）。然后，列表（例如头部和尾巴）上的某些功能的类型变得足够精确，我们可以使其总计。您的堆栈堆栈是同质的（即仅包含整数还是双打或...）？

其他属性也可以编码（并执行），但是走这条路线可能需要大量的程序员努力。

Answer 4

我认为这应该没有问题，但是每当您尝试在循环中做某事时，您都会遇到问题。比您需要这样的有趣的事情，例如类型级的自然数。考虑这样的功能：

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

但是，如果您不需要这样的事情，请随时做任何您想做的事情。顺便说一句，循环仅在元素之前和之后的元素数量相同时起作用，Elseway不会编译。 （A-LA无限类型）。

您可以尝试使用类型类别来解决此问题，但是我想对于您尝试做什么，最好使用具有依赖类型的语言。