Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

jvm: make call* variadic in the unsafe interface #135

Merged
merged 13 commits into from
Nov 22, 2019
Merged

Conversation

mboes
Copy link
Member

@mboes mboes commented Nov 17, 2019

This PR is mutually exclusive with #133.

call previously took a list of JValue's. Using the dictionaries
embedded in each element, it could construct a MethodID. However, this
MethodID was not cached as well as one would hope, say when multiple
calls are made to the same method at the same argument types but
different values. Another problem was that all arguments to the method
had to be packed into a list and coerced into a JValue before being
passed to the method. This was syntactic overhead. The solution is to
make call, new and callStatic variadic, using the same GADT
solution as for variadic printf.

We now pass an extra spec argument to call. Like the format string in
printf, this argument determines how many more arguments need to be
passed to call. Example:

call obj "frobnicate" With3Args x y z

We no longer need to coerce x, y, z, nor pack them into a list.
Furthermore, this solution leads to decent error messages if arguments
are missing.

@facundominguez
Copy link
Member

facundominguez commented Nov 18, 2019

However, this MethodID was not cached as well as one would hope, say when multiple calls are made to the same method at the same argument types but different values.

Have you checked that the MethodID is actually cached? By looking at the code, it looks to me like the internal calls newJ, callToJValue and callStaticToJValue still receive a list ([JValue]), which makes impossible to compute the MethodID from the types of the arguments.

@mboes
Copy link
Member Author

mboes commented Nov 18, 2019

I had missed that part of the changes in #133, but we can do the same here. You changed callToJValue to accept a list singletons for each argument, in addition to the values. We can do the same here. We already have SingI ty dictionaries packed in each Arity constructor, because SingI ty is a superclass constraint of Coercible ty. Incidentally (again pinging @goldfirere, but as an FYI), binding type arguments in patterns would make that a lot more convenient.

@mboes mboes force-pushed the method-specs branch 2 times, most recently from 28105d2 to 9269909 Compare November 19, 2019 18:20
@mboes
Copy link
Member Author

mboes commented Nov 19, 2019

@facundominguez PTAL. I rewrote the patch with the following differences:

  • We reuse the code from Make the singletons of arguments to foreign calls depend only on types. #133 that keeps type singletons and arguments separate all the way through, so that MethodID's can be cached.
  • Arguments are no longer packed in tuples or lists, nor are extraneous "arity" specifications passed in. Similarly to what @goldfirere ach function is made variadic by making it a method of a private type class with instances for many arities. There is some Template Haskell code to generate these instances for us.

As noted in the commit message, the error messages are pretty much as good as they get. I shied away from using anything fancy like closed type families, for fear that the implementation detail would leak in error messages. The price to pay is more verbose instance implementations, but we have Template Haskell to write the boilerplate for us.

`call` previously took a list of `JValue`'s. Using the dictionaries
embedded in each element, it could construct a `MethodID`. However, this
`MethodID` was not cached as well as one would hope, say when multiple
calls are made to the same method at the same argument types but
different values. Another problem was that all arguments to the method
had to be packed into a list and coerced into a `JValue` before being
passed to the method. This was syntactic overhead. The solution is to
make `call`, `new` and `callStatic` variadic, using the same GADT
solution as for variadic `printf`.

Using ad hoc private type classes per function, we make them variadic up
to 32 arguments.

```haskell
call obj "frobnicate" x y z
```

We no longer need to coerce `x`, `y`, `z`, nor pack them into a list.
Furthermore, this solution leads to decent error messages. The private
type class should never appear in error messages. It's hard to think of
any example where the error message would be something else than "could
not deduce `Coercible a` ...". Which is good enough, since it's telling
us that you can pass anything you want to `call`, but it must be
coercible.
@facundominguez
Copy link
Member

I would expect New, Call and CallStatic to appear in error messages of

f :: Maybe Int32 -- or f ::Int32
f = callStatic "java.lang.Math" "abs" (0 :: Int32)

I don't have a problem with error messages of this sort, after all, I was already fine with the class JNIArguments in #133. "could not deduce Coercible a ..." is the most common error I'd expect in both cases.

As @goldfirere suggested, this might be possible to improve with TypeError

TH might not be possible to use in the safe interface yet. Last time I tried, TH didn't allow linear arrows.

Lastly, is this going to work with the safe interface, where we have an abstract monad instead of IO? That is the case that motivated @goldfirere to propose a closed type family.

@mboes
Copy link
Member Author

mboes commented Nov 19, 2019

I would expect New, Call and CallStatic to appear in error message

Why so?

In your example, the error message is:

   • Couldn't match expected type ‘IO Int32’
                  with actual type ‘Maybe Int32’

Which is exactly what it ought to be, in my view, because you're asking for the function to return something in the wrong monad. The type classes you mention are internal details that the user should, as much as possible, not have to worry about.

Lastly, is this going to work with the safe interface, where we have an abstract monad instead of IO?

I tried this, and it works. Even with an abstract monad, GHC does not see overlap in my tests. I kept things in IO for now though because that's an orthogonal change, and for consistency, because currently all the other functions are in IO.

Copy link

@goldfirere goldfirere left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I took a look through. It looks like this new approach works well. I hope you don't mind my small suggestions!

@@ -155,3 +160,20 @@ getStaticFieldAsJValue retsing cname fname = do
SPrim "double" -> JDouble <$> getStaticDoubleField klass field
SVoid -> fail "getStaticField cannot yield an object of type void"
_ -> JObject <$> getStaticObjectField klass field

mkVariadic :: TH.TypeQ -> (TH.TypeQ -> TH.TypeQ -> [TH.PatQ] -> TH.ExpQ -> TH.ExpQ -> TH.DecsQ) -> TH.DecsQ

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know the normal documentation standards in this code, but I would want more documentation here.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's an internal function that's only part of a separate module due to the stage restriction. Haddock won't help document the arguments of the continuation, but we can do that with a regular comment.

@@ -155,3 +160,20 @@ getStaticFieldAsJValue retsing cname fname = do
SPrim "double" -> JDouble <$> getStaticDoubleField klass field
SVoid -> fail "getStaticField cannot yield an object of type void"
_ -> JObject <$> getStaticObjectField klass field

mkVariadic :: TH.TypeQ -> (TH.TypeQ -> TH.TypeQ -> [TH.PatQ] -> TH.ExpQ -> TH.ExpQ -> TH.DecsQ) -> TH.DecsQ
mkVariadic retty k = fmap concat $ for [0..32 :: Int] $ \n -> do

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should 32 be a defined constant somewhere? Presumably, this number is the maximum number of arguments supported in variadic notation, and perhaps clients will want to query it.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed inline-java (which is a package downstream of jvm) currently duplicates the same constant (with a comment pointing here). I'll export a constant.

mkVariadic :: TH.TypeQ -> (TH.TypeQ -> TH.TypeQ -> [TH.PatQ] -> TH.ExpQ -> TH.ExpQ -> TH.DecsQ) -> TH.DecsQ
mkVariadic retty k = fmap concat $ for [0..32 :: Int] $ \n -> do
let -- Coercible type class and Ty associated type defined in downstream module.
coercible = TH.conT (TH.mkName "Coercible")

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This approach is quite fragile -- especially given that there may reasonably be the wrong Coercible in scope. It is possible to concretely specify the defining module, etc., for a name, even before it's in scope. See the mk_name_... functions in https://github.com/goldfirere/singletons/blob/master/src/Data/Singletons/Names.hs

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As noted above, mkVariadic should only be used in Language.Java.Unsafe, not anywhere else (and certainly not by the user). That said, if there is something more robust than mkName (which is only necessary because of stage restriction collateral damage), might as well. I noticed mkNameG_tc and friends in the template-haskell API docs, but they're not documented. What does it do, and how does it differ from mkName?

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Those functions make names tagged with a package and a module; mkName makes a name that unhygienically refers to whatever is in scope. I don't think mkNameG_tc was really meant to be exported from TH, but it works well in this scenario.

-- | Inject a value (of primitive or reference type) to a 'JValue'. This
-- datatype is useful for e.g. passing arguments as a list of homogeneous type.
-- Synonym for 'coerce'.
jvalue :: (ty ~ Ty a, Coercible a) => a -> JValue

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why have the ty type variable here?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is preexisting code that was moved earlier in the file because of the intervening splice leading to scoping errors. So I left it as-is. You're right that ty here serves no purpose. Probably a holdover from the past.

-- | Get the Java class of an object or anything 'Coercible' to one.
classOf
:: forall a sym. (Ty a ~ 'Class sym, Coercible a, KnownSymbol sym)
=> a
-> JNI.String
classOf x = JNI.fromChars (symbolVal (Proxy :: Proxy sym)) `const` coerce x

-- Unexported type classes.
class New r where

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You might want to consider exporting the class (but not the method). This will improve the Haddocks (where the class won't need to be written qualified) and clean up error messages that might happen to mention this class. I agree that it would be nice to avoid such error messages, but I'm sure some will slip through. The documentation should explain that it's an internal class, exported only for Haddocking and error messages. Ditto for other internal classes.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the class does end up leaking in error messages, then it would be better to export, I agree. The downside is that the documentation will end up bloated with 32 * 3 = 96 instances that aren't very interesting to the user. That's why I was trying to keep the class completely unexported. Interestingly, I find it pretty hard to get error messages that mention them. I haven't managed so far.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm, so when the return type is wrong, type errors frequently arise elsewhere before the compiler complains about lack of instances of class Call. But not always. So indeed, Call is leaking.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And, regardless, it will appear if a user says :t call in GHCi. Haskellers who see a variadic function will know that some cleverness lurks nearby, and I don't think they'll be too scared off. There might be a way to convince Haddock not to include the instances. On the other hand, seeing the instances will make it very clear what constraints will need to be satisfied by the arguments to call, if a user wants to take the time to piece all of this together.

@facundominguez
Copy link
Member

facundominguez commented Nov 19, 2019

Why so?

/home/centos/inline-java/tests/common/Language/Java/InlineSpec.hs:32:17: error:
    • No instance for (Language.Java.Unsafe.CallStatic
                         (Int32 -> Maybe ()))
        arising from a use of ‘callStatic’
        (maybe you haven't applied a function to enough arguments?)
    • In the expression:
        callStatic
          (fromString "java.lang.Math") (fromString "abs") (0 :: Int32)
      In an equation for ‘f’:
          f = callStatic
                (fromString "java.lang.Math") (fromString "abs") (0 :: Int32)
      In the second argument of ‘($)’, namely
        ‘do let f :: Maybe ()
                f = callStatic
                      (fromString "java.lang.Math") (fromString "abs") (0 :: Int32)
              return () :: IO ()’
   |        
32 |             f = callStatic (fromString "java.lang.Math") (fromString "abs") (0 :: Int32)
   |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^         
$ git diff
diff --git a/tests/common/Language/Java/InlineSpec.hs b/tests/common/Language/Java/InlineSpec.hs
index a26fe7f..ac55298 100644
--- a/tests/common/Language/Java/InlineSpec.hs
+++ b/tests/common/Language/Java/InlineSpec.hs
@@ -10,6 +10,7 @@
 module Language.Java.InlineSpec(spec) where
 
 import Data.Int
+import Data.String
 import Foreign.JNI (JVMException)
 import Language.Java
 import Language.Java.Inline
@@ -27,7 +28,9 @@ spec :: Spec
 spec = do
     describe "Java quasiquoter" $ do
       it "Can return ()" $ do
-        [java| { } |] :: IO ()
+        let f :: Maybe ()
+            f = callStatic (fromString "java.lang.Math") (fromString "abs") (0 :: Int32)
+        return () :: IO ()
 
       it "Evaluates simple expressions" $ do
         [java| 1 + 1 |] `shouldReturn` (2 :: Int32)

Using f :: Maybe Int32 or f :: Int32, gives me the same sort of error as well.

Copy link
Member Author

@mboes mboes left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@goldfirere thanks for the comments.

@@ -155,3 +160,20 @@ getStaticFieldAsJValue retsing cname fname = do
SPrim "double" -> JDouble <$> getStaticDoubleField klass field
SVoid -> fail "getStaticField cannot yield an object of type void"
_ -> JObject <$> getStaticObjectField klass field

mkVariadic :: TH.TypeQ -> (TH.TypeQ -> TH.TypeQ -> [TH.PatQ] -> TH.ExpQ -> TH.ExpQ -> TH.DecsQ) -> TH.DecsQ
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's an internal function that's only part of a separate module due to the stage restriction. Haddock won't help document the arguments of the continuation, but we can do that with a regular comment.

@@ -155,3 +160,20 @@ getStaticFieldAsJValue retsing cname fname = do
SPrim "double" -> JDouble <$> getStaticDoubleField klass field
SVoid -> fail "getStaticField cannot yield an object of type void"
_ -> JObject <$> getStaticObjectField klass field

mkVariadic :: TH.TypeQ -> (TH.TypeQ -> TH.TypeQ -> [TH.PatQ] -> TH.ExpQ -> TH.ExpQ -> TH.DecsQ) -> TH.DecsQ
mkVariadic retty k = fmap concat $ for [0..32 :: Int] $ \n -> do
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed inline-java (which is a package downstream of jvm) currently duplicates the same constant (with a comment pointing here). I'll export a constant.

mkVariadic :: TH.TypeQ -> (TH.TypeQ -> TH.TypeQ -> [TH.PatQ] -> TH.ExpQ -> TH.ExpQ -> TH.DecsQ) -> TH.DecsQ
mkVariadic retty k = fmap concat $ for [0..32 :: Int] $ \n -> do
let -- Coercible type class and Ty associated type defined in downstream module.
coercible = TH.conT (TH.mkName "Coercible")
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As noted above, mkVariadic should only be used in Language.Java.Unsafe, not anywhere else (and certainly not by the user). That said, if there is something more robust than mkName (which is only necessary because of stage restriction collateral damage), might as well. I noticed mkNameG_tc and friends in the template-haskell API docs, but they're not documented. What does it do, and how does it differ from mkName?

-- | Inject a value (of primitive or reference type) to a 'JValue'. This
-- datatype is useful for e.g. passing arguments as a list of homogeneous type.
-- Synonym for 'coerce'.
jvalue :: (ty ~ Ty a, Coercible a) => a -> JValue
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is preexisting code that was moved earlier in the file because of the intervening splice leading to scoping errors. So I left it as-is. You're right that ty here serves no purpose. Probably a holdover from the past.

-- | Get the Java class of an object or anything 'Coercible' to one.
classOf
:: forall a sym. (Ty a ~ 'Class sym, Coercible a, KnownSymbol sym)
=> a
-> JNI.String
classOf x = JNI.fromChars (symbolVal (Proxy :: Proxy sym)) `const` coerce x

-- Unexported type classes.
class New r where
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the class does end up leaking in error messages, then it would be better to export, I agree. The downside is that the documentation will end up bloated with 32 * 3 = 96 instances that aren't very interesting to the user. That's why I was trying to keep the class completely unexported. Interestingly, I find it pretty hard to get error messages that mention them. I haven't managed so far.

@facundominguez
Copy link
Member

I kept things in IO

This is fine for the unsafe interface. Orthogonal or not, the linear interface uses an abstract monad, and we need to solve caching of MethodIDs there as well for our benchmarks.

@facundominguez
Copy link
Member

This PR is breaking inline-java when built with the linear-types-enabled GHC.
I think I could address these errors when we are satisfied with the PR, if you don't want to fix them yourself.

    /mnt/inline-java/jvm/src/linear-types/Language/Java/Safe.hs:232:21: error:
        • Couldn't match expected type ‘IO (Java.J a0)’
                      with actual type ‘[Java.JValue] -> IO (Java.J ('Class sym))’
        • Probable cause: ‘Java.newJ’ is applied to too few arguments
          In the second argument of ‘(<$>)’, namely
            ‘Java.newJ @sym (toJNIJValues args)’
          In the first argument of ‘(Prelude.<*)’, namely
            ‘JObject . J <$> Java.newJ @sym (toJNIJValues args)’
          In the second argument of ‘(Prelude.$)’, namely
            ‘JObject . J <$> Java.newJ @sym (toJNIJValues args)
               Prelude.<* deleteLinearJObjects args’
        |
    232 |     JObject . J <$> Java.newJ @sym (toJNIJValues args)
        |                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

@mboes
Copy link
Member Author

mboes commented Nov 19, 2019

That would be great. I don't feel confident about (or have much time for) hacking on the linear variant. I expect those modules can use similar type classes to the unsafe interface, with or without @goldfirere's NumArg trick if the abstract monad in the linear interface causes problems.

Meanwhile, I believe it's possible to hide the variadic type classes from all error messages using a catchall (and yes, overlapping) instance with GHC.TypeLits.TypeError in the context. I have never used those before so am experimenting.

Variadic functions all have a constraint, which appears in their type
signature. In an effort to further hide this constraint, we replace it
in each case with a generic `Variadic "foo" r` constraint, where `foo`
is the name of the variadic function. That way we can explain in
a single place what this one constraint means throughout the module.

This constraint should only appear in Haddock. In principle, it should
never appear in error messages.
Using TypeError, we can replace the error message that GHC provides to
the user when a constraint is not satisfied. We can in particular
arrange for such a custom message to be displayed whenever GHC would
instead talk about potentially private constraints that mean nothing
to the user.

This requires a catchall instance that overlaps with all others. The
overlap is benign, because the overlapping instances are for private
constraints that are never exported. Also, the error instance doesn't
have any operational meaning. It's just to throw an error at the user
when the program doesn't type check anyways.
@mboes
Copy link
Member Author

mboes commented Nov 20, 2019

@facundominguez @goldfirere I added catchall instances with TypeError in the context. The idea is that if no instance matches, then the catchall one does, always. This instance explains to the user what shape of type is expected vs what type we got. Overlap is ok because these are private classes with all instances in a single module, and the catchall instance is just to override an error message with another one - either way the program doesn't compile.

With this change, I believe that it's not necessary to expose the private classes in the Haddocks. We now mark all variadic functions in a uniform way using a single Variadic constraint used in all variadic function signatures.

Copy link
Member

@facundominguez facundominguez left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Documentation can be improved, but I can contribute that.

I think we can go with this approach. The only question I'd like discussed a bit, is whether we can have a more descriptive and/or decoupled Variadic type class/family.

@@ -319,7 +327,7 @@ $(mkVariadic [t| J ('Class $(TH.varT (TH.mkName "sym"))) |] $ \ctx typ pats args
-- @
--
-- You can pass any number of 'Coercible' arguments to the constructor.
new :: New r => r
new :: Variadic "new" r => r
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe the type of new would be more informative if the return type was present in the context.

new :: (Coercible a (J ('Class class)), Variadic "new" r (IO a)) => r
-- or
new :: (Coercible a (J ('Class class)), Variadic "new" r) => r (IO a)

One could also wish for the constraints of the arguments to be explicit:

new :: (Coercible a (J ('Class class)), Variadic "new" Coercible r (IO a)) => r
-- or
new :: (Coercible a (J ('Class class)), Variadic "new" r ) => r Coercible (IO a)

As it is now, the documentation of the functions that use Variadic and Variadic itself need to compensate for this opaqueness.

Furthermore, would it be possible to make a standalone version of Variadic, that is not specific to inline-java?
Adding a parameter to describe the "fixed" arguments, it could be possible to subsume New, Call and CallStatic with a single type class which is instantiated with specific parameters on each case.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A challenge with variadic programming is that Haskell considers functions to be just like all other data. But a variadic function can't return a function, or else we don't know how many parameters there are. That's why having a result in IO works easily, but have a general monad does not work as easily. Still, I agree that this could be generalized.

Copy link
Member Author

@mboes mboes Nov 20, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Variadic itself isn't exported, so the documentation for it won't help much. What we have is an explanation of the Variadic constraint at the module level, and in the documentation of each function.

A standalone version of Variadic would be very nice. But it would have to look different than it does now. Indexing with a symbol allows us to use the exact same name as the function: Variadic "foo" says foo is variadic. But if Variadic were to escape the scope of the current module, then we'd have to be careful that no other module exports a variadic function also called foo. The fix is to use an empty datatype instead of a symbol as the index.

I'm okay with generalizing Variadic with the extra indices that you suggest, especially if Variadic is to be spun out, though I'd keep r :: * as in your first example. Because it will be hard to have an r :: Constraint -> * -> * be anything other than a data/newtype.

Keep in mind that even with extra indices, Variadic is still a special case of variadic functions. The prototypical one is printf, where one would normally want the freedom to specify arbitrary serializers/formats for each argument, rather than be constrained to canonical serializers given by type class instances (like the non-type-class-based one does). The inline-java case is a special case.

@@ -161,14 +162,18 @@ getStaticFieldAsJValue retsing cname fname = do
SVoid -> fail "getStaticField cannot yield an object of type void"
_ -> JObject <$> getStaticObjectField klass field

-- | The maximum supported number of arguments to variadic functions.
maxVariadicArgs :: Int
maxVariadicArgs = 32
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nitpick: Is it hard to get the constant used at the type level in the TypeError message that refers to it? 😈

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, you could have

type MaxVariadicArgs = 32

maxVariadicArgs :: Int
maxVariadicArgs = fromInteger $ natVal @MaxVariadicArgs Proxy

Gee, it would be nice to have dependent types... :)

@facundominguez
Copy link
Member

I'm adapting @goldfirere last proposal to work with a finite amount of instances and no TH.

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

import qualified Data.Coerce as Coerce

class Coercible a
instance Coercible ()
instance Coercible Int
instance Coercible Bool
instance Coercible Char

data Ty a
type family J a
type instance J (Ty a) = a
class IsReferenceType a
instance IsReferenceType (Ty Ref)

data Nat = Zero | Succ Nat

type family NumArgs r where
  NumArgs (a -> b) = Succ (NumArgs b)
  NumArgs other    = Zero

class CallResult_ (num_args :: Nat) r where
instance Coercible b => CallResult_ Zero (m b) where
instance (Coercible a, CallResult_ n r) => CallResult_ (Succ n) (a -> r) where

type CallResult r = CallResult_ (NumArgs r) r

call :: (IsReferenceType (Ty a), Coerce.Coercible a (J (Ty a)), Coercible a, CallResult r)
     => a -> String -> r
call = undefined

data Ref
instance Coercible Ref

newRef :: IO Ref
newRef = undefined

test :: IO ()
test = do
  ref <- newRef
  () <- call ref "nullary"   -- need the () <- so that GHC knows the result is Coercible
  _ :: Int <- call ref "nullary returning int"
  () <- call ref "unary" True
  () <- call ref "binary" 'x' (5 :: Int)
  return ()

I would try something similar on top of this PR, unless I'm missing something essential.

@facundominguez
Copy link
Member

facundominguez commented Nov 20, 2019

hm, when the monad is abstract the Call/CallResult constraint still leaks.

Compiling this in @goldfirere program (either with or without my modifications):

f :: MonadIO m => m ()
f = call Ref "binary" 'x' (5 :: Int)

yields

test.hs:52:5: error:
    • Could not deduce (CallResult_
                          ('Succ ('Succ (NumArgs (m ())))) (Char -> Int -> m ()))
        arising from a use of ‘call’
        (maybe you haven't applied a function to enough arguments?)
      from the context: (CallResult_ (NumArgs (m ())) (m ()), MonadIO m)
        bound by the type signature for:
                   f :: forall (m :: * -> *).
                        (CallResult_ (NumArgs (m ())) (m ()), MonadIO m) =>
                        m ()
        at test.hs:51:1-61
    • In the expression: call Ref "binary" 'x' (5 :: Int)
      In an equation for ‘f’: f = call Ref "binary" 'x' (5 :: Int)
   |
52 | f = call Ref "binary" 'x' (5 :: Int)
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

ErrorType can hide CallResult_ in the error message, but fixing the error requires access to CallResult_:

f ::
  (CallResult_
     (NumArgs (Char -> Int -> m ()))
     (Char -> Int -> m ())
  , MonadIO m
  ) => m ()
f = call Ref "binary" 'x' (5 :: Int)

In #133, the original signature (f :: MonadIO m => m ()) would work without modification.

@mboes
Copy link
Member Author

mboes commented Nov 20, 2019

Could we please proceed incrementally? The safe interface is wholly separate from the unsafe interface. The quick way forward is to simply adapt the safe interface to the changes in Language.Java.Internal, which are identical to the ones in #133 for that module.

@facundominguez facundominguez changed the title jvm: make call* variadic jvm: make call* variadic in the unsafe interface Nov 20, 2019
@facundominguez
Copy link
Member

Works for me.

@mboes mboes mentioned this pull request Nov 20, 2019
@facundominguez
Copy link
Member

facundominguez commented Nov 20, 2019

There you go. #138 is a PR over this one to simplify the type class instance business.

, [| fromString $(TH.stringE ("io.tweag.inlinejava." ++ mangle thismod)) |]
, [| fromString $(TH.stringE mname) |]
] ++ map TH.varE thnames')
)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This code is used both by the linear and the non-linear interfaces. Looks like we will have to abstract the way in which arguments are passed.

@facundominguez
Copy link
Member

I'm waiting for CI to merge.

@facundominguez facundominguez merged commit 4431b29 into master Nov 22, 2019
@facundominguez facundominguez deleted the method-specs branch November 22, 2019 18:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants