Random thought With higher kinds using arrow meta can we hav

Question

Random thought With higher kinds using arrow meta can we have something like ` higherkind interface Eq lt A gt ` ` higherkind interface Show lt A gt Eq lt A gt ` With the current encoding this is not possible because we d inherit from two Kinds `Kind lt ForEq A gt ` and `Kind lt ForShow A gt ` This is quite useful when defining deriving these instances for example by using the `Divisible` typeclass family

Jannis · Answer

This is also something that is not in haskell probably for different reasons and the solution over there is to just newtype wrap all the typeclasses that you d want this for

raulraja · Answer

Yes

raulraja · Answer

We are gonna have more

raulraja · Answer

In the presence of instances of Eq plus etc the type class extensions have precedence over the Lang operators

raulraja · Answer

The new encoding for types includes it s inline newtype and a run time proof so there is no runtime and no need for ListK wrappers or similar

raulraja · Answer

Show eq order etc are always discovered implictly and constrains in polymorphic functions are regular Kotlin type bounds

raulraja · Answer

Anything can now extend synthetically Eq a directly

raulraja · Answer

And it works with the existing system for subtype Polymorphism

raulraja · Answer

No need for given or arguments injections so it s compatible with existing subtype polymorphic Kotlin

raulraja · Answer

The issue in this area right now it s that at the moment it s just me working on proofs and there is a fair amount to finish

raulraja · Answer

All parts are almost ready except laws tests inductive derivation and Lang operator overload and the actual arrow migration once tests and laws are ready

Jannis · Answer

That sounds really cool sweat smile Especially using == over eqv ^ ^ Although this needs some sort of note from a ide plugin or so if it happens to prevent ambiguity for the person reading it

Jannis · Answer

One more thing currently I have a slight issue in the schedule pr where I really want to define variance for the generics but due to it inheriting the `Kind3 lt ForSchedule gt ` the compiler prevents that This leads to some typecasts and the necessity to provide generic types in a few places

raulraja · Answer

Yes injections are highlighted differently and include the path to where it comes from