Suppose we're implementing an interpreter for the bytecode of some stack machine. Let every element of the stack be a Word8, and let the stack be represented by a list:
type Stack = [Word8]
We'll need opcodes for addition, subtraction, and unary negation. However, apart from acting on Word8s, we might want to treat the top two elements together as a Word16, and then the next two as another Word16, and then do something to those. To keep things simple:
data DataSize = OneByte | TwoBytes | FourBytes deriving (Eq, Ord, Read, Show)
data OpCode = ... | Add DataSize | Subtract DataSize | Negate DataSize | ...
deriving (Eq, Ord, Read, Show)
Add OneByte performs addition of Word8s, Add TwoBytes performs addition of Word16s, etc.
We'll use some monad to store the state of our computation. It doesn't really matter what we use, so we'll just represent it with M here. Our function to execute one instruction might be
exec :: OpCode -> M ()
and ideally we'd like to write
exec (Add size) = perform get2 (+) size
exec (Subtract size) = perform get2 (-) size
exec (Negate size) = perform get1 negate size
where perform get2 f size pops two objects of the given size, applies f to them, then pushes the result on the stack.
The question, now, is how close we can come to implementing perform. Intuitively, the type is something like
-- Stackable is some class of things we can push and pop.
-- c is any constraint. In the examples above, it would be num.
-- fn{a} is a type with one free variable a. Haskell does not allow
-- generalising this way, which is why I'm using the non-existent fn{a}
-- notation.
perform :: (forall a. (Stackable a, c a) => fn{a} -> Proxy a -> M ())
-> (forall a. c a => fn{a})
-> Size
-> M ()
For any choice of fn, this function is easily implemented:
perform act f = go
where go OneByte = act f (Proxy :: Proxy Word8)
where go TwoBytes = act f (Proxy :: Proxy Word16)
where go FourBytes = act f (Proxy :: Proxy Word32)
Unfortunately, we can't just say forall fn (nor, for that matter, forall c). Here's a solution I came up with to allow a single definition of perform in the presence of this. I've simplified a little to reduce the amount of code, so M is IO and we assume all values involved support plenty of operations.
{-# LANGUAGE RankNTypes, ConstraintKinds, TypeFamilies, EmptyDataDecls #-}
{-# LANGUAGE FlexibleInstances, ViewPatterns #-}
import Data.Proxy
-- This is the runtime value we'll use to decide what type we're operating on.
data DataSize = DSInt | DSDouble
-- I haven't found a way to support arbitrary constraints, so the solution
-- for now is to throw in a bunch that I know the types involved will support.
type SimpleNum a = (Num a, Eq a, Ord a, Read a, Show a)
-- We use this as a placeholder for a in the types
data Hole
-- This is meant to be something like a lambda on the type level.
-- fn should be a type with some "holes" in it, and Lambda fn a should
-- be isomorphic to the type with the holes filled with a.
data family Lambda fn a
data instance Lambda (Hole -> r) a = LambdaTakingHole { getLambdaTakingHole :: a -> Lambda r a }
data instance Lambda Hole a = LambdaHole { getLambdaHole :: a }
data instance Lambda (IO ()) a = LambdaIO { getLambdaIO :: IO () }
-- This is a helper typeclass to allow uniform conversion to and from
-- values of the form Lambda fn a. With the recursion going on, this makes
-- wrapping far easier.
class LambdaLike fn where
-- UnderlyingFun fn a is the type that Lambda fn a should be isomorphic to.
-- wrapf and unwrapf are the isomorphism.
type family UnderlyingFun fn a
wrapf :: UnderlyingFun fn a -> Lambda fn a
unwrapf :: Lambda fn a -> UnderlyingFun fn a
instance LambdaLike r => LambdaLike (Hole -> r) where
type UnderlyingFun (Hole -> r) a = a -> UnderlyingFun r a
wrapf f = LambdaTakingHole (wrapf . f)
unwrapf (LambdaTakingHole f) = unwrapf . f
instance LambdaLike Hole where
type UnderlyingFun Hole a = a
wrapf = LambdaHole
unwrapf = getLambdaHole
instance LambdaLike (IO ()) where
type UnderlyingFun (IO ()) a = IO ()
wrapf = LambdaIO
unwrapf = getLambdaIO
-- Here are some example functions we could write
-- These are given a specific instantiation of the function they need
-- to work with, and then a proxy to indicate the type involved.
runWith2 :: SimpleNum a => (Lambda (Hole -> IO ()) a) -> Proxy a -> IO ()
runWith2 (unwrapf -> f) _ = f 2
runWithUserInput :: SimpleNum a => (Lambda (Hole -> IO ()) a) -> Proxy a -> IO ()
runWithUserInput (unwrapf -> f) _ = getLine >>= f . read
runWith2andPrint :: SimpleNum a => (Lambda (Hole -> Hole) a) -> Proxy a -> IO ()
runWith2andPrint (unwrapf -> f) _ = print $ f 2
runWith2and5 :: SimpleNum a => (Lambda (Hole -> Hole -> IO ()) a) -> Proxy a -> IO ()
runWith2and5 (unwrapf -> f) _ = f 2 5
perform :: (forall a. SimpleNum a => Lambda fn a -> Proxy a -> IO ())
-> (forall a. SimpleNum a => Lambda fn a)
-> DataSize
-> IO ()
perform fn f = go
where go DSInt = fn f (Proxy :: Proxy Int)
go DSDouble = fn f (Proxy :: Proxy Double)
main = do
perform runWith2 (wrapf print) DSInt
perform runWith2 (wrapf print) DSDouble
perform runWith2andPrint (wrapf (+1)) DSInt
perform runWith2and5 (wrapf $ \x y -> print $ x + y) DSInt
perform runWith2and5 (wrapf $ \x y -> print $ x * y) DSDouble
Is this a good solution to the problem? Am I reinventing some wheel here?
