CODEWITHSUNDEEP
haskelllambda-calculus
Javran
Javran

Reputation: 3434

Is that possible to implement a stack with lambda expressions only?

This might not be a very practical problem, I'm just curious if I can implement a stack with only lambda expressions.

A stack supports 3 operations: top, pop and push, So I begin with defining the stack to be a 3-tuple:

data Stack a = Stack a (a -> Stack a) (Stack a)
             | Empty

Here Empty stands for the empty stack so we at least have one inhabitant to begin with.

Under this definition, eveything looks good except for push operation:

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 complete the code, I should be able to run it and get something like [1,3,2]

However, I find myself expanding the definition of push infintely:

push should construct a new stack, with first element being the item just pushed onto the stack and third element the current stack:

push :: a -> Stack a -> Stack a
push x s = Stack x _ s

To fill in the hole, we need the stack being created, so I need a let-expression:

push :: a -> Stack a -> Stack a
push x s = let s1 = Stack x (\x1 -> Stack x1 _ s1) s
           in s1

To fill in the 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 that there's always a hole in my push definition however I expand it.

I kind of understand the magic behind Data.Function.fix and guess some similiar magic can be applied here, but can't figure that out.

I'm wondering

Upvotes: 3

Views: 150

Answers (2)

David Young
David Young

Reputation: 10793

You can implement it entirely using function types with a Church encoding:

{-# 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 says that a Stack is a function that takes a function which takes the top element and the rest of the stack as its arguments. The Stack function's second argument is a default that is used if the stack is empty. I implemented the peek function but I left cons and the rest as an exercise (let me know if you need more help. Also, you leave in the underscore I put in cons, GHC will tell you what type it expects and list some possibly relevant bindings).

The rank-2 type is says that, given a Stack a, we can give it a function that returns any type of value, unconstrained by the a type variable. This is handy because we might not want to work with the same type. Consider a stack of lists and we want to use the function in Stack to get the length of the top element. More importantly, it says that a function like cons can't manipulate the result in any way. It must return the r type value it gets from the function (or from the default value, if the stack is empty), unchanged.

Another good exercise is to implement toList :: Stack a -> [a] and fromList :: [a] -> Stack a and show that those two functions form an isomorphism (meaning that they are inverses of each other).

In fact, as far as I know, all Haskell data types have a representation as a Church encoding. You can see three of the basic ways of combining types (sum types, product types and "type recursion") in action in this Stack type.

Upvotes: 7

Cactus
Cactus

Reputation: 27636

The result of push is exactly what you want to keep pushing to, so you can tie the knot 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 tie the knot via 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

Upvotes: 4

Related Questions