Validating a program using phantom types in Haskell

Question

Suppose I work with a stack computer code that can perform some simple operations (push, add, mul, dup, swap, pop, convert types) on ints and double.

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

I suspect that you can use Haskell type checking to fix some errors, for example:

• popping out of an empty stack
• multiplication doubles using int multiplication

I thought I could declare, for example:

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

etc. But then I do not know how to generate the code and calculate the size of the stack.

Is it possible to do so? And will it be easy / convenient / worth it?

Answer 1

See Chris Okasaki's "Haskell Postfix Languages ​​Implementation Methods": http://www.eecs.usma.edu/webs/people/okasaki/pubs.html#hw02

In addition, these are:

 {-# 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 (fxy) 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 is different in type, you cannot 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, it should be simple, enjoyable, and statically checked.

Answer 2

This may interest you:

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

This is a simple assembler that supports the stack size of its type. For example. the following two signatures indicate that binOp , a given code that runs in two registers and leaves the as-is stack size, creates code that issues two arguments from the stack and pushes the result. compileExpr uses binOp and other constructors to create code that evaluates the expression and pushes it on top of the stack.

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

Please note that this is just proof that I just uploaded it to GitHub just to show you, so don't expect to find anything good in it.

Answer 3

Simple and convenient? I'm not sure.

I would start by describing the problem. The challenge is to move from the informal to the specification, which is closer to what we have in Haskell (types).

There are two problems here: forced inclusion of invariants based on input in the input language (arithmetic expressions?) And ensuring that the source language expression compiled into the stack computer program actually does what we want.

The first can be easily solved using GADT: you just need to index expressions by their types (for example, Expr a for expressions that evaluate to a value of type a).

Second, not so sure. Of course, you can, of course, index lists by type of straight (for example, using GADT). The types of certain functions in lists (for example, head and tail) become so precise that we can make them total. Is your stack machine stack homogeneous (i.e. it contains only integers or only doubles or ...)?

Other properties may be encoded (and forced), but this route may require significant effort on the part of the programmer.

Answer 4

I think this should be possible without problems, but you encounter problems when you try to do something in a loop. Than you need such fun things as natural type numbers. Consider the following function:

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

But if you don’t need such things, feel free to do whatever you want. BTW, loops only work if the number of elements is the same before and after, otherwise it will not compile. (A-la infinite type).

You can try to fix this using type classes, but I assume that you are trying to make it better to use a language with dependent types.