Programming Language Design 2

STLC Declarations, Modules and Imports

---

So far we have constructed our little STLC-based programming language from inside out, but here we look at the language from a different view-point: from outside in — the programmers point-of-view. We will dive into the following topics:

• How to definite multiple functions in a single source code file: we add declarations.
• How to implement a simple module system with imports.

Declarations

In theory, a declaration is simply a pair of the function name and its type signature. In practice, declarations mean various things in different programming languages.

In Gleam and Rust, the type signature of a function is declared at the same time as its definition. For example:

pub fn add(a: i32, b: i32) -> i32 {
    a + b
}

The example code declares a function add : fn(i32, i32) -> i32, and defines it as “the abstraction over a + b with parameters a : i32, b : i32”.

When working with traits in Rust, one often sees just the declaration of the function inside a trait’s definition:

trait Add {
    fn add(a: i32, b: i32) -> i32;
}

In Rust, declarations in traits require name parameters, but they do not affect the type signature.

However, in Haskell, declarations of functions are written on a separate line from the defining equations.

add :: Integer -> Integer -> Integer
add a b = a + b

There, add :: Integer -> Integer -> Integer is the declaration, and add a b = a + b is the only defining equation.

We will implement this style of declarations to our language.

Declarations in STLC++

We are moving onwards from just the language of the simply typed lambda calculus toward a more serious programming language. We shall call the language STLC++.

STLC++ inherits the statics and dynamics from . We only add a new class of syntax for writing declarations and imports. Declaration and import syntax can not appear in terms.

A sample STLC++ program looks like this:

import std

x : Integer
x = sum (range 1 10)

With the file std.stlc containing the following declarations:

range : Integer -> Integer -> [Integer]
range = fun start : Integer, fun end : Integer,
    if start == end then
        nil Integer
    else
        cons start (range (start + 1) end)

sum : [Integer] -> Integer
sum = fun xs : [Integer],
        lcase xs of
        | nil => 0
        | cons x xs => x + sum xs

Declarations in STLC++ are allowed to be recursive, and every declaration is turned into a term using a fixed point combinator.

Declarations may only refer to functions declared prior.

A simple STLC++ syntax highlighting plugin for VS Code is provided.

Loading Exercise...