驗證使用虛擬類型在Haskell程序的正確性

想我對整數和雙打堆棧機的代碼，它可以做一些簡單的操作（推不變，加，MUL，DUP，掉期，流行音樂，進行類型轉換）工作。驗證使用虛擬類型在Haskell程序的正確性

現在我正在寫程序都將在其他一些語言的描述，並將其轉換成代碼對於這種疊層機。我也需要計算堆棧的最大尺寸。

我懷疑這是可以使用Haskell的類型檢查，以消除一些錯誤，例如：

從空堆棧彈出
倍增雙打使用INT乘法

我認爲我可以申報，例如：

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

等等。但後來我不知道如何生成代碼和計算堆棧大小。

是否有可能做這樣的嗎？它會是簡單/方便/值得嗎？

來源

2011-01-26 mik01aj

你是什麼意思「但是我不知道如何生成代碼和計算堆棧大小。」 – 2011-01-26 14:57:32

我認爲這些類型會使得傳遞結果更難 - 例如，我將能夠編寫`do {pushInt 2; DUP; addInts}`？ – mik01aj 2011-01-26 16:09:05

見克里斯·奧卡薩基的「爲嵌入在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，但這是一個不同的故事），但除此之外，這應該是簡單，愉快和靜態檢查。

來源

2011-01-26 20:08:39 sclv

我想這應該是可能沒有問題，但你遇到問題，只要你嘗試做一些在一個循環。比你需要類型級自然數這樣有趣的東西。考慮這樣的功能：

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

但是，如果你不需要這樣的事情，感覺自由地做任何你想要的。順便說一句，循環只有在元素數量相同之前和之後都是一樣的，否則它不會編譯。（A-la無限型）。

你可以嘗試解決此使用類型類，但我猜你嘗試做最好使用與依賴的類型，而不是一門語言是什麼。

來源

2011-01-26 13:32:05 fuz

這可能是你的興趣：

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上剛纔給你看，所以不要指望找到任何在它的偉大。

來源

2011-01-26 15:10:29 Cactus

簡單方便？我不確定。

我會從問題描述開始。我們的任務是從一個非正式的規範變成一個更接近Haskell（類型）的規範。

有兩個問題在這裏：執行輸入語言基於類型的不變量（算術表達式？），並確保編譯成堆棧機程序的源語言表達其實就是做我們想要的。使用GADTs可以輕鬆解決第一個問題：您只需要根據類型對錶達式進行索引（例如，Expr a用於評估類型a值的表達式）。

第二，不太確定。當然，您可以按類型級別的自然數（例如使用GADT）來索引列表。列表上某些函數的類型（例如頭部和尾部）然後變得足夠精確，以至於我們可以使它們成爲總數。堆棧機器的堆棧是否是同質的（即，只包含整數或僅包含雙精度或...）？

其他屬性也可以編碼（並強制執行），但走這條路線可能需要編程人員付出相當大的努力。

來源

2011-01-26 16:52:24

驗證使用虛擬類型在Haskell程序的正確性

回答

相關問題