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 webpage.
Make sure to mark your calendar for the following key sessions:
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:
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.