Is it possible to implement a stack with only lambda expressions?
This might not be a very practical problem, I'm just wondering if I can implement a stack with only lambda expressions.
Stack supports three operations: top
, pop
and push
. So I start by defining the stack as a 3-tuple:
data Stack a = Stack a (a -> Stack a) (Stack a)
| Empty
Here Empty
stands for empty stack, so we have at least one inhabitant to start with.
In this definition, eveything looks good, except for the operation push
:
import Control.Monad.State
import Control.Monad.Writer
import Data.Maybe
data Stack a = Stack a (a -> Stack a) (Stack a)
| Empty
safePop :: Stack a -> Maybe (Stack a)
safePop Empty = Nothing
safePop (Stack _ _ s) = Just s
safeTop :: Stack a -> Maybe a
safeTop Empty = Nothing
safeTop (Stack x _ _) = Just x
push :: a -> Stack a -> Stack a
push x s = _
stackManip :: StateT (Stack Int) (Writer [Int]) ()
stackManip = do
let doPush x = modify (push x)
doPop = do
x <- gets safeTop
lift . tell . maybeToList $ x
modify (fromJust . safePop)
return x
doPush 1
void doPop
doPush 2
doPush 3
void doPop
void doPop
main :: IO ()
main = print (execWriter (execStateT stackManip Empty))
So when I fill in the code, I have to run it and get something like [1,3,2]
However, I find myself now expanding the definition push
:
push
should build a new stack, with the first element being the element that is simply pushed onto the stack, and the third being the current stack:
push :: a -> Stack a -> Stack a
push x s = Stack x _ s
To fill the hole, we need a created stack, so I need to express an expression:
push :: a -> Stack a -> Stack a
push x s = let s1 = Stack x (\x1 -> Stack x1 _ s1) s
in s1
To fill a new hole, I need another let-expression:
push :: a -> Stack a -> Stack a
push x s = let s1 = Stack x (\x1 ->
let s2 = Stack x1 _ s1
in s2) s
in s1
So you can see there is always a hole in my definition push
, but I am expanding it.
I kind of understand the magic behind Data.Function.fix
, and I think there might be some similar magic applied here, but she can't figure it out.
I'm curious
- Is it possible?
- If so, what's the magic behind that?
source to share
You can fully implement it with function types using the encoding in Church:
{-# LANGUAGE Rank2Types #-}
newtype Stack a = Stack (forall r. (a -> Stack a -> r) -> r -> r)
cons :: a -> Stack a -> Stack a
cons x (Stack f) = Stack (\g nil -> _)
peek :: Stack a -> Maybe a
peek (Stack f) = f (\x _ -> Just x) Nothing
This suggests that a Stack
is a function that takes a function that takes the top item and the rest of the stack as arguments. The second argument to the function Stack
is the default value, which is used if the stack is empty. I implemented the function peek
, but I left it cons
, and the rest is as an exercise (let me know if you need more help. Also you leave in the underscore I put in cons
, the GHC will tell you what type it expects and lists some possibly relevant bindings ).
The type of rank-2 says that with a Stack a
we can give it a function that returns any value type not limited to the type variable a
. This is convenient because we don't want to work with the same type. Consider a stack of lists, and we want to use a function in Stack
to get the length of the top element. More importantly, it says that a function like cons
this cannot manipulate the result in any way. It should return the type value r
it gets from the function (or from the default if the stack is empty), unchanged.
Another good exercise is to implement toList :: Stack a -> [a]
and fromList :: [a] -> Stack a
and show that these two functions form an isomorphism (which means that they are inverse of each other).
In fact, as far as I know, all Haskell data types have a representation as church coding. You can see the three main ways of combining types (sum types, product types and "type recursion") in action in this type Stack
.
source to share
The result push
is exactly what you want to keep push
ing, so you can bind the node like this:
push :: a -> Stack a -> Stack a
push x s = let s' = Stack x (flip push s') s in s'
If you want to bind a knot with Data.Function.fix
, you can transform the above definition like this:
push :: a -> Stack a -> Stack a
push x s = fix $ \s' -> Stack x (flip push s') s
source to share