Hi, I think I saw at some point something like @given in an example. Are we going to have KEEP-87 im...

# arrow

[gabib]

Hi, I think I saw at some point something like @given in an example. Are we going to have KEEP-87 implemented with Arrow Meta?

[raulraja]

yep https://github.com/arrow-kt/arrow-meta/blob/dfb1f1f5fe263cc00a39213a9f5dffb171ac479a/compiler-plugin/src/test/kotlin/arrow/meta/plugins/typeclasses/TypeClassesTest.kt#L45

[raulraja]

But most importantly syntax of type classes is auto projected over data types by global coherent proof so in most cases you don’t even need to require anything with @given unless you are writing polymorphic functions where you require type arguments to be constrained by them.

[raulraja]

It also uses a mechanism to be compatible with the same style of declaration of subtype bounds since proofs in meta use the notion of a synthetic subtype that is replaced by the proof to tie up the relationship between a data type and its type class

[gabib]

Cool, thank you

[raulraja]

@Proof(TypeProof.Extension)
fun String.Companion.monoid(): Monoid<String> =
  StringMonoid

@Proof(TypeProof.Extension)
fun String.semigroupSyntax(): Semigroup.Syntax<String> =
  StringSyntax(this)

[raulraja]

that says the String companion gets all constructors and members of Monoid<String> and string values get all syntax of semigroup and enables:

String.empty()
"a".combine("b")

[raulraja]

without imports

[gabib]

This is great, looks awesome

[CLOVIS]

Wow that's amazing

So it's something like a extension inheritance? As in, you can create an ‘extension interface' and make a class you don't control inherit it via extension functions? If so, that's amazing

[raulraja]

Yes that is what it is

[raulraja]

imply in logic is equivalent to subtyping in kotlin

[raulraja]

It's an impl of Programs as proofs as in the Curry Howard Lambek correspondence

[raulraja]

Ad hoc policies between types as a compiler and ide plugin