Plange is an open-source project to create a development suite including a programming language, standard library, and runtime.

- license: New BSD
- source code: git repository
- status: pre-alpha
- monetization: compute resources and pro support
- pronunciation: plænd͡ʒ [ipa]

The Plange language is an extensible, mixed languae of proof and type systems, solvers, and functional and imperative programs on variables, functions, types, and other objects. See the goals page. It is traditional to start with the __Hello World__ program.

print("Hello, world!");

Comments are created using two syntactic variations.

End of line comment (red is comment text)

```
print("My name is HAL 9000."); //only kidding!
```

Inline comment (red is comment text) source

getRandomNumber := { return 4; /*choosen by fair dice roll*/ }; //guaranteed to be random

Some Unicode characters are included for completeness. Many have typable equivalents. For example, implication can be typed as `⇒`

or `=>`

. Unicode characters will be used in documentation. See the partial list.

A variable may take place in a constraint system, be free or bound, and may have storage allocated to it. A variable can be assigned a value and be changed freely using the assignment operator `←`

, or `<-`

.

Assign a value to a variable

x ← 1337;

Variables can be reassigned.

Reassign a variable

color ← "Blue"; color ← "Red";

A variable may be constrained to a type.

Type constraint on a variable

<Number> x ← 1337;

Values may be stored on the stack, heap, reference counted heap, or garbage collected heap. The Pointer type provides addressing of memory.

Unbound variables can be targets for symbolic or numerical solutions. In specific normal and canonical forms, constraints on variables define a problem space for which solutions are desired. The capabilities are limited by availability and applicability of known processes, such as those upon convergent power series, linear systems, etc.

Symbolic manipulation

x = 1337; tan(y*2) = x; print y; // arctan(1337) / 2 = { 1.570048, -1.571544 };

A symbol with an immutable value is a constant.

Example

print(π); //print pi

`π`

or `pi`

is a predefined constant, and provides arbitrarily high precision in symbolic manipulation.

Constants are created using the definition operator `:=`

Example

daysInAWeek := 7;

Function are created with parenthesis `( )`

containing the parameter list, and curly braces `{ }`

containing the implementation. Nullary functions may elide their parameter list.

Example

doubler := (x) { return x * 2; };

Functions have arity.

A binary function

geometric_mean := (x, y) { return √(x * y); };

Constants and variables may be strongly typed implicitly or explicitly, late bound, or duck typed.

Explicit strong typing

<Int> x ← 10;

`Int`

or `ℤ`

is shorthand for integer. The first line constrains x to `Int`

values. See Type System.

Create function types using the `→`

operator, or `->`

.

Example

<Int → Int> doubler = (x) { return x * 2; };

doubler will only accept an `Int`

as input, and will only return an `Int`

. Function arguments may also be given types.

Semantically equivalent to the previous example

doubler := (<Int> x) { return x * 2; };

Variables that have no specified type constraint are dynamically typed.

Assigning objects of varied type to a variable

x ← 10; x ← "Alice"; x ← { print("fubar"); };

The `type`

keyword (not capitalized) is used to make a new `Type`

object (capitalized).

Example

Color := type { <Double> r; <Double> g; <Double> b; }; <Color> red ← (| 1, 0, 0 |); print(type_of( (| 1, 0, 0 |) )); // output: Tuple<Number, Number, Number> print(type_of(red)); // output: Color print(type_of(Color)); // output: Type

Parametric types are functions that return Type objects.

Example

Node := (<Type> valueType) { return type { <valueType> v; Maybe<Node<valueType>> next; }; };

Constant folding evaluates some invocations of type functions at compile time. Functions that return Type objects (or another type function) should be called with the angle bracket syntax:

Example invoking List using angle bracket syntax

<List<Int>> myList;

Pattern matching decomposes values into unbound symbols. Patterns are tested sequentially in the order given.

Tail recursive function to print the last element of a list

<List<_> → Void> printLast := (_ & tail) { printLast(tail); } | (x) { print(x); }; myList := [ 5, 12, 8, 9 ]; printLast(myList);

Output

9

The prepend operator `&`

takes a value on the left, and a list on the right. In the examples above the first parameter to the function is being broken apart into two pieces.

Note the use of the underscore `_`

character. It's substituted for a variable when the code doesn't care about the value. In the first line of the example above, we are unconcerned with the type of the elements the input list contains, and only need to ensure that the input is a list of something. In the second line, we don't need to know the value of the head element. The underscore keyword is called dont_care.

Another recursive function to filter values

filter := (head & tail, predicate) { return predicate(head) ? head & select(tail, predicate) : this_func(tail, predicate); } | ([], predicate) { return []; };

The inheriting keyword, used in conjunction with the type keyword, makes a new Type object inheriting the members of the specified base Types. See also: implementing

Example

// base Type Widget := type { <Void → Image> Paint; }; // derived Type TextBox := type inheriting Widget { <String> text ← "Hello, world!"; // override the inherited Paint method Paint ← (<Canvas> c) { return c.print(text); }; };

Types can be combined together to make algebraic Types using the compound operator `|`

.

Example

Some := (t) { return type { <t> value; }; }; None := type {}; Maybe := (t) { return Some<t> | None }; <Void → Maybe<Int>> get_age := { return coerce(input("What's your age? You don't have to tell me.")); }; print(get_age());

Many interesting problems may be constructed as one or more constraints using operators and functions. When an appropriate normal form or canonical form is given, constant folding, satisfiability solving, and symbolic manipulation yield equality constraints upon termination. See the computer algebra systems page. All the results in this section have been computed manually for demonstrative purposes.

Example

children := {| abe, dan, mary, sue |}; ages := {| 3, 5, 6, 9 |}; children ↔ ages; // One child per one age (bijection operator) abe > dan; //abe is older than dan sue < mary; //sue is younger than mary sue = dan + 3; //sue's age is dan's age plus 3 years mary > abe; //mary is older than abe print(abe); print(dan); print(mary); print(sue);

The output when ran:

Output

5 3 9 6

Example of a linear system

<Real * Real * Real → Real> linear_interpolation := (min, max, x) { min * (1 - x) + max * x } ; inverted_linear_interpolation := (min, max, interpolated) { interpolated = linear_interpolation(min, max, x); //x is a free variable return x; } linear_map := (minIn, maxIn, v, minOut, maxOut) { v = linear_interpolation(minIn, maxIn, x); return linear_interpolation(minOut, maxOut, x); } assert(x = inverted_linear_interpolation(y, z, linear_interpolation(y, z, x));

One well studied domain is initial value problems. An ordinary differential equation is given with boundary conditions on free variables:

Example: Aerodynamic Drag On A Projectile

projectilePosition := ( <Vector3D> initialPos, <Vector3D> initialVel, <Real> mass, <Real> drag, <Vector3D> gravity, <Real> t ) { // declare the position function, x <Real → Vector3> x; // model x as a differential equation mass * Δ^2x(t)/Δt^2 = -drag * Δx(t)/Δt + mass * gravity; // with boundary conditions x(0) = initialPos; Δx(0)/Δt = initialVel; // solve, substitute, evaluate return x(delta_t); };

ODE solving gives a symbolic solution for x such that the following program is functionally equivalent. This constant folding is performed and cached at compile time.

Example (continued)

projectilePosition := ( <Vector3D> initialPos, <Vector3D> initialVel, <Real> mass, <Real> drag, <Vector3D> gravity, <Real> t ) { a := 𝑒^(drag*t/mass); return ( gravity * (mass-(mass*a + drag*t)) + initialPos*a*drag^2 + drag*mass*initialVel*(a-1) ) / (a*drag^2); };

Constraint solving is intractible in the general case. Users must familiarize themselves with the capabilities of the language, which are expected to expand. A demonstration of a semantically correct but nonfunctional program is in order.

Counter Example

<Collection * BinaryRelation → Collection> sort := (items, ordering) { result ↔ items; // result and items make a bijection ∀ { ordering(result[i - 1], result[i]) | i ∈ (0...|result|) }; //the result has to be sorted return result; // solve, substitute, and return };

The above function, sort, is functionaly equivalent to the sorting functions. However, this constraint based problem is not yet solvable using available techniques.

copyright © Brent Lewis 2013-2018