Inheritance

[mitchellwrosen]

Hi, are there any plans to add support for Java inheritance? From scanning the docs, all I found was

upcast :: J a -> J (Class "java.lang.Object")

and

unsafeCast :: J a -> J b

However, it would be nice to have some sort of

upcast :: Extends a b => J b -> J a

instance Extends a (J (Class "java.lang.Object"))

instead.

Thanks!

[mitchellwrosen]

To this end, I've started work on a repo here: https://github.com/mitchellwrosen/java-apache-lucene/blob/master/jvm-extra/src/Language/Java/Extra.hs

However, the interface is inchoate and unstable, as there are many details in the Java type system (inheritance, generics, bounded generics in class/interface definitions e.g. <T extends Number>, wildcard/bounded generics in types, e.g. List<? super Integer>, and on and on, that are quite tricky to model!

I only mention my work here so anyone else interested in tackling this problem can get in touch to compare notes. Or, if there's prior work in this area, maybe I'm wasting my time. Either way, it's fun!

[facundominguez]

Another possible design is having a class

class Extends (ty1 :: JType) (ty2 :: JType) where

and functions

upcast :: Extends ty1 ty2 => J ty1 -> J ty2
downcast :: Extends ty1 ty2 => J ty2 -> IO (J ty1)
-- Doesn't check at runtime if the input reference has the expected type.
unsafeDowncast :: Extends ty1 ty2 => J ty2 -> J ty1

For a class instance like

class MyClass<A extends BClass & CInterface> extends MySuperClass<A> {
}

We could generate with Java reflection and template haskell:

instance (Extends ty ('Class "BClass"), Extends ty ('Iface "CInterface")) => Extends ('Class "MyClass" <> '[ ty ]) ('Class "MySuperClass" <> '[ ty ])

[puffnfresh]

I think Eta did a good job at this. It's very similar to what you've proposed @facundominguez.

[facundominguez]

The designs with type classes require the caller to explicitly cast references. There is another alternative which is using Liquid Haskell to track inheritance.

{-@ f :: {x:_ | classOf x `isSubClassOf` "someClass" } -> IO () @-}

-- and we can abbreviate it with a type alias
{-@ type SubClassOf C = {x:JObject | classOf x `isSubClassOf` "someClass" } @-}

{-@ f :: SubClassOf "someClass" -> IO () @-}
f :: JObject -> IO ()
f = ...

{-@ y :: SubClassOf "someSubClass" @-}
y :: JObject
y = ...

-- Now we can call f and Liquid Haskell can check that the argument
-- to the call is of a compatible type. See: no upcast call needed.
test :: IO ()
test = f y

-- | Somehow we need to assert the inheritance relations we are aware of
{-@ assume inheritanceDeclaration :: { isSubClassOf "someSubClass" "someClass" } @-}
inheritanceDeclaration :: ()
inheritanceDeclaration = ()