search

derive4j / hkt

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

Leibniz equality #18

Closed jbgi closed 8 years ago

jbgi commented 8 years ago

WIP, need more work (javadoc, lift2, lift3, ...). for initial review by @gneuvill and @clinuxrulz.

This will allow to implement #17 as well as to use Leibniz for GADT in, eg., derive4j.

clinuxrulz commented 8 years ago

Nice work! Looks good.

On hackage they have lower2, lower3 as well, but don't know how useful it really is.

jbgi commented 8 years ago

lower2/3 will need to be unsafe in Java (as in scala), for lack of the haskell "type families" feature. cf. https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Leibniz.scala#L152

Do we still want to include them?

edit: even in Haskell it seams that the extensions that allow to write lower2/3 without coerce also allow to derive inconsistencies: http://okmij.org/ftp/Haskell/impredicativity-bites.html

clinuxrulz commented 8 years ago

in that case. No, leave lower2,lower3 out for now.

jbgi commented 8 years ago

Also we need to decide over a "narrow" method name. @derive4j/hkt Please vote:

  1. Leibniz.ofHkt
  2. Leibniz.fromHkt
  3. Leibniz.narrow
  4. Leibniz.hktAsLeibniz
  5. ???
gneuvill commented 8 years ago
  1. is fine by me
jbgi commented 8 years ago

Of course, eventually, the implementation of the narrow (ofHkt) methods will need to be generated by the processor. Only then the implementation will be completely safe.

clinuxrulz commented 8 years ago

i'll vote for 1

DanielGronau commented 8 years ago

I have to admit to have some nostalgic feelings concerning narrow: Once upon a time, when punch cards were still a thing, there was an ancient object request broker protocol called CORBA... There you have it, I feel really, really old now :-/

But I don't have a strong opinion, and ofHTK seems to be more specific.