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!

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.

Stay Positive

Let us 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.