Fancy Haskell advice: Add recursion to a strongly-typed stack machine

Learn
1

Hi all, I’ve built a small stack machine that uses the type system to guarantee no stack underflow:


data FreeCat k a b where
  End :: FreeCat k a a
  (:*) :: k a b -> FreeCat k b c -> FreeCat k a c

infixr 5 :*

(<:>) :: FreeCat k a b -> FreeCat k b c -> FreeCat k a c
End       <:> ys = ys
(x :* xs) <:> ys = x :* (xs <:> ys)

infixr 5 <:>

data Instr a b where
  And    ::                                           Instr ('S ('S n))   ('S n)
  Add    ::                                           Instr ('S ('S n))   ('S n)
  Eq     ::                                           Instr ('S ('S n))   ('S n)
  Dup    ::                                           Instr ('S n)        ('S ('S n))
  Swap   ::                                           Instr ('S ('S n))   ('S ('S n))
  Push   :: Int ->                                    Instr n             ('S n)
  Pop    ::                                           Instr ('S n)        n
  Branch :: FreeCat Instr a b -> FreeCat Instr a b -> Instr ('S a)        b

exec1 :: Instr a b -> Vec a Int -> Vec b Int
exec1 And      (x ::: y ::: zs)  =                   x .&. y ::: zs
exec1 Add      (x ::: y ::: zs)  =                     x + y ::: zs
exec1 Eq       (x ::: y ::: zs)  = (if x == y then 1 else 0) ::: zs
exec1 Dup      (      n ::: as)  =                   n ::: n ::: as
exec1 Swap     (x ::: y ::: zs)  =                   y ::: x ::: zs
exec1 (Push x)              zs   =                         x ::: zs
exec1 Pop      (      _ ::: zs)  =                               zs
exec1 (Branch t f) (x ::: zs)
  | x == 0    = exec t zs
  | otherwise = exec f zs

exec :: FreeCat Instr a b -> Vec a Int -> Vec b Int
exec End        zs = zs
exec (i :* is)  zs = exec is (exec1 i zs)

This is my implementation of nth Fibonacci:

fib :: FreeCat Instr ('S n) ('S n)
fib =                           -- [n]
  Dup :*                        -- [n, n]
  Branch                        -- [n]
    End -- n == 0              
    ( Dup :*                    -- [n, n]
      Push 1 :*                 -- [n, n, 1]
      Eq :*                     -- [n, n==1]
      Branch                    -- [n]
        ( Dup :*                -- [n, n]
          Push (-1) :*          -- [n, n, -1]
          Add :*                -- [n, n-1]
          fib <:>               -- [n, fib(n-1)]
          Swap :*               -- [fib(n-1), n]
          Push (-2) :*          -- [fib(n-1), n, -2]                
          Add :*                -- [fib(n-1), n-2]
          fib <:>               -- [fib(n-1), fib(n-2)]
          Add :*                -- [fib(n)]
          End
        ) 
        End :* -- n == 1
      End
    )
  :* End

As you can see, recursion is possible, but only by exploiting Haskell’s laziness.

The program representation is essentially a tree, albeit a laziliy unfolded infinite tree where the recursion is concerned.

The drawback to this is that many analyses become impossible, at least without sharing-detection hacks.

How can I explicity encode looping structure? I’d like to move this closer to how actual assembler instructions are laid out.

I could have a constructor

Loop :: FreeCat Instr n ('S n) -> Instr ('S n) n

that cycles as long as the stack is topped with zero, but that means the input and output will always need to have the same number of args. I’m looking to enable the recursion pattern where the stack grows as the recursion descends.

I’m open to exploring deeper down the categorical hierarchy, and changing the kind of the params, e.g. to encode multiple possible stacks.

Any suggestions on this question, or other feedback on this design, is most welcome!

2 Likes
2

Perhaps

Loop
  :: Proxy m
  -> (forall l. FreeCat Instr (S     l) (S m + l))
  -> (forall l. FreeCat Instr (S m + l) (S     l))
  -> Instr (S n) (S n)

This carries some state through each step, grows the stack until that state satisfies some condition, then crunches it back down.

3

Nice idea, @Leary. I can see that working.

That would, however, enforce quite a lot of awkwardness in the way programs are written. I’m trying to keep fairly close to how asseembly language is structured (while still beig able to get nice guaranteed properties).

One of the goals of this exercise for me is to get deeper insight into the categorical structure of assembly language.

4

One idea is to add functions to your language. Parameterize Instr with a type of “function names”

data Instr (f :: Nat -> Nat -> Type) a b where
  ...
  Call :: f a b -> Instr f (a + n) (b + n)

A complete program must then associate a block of instructions to every function name:

type Program f = forall a b n. f a b -> FreeCat (Instr f) (a + n) (b + n)

You can also use a more concrete representation for introspection.

The interpreter is then parameterized by the full program to be called when interpreting Call.

exec1 :: Program f -> Instr f a b -> Vec a Int -> Vec b Int
exec1 prog (Call f) zs = prog f zs
5

That looks interesting, but I don’t understand it. Can you elaborate?

6

To give you an example, here’s fibonacci. The interface is given by a GADT: there is one function Fib. Then the program pattern-matches on that name and returns its instructions. Instead of making a direct recursive call to fib, use the Call Fib instruction to let the interpreter make that call.

data Fib a b where
  Fib :: Fib (S Z) (S Z) -- one input, one output

fib :: Program Fib
fib Fib =                           -- [n]
  Dup :*                        -- [n, n]
  Branch                        -- [n]
    End -- n == 0              
    ( Dup :*                    -- [n, n]
      Push 1 :*                 -- [n, n, 1]
      Eq :*                     -- [n, n==1]
      Branch                    -- [n]
        ( Dup :*                -- [n, n]
          Push (-1) :*          -- [n, n, -1]
          Add :*                -- [n, n-1]
          Call Fib <:>               -- [n, fib(n-1)]
          Swap :*               -- [fib(n-1), n]
          Push (-2) :*          -- [fib(n-1), n, -2]                
          Add :*                -- [fib(n-1), n-2]
          Call Fib <:>               -- [fib(n-1), fib(n-2)]
          Add :*                -- [fib(n)]
          End
        ) 
        End :* -- n == 1
      End
    )
  :* End
2 Likes
7

See also the paper Turing Completeness Totally Free by Conor McBride for more on this approach to recursion.

1 Like