My working definition for value is a special kind of expression that evaluates to itself. So 1 is a value, and 1 + 1 is valuable but not a value because it evaluates to 2.
A datatype constructor like SOME has type 'a -> 'a option in the SMLNJ REPL, but I don't think it's strictly a function. Is it?
Since SOME and SOME 1 are both valuable expressions that evaluate to themselves (can't be reduced), are they considered values too? Is SOME guaranteed to be total, meaning given a value x : 'a, SOME x reduces to a value? That is trivially true if SOME x is a value itself.
The short answer is yes.
A constructor like SOME is a function, even though it is not a λ-function but rather a function constant. Though, if you prefer to uniformly have all functions as lambdas, you can view SOME without arguments as a shorthand for its η-expansion fn x => SOME x, assuming the constructor application SOME x is a special construct instead of a regular application. And that is indeed how a compiler will typically translate such a use.