For efficiency and easy of use it be useful to treat some basic types like Nat, Bool, String, List in a special way.

For example, Nat could be compiled to the integer type for each backend to support fast arithmetic.

In examples we have added bridge functions to convert from the backend Bool type to the minijuvix Bool type, so we can reuse functions in the backend that return Bool (see https://github.com/heliaxdev/minijuvix/blob/f9d9b10fc90acb2ba2cb83e249a7b4370644eeb2/tests/positive/FullExamples/PolySimpleFungibleToken.mjuvix for example):

foreign ghc {
  bool :: Bool -> a -> a -> a
  bool True x _ = x
  bool False _ y = y
};

foreign c {
  void* boolInd(_Bool b, void* then, void* else) {
    return b ? then : else;
  \}
}

axiom bool : BackendBool → Bool → Bool → Bool;
compile bool {
  ghc ↦ "bool";
  c ↦ "boolInd";
};

from-backend-bool : BackendBool → Bool;
from-backend-bool bb ≔ bool bb true false;

We should add support for this kind of bridging directly into the compiler.

Agda has a description of a similar feature: https://agda.readthedocs.io/en/latest/language/built-ins.html#

BackendAgda is in dev - https://github.com/heliaxdev/minijuvix/blob/7b1371c4b95752c23b54d40fe781f356c0ffb8dc/src/MiniJuvix/Syntax/Backends.hs#L5.

So I think we should remove it in a separate PR.

Originally posted by @paulcadman in https://github.com/heliaxdev/minijuvix/pull/68#discussion_r865053542

Our eventual goal is to compile validity predicates to WASM. As a first step we will compile to C.

For this issue we will generate C code from MonoJuvix (the monomorphized MiniJuvix dialect). Once this is available we will then generate WASM via LLVM or https://emscripten.org.

• Update the parser
• Update the scoper

35bca36fc3525204a4992c32a2861377cf005348

There is a list of warnings that we want to enable:

• -Wno-partial-fields
• -Wno-monomorphism-restriction
• -Wno-missing-local-signatures
• -Wno-all-missed-specialisations
• -Wno-missed-specialisations
• -Wno-missing-exported-signatures

Also, add NoFieldSelectors extension

We have a typechecked example of a dummy validity predicate at https://github.com/heliaxdev/minijuvix/blob/1e047b61b3633d4b3d9bb0080c8e682bbbf44e28/tests/positive/VP/SimpleFungibleToken.mjuvix

We should:

• Build a stub version of the Anoma vm_env library functions (read_pre etc) we're calling via FFI. (See the "extern C" interface at https://github.com/anoma/anoma/blob/3fb5b53dbc7961a8d0a4b1c425316a1c7752aa17/vm_env/src/imports.rs#L584)
• Figure out the GHC FFI code to make vm_env functions available in the microjuvix code.
• Add a main to SimpleFungibleToken.mjuvix so we can run the validity predicate.
• Figure out the steps to build / link / run the resulting artefact.

Higher order functions are not supported in the C backend.

This means we cannot compile functions like:

foldl : (A : Type) → (B : Type) → (B → A → B) → B → List A → B;

To do this we will need some way to represent closures C. An option for this is to use libffi.

Because of the implementation of the lexer, when there is a comment in the code that comes after a keyword,
the comment is highlighted as part of the keyword.
Example (in this case the keyword is ;:

When piping the output of minijuvix to a file we don't want the output to contain ANSI color codes.

We can achieve this by using:

hSupportsANSI :: Handle -> IO Bool

from the ansi-terminal package.

For example: Ansi.hSupportsANSI IO.stdout indicates whether stdout supports ANSI codes.

When prettyprinting:

• We should autodetect ANSI by default if no flag is specified.
• Respect the --no-color flag to disable ANSI codes.
• Respect the --color flag to enable ANSI codes.

See https://hackmd.io/A72oR4wYR-msPuFmU8f5rg?view

We want to see if we can achieve the following goal using the minihaskell backend (as opposed to going via LLVM).

Validity predicates

The first few VPs can be very simple. These neeed to be able to compile through LLVM to WASM and be compatible with the validity predicate interface of the Anoma ledger.

For background on the validity predicate interface of the Anoma ledger, see vp_template for the interface a validity predicate needs to provide - we’ll need to have this validate_tx interface provided by the WASM output of MiniJuvix. See here for some functions that should be available (as extern in > MiniJuvix) to validity predicates written in the MiniJuvix frontend, which then need to be compiled to appropriate calls in the LLVM/WASM (they are already defined using the C FFI, so hopefully this should be straightforward to implement).

For this issue we will see if we compile the minihaskell output to WASM, including the aroma FFI calls.

Current thoughts:

In MiniJuvix, a function declaration is a type signature and a group of definitions called function clauses.
To not bring inconsistencies by function declarations, MiniJuvix requires all functions to be total. In other words,
the program has to pass the termination checker and the coverage checker (future work).

fun : A → B;
fun case1 := ...;
fun case2 := ...;
fun case3 := ...;

The former requirement is vital but often tricky to fulfill for programs in a total language like MiniJuvix. This is why it is convenient to have a way to bypass the termination checking. The user may know their program is terminating when the termination checker algorithm can not see it. We support this feature in MiniJuvix with the terminating keyword. The syntax is the following.

terminating fun : A → B;

If a program fails the terminating checking, MiniJuvix will report to the user which function and function clauses failed the test. The report can be an error/warning to instruct the user where are the problematic calls.

The terminating keyword semantics. Annotating a function as terminating means that all its function clauses pass the termination checker's criterion, no matter what.

Not to be implemented but to be considered

• We may want to offer the possibility of marking a subset of the function clauses as terminating for the convenience of writing proofs/programs. Agda, for example, only reports the first problematic call and stops. It's quite strict, and I believe this approach opaques the development process. One solution to this issue is to make a separate lemma for the problematic function clause and mark it as terminating. Not nice! We could solve this inconvenience by permitting function clauses to be terminating.

terminating non-trivial: A → B;
non-trivial := ...;

... 
fun case3 := non-trivial a ;

vs

terminating fun case3 := ... ;

• Warn the user that a certain function passes the termination checker because one of its function calls was marked as being terminating

it should be removed

By default, we want to write programs that are terminating. Currently, the termination checker is not part of the Pipeline. It is just another command. The proposal here is to run this check just after running upToAbstract.

As part of solving this issue, a new global flag (e.g. --no-termination) can be added to disable the termination checker during the compilation.

Both pretty and typecheck subcommand should parse, scope and translate a MiniJuvix file to MicroJuvix.

The pretty subcommand should pretty print the resulting MicroJuvix file.
The typecheck subcommand should typecheck the MicroJuvix file and print any type errors.

Tasks:

• New folder lab for experimentations and notes
• move agda stuff and related files to lab
• Move wiki notes to lab

Code related tasks:

• Create meaningful labels
• Bump version to (0.1.0)
• Create the next two milestones (0.1.1) (0.1.2)
• Cleanup Makefile
• Remove unused Haskell packages
• Fix warnings as much as possible

In the following example:

module Poly;

inductive Bool {
  true : Bool;
  false : Bool;
};

inductive Pair (A : Type) (B : Type) {
 mkPair : A → B → Pair A B;
};

fst : (A : Type) → (B : Type) → Pair A B → A;
fst _ _ (mkPair a b) ≔ a;

fst-bool : Pair Bool Bool → Bool;
fst-bool ≔ fst Bool Bool;

end;

After running minijuvix --no-colors --show-name-ids monojuvix Poly.mjuvix:

module Poly@0 where

data Bool@1 =
  true@2
  | false@3

data Pair@14 =
  mkPair@15 Bool@1 Bool@1

fst@16 :: Pair@14 -> Bool@1
fst@16 (mkPair@7 a@11 b@12) = a@17

fst-bool@13 :: Pair@14 -> Bool@1
fst-bool@13 = fst@16

Notice that constructor mkPair@7 in the pattern of fst@16 doesn't match the constructor name mkPair@15. Also the local variable a@17 in the same pattern should be a@11.

When editing a minijuvix file, if there is a parse or scoper error when loading the file, a message like Symbol's value as variable is void: ....
This should be improved somehow.

Currently, the colors are not displayed prpoperly in the presence of import statements since there is overlapping of text properties.
Example:

Error with undefined or underscores

https://github.com/heliaxdev/minijuvix/blob/cb8e0fb91168c8827d63d8aa9d578e66dee3a80f/.github/workflows/ci.yml#L5

For scoper ambiguous symbol and ambiguous module symbol errors we currently report "TODO Ambiguous symbol" and "TODO Ambiguous module symbol" to the user.

We should provide a more informative error message (including locations of symbol definitions for example) to help the user resolve the ambiguity.

Currently the scope checker mangles top-level module names (as it does for all identifiers) to avoid name ambiguity. There will be no name ambiguity for top-level module names because they are required to be present in the file-system.

This is a problem for minihaskell because the output must be valid Haskell and in particular the top-level module name must match the filename.

For this issue we will exclude top-level module names from name-mangling.

when we check for equality between two different ast's, if it fails, we should be able to see a colored diff of both as'ts

When a file contains multiple type checker errors should we display all errors or just the first?

The issue with displaying all errors is that for each error we have to decide to continue typechecking or to immediately stop (we need to immediately stop in some cases - see for example: https://github.com/heliaxdev/minijuvix/issues/41).

Arguments for:

• Better quality of life for users - they can see many the errors with the program at once which provides additional context.

Arguments against:

• Agda / Coq displays only the first error
• Perhaps in a dependently-typed language subsequent errors are more likely to be useless
• It can be a source of bugs and complicate the code.

Questions:

• Does Idris show multiple type errors?
• Can we have make an effect which gives the user the option of displaying all errors or just the first?

The typechecker crashes in this example:

module WrongConstructorArity;
  inductive T {
    A : T;
  };

  f : T → T;
  f (A i) ≔ i;
end;

Expected: Typechecker to fail because the A constructor is being matched against too many arguments.
Actual: The error:

minijuvix: impossible
CallStack (from HasCallStack):
  error, called at src/MiniJuvix/Prelude/Base.hs:211:14 in minijuvix-0.1.2-1oY8JQK47NgCY1PjaTxoQm:MiniJuvix.Prelude.Base
  impossible, called at src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs:117:37 in minijuvix-0.1.2-1oY8JQK47NgCY1PjaTxoQm:MiniJuvix.Syntax.MicroJuvix.TypeChecker

clang supports wasm{32,64}-unknown-unknown and wasm{32,64}-unknown-wasi compilation targets. And the WebAssembly project provides a C toolchain that provides a libc for things like malloc, free, io etc..

For our use-case this seems like a better approach than emscripten (which is a project more focused on generating WASM/JS for browser runtime).

The goal of this issue is to get the minic tests running in CI with clang compiler.

Setup WASM cross compilation toolchain

wasi-sdk publishes precompiled releases of the wasm toolchain. The libclang_rt.builtins-wasm32-wasi-15.0.tar.gz archive should be extracted in the clang installation root (e.g /usr/lib/clang/14 on Ubuntu). And the wasi-sysroot-15.0.tar.gz archive can be extracted anywhere locally.

Clang can then be used as follows:

clang-14 -nodefaultlibs -lc --target=wasm32-wasi --sysroot /home/ubuntu/wasi-sysroot hello.c -o hello.wasm

Where /home/ubuntu/wasi-sysroot is the path where the sysroot archive was extracted to.

-nodefaultlibs -lc is important here because (on ubuntu, perhaps other linux systems) clang passes -lc -lgcc to the linker by default (and gcc lib is not available in the wasm sysroot).

Currently the scope checker mangles the main function name (as it does for all identifiers) to avoid name ambiguity.

For minihaskell the main function name must not be mangled as it serves as the entry point for the application.

For this issue we will exclude all main function names from name-mangling.

Currently we use c-language to serialize our C AST to actual C code.

We should replace this with a pretty printer for the C AST along the same lines as the pretty printer we have for microjuvix, monojuvix etc.

Suggestion:

minijuvix autocomplete zsh
minijuvix autocomplete fish

will output the corresponding autocompletion file to stdout.

The contents of the file are irrelevant for now.

To make the project README focused on getting new users started with minijuvix we should move the developer tooling sections (emacs made and syntax highlighting) to a separate documentation file (linked from the README) and replace them with some usage examples.

For example, the following is printed:

mkPair Nat → Nat Nat

where it should print

mkPair (Nat → Nat) Nat

Let's provide a user-friendly static website to follow the MiniJuvix development.
Initially, the website will include the following sections (as links in the navbar):

• Documentation (Quick Start/Installation, First Examples)
• Changelog (using the same info from CHANGELOG.md.)
• Blog (Informal technical explanations about implementation topics)
• About (Team, Heliax)

Ref:
https://github.com/heliaxdev/minijuvix/tree/sphinx-docs

Add support for other GHC and Stack stable versions.

Possibly, we want to support GHC 9.0 and 8.10.7

See https://github.com/heliaxdev/minijuvix/issues/42 for context.

We decided to return to the behaviour of stopping type-checking after the first type error, reverting work done in https://github.com/heliaxdev/minijuvix/pull/30

We want the following passes for our Github CI:

• stack build
• hlint
• ormulu

Supporting the latest versions of Ubuntu and OSX and the latest version of GHC and Stack.

In the future, we may want to automatically publish the releases to Hackage.

• automatic releases on hackage

Expected jobs:

• build
• test
• ormolu
• hlint