Skip to content

Juvix Blog

Welcome! Join us in our cozy corner as we explore functional programming and next-generation distributed apps, sharing insights on Juvix, its development, and discussing related concepts. Stay tuned for our upcoming events and let's embark on this exciting journey together!

Compiling to VampIR through Geb


The compilation described is currently not supported by the newest version of Juvix and Geb. Changes are forthcoming.

Before, we discussed the standard normalization approach to compiling Juvix programs to VampIR. An alternative backend is provided by the Geb project currently implemented in Lisp providing a categorical view of the needed translations.

The post will be devoted to discussing the core ideas of Geb, the practical steps to take in order to use the corresponding pipeline, as well as the current limitations the backend faces.

We assume basic familiarity with categorical concepts and VampIR.

Geb Pipeline

Geb is a developing language providing a useful interface for specifying categorical constructs and helping define compilers in terms of functors. The approach is inspired by a classical observation that instead of dealing with 'good' compilation procedures one can instead specify functors between appropriate categories representing the languages one initially considers.

In the current state of development, Geb is a fairly simple category in which one can do "basic arithmetic." It is a category freely spanned by terminal/initial objects and finite (co)products with additional constructs for objects representing n-bit natural numbers. The pipeline itself is a string of functors between categories:

Compiling Juvix programs to arithmetic circuits via Vamp-IR

Since version 0.3.5, the Juvix compiler supports the vampir target which generates Vamp-IR input files that can be compiled to various proof systems based on arithmetic circuits, like Plonk or Halo 2. Vamp-IR is a proof-system-agnostic language for writing arithmetic circuits.

In this post, we will not be discussing the details of Vamp-IR or the circuit computation model. Instead, we will describe how high-level functional Juvix programs can be compiled to circuits, what the common pitfalls and current limitations are. The reader is assumed to have at least basic familiarity with Vamp-IR.

Iterator syntax

A common pattern in functional programming is the traversal of data structures, particularly lists, in a specified order accumulating some values. If you've used languages like Haskell or OCaml, you must have come across the "fold left" (foldl) and "fold right" (foldr) higher-order functions which implement this pattern. These functions are also available in Juvix. In this blog post, I describe an iterator syntax I designed for Juvix which allows expressing folds (and maps, filters and more) in a readable manner.

Join Juvix Team at ETHPrague

The Juvix team is excited to announce our participation in ETHPrague 2023, an Ethereum-focused event happening in Prague, Czech Republic, from June 8-11.

Join us for an immersive experience where you can learn about the current state of the Juvix language, explore and create real-world applications built with Juvix, and engage in discussions about the future possibilities and exciting plans we have in store.

The event

ETHPrague is a premier blockchain event that brings together the global Ethereum community to discuss the future of Ethereum, blockchain technology, and new concepts. It provides a platform for knowledge sharing, networking, and collaboration among enthusiasts, experts, and visionaries.

The event features an impressive lineup of speakers, including the esteemed Vitalik Buterin. With engaging panels, workshops, and even a hackathon, ETHPrague offers abundant opportunities to learn, network, and connect with exceptional individuals and communities.

The event will take place from June 8th to June 11th in the beautiful city of Prague, Czech Republic. For more information, please visit the official event webpage.

Make sure to mark your calendar for the following key sessions:

  • Talk by Veronika Romashkina: On Saturday, June 10th, from 14:10 - 14:30 at the Institute of Cryptoanarchy, Veronika, Developer Relations at Heliax, will present a talk titled "Juvix: Toward a Functional Programming Language for Decentralized Applications and Beyond."
  • Workshop by Paul Cadman: Also on Saturday, June 10th, from 16:20 - 17:20 at the Paper Hub, Paul, Compiler Engineer at Heliax, will host a workshop titled "Discovering Juvix: The High-Level Functional Programming Language for Building Next-Generation dApps."

Stay Positive with Your Data Types

In this discussion, we will explore the concept of strictly positive inductive data types, a critical requirement within the Juvix framework for classifying a data type as well-typed.

An inductive type is considered strictly positive if it either:

  1. Does not appear within the argument types of its constructors, or
  2. Appears strictly positively within the argument types of its constructors.

A name is considered strictly positive for an inductive type if it never appears in a negative position within the argument types of its constructors. The term negative position denotes instances located to the left of an arrow in a type constructor argument.