LNP

American religious leader Joseph Smith once called writing in natural language a "little narrow prison". Completely unrelatedly, I'm calling this little programming language LNP, which experiments with some concepts that enable programming in a style that more closely resembles natural language.

Basic Features

LNP is a functional language with a core based on the lambda calculus. Besides functions, it has a handful of basic data types and a small standard library. It also has some constructs such as let statements for convenience.

Primitive Values

There are three atomic data types:

1. Numbers, which have type Num. Booleans are represented as Num in the standard library.
2. Strings, which have type Str, are written surrounded by double quotes. Currently there is no concept of escape sequences in strings.
3. Unit, with type Unit, is written (). For those unfamiliar with functional programming, you can think of this value as something like null, or as a placeholder that contains no data.

Lambdas (anonymous functions) are written with the syntax fn (param1: Type1, param2: Type2, ...) => body, where the body is an expression. Applying (calling) a function follows scheme-like syntax, simply placing a function and its arguments next to each other, like f arg1 arg2.

Atomic values and functions can be combined into lists or pairs. Pairs are constructed by (left, right), and lists are made using cons and nil from the standard library.

Types

The type system is based on System F. This means that in addition to creating anonymous functions to abstract behavior at the runtime level, the language also provides a kind of "anonymous function" at the type level. This is a generalization of how mainstream languages which provide polymorphic/generic functions. LNP uses the syntax FN (R, S, T, ...) => body for type level lambdas (note the uppercase FN). For example, an identity function that could take in a value of any type and return it unchanged could be written FN (T) => fn (x: T) => x. Applying (calling) the type-level function is done by surrounding the type-level function and its arguments in angle brackets. For instance, taking our polymorphic identity function from earlier, we could produce an identity function that only works for numbers by doing <(FN (T) => fn (x: T) => x) Num>, which is equivalent to fn (x: Num) => x. In practice, the (very basic) type inference/unification system is able to infer the type that should be used as the argument to a type-level function when it is used as the operator of a value-level function call. For instance, most of the time you should be able to write something like filter listOfNumbers predicate, instead of having to explicitly say <filter Num> listOfNumbers predicate.

Function types are written (arg1: Type1, arg2: Type2, ...) -> ReturnType, and the type of a type level function is all (T, R, ...) -> ReturnType. Atomic types are written Num, Str and Unit. Compound types are written List<ElementType> and Pair<LeftType, RightType> respectively.

Types can also be aliased using a type statement (ex: type Int = Num). This introduces the concept of strict and loose type equality. For almost all purposes, an aliased type behaves exactly as the type it is defined to be (Int is loosely equal to Num). However, defining a type alias also produces a runtime function of the same name, when given a value, returns 1 if the value has precisely that type (Int is not strictly equal to Num), and 0 if not. So if i is defined to be an Int and n is a Num, then Int i evaluates to 1, while Int n evaluates to 0.

Other Constructs

Expressions are one of

1. values
2. function calls (both at the value and type level)
3. blocks

A block is notated { statement1. statement2. ... }. Statments are separated by periods, and the final statement of a block is the return value of the block. A statment can be:

1. Simply an expression
2. A let statement let name: T = expression. Let statements coerce the value to be a particular type for the purposes of strict equality.
3. A type statement type name = Type
4. A def, which will be explained in Case Frames

The Standard Library

The following values are included in the top-level environment at the beginning of a program:

• fst: all (L, R) -> (pair: Pair<L, R>) -> L returns the first element of a pair
• snd: all (L, R) -> (pair: Pair<L, R>) -> R returns the second element of a pair
• head: all (T) -> (list: List<T>) -> T returns the first element of a list, or crashes if empty
• tail: all (T) -> (list: List<T>) -> List<T> returns every element but the first of a list, or crashes if empty
• cons: all (T) -> (item: T, rest: List<T>) -> List<T> produces a new list by prepending an item onto an existing list
• nil: all (T) -> List<T> the empty list
• eq: all (A, B) -> (a: A, b: B) -> Num returns 1 if a and b are equal, 0 if not.
• fix: all (I, O) -> (f: (rec: (in: I) -> O, in: I) -> O) -> ((in: I) -> O) takes in a "fixable" function and makes it recursive
• if: all (T) -> (cond: Num, then: (_: Unit) -> T, else: (_: Unit) -> T) -> T returns the result of calling then if cond is anything other than 0, or else returns the result of calling else
• gt: (a: Num, b: Num) -> Num returns 1 if a is greather than b, or else returns 0
• Num: (n: Num) -> Num, Str: (s: Str) -> Num, Unit: (u: Unit) -> Unit type predicates for the built in atomic types
• ListOf: all (T) -> (predicate: (t: T) -> Num) -> ((list: List<T>) -> Num) takes in a type predicate and returns a predicate for lists of that type
• a: all (T) -> (predicate: (t: T) -> Num) -> T, the: all (T) -> (predicate: (t: T) -> Num) -> T, every: all (T) -> (predicate: (t: T) -> Num) -> List<T> inspect the environment to find values that satisfy the predicate. See Implicit Arguments for more details.

Additional Features

The above featurs are all fairly standard features for a simple functional programming languages. What follows are less common features that LNP includes.

Overloading

If a new variable is declared (using let, parameters, etc) with the name of an existing variable, the standard behavior is to shadow the existing variable. However, in LNP, if the variables have different types, both can still be accessed depending on the type environment. For instance, in the following program, f is declared twice with different types. At the end of the block, because the argument is a number, the first f declaration is used.

{
    let f: (n: Num) -> Num = fn (n: Num) => n.
    let f: (u: Unit) -> "won't call this".
    f 42
}

If there is ever a situation where overloading (or any other feature) causes there to be multiple valid typings for the entire program, typechecking fails and the programmer is directed to resolve the ambiguity.

Implicit Arguments

A function can be defined to have implicit arguments, in addition to its explicit ones. A function with implicit arguments is written fn [implicitArg: Type1, ...] (arg: Type2, ...) => body, and has the type [implicitArg: Type1, ...] (arg: Type2, ...) -> ReturnType. A function can be given its implicit arguments explicitly by placing them in square brackets at the beginning of an application [implictArg1, implicitArg2] f arg1 arg2, or they can be omitted. When they are omitted, the function application will search the environment for a value whose type matches the expected type using strict equality.

Expression Lifting

Note that function types in LNP have named parameters. If a context expects a function-typed value (such as the right hand side of a let or an argument site), LNP will first try to typecheck the expression as normal, but if that fails, LNP will try to "lift" the expression to be a function. This is done by introducing into the type environment the parameters of the function-type which is the target and then retrying the typecheck. For instance, say we had a function filter: (list: List<Num>, predicate: (item: Num) -> Num) -> List<Num>. We can then write an expression filter myList (gt item 42). gt item 42 fails to typecheck on its own since item is not bound. However, because predicate has the type (item: Num) -> Num, we try as a fallback typing gt item 42 under an extended environment where item: Num. Under the extended environment, gt item 42 typechecks, so we interpret it as a function equivalent to fn (item: Num) => gt item 42.

Case Frames

In natural language constituent theories of grammar, one can view some words as functions which take specific kinds of phrases as arguments. For instance, a preposition may be viewed as a function which takes a noun phrase as an argument. However, in many cases, the argument is not given on the right of the operator. A transitive verb takes two arguments, a subject and object phrase. In English, the object phrase is on the right as normal, but the subject phrase is on the left.

Thus, in LNP, one can define a function to take arguments either on the left or right, using a def phrase. A def phrase has the syntax def [leftArgs] *name [rightArgs] => body. Instead of standard function application, LNP has "phrases", which are a sequence of whitespace-separated expressions. Each subexpression is typechecked separately, and if it is a function type, is is considered a possible operator for the phrase. Once one is found, the typechecker recursively tries to typecheck the subexpressions on the left and right of the candidate operator until an atom is found. This means that in many cases, parentheses can be entirely omitted. However, if there is ambiguity, typechecking fails and the developer is prompted to resolve the ambiguity.

For instance, you could define a version of gt as an infix operator like so:

{
    def (a: Num) *gt (b: Num) => gt a b.
    42 gt 35
}

Example

The following program shows an example using all of the above features. Ultimately, we end up with a definition that reads a lot like natural language.

def *highEarners (_: List<Wages>) =>
    each item in the ListOf Wages thatIs greaterThan 50.

The full program is as follows

{
type Bool = Num.
let filter: all (T) -> (list: List<T>, pred: (x: T) -> Bool) -> List<T> =
    FN (T) => fn (list: List<T>, pred: (x: T) -> Bool) => {
        let do: (list: List<T>) -> List<T> =
            fix (fn (filter: (list: List<T>) -> List<T>, list: List<T>) =>
                if (eq list ())
                    <nil T>
                    (
                        if (pred (head list))
                            (cons (head list) (filter (tail list)))
                            (filter (tail list))
                    )
            ).
        do list
    }.

let has: all (T, S) -> (p: Pair<T, S>, pred: (t: T) -> Bool) -> Bool = 
    FN (T, S) => fn (p: Pair<T, S>, pred: (t: T) -> Bool) => pred (fst p).

let thatIs: all (T) -> (pred: (item: T) -> Bool) -> ((item: T) -> Bool) =
    FN (T) => fn (pred: (item: T) -> Bool) => pred.

let in: all (T) -> (list: List<T>) -> List<T> = FN (T) => fn (list: List<T>) => list.

let each: all (T) -> (id: (item: T) -> T, list: List<T>, pred: (item: T -> Bool)) -> List<T> =
    FN (T) => fn (id: (item: T) -> T, list: List<T>, pred: (item: T -> Bool)) =>
        filter list pred.

let greaterThan: (n: Num) -> ((m: Num) -> Bool) =
    fn (n: Num) => fn (m: Num) => gt m n.

type Wages = Num.
def *highEarners (_: List<Wages>) =>
    each item in the ListOf Wages thatIs greaterThan 50.

let list: List<Wages> = cons 100 cons 50 cons 10 <nil Num>.

highEarners list

}

How to Use

Currently there is no command line interface or other way of consuming a file as input. Instead I have just been passing strings defined in the file Program.fs to the run function which interprets a string as a program.

Roadmap

Some things I'd like to add in the future:

• Extend the idea of case frames to have secondary words. For instance, you could write something like def *add (a: Num) to (b: Num) => .... add becomes the primary name of the function, but for it to typecheck properly, it must be given, in order, a phrase typing to a Num, the identifier to, and another phrase typing to Num, allowing you to write something like add 42 to 35 and have it typecheck properly.
• Allow type parameters on def statements.
• Some kind of polymorphism relating to the names of parameters. The goal would be to allow a phrase like every item where (predicate item). The first instance of item essentially names the parameter, then it is used in the latter phrase.
• type inference for let statements, so that they don't have to be explicitly typed
• Add PairOf to the standard library
• Better error messaging for parsing, typechecking, and interpretation
• Actual ADTs, replacing the strict/loose type equality distinction