Scala DSL

[tribbloid]

Purpose

Introducing a secondary tensor operation DSL (Domain Specific Language) written in & optimised for Scala language & various compilers (the most common of which are JVM based scalac 2.12+, other options are Scala.js & Dotty)

Despite not being a dependently typed language, Scala may be favourable for some reasons:

• Scala is the preferred language of Apache Spark, Apache Flink, CHISEL (Constructing Hardware In Scala Embedded Language) and NVidia RAPIDS, all of which are important infrastructures for large scale grid learning.
• Singleton types (shapeless / 2.13) allows arbitrary number of shape types to be generated on-demand, without relying on code generator or metaprogramming
• Path-dependent types allows shape algebra to be defined for both symbols & numbers
• Type inference by summoning implicits is more flexible for theorem proving than inheritance & delegation
• Operator overloading & infix syntax allows DSL to be closer to math notations, e.g. vec1 dot_* vec2 can be easier to read than dotProduct(vec1, vec2)
• Advanced type algebra can be expressed in macro & roadmap features. Specifically, the singleton-ops library and it’s associated discussions in SIP-23 have suggested that Scala 2.13 & Dotty will use a more direct & expressive approach

Usage

A PoC project has been submitted at:

https://github.com/tribbloid/shapesafe/tree/master

At this moment (06/07/2020) it only implemented very few operations (dot_product, concat) for double vectors. However most features in the following list has been proved and can be showcased by running gradle test on DoubleVectorSpec.scala.

Required & proven features:

• Type-level shape representation for vector
• Compile-time shape safety for operations with constant shapes (1)
• Run-time shape safety for operations with variable shapes (2)
• (1) can smoothly degrade to (2) for more flexible programming paradigm
• Not relying on compile-time code generation or defining large number of compile-time classes, both of which may stress a JVM classloader
• Not relying on esoteric compiler plugin, macro or unstable libraries. (the PoC only uses singleton-ops which is actively maintained by lightbend core team)

Required & unproven:

• Type-level shape representation for matrix
• Type-level shape representation for arbitrary tensor, with no limitation on its arity and dimensionality (ideally through using recursive generic types, the same technique that defined shapeless.HList)
• Support for UInt & Float element data types
• Support for more operations, particularly if used frequently by ANN

Nice to have:

• Not relying on church type encoding (The only violation in my PoC is shapeles.Nat), which causes slow compilation
• Compile-time & run-time shape safety for named tensor
• Shape algebra defined for symbols instead of number supported by user-defined axioms & compile-time theorem proving
• Dotty or Scala.js support

Not in the scope:

• AutoDiff / Differentiable Programming: should be agnostic to DSL
• Interoperability with Apache Spark, NVidia RAPIDS or any other library, models should manifest into different executions regardless of DSL being used
• Shape safe compositor / pipeline API, too much work

How it fits into roadmap

The competition for supremacy of deep learning ecosystem is brutal and unforgiving. With torch & tensorflow dominating both research & development phase, people have little reasons to steer away from Python & a dynamically typed, procedurally validated scaffolding paradigm. But there are exceptions: the large scale, mission critical, complex systems in production, like autopilot and SLAM, most likely prefers spending much effort reinventing & maintaining a more verbose and arduous code base written in C++ or other low level languages. For these systems, demands for built-in correctness and predictability of execution far outweights the ability to write more concise code.

This is, IMHO, the market niche where kotlingrad can fit in: for mega-engineering rather than prototyping. In particular, to enable users to:

• write provably valid neural architecture WITHOUT sanity test
• if not possible, write neural architecture with lower test coverage that validates the part that cannot be proven, the 80-20 rule in test coverage is very real and account for most edge case failures in an architecture that lacks any type.
• under the above premise, write short & easy to understand code

. in that order. My design & optimisation of DSLs should be consistent with this doctrine. The chosen of Scala & JVM as carrier should naturally put kotlingrad in the ecosystem of Apache Spark, and maybe of RISC-V on the long run, both of which are for large scale production.

[tribbloid]

Hi Breandan, haven't heard from you & Thorsten for a while, what are you guys scheming on lately?

[breandan]

Hey @tribbloid, looks cool! I won't have time to review this for a couple weeks, but encourage you to keep going! Who do you see as the audience for the Scala DSL? Is this just for Scala users, or would it be possible to consume the Scala DSL from Kotlin/Java, and how would that look? It would be helpful to have some usage examples with different algorithms for reference, e.g. matrix multiplication, linear regression, MLP, RNNs. I know you're a Scala fan, so I won't try to convert you, but have you looked into arrow-kt? I know it has a lot of Scala-like functionality.

BTW I recently looked into using TVM4J, but it looks like they're sorting out some stuff, so it might be good to circle back when they decide to publish a JVM library. Seems like TF4J is also making some progress, so it will probably be between the two. Haven't seen @tscholak in a while, but I saw he's doing a GSoC with hasktorch. It would be great to catch up at some point after all the dust settles down. How are things on your end? Hopefully things return to normal again soon!

[tribbloid]

For arrow-kit

Scala DSL should be for scala users, kotlin follows a different design philosophy.

But I'm tempted, so I wrote some random showcase in both scala & kotlin:

• in scala:

    val x3 = DoubleVector(1.0, 2.0, 3.0)
    val x50 = DoubleVector(
      1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 0.0, //
      1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 0.0, //
      1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 0.0, //
      1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 0.0, //
      1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 0.0, //
    )

    val y3 = DoubleVector.random(3)
    val y6 = DoubleVector.random(6)
    val y50 = DoubleVector.random(50)
    val y53 = DoubleVector.random(53)

    println(x3 dot_* y3)

//    x3 dot_* y4  doesn't compile

    println((y3 concat y50) dot_* y53)

    println((x50 concat y3) dot_* y53)

//    (x50 concat y3) dot_* y6  doesn't compile

• In kotlin:

    val x3 = DoubleVector(1.0, 2.0, 3.0)
// throws 'Too many arguments for public constructor'
    val y3 = DoubleVector.random(3)
// throws 'Does not conform to expected type'

Oops, doesn't work. I guess scala use too much syntax sugar for compiling.

I didn't have a lot of experience with kotlin, but I can see that arrow is very ambitious, almost equivalent to rewriting the compiler. Not doubt it will make many things easier (e.g. getting rid of that code generator). However, I still didn't see the ability to summon axioms & proofs at type level, which is important once tensor operation start to get hairy (e.g. the concat in the above showcase, the compiler automatically summoned the proof that 50+3 == 53). I'll be surprised if they add this feature later, as kotlin's design philosophy deliberately stated that compilation should be fast.

[tribbloid]

For TVM4J

We don't need to wait for TVM4J release/publishing, it is at the opposite end of our layer of abstraction. We could only think about AutoDiff, shape safety & forward/backward rule generation, while let the boys at DMLC to worry about model compilation and deployment, their tools will definitely keep up with latest TVM release.

Then I just realised that TVM just moved out from DMLC lately, so I may need to study their politics before making a prediction :-<

[breandan]

I still didn't see the ability to summon axioms & proofs at type level,

I believe the Arrow folks are adding support for type proofs, but it's still early in development. I had a chat with @pakoito about type level integers a while ago, not sure if this is a prototype for arrow-meta proofs or just a design discussion. It would be interesting to see if were possible to push this direction a bit further, maybe it is possible to do some form of type-level arithmetic for concatenation and slicing. Maybe you could even implement shape-safe convolution operators. Tempted to try.

Scala DSL should be for scala users, kotlin follows a different design philosophy.

I see, so you want to consume Kotlin∇ from Scala. I guess it makes sense. I know there is an existing shape-safe tensor library for Scala called nexus, it might be interesting to compare what @ctongfei was doing with your planned DSL to see if there is anything that could be borrowed or improved. Right now, our AD implementation is pretty coupled with the shape-checking stuff, but it should be possible to provide a shapeless AD implementation, as you mention it would probably be a lot easier to implement the Kotlin∇ shape system in Scala anyway.

[tribbloid]

On nexus

No they don't, I've used it for a long time and it's in his TODO list forever:

[TODO] Typesafe tensor sizes using literal singleton types (Scala 2.13+)

I probably should remind him that 2.13 is not required

[breandan]

Interesting, I was not aware of this! Do you think singleton types are capable of supporting convolutional arithmetic? I have seen implementations of addition and subtraction using Presburger arithmetic.

If you were able to persuade Scala/Shapeless into performing multiplication and division at the type level, that would be pretty impressive/paperworthy. Maybe you could start out with something simple like unit strides which just requires doubling, addition and subtraction:

Then maybe work your way up to dialated convolution which requires multiplication, division and floor:

[tribbloid]

Yep, easy. See my example at: https://github.com/tribbloid/shapesafe/blob/49a1c5b29d6d1ec619b2decd38c4b716cdeef713/demo/src/main/scala/edu/umontreal/kotlingrad/shapesafe/demo/DoubleVectorDemo.scala#L35-L35

{
  val conved = x50.conv(x3)
  println(conved.data.size)

  conved.arity.internal.requireEqual(48)
  //    conved.arity.internal.requireEqual(49) // doesn't compile
}

{
  val conved = x50.pad(5).conv(x3, 2)
  println(conved.data.size)

  conved.arity.internal.requireEqual(29)
  //    conved.arity.internal.requireEqual(28) // doesn't compile
}

OK it’s not easy at all, I spent too much time trying to get implicit view pattern & singleton summoner pattern to work, until the legendary @DmytroMitin pointed out that type class is still the best option.

The experiment code had some drastic changes to allow short definition of complex arithmetic, the one related to convolution is right here:

https://github.com/tribbloid/shapesafe/blob/49a1c5b29d6d1ec619b2decd38c4b716cdeef713/core/src/main/scala/edu/umontreal/kotlingrad/shapesafe/core/tensor/DoubleVector.scala#L99-L99

[tribbloid]

just found his project:

https://summerofcode.withgoogle.com/projects/#5862505638789120

Nice work!

[breandan]

Very nice! I've been playing around with this a bit and just had a few comments/questions:

• Vectors do not (yet?) compose. Vector(Vector(0.0), Vector(0.0)) produces:

[Error] ... could not find implicit value for parameter proofOfType: edu.umontreal.kotlingrad.shapesafe.m.util.Constraint.ElementOfType[edu.umontreal.kotlingrad.shapesafe.core.tensor.DoubleVector[edu.umontreal.kotlingrad.shapesafe.m.arity.Arity.FromOp[singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.ToInt,shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]],Int(0),Int(0)]]] :: edu.umontreal.kotlingrad.shapesafe.core.tensor.DoubleVector[edu.umontreal.kotlingrad.shapesafe.m.arity.Arity.FromOp[singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.ToInt,shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]],Int(0),Int(0)]]] :: shapeless.HNil,Double]

• Singleton types are unreadable. May be it's possible to have literal singletons as you mentioned above?

val x3: DoubleVector[Arity.FromOp[NatAsOp[Succ[Succ[Succ[_0]]]]]] = DoubleVector(1.0, 2.0, 3.0)
val x3: DoubleVector[3] = DoubleVector(1.0, 2.0, 3.0)

• How do you define a function with a fixed arity?

def vec6id(vec: DoubleVector[Arity.FromOp[NatAsOp[Succ[Succ[Succ[Succ[Succ[Succ[_0]]]]]]]]]) = vec
val t = vec6id(x3 concat y3)

[Error] ... polymorphic expression cannot be instantiated to expected type;
 found   : [P <: edu.umontreal.kotlingrad.shapesafe.m.arity.Proof]edu.umontreal.kotlingrad.shapesafe.core.tensor.DoubleVector[P#Out]
 required: edu.umontreal.kotlingrad.shapesafe.core.tensor.DoubleVector[edu.umontreal.kotlingrad.shapesafe.m.arity.Arity.FromOp[edu.umontreal.kotlingrad.shapesafe.m.arity.Utils.NatAsOp[shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless.Nat._0]]]]]]]]]
    (which expands to)  edu.umontreal.kotlingrad.shapesafe.core.tensor.DoubleVector[edu.umontreal.kotlingrad.shapesafe.m.arity.Arity.FromOp[singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.ToInt,shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]]]],Int(0),Int(0)]]]

• How do you write a function where one argument is fixed and the other is generic?

def vec3id(x3: DoubleVector[Arity.FromOp[NatAsOp[Succ[Succ[Succ[_0]]]]]], y3: DoubleVector[Arity.FromLiteral[Lt[Int]#T]]) = x3
val t = vec3id(x3, x3) dot_* x3

[Error] ... type mismatch;
 found   : edu.umontreal.kotlingrad.shapesafe.core.tensor.DoubleVector[edu.umontreal.kotlingrad.shapesafe.m.arity.Arity.FromLiteral[Int(3)]]
 required: edu.umontreal.kotlingrad.shapesafe.core.tensor.DoubleVector[edu.umontreal.kotlingrad.shapesafe.m.arity.Arity.FromLiteral[shapeless.Witness{type T <: Int}#T]]

• Minor issue, but the Scala plugin for IntelliJ IDEA does not type check compound expressions and must wait for compilation. This is probably the correct behavior for type proofs, but it might be possible to make this easier for the IDE to check.

[tribbloid]

at your service. These are my answers:

Vectors do not (yet?) compose.

The POC had only implemented DoubleVector, Not matrix or tensor. They are not difficult (ideally by stealing code from dotty tuple: scala/scala3#2199), just need a lot of code. Also, I'm using good old breeze as data representation but its a bit obsolete, it should move to a representation that supports at least big data (Apache Arrow, DJL), symbols and dual numbers (your library), or both.

[tribbloid]

How do you define a function with a fixed arity?

easy:

    val _3 = Arity(3)

    def printD3[A <: Shape](v: DoubleVector[A])(
      implicit
      proofOfArity: A MayEqual _3.Out ~~> Proof
    ): Unit = {

      println(v)
    }

    printD3(DoubleVector.random(3))

//    printD3(DoubleVector.random(4)) // doesn't compile

I'm kind of bothered by the church encoded Nat type as it crashed my compiler fairly often. I would recommend converting them ASAP using an implicit edu.umontreal.kotlingrad.shapesafe.m.arity.nullary.OfSize, or avoiding them all together and use strictly Witness or 2.13 Singleton

[tribbloid]

How do you write a function where one argument is fixed and the other is generic

You just need to summon proofOfArity for 1 of them, something like:

    def printD3[A <: Shape, B <: Shape](v1: DoubleVector[A], v2: DoubleVector[B])(
      implicit
      proofOfArity: A MayEqual _3.Out ~~> Proof
    )
...

edu.umontreal.kotlingrad.shapesafe.core.tensor.Shape -> Operand is just a computation graph, Only after implicit proof Summoning (Operand ~~> Proof | Proof.Out) could it be transformed into Arity. if you don't summon the proof they will never be computed. Some of my Vector API (e.g. pad) doesn't summon the proof because they will always succeed. You can even avoid summoning in all APIs and do it lazily (by using DoubleVector.reify at last) but it is kind of shabby

[tribbloid]

Minor issue, but the Scala plugin for IntelliJ IDEA does not type check compound expressions and must wait for compilation

Even worse, sometimes it gives false errors for type check. I'm always kind of jealous of F# programmers on Windows, they IDE never diverge from the compiler. But it is bad politics, Jetbrains thinks scalac:

• changes too fast at the whim of Prof Odersky

• has a conflict of interest with kotlin

So it probably doesn't worth their time. The problem is well know in scala community, and I heard that dotty PM has ditched their grad-student descent based methodology

[tribbloid]

I also have a few questions for you:

• How hard it is to implement graph simplification?

https://enoki.readthedocs.io/en/master/autodiff.html#graph-simplification

For symbolic diff this could be tested by:

$$ \frac{d (2 x^2 + 3 x^2)}{d x} = 5 x $$

• Do you have an example or test case for symbolic diff?

The reason I'm asking is to see the difficulty of writing in JVM that implements/extends operands and graph nodes of a low level autodiff IR (e.g. RelayIR in TVM2). I was initially against it as I thought it embodies too much work, but on second thought I believe you made the right decision: In prototyping stage people may encounter all kinds of esoteric functions, and if they can't insert it into the graph without some serious hacking, they may be forced to ditch the effort.