-
-
Save jdegoes/6842d471e7b8849f90d5bb5644ecb3b2 to your computer and use it in GitHub Desktop.
class Option<A> { | |
protected Option() { } | |
} | |
interface App<F, A> { | |
F proof(); | |
} | |
class OptionF { | |
private OptionF() {} | |
private static class AppOption<A> implements App<OptionF, A> { | |
public final Option<A> value; | |
AppOption(Option<A> value) { | |
this.value = value; | |
} | |
public OptionF proof() { | |
return new OptionF(); | |
} | |
} | |
public static <A> App<OptionF, A> fromOption(Option<A> v) { | |
return new AppOption(v); | |
} | |
public static <A> Option<A> toOption(App<OptionF, A> v) { | |
return (((AppOption<A>)v).value); | |
} | |
} | |
interface Function<A, B> { | |
B apply(A a); | |
} | |
interface Functor<F> { | |
<A, B> App<F, B> map(Function<A, B> f, App<F, A> fa); | |
} |
Not really safe though. But with a JSR269 annotation processor we can make a similar encoding safe (WIP: https://github.com/derive4j/hkt):
public static void main(String[] args) {
OptionF.toOption(new FakeAppOption<>(OptionF.fromOption(new Option<String>()))); // ClassCastException !!!
}
static class FakeAppOption<A> implements App<OptionF, A> {
private final App<OptionF, A> appOption;
FakeAppOption(App<OptionF, A> appOption) {
this.appOption = appOption;
}
public OptionF proof() {
return appOption.proof();
}
}
@jbgi It's safe because the constructor is private — the only way an OptionF
can be constructed is from fromOption
. However, derive4j looks quite cool!
@jdegoes yes, but this does not change the fact that my example exhibit a ClassCastException (ie. not safe).
(I updated my preceding comment to be more explicit)
You are explicitly constructing a new FakeAppOption
, which is where the unsafety arises. If you prevent construction of this value by making the constructor private, the code becomes safe (up to null and reflection and other crap that we have to ignore, anyway).
@jdegoes. well sure, if I cannot construct a FakeAppOption
then of course I cannot demonstrate the unsafety of the API with it. It is not the point though: FakeAppOption
is perfectly valid java that follows the scalazzi rules.
@jbgi Well, in my example, there is one and only one way to create App<OptionF, A>
(without null / runtime reflection crap), and that's by using the helper function fromOption
, and that guarantee is enforced by the compiler and cannot be broken by a user of the library, because the constructor is private. Because we have this guarantee, the only cast in line 27 is provably safe, which renders the technique type-safe, and suitable for use without annotations, in Java 7 or earlier, etc.
I'm not saying it's the only way to encode this in Java or even the best, just that it is a simple and valid way of converting a compile-time proof to a runtime proof, and leveraging Java's access modifiers to ensure type-safety up to the boundaries of sane coding in Java.
@jdegoes, if there is only one way to construct a App<OptionF, A>
then how do you explained that I could compile and construct a FakeAppOption<A>
which is an instance of App<OptionF, A>
, in my user code, without using any null / runtime reflection crap??
@jbgi I am not referring to your code, which was not designed using the above pattern. I am referring to my own code. The code snippet you provided is definitely type-unsafe, because anyone can construct instances of the type. There are zero guarantees.
@jdegoes, so the "proof" is not really one then. The encoding is just a particular convention that you can easily circumvent without resorting to unsafe code and yet gain a bogus "proof". As you say, the encoding provides zero (hard) guarantees.
@jbgi Sure, it is a proof — it's just one that requires manual inspection of a few lines of code to verify (that both the constructor is private and that it is only used in introduction and elimination). Also, if you're a library author, you can ship your OptionF
equivalent and library users have strong guarantees, since they cannot access the source nor tamper with your decisions.
Your way of reasoning would suggest that a type like abstract class Void { public <A> A absurd(Void v) { throw new InternalError(); } }
is not useful, because someone can change the abstract
and therefore people will be able to create instances of Void
, thereby rendering the absurd
function, well, absurd.
I understand that way of thinking about the problem, but when working with weaker-typed languages (weaker than full pi types), as I often do, I benefit greatly from proofs that can be tampered with, but which provide reasonable control against tampering, and reasoning power in the absence of tampering.
@jdegoes Void
is useful. In fact, I actually added it to functionaljava: https://github.com/functionaljava/functionaljava/blob/master/core/src/main/java/fj/Void.java
Void
is totally fine because absurd
cannot be implemented without violating parametricity or using bottoms, so one can apply Fast and Loose Reasoning.
Unfortunately this is not the case for the proof
method of App<OptionF, A>
: third party code can implement the interface without modifying the original library and without any violations of parametricity nor using bottoms or reflection, as my snippet demonstrate.
This is why I think the type system must be augmented (eg. via an annotation processor) so that it is actually guaranteed that only AppOption<A>
can implements App<OptionF, A>
. Otherwise you must have faith that usercode will not use some valid constructs (in my snippet, simple encapsulation of an AppOption<A>
in order to implements App<OptionF, A>
).
Bottom-line: I can blame user code for using bottoms or reflection but I don't want to blame user code for using perfectly valid java (as in my snippet), unless they have explicitly deactivated an annotation processor that produce compile errors for such constructs.
This is why I think the type system must be augmented (eg. via an annotation processor) so that it is actually guaranteed that only AppOption can implements App<OptionF, A>. Otherwise you must have faith that usercode will not use some valid constructs (in my snippet, simple encapsulation of an AppOption in order to implements App<OptionF, A>).
Again, this is not possible if you are a library user of Option
/ OptionF
. The Java compiler prevents you from creating an instance of OptionF
, because the constructor is private, and the only way such instance may be introduced is via the helper function in OptionF
.
If you are not a library user of Option
/ OptionF
, but you are the creator of these types, then yes, nothing stops you from changing the constructor to public, or from introducing additional helper functions which create instances of the types. If you do either of these things, then the code becomes type-unsafe.
However, I would point out the symmetry with Void
. If Void
is defined in a library, you cannot create instances of that type, because it is defined as abstract
and there is no constructor. You have a compile-time guarantee of this.
But if Void
is defined in your own library, then you can introduce a public or protected constructor, or introduce other ways of creating instances of the type Void
, all of which will destroy safety and reasoning.
I am not arguing that annotation processors are not useful (they are!), but fundamentally, we are talking degrees of powers of reasoning here; and degrees of being resistant to tampering. Ultimately if a user controls your types, they can make whatever they want happen; you achieve safety to the maximum degree only by not giving them control over the types, and putting them in a library they can't change; and also by using very strong types which the compiler can verify completely without the need for you to rely on manual proofs.
Again, this is not possible if you are a library user of Option / OptionF. The Java compiler prevents you from creating an instance of OptionF, because the constructor is private, and the only way such instance may be introduced is via the helper function in OptionF.
I think you misread my snippet: it does not build an instance of OptionF
via its constructor: it simply delegate to a valid App<OptionF, A>
to implement the proof
method.
My snippet only use public methods from your gist, namely fromOption
and toOption
. Yet it produce it produce a ClassCastException.
FWIW... In higher I used a token based control access policy
https://github.com/palladin/Higher/blob/master/src/Higher.Core/CoreTypes.fs
I've been mucking around with this trick for a little while, it starts to get a bit ugly when you have more than one level of nesting of types, e.g. F<G<A>>
sometimes needs to be represented as App<F, App<G, A>>
and other times as App<App<F, G>, A>
. You'll run into that if you try to represent Functor composition, for example.
@jbgi your project looks really interesting, thanks for sharing it. I've been purposefully ignoring the fact that a user could provide a false implementation of the type so far. I had an inkling that the casts could be made safe with a pre-processor, but hadn't looked into it yet.
@jbgi This version fixes your example:
class Option<A> {
protected Option() { }
}
interface App<F, A> {
F proof();
}
class OptionF {
private final Option<?> value;
private OptionF(Option<?> value) {
this.value = value;
}
public static <A> App<OptionF, A> fromOption(Option<A> v) {
return new App<OptionF, A>() {
public OptionF proof() {
return new OptionF(v);
}
};
}
public static <A> Option<A> toOption(App<OptionF, A> v) {
return (Option<A>) v.proof().value;
}
}
interface Function<A, B> {
B apply(A a);
}
interface Functor<F> {
<A, B> App<F, B> map(Function<A, B> f, App<F, A> fa);
}
@TomasMikula, indeed! But unfortunately this just move unsafety onto the type parameter:
public static void main(String[] args) {
App<OptionF, Integer> intOption = OptionF.fromOption(new Option<Integer>());
App<OptionF, String> fakeStringOption = new App<OptionF, String>() {
@Override
public OptionF proof() {
return intOption.proof();
}
};
Option<String> notAstringOption = OptionF.toOption(fakeStringOption); // unsafe cast of an Option<Integer> to an Option<String> !!
}
@jbgi Ah, you're right! Thanks for being so patient. 🙏
Although, I'd point out the following: this is not accidental type unsafety, but malicious type unsafety, in the sense that, a user would have to intentionally work around the limited options for constructing OptionF
.
I have another idea to fix this loophole by moving closer to the paper, representing an existential type via skolemization, and forcing delimited modules on the user... I'll give it a try this weekend and post back.
@jbgi Ah yeah. Second attempt:
class Option<A> {
protected Option() { }
}
interface App<F, A, Self extends App<F, A, Self>> {
<T> T accept(Function<App<F, A, ? extends F>, T> f);
}
class OptionF {
private OptionF() {}
private static class AppOption<A> extends OptionF implements App<OptionF, A, AppOption<A>> {
public final Option<A> value;
AppOption(Option<A> value) {
this.value = value;
}
public <T> T accept(Function<App<OptionF, A, ? extends OptionF>, T> f) {
return f.apply(this);
}
}
public static <A> App<OptionF, A, ?> fromOption(Option<A> v) {
return new AppOption<A>(v);
}
public static <A> Option<A> toOption(App<OptionF, A, ?> v) {
return v.accept(app -> (AppOption<A>) app).value;
}
}
interface Function<A, B> {
B apply(A a);
}
interface Functor<F> {
<A, B> App<F, B, ?> map(Function<A, B> f, App<F, A, ?> fa);
}
Well, this one is harder. But once you start using F-bounded polymorphism in conjunction with parametric polymorphism then they are cases where the compiler just accept anything, like this one:
public static void main(String[] args) {
App<OptionF, String, ?> fake = fake();
OptionF.toOption(fake); // ClassCastException
}
static <A, F extends OptionF & App<OptionF, A, F>> App<OptionF, A, F> fake() {
return new App<OptionF, A, F>() {
@Override public <T> T accept(Function<App<OptionF, A, ? extends OptionF>, T> f) {
return f.apply(this);
}
};
}
Interesting. One more try 😄. The difference here is addition of method
Self self();
to the App
interface.
class Option<A> {
protected Option() { }
}
interface App<F, A, Self extends App<F, A, Self>> {
<T> T accept(Function<App<F, A, ? extends F>, T> f);
Self self();
}
class OptionF {
private OptionF() {}
private static class AppOption<A> extends OptionF implements App<OptionF, A, AppOption<A>> {
public final Option<A> value;
AppOption(Option<A> value) {
this.value = value;
}
public <T> T accept(Function<App<OptionF, A, ? extends OptionF>, T> f) {
return f.apply(this);
}
public AppOption<A> self() {
return this;
}
}
public static <A> App<OptionF, A, ?> fromOption(Option<A> v) {
return new AppOption<A>(v);
}
public static <A> Option<A> toOption(App<OptionF, A, ?> v) {
return v.self().accept(app -> (AppOption<A>) app).value;
}
}
interface Function<A, B> {
B apply(A a);
}
interface Functor<F> {
<A, B> App<F, B, ?> map(Function<A, B> f, App<F, A, ?> fa);
}
@TomasMikula: It looks like a good solution... but only for data types with 1 type parameters. A major problem with encoding of hkt that make use F-Bounded polymorphism is that it does not scale well to multiple type parameters: you would have to create a new, independent interfaces AppX
for each data types of X type parameters, because App2
cannot extends App
(due to the F-Bounded constraint). Eg.
interface App2<F, A, B, Self extends App2<F, A, B, Self>> {
<T> T accept2(Function<App2<F, A, B, ? extends F>, T> f);
Self self2();
}
Then how to retrieve an App
from an App2
(eg. to make use for Functor
) without giving up information on type parameters ?? I tried something like:
interface App2<F, F2, A, B, Self extends App2<F, F2, A, B, Self>> {
<T> T accept(Function<App2<F, F2, A, B, ? extends F2>, T> f);
Self self();
App<F, B, ?> toApp();
}
class EitherF<A> {
private EitherF() {}
private static class AppEither<A, B> extends EitherF<A> implements App<EitherF<A>, B, EitherF.AppEither<A, B>> {
public final Either<A, B> value;
AppEither(Either<A, B> value) {
this.value = value;
}
@Override public <T> T accept(Function<App<EitherF<A>, B, ? extends EitherF<A>>, T> f) {
return f.apply(this);
}
@Override public AppEither<A, B> self() {
return this;
}
}
static class EitherF2 {
private EitherF2() { }
private static class App2Either<A, B> extends EitherF2 implements App2<EitherF<A>, EitherF2, A, B, EitherF2.App2Either<A, B>> {
public final Either<A, B> value;
App2Either(Either<A, B> value) {
this.value = value;
}
@Override public <T> T accept(Function<App2<EitherF<A>, EitherF2, A, B, ? extends EitherF2>, T> f) {
return f.apply(this);
}
@Override public EitherF2.App2Either<A, B> self() {
return this;
}
@Override public App<EitherF<A>, B, ?> toApp() {
return new EitherF.AppEither<>(value);
}
}
}
public static <A, B> App2<EitherF<A>, EitherF2, A, B, ?> fromEither(Either<A, B> v) {
return new EitherF2.App2Either<A, B>(v);
}
public static <A, B> Either<A, B> toEither(App2<?, EitherF2, A, B, ?> v) {
return v.self().accept(app -> (EitherF2.App2Either<A, B>) app).value;
}
public static <A, B> Either<A, B> toEither(App<EitherF<A>, B, ?> v) {
return v.self().accept(app -> (EitherF.AppEither<A, B>) app).value;
}
}
While it appears to works (very verbosely) until then, it stops to works as soon as you try to use something like a BiFunctor
on an App2: then you lost information on the first type parameter of App2
, and with it, the ability to retrieve a useful App
from the App2
.
The encoding in https://github.com/derive4j/hkt/blob/master/src/main/java/org/derive4j/hkt/__2.java does not have this problem: App2
simply extends App
.
And since the annotation processor is packaged with the library providing the AppX
interfaces (named __X
), type-safety will be ensured as long as the user does not explicitly deactivate annotation processing (which I would qualified as malicious/intentional in the same sense as my specially crafted counter-examples).
OK, I'm not going to claim it's pretty... 😆
public class Test {
public static void main(String[] args) {
String result = OptionModule.inject(new OptionConsumer<String>() {
public <OptionF> String consume(OptionModule<OptionF> provider) {
Option<Integer> answer = Option.some(42);
App<OptionF, Integer> answerF = provider.fromOption(answer);
App<OptionF, String> answer2 = provider.functor().map(new Function<Integer, String>() { public String apply(Integer i) { return i.toString(); } }, answerF);
return provider.toOption(answer2).getOrElse("");
}
});
System.out.println(result);
}
}
interface Function<A, B> {
B apply(A a);
}
abstract class Option<A> {
private Option() { }
public A getOrElse(A def) {
return fold(def, new Function<A, A>() { public A apply(A a) { return a; } });
}
public static <A> Option<A> none() {
return new Option<A>() {
public <Z> Z fold(Z none, Function<A, Z> some) {
return none;
}
};
}
public static <A> Option<A> some(A a) {
return new Option<A>() {
public <Z> Z fold(Z none, Function<A, Z> some) {
return some.apply(a);
}
};
}
public abstract <Z> Z fold(Z none, Function<A, Z> some);
}
interface App<F, A> { }
interface Functor<F> {
<A, B> App<F, B> map(Function<A, B> f, App<F, A> fa);
}
interface OptionConsumer<Z> {
<OptionF> Z consume(OptionModule<OptionF> provider);
}
class OptionModule<OptionF> {
private OptionModule() { }
public <A> App<OptionF, A> fromOption(Option<A> v) {
return new AppOption<A>(v);
}
public <A> Option<A> toOption(App<OptionF, A> v) {
return (((AppOption<A>)v).value);
}
public Functor<OptionF> functor() {
return new Functor<OptionF>() {
public <A, B> App<OptionF, B> map(Function<A, B> f, App<OptionF, A> fa) {
Option<A> o1 = toOption(fa);
return fromOption(o1.fold(Option.none(), new Function<A, Option<B>>() { public Option<B> apply(A a) { return Option.some(f.apply(a)); } }));
}
};
}
public static <Z> Z inject(OptionConsumer<Z> consumer) {
return consumer.consume(new OptionModule<OptionFTag>());
}
private class AppOption<A> implements App<OptionF, A> {
public final Option<A> value;
AppOption(Option<A> value) {
this.value = value;
}
}
private static class OptionFTag { private OptionFTag() { } }
}
@jdegoes, this one was easy 😄
public static void main(String[] args) {
OptionModule.inject(new OptionConsumer<String>() {
public <OptionF> String consume(OptionModule<OptionF> provider) {
provider.toOption(new App<OptionF, String>() {}); // ClassCastException
return "";
}
});
}
@TomasMikula even if it is obscure, if that does not impact client code and code can be generated it could have been a good solution.
A simple modification renders the original "safe up to null", again:
class Option<A> {
protected Option() { }
}
abstract class App<F, A> {
protected F proof();
}
class OptionF {
private OptionF() {}
private static class AppOption<A> extends App<OptionF, A> {
public final Option<A> value;
AppOption(Option<A> value) {
this.value = value;
}
protected OptionF proof() {
return new OptionF();
}
}
public static <A> App<OptionF, A> fromOption(Option<A> v) {
return new AppOption(v);
}
public static <A> Option<A> toOption(App<OptionF, A> v) {
return (((AppOption<A>)v).value);
}
}
interface Function<A, B> {
B apply(A a);
}
interface Functor<F> {
<A, B> App<F, B> map(Function<A, B> f, App<F, A> fa);
}
@jdegoes, I don't think so. My original counter-example still produce a ClassCastException:
https://gist.github.com/jdegoes/6842d471e7b8849f90d5bb5644ecb3b2#gistcomment-1818237
Damn access methods. If only Java had protected[this]
! Or an abstract private method that could be implemented and seen only by subclasses...
Woah...that's a lot of code. :-)