Vouivre Digital

Dependent type infrastructure for machine learning

Vouivre

Partial function application, compile time arity verification, automatic differentiation, and built to coexist with Scheme using the Guile compiler.

> (reduce + (map (flip expt 2) '(0 1 2 3)))
14

Partial application

The sum of squares of a list.

(definec (f x θ) (adot θ x 1))

(definec (mse x y) (mean (expt (- y x) 2)))

(definec loss (∘ (mse #0(1)) (f #(1/4 3/4))))

> (map loss '(#(4 4/3) #(1 0) #(2 2/3)))
(1 9/16 0)

Defining new functions

Loss over parameters `θ' of a model `f' evaluated at `x' = #(1/4 3/4) using the mean square error `mse' with respect to an expected output of 1.

> (map (rdiff loss) '(#(4 4/3) #(1 0) #(2 2/3)))
(#(1/2 3/2) #(-3/8 -9/8) #(0 0))

> (map (fdiff (flip expt 2)) '(0 1 2 3))
(0 2 4 6)

Automatic differentiation

The derivative of the loss at each input and the derivative 2x of x^2.

> (type-of 'not)
(0 . 0)


> (type-of '∘)
((6 . 7) . ((8 . 6) . (8 . 7)))

Types

Currently, cons cell are function types, 0 is the type of anything but functions, and numbers greater than 0 are type variables.

newstutorialdocumentationdownload

In development

Features we are currently working on.

(∷ concatenate-vectors
   (Π (: a Set)
      (Π (: m ℕ)
	 (Π (: n ℕ)
	    (→ (Vec a m)
	       (→ (Vec a n)
		  (Vec a (+_ℕ m n))))))))

(concatenate-vectors ℝ 1 2 #(-0.66) #(0.06 -0.34))

Dependent types

Prototypical, sugar-free example, expressing the type of a function that returns a vector the length of which is the sum of lengths of two input vectors, all vectors having elements of the same type.

More

  • Single-precision floating-points.
  • Parallelization.
  • Higher order differentiation.
  • Adam, convolutions, transformers, etc.
  • Improved embedding of the type system in Scheme.

Acknowledgements

We acknowledge and are grateful for the support of the NGI Zero Core project from NLnet.

Next Generation Internet initiative logo

License

The code distributed by Vouivre Digital is freedom software released under the GNU General Public License

Copyright (C) 2023-2024 Vouivre Digital Corporation

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program.  If not, see <https://www.gnu.org/licenses/>