Typed Holes in Scala?

Question

Haskell offers typed holes.

Example:

f :: Int -> String -> Bool
f x y = if (x > 10) then True else (g y)

g :: String -> Bool
g s = _

Compilation:

Prelude> :l HoleEx.hs
[1 of 1] Compiling Main             ( HoleEx.hs, interpreted )

HoleEx.hs:6:7:
    Found hole `_' with type: Bool
    Relevant bindings include
      s :: String (bound at HoleEx.hs:6:3)
      g :: String -> Bool (bound at HoleEx.hs:6:1)
    In the expression: _
    In an equation for `g': g s = _
Failed, modules loaded: none.

When programming in Scala, I typically use ??? as placeholders in my Scala code that I've not yet written.

However, using typed holes appears to be more powerful to me. Note that I could replace the above else (g y) with else (g 55), yet I'd get a compile-time error:

Prelude> :l HoleEx.hs
[1 of 1] Compiling Main             ( HoleEx.hs, interpreted )

HoleEx.hs:3:39:
    Couldn't match type `Int' with `[Char]'
    Expected type: String
      Actual type: Int
    In the first argument of `g', namely `x'
    In the expression: (g x)
Failed, modules loaded: none.

Although I can use ??? in Scala to get placeholder implementations to compile, unlike holes, I'll get run-time errors with ???.

scala> def g(x: Int): Int = ???
g: (x: Int)Int

scala> g(5)
scala.NotImplementedError: an implementation is missing

Does Scala have typed holes?

Answer 1

For me a hole in a program helps me progress the implementation. It does that by telling me what type I need next. You can get something a little like that by triggering a regular Scala type error.

The trick is to define a type you know will be wrong, and then use it. For example:

object hole

You can then use that in code and you'll get an appropriate type error:

The error here is telling me the "hole" needs to be a B, suggesting I can progress by using g in some way. And if I progress the code to a => f(g(hole)) the compiler will tell me the hole needs to be an A.

That's a kind of hole, but unlike other languages (Idris etc)...

• my program is just not compiling, rather than having a recognized hole as such;
• there's no help to tell me the types in scope (although IDE code completion my give some suggestions);
• I can't nicely name a hole;
• I can't automatically lift a hole to a function definition;
• I can't automatically solve the hole (as Idris can, sometimes);
• I must type the expected return value, otherwise Scala will infer that hole is an acceptable type!
• ...and probably many other features.

As you say ??? is a useful placeholder, but it has type Nothing -- which means the program compiles, but it doesn't help you fill in the implementation. At least object hole, although kind of trivial, does give you some type information to progress.