EOPL - 2.3.2 - Exercise 2.15

I solved this exercise in quite a "lispy" way, so it's a bit alien in F#. It works, but in a quite awkward way. The idea was to maintain the stack as a pair containing the current top element and the old stack, and this means that, in F#, each operation that adds or removes elements produces a stack with a different type than the original. An interesting consequence of this is that the stack size is reflected in its type, so that we could define functions that work on "stacks of size 3" or so on. Who needs dependent types? :)

So here's the code. It first defines a type synonym to ease working with stacks, and then the functions that implement basic operations.

type 'a stack = (unit -> 'a) * (unit -> bool)

let empty_stack () = 
    let top () = failwith "The stack is empty, no top element" in
    let is_empty_stack () = true in
    (top, is_empty_stack)

let push elt stk = 
    let top () = (elt, stk) in
    let is_empty_stack () = false in
    (top, is_empty_stack)
    
let pop stk = 
    let oldstk : 'a stack = snd ((fst stk) ()) in
    let top = fst oldstk in
    let is_empty_stack = snd oldstk in
    (top, is_empty_stack)
    
let is_empty_stack stk = 
    let empty = snd stk in empty ()
    
let top stk = 
    let t = fst stk in fst (t ())

And it is used like this: you must assign a type for the empty_stack call, otherwise you are nagged by the value restriction again. That's where the type synonym comes in handy:

> let (x : int stack) = (empty_stack());;

val x : int stack

Then you can push elements into x. Note how the type of the result is different from int stack, even considering type synonyms.

> push 3 x;;
val it : (unit -> int * int stack) * (unit -> bool)
       = (<fun:push@173>, <fun:push@174>)
> push 4 (push 3 x);;
val it : (unit -> int * 
            ((unit -> int * int stack) * (unit -> bool))) * 
         (unit -> bool) 
       = (<fun:push@173>, <fun:push@174>)
> 

If you pop elements, the types get back to what they were, obviously. A funny side-effect of this strange definition is that top and pop don't work on empty stacks because of type-checking, not any run-time checking -- so that the failwith in the definition of empty_stack will never be executed. Empty stacks have actually a different type.

There must be a more type-friendly implementation of stacks using a procedural representation, but I decided to leave it for now and publish this solution because it is quite interesting by itself (although almost unusable in real code).