Skip to content
Juvix imports 

module prelude;

import Stdlib.Trait open public;
import Data.Set.AVL open;

Common Types - Juvix Base Prelude

The following are frequent and basic abstractions used in the Anoma specification. Most of them are defined in the Juvix standard library and are used to define more complex types in the Anoma Specification.

Nat

The type Nat represents natural numbers (non-negative integers). Used for counting and indexing.

import Stdlib.Data.Nat as Nat open using {Nat; zero; suc; natToString} public;

For example,

ten : Nat := 10;

Bool

The type Bool represents boolean values (true or false). Used for logical operations and conditions.

import Stdlib.Data.Bool as Bool open using {Bool; true; false; ite; &&; not; or; and} public;

For example,

verdad : Bool := true;

String

The type String represents sequences of characters. Used for text and communication.

import Stdlib.Data.String as String open using {String} public;

For example,

hello : String := "Hello, World!";

Unit

The type Unit represents a type with a single value. Often used when a function does not return any meaningful value.

import Stdlib.Data.Unit as Unit open using {Unit; unit} public;

For example,

unitValue : Unit := unit;

Pair A B

The type Pair A B represents a tuple containing two elements of types A and B. Useful for grouping related values together.

import Stdlib.Data.Pair as Pair;

open Pair using {Pair} public;

open Pair using {,};
import Stdlib.Data.Fixity open;

syntax operator mkPair none;

syntax alias mkPair := ,;

For example,

pair : Pair Nat Bool := mkPair 42 true;

Projections

fst {A B} : Pair A B -> A
  | (mkPair a _) := a;
snd {A B} : Pair A B -> B
  | (mkPair _ b) := b;

Result A B

The Result A B type represents either a success with a value of ok x with x of type A or an error with value error e with e of type B.

import Stdlib.Data.Result.Base as Result;

open Result using {Result; ok; error} public;

Either A B

The type Either A B, or sum type of A and B, represents a value of type A or B. It is equivalent to Result A B, however, the meaning of the values is different. There is no such thing as an error or success value in the Either type, instead the values are either left A or right B. either left A or right B.

syntax alias Either := Result;

syntax alias left := error;

syntax alias right := ok;

For example,

thisString : Either String Nat := left "Error!";

thisNumber : Either String Nat := right 42;

List A

The type List A represents a sequence of elements of type A. Used for collections and ordered data.

import Stdlib.Data.List as List open using {List; nil; ::} public;

For example,

numbers : List Nat := 1 :: 2 :: 3 :: nil;

niceNumbers : List Nat := [1; 2; 3];

Option A

The type Option A represents an optional value of type A. It can be either Some A (containing a value) or None (no value). This type is an alias for Maybe A from the standard library.

import Stdlib.Data.Maybe as Maybe;

open Maybe using {Maybe; just; nothing};
syntax alias Option := Maybe;

syntax alias some := just;

syntax alias none := nothing;

Map K V

The type Map K V represents a collection of key-value pairs, sometimes called a dictionary, where keys are of type K and values are of type V.

import Data.Map as Map public;

open Map using {Map} public;

For example,

codeToken : Map Nat String := Map.fromList [1, "BTC"; 2, "ETH"; 3, "ANM"];

Set A

The type Set A represents a collection of unique elements of type A. Used for sets of values.

import Data.Set as Set public;

open Set using {Set} public;

For example,

uniqueNumbers : Set Nat := Set.fromList [1; 2; 2; 2; 3];

Undefined values

The term undef is a placeholder for unspecified values.

axiom undef : {A : Type} -> A;

For example,

undefinedNat : Nat := undef;

-- TODO: perhaps remove the following sections once the stdlib is updated

Functor

import Stdlib.Trait.Functor.Polymorphic as Functor;

Applicative

import Stdlib.Data.Fixity open public;

{-# isabelle-ignore: true #-}
trait
type Applicative (f : Type -> Type) :=
  mkApplicative {
    {{ApplicativeFunctor}} : Functor f;
    pure : {A : Type} -> A -> f A;
    ap : {A B : Type} -> f (A -> B) -> f A -> f B
  };

For example, the Option type is an instance of Applicative.

{-# isabelle-ignore: true #-}
instance
maybeApplicative : Applicative Option :=
  mkApplicative@{
    pure := some;
    ap {A B} : Option (A -> B) -> Option A -> Option B
      | (some f) (some x) := some (f x)
      | _ _ := none
  };

Monad

{-# isabelle-ignore: true #-}
trait
type Monad (f : Type -> Type) :=
  mkMonad {
    {{MonadApplicative}} : Applicative f;
    builtin monad-bind
    bind : {A B : Type} -> f A -> (A -> f B) -> f B
  };
syntax operator >>= seq;

{-# isabelle-ignore: true #-}
>>= {A B} {f : Type -> Type} {{Monad f}} (x : f A) (g : A -> f B) : f B :=
  Monad.bind x g;
{-# isabelle-ignore: true #-}
monadMap {A B} {f : Type -> Type} {{Monad f}} (g : A -> B) (x : f A) : f B :=
  map g x;

For example, the Option type is an instance of Monad.

{-# isabelle-ignore: true #-}
instance
maybeMonad : Monad Option :=
  mkMonad@{
    bind {A B} : Option A -> (A -> Option B) -> Option B
      | none _ := none
      | (some a) f := f a
  };
open Applicative public;

open Monad public;

AVLTree

terminating
AVLfilter {A} {{Ord A}} (pred : A -> Bool) (t : AVLTree A) : AVLTree A :=
  let
    merge : AVLTree A -> AVLTree A -> AVLTree A
      | t empty := t
      | empty t := t
      | t1 t2 :=
        case lookupMin t2 of
          | nothing := t1
          | some minVal :=
            let
              newT2 := delete minVal t2;
            in balance (mknode minVal t1 newT2);
  in case t of
       | empty := empty
       | node x _ l r :=
         let
           terminating
           filteredLeft := AVLfilter pred l;
           terminating
           filteredRight := AVLfilter pred r;
         in case pred x of
              | true := balance (mknode x filteredLeft filteredRight)
              | false := merge filteredLeft filteredRight;