Verifying program correctness using phantom types in Haskell

Question

Suppose I'm working with code of a stack machine, which can do some simple operations (push constant, add, mul, dup, swap, pop, convert types) on ints and doubles.

Now the program I'm writing takes a description in some other language and translates it into code for this stack machine. I also need to calculate maximum size of the stack.

I suspect it's possible to use the Haskell type checker to eliminate some bugs, e.g.:

• popping from an empty stack
• multiplying doubles using int multiplication

I thought that I could declare, for example:

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

and so on. But then I don't know how to generate the code and calculate stack size.

Is it possible to do it like this? And would it be simple/convenient/worth it?

Answer 1

See Chris Okasaki's "Techniques for Embedding Postfix Languages in Haskell": http://www.eecs.usma.edu/webs/people/okasaki/pubs.html#hw02

Also, this:

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

-}

Since your stack varies in type, you can't pack it into a regular state monad (although you can pack it into a parameterized monad, but that's a different story) but other than that, this should be straightforward, pleasant, and statically checked.