thealmarty

--As modified from the Prelude:
zip_no_zero ::(Num a, Eq a, Num b, Eq b)=> [a] -> [b] -> [(a,b)]
zip_no_zero []     _bs    = []
zip_no_zero _as    []     = []
--Add to p: when any of the input lists' first element is zero.
zip_no_zero (0:as) _bs    = []
zip_no_zero _as    (0:bs) = []

zip_no_zero (a:as) (b:bs) = (a,b) : zip_no_zero as bs

thealmarty

-- | The 'zipWith8' function takes a function which combines eight
-- elements, as well as eight lists and returns a list of their point-wise
-- combination, analogous to 'zipWith'.
zipWith8                :: (a->b->c->d->e->f->g->h->i) ->
                           [a]->[b]->[c]->[d]->[e]->[f]->[g]->[h]->[i]
zipWith8 z (a:as) (b:bs) (c:cs) (d:ds) (e:es) (f:fs) (g:gs) (h:hs)
                   =  z a b c d e f g h : zipWith8 z as bs cs ds es fs gs hs
zipWith8 _ _ _ _ _ _ _ _ _ = []

-- | The 'zip8' function takes eight lists and returns a list of

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

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

thealmarty

MVP unification implementation plan

The implementation of unification (inference) following this document can be split into a few smaller, separate tasks/PRs for smoother transition and easier testing.

Stage 1: Type checker enhancement

At the time of writing, the first stage of the totality checker MVP is finished. But the second and third stages, namely type checking data type and function declarations are required before unification can be implemented.

At the end of this stage, conversion/type checking for constructors is implemented.