mirror of
https://github.com/anoma/juvix.git
synced 2024-12-14 17:32:00 +03:00
Juvix empowers developers to write code in a high-level, functional language, compile it to gas-efficient output VM instructions, and formally verify the safety of their contracts prior to deployment and execution.
cbd8253afd
* Closes #2426 A coercion from trait `T` to `T'` can be declared with the syntax ``` coercion instance coeName {A} {{T A}} : T' A := ... ``` Coercions can be seen as instances with special resolution rules. Coercion resolution rules ------------------------- * If a non-coercion instance can be applied in a single instance resolution step, no coercions are considered. No ambiguity results if there exists some coercion which could be applied, but a non-coercion instance exists - the non-coercion instances have priority. * If no non-coercion instance can be applied in a single resolution step, all minimal coercion paths which lead to an applicable non-coercion instance are considered. If there is more than one, ambiguity is reported. Examples ---------- The following type-checks because: 1. There is no non-coercion instance found for `U String`. 2. There are two minimal coercion paths `U` <- `U1` and `U` <- `U2`, but only one of them (`U` <- `U2`) ends in an applicable non-coercion instance (`instU2` for `U2 String`). ``` trait type U A := mkU {pp : A -> A}; trait type U1 A := mkU1 {pp : A -> A}; trait type U2 A := mkU2 {pp : A -> A}; coercion instance fromU1toU {A} {{U1 A}} : U A := mkU@{ pp := U1.pp }; coercion instance fromU2toU {A} {{U2 A}} : U A := mkU@{ pp := U2.pp }; instance instU2 : U2 String := mkU2 id; main : IO := printStringLn (U.pp "X") ``` The following results in an ambiguity error because: 1. There is no non-coercion instance found for `T Unit`. 2. There are two minimal coercion paths `T` <- `T1` and `T` <- `T2`, both of which end in applicable non-coercion instances. ``` trait type T A := mkT { pp : A → A }; trait type T1 A := mkT1 { pp : A → A }; trait type T2 A := mkT2 { pp : A → A }; instance unitT1 : T1 Unit := mkT1 (pp := λ{_ := unit}); instance unitT2 : T2 Unit := mkT2 (pp := λ{_ := unit}); coercion instance fromT1toT {A} {{T1 A}} : T A := mkT@{ pp := T1.pp }; coercion instance fromT2toT {A} {{T2 A}} : T A := mkT@{ pp := T2.pp }; main : Unit := T.pp unit; ``` The following type-checks, because there exists a non-coercion instance for `T2 String`, so the coercion `fromT1toT2` is ignored during instance resolution. ``` trait type T1 A := mkT1 {pp : A -> A}; trait type T2 A := mkT2 {pp : A -> A}; instance instT1 {A} : T1 A := mkT1@{ pp := id }; coercion instance fromT1toT2 {A} {{M : T1 A}} : T2 A := mkT2@{ pp := T1.pp {{M}} }; instance instT2 : T2 String := mkT2@{ pp (s : String) : String := s ++str "!" }; main : String := T2.pp "a"; ``` |
||
|---|---|---|
| .devcontainer | ||
| .github | ||
| app | ||
| assets | ||
| bench | ||
| examples | ||
| gnuplot | ||
| juvix-stdlib@6a76d4f2ae | ||
| licenses | ||
| runtime | ||
| src/Juvix | ||
| test | ||
| tests | ||
| .clang-format | ||
| .github_changelog_generator | ||
| .gitignore | ||
| .gitmodules | ||
| .hlint.yaml | ||
| .pre-commit-config.yaml | ||
| cabal.hie.yaml | ||
| cabal.project | ||
| cabal.project.freeze | ||
| CHANGELOG.md | ||
| cntlines.sh | ||
| CONTRIBUTING.md | ||
| LICENSE.md | ||
| Makefile | ||
| package.yaml | ||
| README.md | ||
| stack.hie.yaml | ||
| stack.yaml | ||
Juvix
| CI Status |
|---|
|
|
|
|
| Codebase |
|
|
|
This repository is specifically dedicated to the compiler of the Juvix programming language.
For any Juvix-related inquiries, we strongly advise visiting the following resources.
Our documentation offers an in-depth understanding of the Juvix programming language. It encompasses a language reference, examples, blog posts, and numerous other resources to facilitate effective use of Juvix.