https://kotlinlang.org logo
Join Slack
Powered by
I am not hugely familiar with arrow, and it uses a...
# arrow
h
I am not hugely familiar with arrow, and it uses a lot of names that I do not recognize. I'm wondering if arrow offers some magic that would help me with a problem I'm having: I've been writing a units of measurement library for awhile now, and my biggest disappointment is that I can't find a way to get the compiler to automatically know that a conversion between quantity types results in a specific quantity type (instead of erased type) e.g.
Copy code
val distance = 512.m
val time = 70.s

val speed = distance / time
The compiler only recognizes 
speed
to be of type 
Quantity<*>
instead of 
Quantity<Velocity>
, even though in the code this operation is specifically instantiating a quantity of velocity. Is there some kind of magic in Arrow that could ensure this without me having to hard code every compound quantity conversion? I'm almost certain at this point that this is impossible to do.
k
When you're saying the compiler doesn't know that a conversion between quantity types results in specific quantity type, do you mean this generally? As in, are you trying to write a one div function to handle any quantity division?
s
Could you perhaps share a link to a more complete example?
p
What you want is to make a new type that had unit. Like, for example, 
inline Measured<T>(Val v: Double)
. Then you make several phantom types such as class 
Meters private constructor()
and definie addition just for the same matching type
Copy code
operator fun <T> Measured<T>.plus(o: Measured<T>, AP: Applicative<ForMeasured>) =
  AP.just(v + o.v)
And NEVER make Meters inherit Kilometers or the other way around. Each phantom type is unique in it's inheritance tree
And then you can start getting cute with things lile
Like
Copy code
operator fun Measured<Meter>.plus(o: Measured<Kilometer>, AP: Applicative<ForMeasured>): Measured<Meter> =
  AP.just(v + o.v *1000)
To emphasize, that specialization only works if Meter is not a Kilometer and viceversa
Otherwise you get into ambiguity issues and the compiler won't be able to pick the correct specialization for you
Don't do a sealed class of measurement units to make a requirement for T either, you'll get on the same ambiguity problem
If you want to limit the values of T, hide the main constructor or Measured and give a constructor per metric in the companion object, for example
Copy code
class Measured<T> private constructor (val v: Double) {
  companion object {
    fun meters (d: Double): Measured<Meters> = ...
  }
}
> that could ensure this without me having to hard code every compound quantity conversion? I didn’t read this. Some of the type requirements is solved above. If you do 
Speed<T>
and 
Time<U>
and 
Velocity<T, U>
you can get away with some of it
conversions between the same qualifier need to be done manually, sadly
If you do a sealed class you’ll run into challenges when a class has multiple units, so an interface or another phantom type can help here
Copy code
sealed class Measure<T>(…) {
  class Velocity<U>(…): Measure<Composed<T, U>>
}

class Composed<T,U> private constructor()
that way you can express composed types
this…isn’t too great
problem is, he wants speed to be in m/s and making adding two distances first converts them to the same scale
Copy code
operator fun Measurement.Distance.div(other: Measurement.Time): Int
oooh fancy 😄 nice
r
you can support that use case just adding nodes to the ADT or making the Number type generic and constrained by subtypes of Number in the type args of the ADT constructor
r
I also have had to tackle this problem, I turned to code generation using an annotation processor: https://github.com/Octogonapus/kt-units It could be combined with the algebra above, that might be pretty good. The real solution is to write a compiler plugin so you have zero overhead, though.
r
You can write this with 0 cost with arrow meta and Type Proofs which will be merged into master soon
Unions, Refined Types and Type Classes are modeled with type proofs
in this case you can add proofs for the conversions that are safe and eliminate the wrapping between literals and the ADT and use instead an inline class that is erased
h
I'm exploring all the answers, but I figured I should expand a little bit on the intended logic of this library. In physics, all quantities have a "dimension" which can be expressed as a product of the 7 base dimensions (Length, Mass, Time, ...) raised to some corresponding exponents 
LᵃMᵇTᶜ...
In the example in OP, when we divide 
distance (L¹)
by 
time (T¹)
our resulting dimension is 
L¹T⁻¹
which corresponds to the quantity Velocity. So essentially I'm trying to write a single function 
operator fun <A: Quantity<A>, B: Quantity<B>, R: Quantity<R>> A.times(other: B): R
such that the compiler can infer the return type by looking up whatever the resultant dimension maps to
I'm looking more into ADT to see how it can help me here, but as I said, I'm worried this is impossible
k
I've tried to tackle this exact problem before. I'm fairly certain it's not possible in Kotlin without the help of some metaprogramming as you'd have to represent integer arithmetic at the type level. Kotlin does not have recursive type inference, so typical approaches like type-level church numerals are quite impractical.
In my own units-of-measure library (github.com/kunalsheth/units-of-measure), I just decided to generate a new function for every dimensional relationship the user wanted. Though, I am quite interested in what Arrow has to offer with regard to type-level integers!
h
yeah, but to cover every conversion would require an astronomical amount of code when you take into account extensively compound units like 
JoulesPerMoleKelvin
and the like. in a perfect world, the code could recognize a quantity of any dimension, considering there are potentially infinite
👍 1
k
Actually, not that much. ~17,000 lines for all conversions between all named SI-units.
An improvement would be to detect what functions the user needs and generate only those, but I haven’t found a good way to do that.
I wonder if Arrow offers some way of representing type-level integers, in which case this problem would be solved.
h
well, they could actually need infinity funcitons
k
Sort of, but they can be generated on an as-needed basis. I.e. 
One.plus(x: Two)
doesn’t exist until the user calls it.
h
yeah...
I'm going to just use your library for now, i think. It's seems to achieve nearly identically everything I was planning to add to mine
👍 1
k
Awesome, let me know if you need any help!
h
why'd you choose to handle the prefixes as 
3.kilo(Metre)
instead of 
3.kilo.Metre
? Not judging. Curious
r
This will be possible with type proofs
once we have them in Arrow Meta, it’s what I’m working on at the moment.
You can proof: DataClass -> TupleN -> Extension
So all extensions for Product and Sum types are automatically inductively available to ad-hoc resolution
h
Awesome
r
But it’s not there yet, I’m currently working on it. I have Unions, and other type system features modeled with it and and graph for the inductive proofs that finds shortest paths between proofs to inductively resolve them
With that you can create extension for HList or Tuples and derive them for other models without the shapeless boilerplate
It does not attempt to bring singleton literals or path dependent types but instead you write extension functions that proof injections or isomorphisms A -> B, A <-> B
those affect the type checker and codegen to resolve ad-hoc polymorphism to conversion calls where otherwise an impossible cast would have happened.
7 Views
Open in Slack
PreviousNext
Powered by