All Projects → tribbloid → shapesafe

tribbloid / shapesafe

Licence: Apache-2.0 license
SHAPE/S∀F∃: static prover/type-checker for N-D array programming in Scala, a use case of intuitionistic type theory

Programming Languages

scala
5932 projects
kotlin
9241 projects
shell
77523 projects

Projects that are alternatives of or similar to shapesafe

Foundational Knowledge For Programmers
List of resources about foundational knowledge for programmers (supposed to last a few decades)
Stars: ✭ 115 (+576.47%)
Mutual labels:  linear-algebra, type-theory
pressio
Model reduction for linear and nonlinear dynamical systems: core C++ library
Stars: ✭ 35 (+105.88%)
Mutual labels:  linear-algebra
reading-material
Reading schedule and our library of pdfs
Stars: ✭ 19 (+11.76%)
Mutual labels:  type-theory
LSQR-cpp
This is a c++ port initially performed by Luis Ibanez of the LSQR library of Chris Paige and Michael Saunders. The same methodology was applied to the LSMR library of David Fong and Michael Saunders.
Stars: ✭ 19 (+11.76%)
Mutual labels:  linear-algebra
susa
High Performance Computing (HPC) and Signal Processing Framework
Stars: ✭ 55 (+223.53%)
Mutual labels:  linear-algebra
JUDI.jl
Julia Devito inversion.
Stars: ✭ 71 (+317.65%)
Mutual labels:  linear-algebra
linalg
Linear algebra library based on LAPACK
Stars: ✭ 42 (+147.06%)
Mutual labels:  linear-algebra
Pseudospectra.jl
Julia package for matrix pseudospectra and related quantities
Stars: ✭ 21 (+23.53%)
Mutual labels:  linear-algebra
minitt-rs
Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust
Stars: ✭ 101 (+494.12%)
Mutual labels:  type-theory
dtt
A C++ header-only for data transfer between linear algebra libraries (Eigen, Armadillo, OpenCV, ArrayFire, LibTorch).
Stars: ✭ 74 (+335.29%)
Mutual labels:  linear-algebra
gidti
Book: Gentle Introduction to Dependent Types with Idris
Stars: ✭ 70 (+311.76%)
Mutual labels:  type-theory
AlgebraLinear
Escrita colaborativa de recursos educacionais abertos sobre álgebra linear.
Stars: ✭ 57 (+235.29%)
Mutual labels:  linear-algebra
GlobalBioIm
A unifying Matlab framework for the development of reconstruction algorithms (solving inverse problems) in computational imaging
Stars: ✭ 60 (+252.94%)
Mutual labels:  linear-algebra
NAGPythonExamples
Examples and demos showing how to call functions from the NAG Library for Python
Stars: ✭ 46 (+170.59%)
Mutual labels:  linear-algebra
voile-rs
Dependently-typed row-polymorphic programming language, evolved from minitt-rs
Stars: ✭ 89 (+423.53%)
Mutual labels:  type-theory
mathcore
Advanced .NET math library (.NET Standard).
Stars: ✭ 24 (+41.18%)
Mutual labels:  linear-algebra
linnea
Linnea is an experimental tool for the automatic generation of optimized code for linear algebra problems.
Stars: ✭ 60 (+252.94%)
Mutual labels:  linear-algebra
flatorize
Generate fast implementations of mathematical expressions. Inclues a linear algebra library.
Stars: ✭ 18 (+5.88%)
Mutual labels:  linear-algebra
zlm
Zig linear mathemathics
Stars: ✭ 67 (+294.12%)
Mutual labels:  linear-algebra
MLweb
Machine learning and scientific computing (linear algebra, statistics, optimization) javascript libraries, with an online lab.
Stars: ✭ 85 (+400%)
Mutual labels:  linear-algebra

SHAPE/S∀F∃

shapesafe is the one-size-fits-all compile-time verifier for numerical linear algebra on JVM, obvious shape and indexing errors in tensor operations are captured by scala's typing system.

Shapesafe allows programs to actively prove themselves while being written. The following capabilities are enabled in release v0.1.0:

static & runtime-dependent tensor shapes of arbitrary rank

S1

named tensor: each dimension is indexed by both its name and ordinal number

S2

tensor contractions & operations that depends on index equality, (all cases of EinSum, dot/cross/matrix/hadamard product)

S3

operations that depends on shape arithmetics (convolution, direct sum, kronecker product, flatten/reshape)

S4

complex function composition, with no implicit scope

S5

These screenshots can be reproduced by compiling our showcases in Visual Studio Code + Scala (Metals) plugin:

It is not a tensor computing library! Instead, it is designed to be embedded into existing libraries to enable less error-prone prototyping (see Roadmap for possible augmentations).

shapesafe started as an experiment to understand intuitionistic type theory used in compiler design, it minimally depends on singleton-ops and shapeless.

Support for scala-2.13 is always guaranteed, supports for scala-2.12 or scala-js should only be enforced intermittently and upon request, please create (or vote for) tickets to backport for a specific compiler.

Build Status

branch \ profile Scala-2.13 Scala-2.13 w/ splain plugin
master CI CI
0.1.4 CI CI
0.1.3 CI CI
0.1.2 CI CI
0.1.1 CI CI
0.1.0 CI CI
dev (latest WIP) CI CI-legacy

Tutorial

Roadmap

High priority
  • Symbolic reasoning for variable dimensions, using Ring/Field axioms and natural deduction
  • Type-checking for EinOps
  • DJL integration
Low priority
  • DL4j & ND4j integration
  • breeze integration (only tensors to up to rank-2 is required)

How to compile

In POSIX shell, run ./dev/make-all.sh

Guaranteed to be working by Continuous Integration

You must have installed a JDK that supports Gradle 7+ before the compilation

Architecture (Recommended for user who finished our tutorial)

Lazy Verification

It can be observed immediately in the tutorial that calling functions in shapesafe requires no implicit summoning of type class. In fact, their return types are represented as computation graphs rather than computed Arities or Shapes. As a trade-off, errors in these computation graphs can't be detected as-is:

val a = Shape(1, 2)
val b = Shape(3, 4)
val s1 = (a >< b).:<<=*("i", "j")
s1.peek

// [INFO] 1 >< 2 >< (3 >< 4) :<<= (i >< j)

This is a deliberate design which allows complex operand compositions to be defined with no boilerplate (see example above and TutorialPart1/StaticReasoning).

Detection of errors only happens once the expression is evaluated (by explicitly calling .eval or .reason), which summons all algebraic rules like a proof assistant:

s1.eval

// [ERROR] Dimension mismatch
//   ...

In the above example, calling eval instructs the compiler to summon a series of type classes as lemmata to prove / refute the correctness of the expression:

lemma expression
(1 >< 2) >< (3 >< 4) :<<= (i >< j)
(prove outer product) = 1 >< 2 >< 3 >< 4 :<<= (i >< j)
(refute naming of tensor: Dimension mismatch) !

Evidently, eval can only be used iff. each shape operand in the expression (in the above example a and b) is either already evaluated, or can be evaluated in the same scope. This is the only case when implicit arguments has to be declared by the user.

At this moment, all algebraic rules are defined to manipulate the following 2 types of expressions:

  • Arity - describing 1D vectors:

Arity

  • Shape - describing ND tensors:

Shape

Shapesafe works most efficiently if dimensions of all tensors are either constants (represented by shapesafe.core.arity.Const), or unchecked (represented by shapesafe.core.arity.Unchecked, meaning that it has no constraint or symbol, and should be ignored in validation). In practice, this can reliably support the majority of applied linear algebra / ML use cases. Support for symbolic algebra for shape variables (represented by shapesafe.core.arity.Var) will be gradually enabled in future releases.

Upgrade to Scala 3

Most features in shapeless & singleton-ops are taken over by native compiler features:

  • shapeless.Witness → singleton type
  • shapeless.Poly → polymorphic function
  • singleton.ops.== → inline conditions & matches
  • singleton.ops._ → scala.compiletime.ops.*
  • shapeless.HList → Tuple
  • shapeless.record → Programmatic Structural Types

... but some are still missing:

  • Product to Tuple conversion, plus its variants:
    • shapeless.NatProductArgs
    • shapeless.SingletonProductArgs
  • ecosystem: Apache Spark, CHISEL, LMS, typelevel stack, and much more

Scala 3/dotty appears to be vastly more capable as a "proof assistant", with 15~20x speed improvement over Scala 2 on implicit search. This seems to indicate that shapesafe could only achieve large scale, production-grade algebraic verification after the upgrade is finished. At this moment (with Scala 2.13), if the implicit search on your computer is too slow, consider breaking you big operand composition into multiple small ones, and evaluate in-between as often as possible.

Extra Read

Credit

This project is heavily influenced by Kotlin∇ (see discussion here) and several pioneers in type-safe ML:

Many have answered critical questions that have guided how the project evolves:

  • Torsten Scholak - API, compiler, gradual typing
  • Alex Merritt - API, IR, documents
  • Cameron Rose - API
  • Arseniy Zhizhelev - Scala 3 upgrade
  • Ryan Orendorff - Automated theorem proving

$$ \frac{\mathrm{S} \mathrm{H} \mathrm{A} \mathrm{P} \mathrm{E}}{: \mathrm{S} : \forall \mathrm{F} : \exists} : \vee : 0.1.4 $$

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].