anoma / juvix Goto Github PK
View Code? Open in Web Editor NEWA language for intent-centric and declarative decentralised applications
Home Page: https://docs.juvix.org
License: GNU General Public License v3.0
A language for intent-centric and declarative decentralised applications
Home Page: https://docs.juvix.org
License: GNU General Public License v3.0
Suggestion:
minijuvix autocomplete zsh
minijuvix autocomplete fish
will output the corresponding autocompletion file to stdout.
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.
The contents of the file are irrelevant for now.
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
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
terminating non-trivial: A → B;
non-trivial := ...;
...
fun case3 := non-trivial a ;
vs
terminating fun case3 := ... ;
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):
CHANGELOG.md.
)Ref:
https://github.com/heliaxdev/minijuvix/tree/sphinx-docs
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.
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.
Tasks:
lab
for experimentations and noteslab
lab
Code related tasks:
For example, the following is printed:
mkPair Nat → Nat Nat
where it should print
mkPair (Nat → Nat) Nat
We want the following passes for our Github CI:
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.
Expected jobs:
Error with undefined or underscores
There is a list of warnings that we want to enable:
Also, add NoFieldSelectors
extension
35bca36fc3525204a4992c32a2861377cf005348
Add support for other GHC and Stack stable versions.
Possibly, we want to support GHC 9.0 and 8.10.7
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.
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.
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:
Arguments against:
Questions:
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.
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:
--no-color
flag to disable ANSI codes.--color
flag to enable ANSI codes.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.
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
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.
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.
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
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.
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).
it should be removed
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.
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
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.
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:
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)SimpleFungibleToken.mjuvix
so we can run the validity predicate.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#
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
.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.