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.

Answer 2

Simple and convenient? I'm unsure.

I'd start with the problem description. The task is to go from an informal one into a specification that is closer to what we have in Haskell (types).

There are two problems here: enforcing type-based invariants on the input language (arithmetic expressions?) and making sure that the source language expression compiled into a stack machine program is actually doing what we want.

The first can be readily tackled using GADTs: you merely need to index expressions by their types (e.g., Expr a is for expressions that evaluate to a value of type a).

The second, not so sure about. You can of course index lists by type-level naturals (using GADTs, for example). Types of certain functions on lists (such as head and tail) then become precise enough that we can make them total. Is a stack of your stack machine homogenous (that is, contains only integers or only doubles or ...)?

Other properties can be encoded (and enforced) as well, but going this route may require considerable effort on the part of the programmer.

Answer 3

I think this should be possible without problem, but you run into problems whenever you try to do something in a loop. Than you need such funny things like type-level natural numbers. Consider a function like this:

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

But if you don't need such things, feel free to do whatever you want. BTW, loops only work if the amount of elements is the same before and afterwards, elseway it won't compile. (A-la infinite type).

You could try to fix this using type-classes, but I guess for what you try to do it's better to use a language with dependent types instead.

Answer 4

This may be of interest to you:

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

It is a simple assembler that maintains stack size in its type. E.g. the following two signatures state that binOp, given code that works on two registers and leaves stack size as-is, creates code that pops two arguments from the stack and pushes the result. compileExpr uses binOp and other constructs to create code that evaluates an expression and pushes it on top of the stack.

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

Note that this is only a proof-of-concept goofing-around thing, I've only uploaded it to GitHub just now to show you, so don't expect to find anything great in it.