thealmarty

(* Define the unfold function.*)
let rec unfold p g b1 b2 =
  if p b1 b2 then [] else
    (match g b1 b2 with (a, (b1prime, b2prime)) ->
       a :: unfold p g b1prime b2prime)
;;

(* Define the zip_sum function.*)
let zip_sum = unfold
  (* Define p.*)

thealmarty

(* Define the unfold function that takes 3 inputs.*)
let rec unfold p g b1 b2 b3 =
  if p b1 b2 b3 then [] else
    (match g b1 b2 b3 with (a, (b1prime, b2prime, b3prime)) ->
       a :: unfold p g b1prime b2prime b3prime)
;;

(* Define the zip3 function.*)
let zip3 = unfold
  (* Define p.*)

thealmarty

let rec unfold p g b =
  if p b then [] else
    (match g b with (a, bprime) ->
       a :: unfold p g bprime)

let fact n =
  List.fold_right 
    (* The fold's function input is the times function.*) 
    (fun x y -> x * y)  
    (* The fold's list input is the result of this unfold. *)

thealmarty

import Data.List  --To enable unfoldr.
fact n =
  foldr
    (*) --Function input
    1   --Base case
    (unfoldr  --List input
      (\n -> if n==0 then Nothing else Just (n, n-1))
      n)

--Print out example results of the fact fn.

thealmarty

--Factorial function, short/standard version.
  
fact 0 = 1
fact n = n * fact (n - 1)

main = do
  print (fact 5)

thealmarty

type account = {
  balance : nat;
  allowances : (address, nat) map;
}

type storage = {
  accounts : (address, account) big_map;
  version : nat; 
  totalSupply : nat;
  name : string;

thealmarty

Potential Juvix features enabled by graph neural networks and machine learning

The rapid development of machine learning (ML) enables practical applications including in smart contract development. As a superior smart contract language, Juvix can provide extra support using ML in the following fronts:

1. Generate correctness proofs

See this paper. When combining the mechanics of Proverbot9001, CoqHammer and CoqGym, a meaningful portion (28%) of the correctness proofs of CompCert (written in Coq) was generated. Note that the difficulties of the generated proofs are evenly distributed - i.e., it is not only generating proofs that are trivial for users to write.

Juvix is built with the intent that smart contracts written in it are more secure because users can write proofs to prove important properties of a contract. However, writing proofs is a tedious and costly task. Juvix would be much more attractive if it can write a significant portion of the proof

thealmarty

Lessons from Idris 2

This note summarizes what Juvix can learn from the implementation of Idris 2. References:

• The paper.
• Scottish summer school 2020 slides/notes.
• Video lectures of the summer school.
• The implementation documentation.

Syntax/theory on linearity

thealmarty

Unification in Idris 2

Unification concerns type/conversion checking with the presence of meta-variables. Meta-variables are variables with unknown values but type checking/elaboration progress could generate constraints that these variables have to satisfy and thus find the solutions to these variables. Implicits (and implicit arguments) are inferred by unification.

Conversion checking (of terms and closures) determines whether the two inputs are equivalent. Similarly, unification determines whether the two inputs are equivalent with the presence of meta-variables. Naturally, unification is implemented as an extension to conversion checking.

thealmarty

Efficient compilation of function definitions with pattern-matching

Function definitions with pattern-matching can be compiled into case-expressions for more efficient evaluation using the pattern matching compiler algorithm. The algorithm translates function definitions into case-expressions and avoids repeated examination of patterns.

I summarize the pattern matching compiler algorithm here as in chapter 5 of The implementation of functional programming languages.

The algorithm

A function definition of the form