search

derive4j / hkt

Higher Kinded Type machinery for Java
BSD 3-Clause "New" or "Revised" License
81 stars 9 forks source link

experimental lower #19

Closed clinuxrulz closed 8 years ago

clinuxrulz commented 8 years ago

I've got an implementation of lower, it uses inheritance to achieve a type (between Lower and Lower_).

Not sure if it is cheating the type-system.

jbgi commented 8 years ago

Interesting! there still cheating going on due to https://github.com/derive4j/hkt/pull/19/files#diff-349805cc9967ae028b3de262d9ccbac0R193

some related post (and comments) I found on the subject:

I think, if we add lower, we can just typecast refl(). Before that we will need to be sure that type constructor in java are injective, but this is probably the case (it is in haskell). On the other hand, I don't know of any compelling use cases for lower... do you know one?

gneuvill commented 8 years ago

type constructor in java are injective

Which means ? (pardon my ignorance)

jbgi commented 8 years ago

Type constructors being injective means that for every type constructor F, F a equals F b imply a equals b. (ie. the definition of lower).

gneuvill commented 8 years ago

Type constructors being injective means that for every type constructor F, F a equals F b imply a equals b. (ie. the definition of lower).

Thanks ! Is 'injective' a cs concept or a mathematical one (such as the bijection that we learn at school) ?

jbgi commented 8 years ago

Yes I think that this is the same concept. If you think of F as a mathematical function, F a is the image of a and F b is the image of b. Since F is injective we can track each distinct value of the co-domain (F a) to a unique and distinct value of the domain (a) and so if two values of the co-domain are equals it means that their inverse images are equals.

jbgi commented 8 years ago

As for safety of lower: with our encoding, type constructor witnesses are tied to a particular class: we cannot safely narrow a hkt term to a subclass of the subclass that implement the __ interface. I think we should also forbid (mutually) recursive type variables as it can result in unsafe code that type checks. If we do that, I think, we can assume the same "injectivity law" for type constructors that is valid for ML/Haskell.

gneuvill commented 8 years ago

Thanks for the explanations. Need to process them for a while...

clinuxrulz commented 8 years ago

Forgive me for trying to push again. I'm just trying to prove to myself that it is not type safe.

I've avoided the typecast from Lower_ to Lower. But maybe something else not allowed is going on. (Note that A and B are simply helpers to get X and Y the right type in the latest example)

clinuxrulz commented 8 years ago

I have a hunch that lift and lower can aid with implementing type families though the use of type constructors and existential type parameters. (as a use case)

And an implementation of type families leads to a correct implementation of syntactic from hackage (open unions) https://hackage.haskell.org/package/syntactic

Which leads to DSLs that are extendable.

Edit: Inside syntactic you can find the following code:

-- | The result type of a symbol with the given signature
type family   DenResult sig
type instance DenResult (Full a)    = a
type instance DenResult (a :-> sig) = DenResult sig

To go from Full a to a I believe I need lower. (And same goes for a :-> sig)

clinuxrulz commented 8 years ago

OK. I believe I've proven type constructors in java are injective. I'm now using no tricks at all. (in the latest commit titled "Complete Type Safety! No Tricks!!!")

jbgi commented 8 years ago

it does compile!! ... but I think it should not. ;) you probably outsmarted the compiler ;) In fact it does not compile in intellij. The reason is that you cannot extract a Leibniz<A,B> from (Lower_<f, ?, ?, X, Y> lower_).leib: you theoretically only get a Leibniz<?,?>. I think it is a javac bug for not catching it.

clinuxrulz commented 8 years ago

Even though leibX and leibY are not used, maybe it helps the compiler to unify CAP#1 and CAP#2 with A and B. In Netbeans it seems the autocomplete knew what type the final leib was.

Edit: Actually your correct, a closer inspection reveals the final leib to have a raw type.

jbgi commented 8 years ago

@clinuxrulz but if you extract Lower.ofHkt(a.subst(new Lower(new Lower_<f, A, A, __<f, A>, __<f, A>>(Leibniz.<A>refl(), Leibniz.<__<f, A>>refl(), Leibniz.<__<f, A>>refl())))) into an intermediate variable it does not compile anymore. But yes, it is maybe the closer we can get to typesafe lower.

clinuxrulz commented 8 years ago

new Lower --> new Lower<>, i think thats my mistake

clinuxrulz commented 8 years ago

OK. I when back to helper type variables. It type checks, no additional type cast, but it may not pass the HKT processor test.

clinuxrulz commented 8 years ago

I was looking at the source for the HTK processor and the last version will fail the test. I might close this for now. Is there a way to work out for sure if Java type constructors are injective?