Let's start with what you think is your basic requirement: the ability to define myFunc some way so that the following is done on the Scala console: the user provides literals. Then, perhaps if we can achieve this, we can try switching to varargs.
myFunc(List(1)) // no problem myFunc(List[Int]()) // compile error!
In addition, we do not want to force users to split the list into head and tail or convert them to :: .
Well, when we are given literals, since we have access to the syntax used to construct the value, we can use macros to verify that the list is not empty. In addition, there is already a library that will do this for us, namely refined !
scala> refineMV[NonEmpty]("Hello") res2: String Refined NonEmpty = Hello scala> refineMV[NonEmpty]("") <console>:39: error: Predicate isEmpty() did not fail. refineMV[NonEmpty]("") ^
Unfortunately, this is still problematic in your case, because you need to put refineMV in the body of your function, after which the literal disappears syntactically and the macromagic doesn't work.
OK, what about a general case that is syntax independent?
// Can we do this? val xs = getListOfIntsFromStdin() // Pretend this function exists myFunc(xs) // compile error if xs is empty
OK, now we are against the wall; there cannot be a compile-time error, since the code has already been compiled, but it is clear that xs may be empty. We will have to deal with this case at runtime, either with a type, or with Option and the like, or with something like runtime exceptions. But perhaps we can do a little better than just raise our hands up. There are two possible ways to improve.
- Somehow provide
implicit evidence that xs is not empty. If the compiler can find this evidence, then great! Otherwise, the user must provide it somehow at runtime. - Track the origin of
xs through your program and statically prove that it must be non-empty. If this cannot be proven, either a compile-time error or somehow forces the user to handle the empty case.
Once again, unfortunately, this is problematic.
- I strongly suspect that this is impossible (but this is still just a suspicion, and I would be happy if I were wrong). The reason is that, in the end, the
implicit resolution has type-directivity, which means that Scala gets the ability to perform type-level calculations by type, but Scala does not have a mechanism that, as I know, performs level-level calculations by values ( i.e. dependent typing). Here we require the latter, because List(1, 2, 3) and List[Int]() are indistinguishable at the type level. - You are now on an SMT-decisive land that has some efforts in other languages (hello Liquid Haskell !). Unfortunately, I do not know any such efforts in Scala (and I believe that in Scala it would be more difficult to complete the task).
The bottom line is that when checking for errors there is no free lunch . The compiler cannot magically force error handling to go away (although it can tell you when you don't need it), the best thing it can do is yell at you when you forget to process certain classes of errors, which in itself is very valuable. To emphasize the lack of a free lunch break, return a language that has dependent types (Idris) and see how it handles non-empty List values and a prototype function that breaks into empty lists, List.head .
First we get a compilation error in empty lists
Idris> List.head [] (input):1:11:When checking argument ok to function Prelude.List.head: Can't find a value of type NonEmpty []
Well, what about non-empty lists, even if they are confused by a couple of jumps?
Idris> :let x = 5 -- Below is equivalent to -- val y = identity(Some(x).getOrElse(3)) Idris> :let y = maybe 3 id (Just x) -- Idris makes a distinction between Natural numbers and Integers -- Disregarding the Integer to Nat conversion, this is -- val z = Stream.continually(2).take(y) Idris> :let z = Stream.take (fromIntegerNat y) (Stream.repeat 2) Idris> List.head z 2 : Integer
It works somehow! What if we really do not allow the Idris compiler to know anything about the amount that we pass and instead get it at runtime from the user? We explode with a really gigantic error message that starts with When checking argument ok to function Prelude.List.head: Can't find a value of type NonEmpty...
import Data.String generateN1s : Nat -> List Int generateN1s x = Stream.take x (Stream.repeat 1) parseOr0 : String -> Nat parseOr0 str = case parseInteger str of Nothing => 0 Just x => fromIntegerNat x z : IO Int z = do x <- getLine let someNum = parseOr0 x let firstElem = List.head $ generateN1s someNum -- Compile error here pure firstElem
Hmmm ... well, what is a signature like List.head ?
Idris> :t List.head -- {auto ...} is roughly the same as Scala implicit head : (l : List a) -> {auto ok : NonEmpty l} -> a
Ah, so we just need to provide a NonEmpty .
data NonEmpty : (xs : List a) -> Type where IsNonEmpty : NonEmpty (x :: xs)
Oh a :: . And we returned to the square.