Add a Java monad like in Eta

[Invisible-Rabbit-Hunter]

I really found the eta solution for object methods interesting, and thought that it would be nice to have a java monad like that in idris-jvm.

[okkero]

Please note that Idris has a stronger and richer type system than Eta, and that possible alternatives (for example, implementing a Java context/resource type for ST) should also be considered.

[Invisible-Rabbit-Hunter]

That is very much true... Hadn't thought of it until you wrote it.

[okkero]

By the way, a limited version of the Java monad from Eta should be fairly easy to implement, if you want it right now. Here is my take:

record Java a ret where
  constructor MkJava
  runJava : a -> JVM_IO ret
  
Functor (Java a) where
  map f (MkJava action) = MkJava ((map f) . action)
  
Applicative (Java a) where
  pure = MkJava . const . pure
  (<*>) (MkJava action1) (MkJava action2) =
    MkJava
      (\a => (action1 a) <*> action2 a)
      
Monad (Java a) where
  (>>=) (MkJava action) f =
    MkJava
      (\a => do
        ret <- action a
        let (MkJava action2) = f ret
        action2 a
      )
      
javaWith : a -> Java a ret -> JVM_IO ret
javaWith = flip runJava

io : JVM_IO ret -> Java a ret
io action = MkJava (const action)

withObject : a -> Java a ret -> Java b ret
withObject obj j =
  io $ javaWith obj j

See it in action: https://gist.github.com/okkero/97d816b72514670ff31f9cfc7fbe1eca