Aliases in Juvix¶
Aliases in Juvix are a powerful feature that allows developers to create shorthand or substitute names for existing ones. This can greatly enhance readability and maintainability of the code.
Syntax¶
The syntax for creating an alias is as follows:
syntax alias <newName> := <originalName>;
Once declared, these aliases can be used interchangeably with the original name. They can be employed in various contexts such as pattern matching, qualification, and module opening.
Application of Aliases¶
One of the key features of aliases in Juvix is their ability to be forward referenced. This means you can use an alias before it has been officially declared in your code. This can be particularly useful when you want to use a more intuitive or shorter name for something that is defined later in the code.
For instance, consider the following example where we define the alias Boolean
for the Bool
type. We also alias the named constructors true
and false
for the Boolean type as ⊤
(top) and ⊥
(bottom) respectively.
syntax alias Boolean := Bool;
syntax alias ⊥ := false;
syntax alias ⊤ := true;
type Bool :=
| false
| true;
not : Boolean -> Boolean
| ⊥ := ⊤
| ⊤ := ⊥;
In addition to global scope, aliases can also be used in local definitions. The following let
expression demonstrates this usage.
not2 (b : Boolean) : Boolean :=
let
syntax alias yes := ⊤;
syntax alias no := ⊥;
in case b of {
| no := yes
| yes := no
};
Just like any other name, aliases can be exported from a module to be used elsewhere. Here's how to do it:
module ExportAlias;
syntax alias Binary := Bool;
syntax alias one := ⊤;
syntax alias zero := ⊥;
end;
open ExportAlias;
syntax operator || logical;
|| : Binary -> Binary -> Binary
| zero b := b
| one _ := one;
The versatility of aliases extends beyond types to terms, including functions
(operators). For example, the binary ||
function can be aliased as or
as
shown below:
syntax alias or := ||;
newor (a b c : Binary) : Binary := (a or b) or c;