mirror of
https://github.com/anoma/juvix.git
synced 2024-12-12 14:28:08 +03:00
2d666fd82c
- closes #1991 This pr implements named arguments as described in #1991. It does not yet implement optional arguments, which should be added in a later pr as they are not required for record syntax. # Syntax Overview Named arguments are a convenient mehcanism to provide arguments, where we give the arguments by name instead of by position. Anything with a type signature can have named arguments, i.e. functions, types, constructors and axioms. For instance, if we have (note that named arguments can also appear on the rhs of the `:`): ``` fun : {A B : Type} (f : A -> B) : (x : A) -> B := ... ; ``` With the traditional positional application, we would write ``` fun suc zero ``` With named arguments we can write the following: 1. `fun (f := suc) (x := zero)`. 2. We can change the order: `fun (x := zero) (f := suc)`. 3. We can group the arguments: `fun (x := zero; f := suc)`. 4. We can partially apply functions with named arguments: `fun (f := suc) zero`. 5. We can provide implicit arguments analogously (with braces): `fun {A := Nat; B := Nat} (f := suc; x := zero)`. 6. We can skip implicit arguments: `fun {B := Nat} (f := suc; x := zero)`. What we cannot do: 1. Skip explicit arguments. E.g. `fun (x := zero)`. 2. Mix explicit and implicit arguments in the same group. E.g. `fun (A := Nat; f := suc)` 3. Provide explicit and implicit arguments in different order. E.g. `fun (f := suc; x := zero) {A := Nat}`. |
||
|---|---|---|
| .. | ||
| Arity | ||
| Asm | ||
| BackendGeb | ||
| Compilation | ||
| Core | ||
| Examples | ||
| Formatter | ||
| Internal | ||
| Parsing | ||
| Reachability | ||
| Runtime | ||
| Scope | ||
| Termination | ||
| Typecheck | ||
| VampIR | ||
| Arity.hs | ||
| Asm.hs | ||
| BackendGeb.hs | ||
| Base.hs | ||
| Compilation.hs | ||
| Core.hs | ||
| Examples.hs | ||
| Format.hs | ||
| Formatter.hs | ||
| Internal.hs | ||
| Main.hs | ||
| Parsing.hs | ||
| Reachability.hs | ||
| Runtime.hs | ||
| Scope.hs | ||
| Termination.hs | ||
| Typecheck.hs | ||
| VampIR.hs | ||