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!
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
showcasing 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.
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.
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.
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.
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
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."
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:
Does not appear within the argument types of its constructors, or
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