Why isn't this true/false implication function working in SML?

Question

val implies =
    fn x y = case x of false andalso case y of false => true
     | fn x y = case x of false andalso case y of true => true
     | fn x y = case x of true andalso case y of false => false
     | fn x y = case x of true andalso case y of true => true;  

I can't get this to compile. I'm relatively new to SML so not quite getting the general language and syntax. What have I done wrong?

Answer 1

There are various things wrong:

• There is no arguments in implies to do pattern matching directly.
• case x of is for pattern matching with specific values, not like if/else expression which accepts boolean expressions.
• The syntax for lambda should start with fn x => ....

A quick fix:

fun implies x y =
    case (x, y) of
      (false, false) => true
    | (false, true) => true
    | (true, false) => false
    | (true, true) => true

which can be rewritten for readability as:

fun implies false false = true
  | implies false true = true
  | implies true false = false
  | implies true true = true

or more concise by using propositional logic rule:

fun implies x y = (not x) orelse y

Answer 2

Regarding the anonymous functions,

fun implies x y = (not x) orelse y

can be written as

val implies = fn x => fn y => (not x) orelse y

however as you see, it doesn't really make any sense to do it this way (in this particular case).

Anonymous functions in SML only take one argument. Currying of arguments works because the fun keyword is syntactic sugar (also called a derived form) of

val rec implies = fn x => fn y =>
    case (x, y) of
      (x,y) => (not x) orelse y

The case is used because we could have had some pattern matching in the original function, which is then translated directly down into the case, and the rec is because the original function might have been recursive.

Thus the second example @pad gave is equivalent to:

val rec implies = fn x => fn y =>
    case (x, y) of
       (false, false) => true
     | (false, true) => true
     | (true, false) => false
     | (true, true) => true