@bigkahuna here is an example of a

type-proof

https://kotlinlang.slack.com/archives/CJ699L62W/p1574067540396900

I really enjoyed this video if you want to hear more , but they’re plenty out there. I cant confidently answer what the difference is between Path dependent types in Scala and Dependent Types in Haskell. At first glance they seem to solve the same problem, but I am not a Haskell programmer, nor Scala.

The only needed or autogenerated boilerplate is:

class `List(_)`

@arrow.proof(conversion = true)
fun <A> Kind<`List(_)`, A>.fix(): List<A> =
  (this as Kinded).value as List<A>

@arrow.proof(conversion = true)
fun <A> List<A>.unfix(): Kind<`List(_)`, A> =
  Kinded(this)

And there is no need to create wrappers

that turns

List

into a kinded value you can use in ad hoc polymorphism

Kinded

is an erased inline class that wraps the concrete value

also the

conversion = true

eliminates the need to ever call

fix

as it looks today when using polymorphic functions because the type proof plugin is able to tell the Kotlin compiler type checker those are kinds given those proofs that are provided by the user.

We have unions, kinds, refined types and in the work to implement also type classes all with just type proofs

It’s a proof at the type level because it’s inspected at compile time but it’s not type level programming in the sense of a type level HList, Nat etc as you seen in Scala and Haskell, but you can use them for similar purposes

FP is about trying to stay as close as possible to Lambda.Calculus and Category theory. It can be done even without HKT (not saying they would not be useful).

And the type proofs plugin coming which models unions, kinds, refined types and morphisms between Kotlin types in general allowing ad hoc subtyping, extensions and polymorphism without inheritance will allow you to bend the type system to your will.

In development parts of the Arrow Prelude https://github.com/arrow-kt/arrow-meta/tree/rr-type-conversions/prelude/src/main/kotlin/arrow

Since you are all functionally inclined. In the category of the Kotlin types where the morphisms are the functions type proofs establishes a trust relationship with the Kotlin compiler where you can tell it you know the path between two types and the implication that has. The arrow prelude demonstrates the Kotlin type system can be extended by providing a custom typechecker based on proofs that eliminate the need for inheritance by exploiting subtype Polymorphism and the top Any? and bottom types Nothing. In Kotlin we can have value holes we can fill in with type proofs in any expression position.

So this is an alternative to inheritance which favors composition and separation of data and behaviors

Or let me put it differently

A

type-proof

has 2 components a

to

and a

from

function. Where we go from

A

to

B

and back. Thus we proof to the compiler, that this conversion is valid. Similar if you would describe an isomorphism between Functor’s

F

and

G

@Imran/Malic this is regardless of kinds or containers of F. It works for all types regardless if they are kinded or not.

is this going to elongate compilation times ?

i have a kotlin analog of pandas... i want to be able to specify a decoder from seralization bytes to Floats, and then perform some aggregations and signal that there will be a list of Floats. currently the only generic options i have are to use Any? and explicitly front-run all of my conversions

e.g. https://github.com/jnorthrup/columnar/blob/507f2b42e732b22d98f53c35325fa6793b78ce44/src/test/java/com/fnreport/mapper/ColumnarTest.kt#L91-L93 How am I able to define a system of functions to start with a column decoder of type A and stuff transforms of type T1....n into a tuple for these proofs to end up decoding input byte[] into output List<Float> ?

i would gladly submit this Columnar aggregation toy as a before and after example for Arrow-kt concepts, it's at a point where it simplifies the unpleasant pandas areas in my actual dayjob, and is purpose-built. I think arrow-kt type-proofs may be the start of a mechanism to track data transformations and potentially rescue SIMD compiler opportunities from combinatorial inputs