F# - Restricting Discriminated Union case in function input

Question

Let's say I'm trying to build a simple Stack in F# as follows:

type Stack =
| Empty
| Stack of String list

(I know I can define it recursively but for this example, let's assume I'd like to have a list in there)

Then I define a push operation like this:

let push item deck =
    match deck with
    | Empty -> Stack [item]
    | Stack d -> Stack (item::d)

But when I reach the pop operation... I'm not having success. I wanted to do something like this:

let pop (Stack d) =
    match d with
    | h::[] -> h,Empty
    | h::t -> h,(Stack t)

For now, let's also try to ignore the fact that I might want a peek/pop pair of operations instead of returning a tuple. What I wanted to try was to write a pop operation which would only accept a Stack which is not empty in the first place.

In other words, I only wanted this function to accept one of the cases of the Discriminated Union. However, I immediately get the warning: "Incomplete pattern matches on this expression. For example, the value 'Empty' may indicate a case not covered by the pattern(s)'.

As expected (after the warning), the following code:

let empty = Empty
let s,st = pop empty

... compiles and fails at run time. I wanted it to fail at compile time.

I'm aware I could use other options for this, such as:

let pop stack =
    match stack with
    | Empty -> None, Empty
    | Stack (h::[]) -> Some h,Empty
    | Stack (h::t) -> Some h,(Stack t)

or:

let pop stack =
    match stack with
    | Empty -> Error "Empty Stack"
    | Stack (h::[]) -> Ok (h,Empty)
    | Stack (h::t) -> Ok (h,(Stack t))

(and on both of these cases I might not even need the Empty case at all...)

But I was trying to make something more restrictive. So... what am I missing here? Is there a way to achieve what I was attempting? Does it even make any sense to want that?

Fyodor Soikin Fyodor Soikin · Accepted Answer · 2018-08-11T13:50:19

Think about what you're trying to achieve carefully. Consider the following function:

let foo (s: Stack) = pop s

Should foo compile or should it be rejected? Think about it.

I will assume here that you have already thought about it, and offered the only reasonable answer: the "restriction" that you seek should now apply to foo as well. That is, whoever calls foo must also supply only non-empty stack.

Ok, fair enough. But let's go all the way to the turtles:

let main argv = 
    printf "Provide directive: "

    let s = 
        match Console.ReadLine() with
        | "empty" -> Empty
        | _ -> Stack [1; 2; 3]

    let p = pop s

    0

Now should this program compile or be rejected? Obviously, it depends on the user input. The type of the program depends on runtime values. This is actually an active area of research, and there is a name for it: such program is called Dependently Typed. In plain terms it's when values (may) carry types with them, but unlike .NET RTTI, the compiler has visibility into those types and can prove things about their relationships. Fascinating stuff.

F#, for better or worse, doesn't support dependent types, and probably never will.

Now, I will assume that you're ok with not having dependent types, and would like instead to have your "restriction" only for cases when it is definitely known (at compile time) that the stack is not empty.

If this is the case, then your problem is easily solvable by splitting your DU in two:

type NonEmptyStack<'a> = NonEmptyStack of top: 'a * rest: 'a list
type Stack<'a> = Empty | NonEmpty of NonEmptyStack<'a>

let push item stack =
    match stack with
    | Empty -> NonEmptyStack (item, [])
    | NonEmpty (NonEmptyStack (top, rest)) -> NonEmptyStack (item, top::rest)

let pop (NonEmptyStack (top,rest)) = 
    match rest with
    | i::tail -> (top, Stack (NonEmptyStack (i, tail)))
    | _ -> (top, Empty)

Notice how push always returns a non-empty stack, and pop accepts only non-empty stack. The types encode the meaning. This is what they're supposed to do.

F# - Restricting Discriminated Union case in function input

2 Answers