Random thought: With higher-kinds using arrow-meta...

# arrow-meta

[Jannis]

Random thought: With higher-kinds using arrow-meta, can we have something like @higherkind interface Eq<A> @higherkind interface Show<A> : Eq<A> ? With the current encoding this is not possible because we'd inherit from two Kinds Kind<ForEq, A> and Kind<ForShow, A>. This is quite useful when defining/deriving these instances (for example by using the Divisible typeclass family)

[Jannis]

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]

Yes

[raulraja]

We are gonna have more

[raulraja]

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

[raulraja]

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]

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

[raulraja]

Anything can now extend synthetically Eq a directly

[raulraja]

And it works with the existing system for subtype Polymorphism

[raulraja]

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

[raulraja]

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]

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]

That sounds really cool 😅 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]

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<ForSchedule,...> the compiler prevents that. This leads to some typecasts and the necessity to provide generic types in a few places

[raulraja]

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