-
Notifications
You must be signed in to change notification settings - Fork 142
Home
Formality-Core (FMC) is a minimal, efficient functional programming language designed to be a "low-level" compile-target for more feature-rich functional languages. Differently from most functional languages, FMC has amazing computational characteristics such as not requiring a garbage-collector, beta-reduction being a constant-time operation, being able to perform dynamic fusion, being strongly normalizing and massively parallelizable. In other words, FMC is really, really fast, and aims to be the ultimate assembly of resource-aware functional languages.
In order for all that to be possible, FMC makes some fundamental changes to the memory model behind the λ-calculus, allowing it to be compatible with an optimal functional runtime as Lamping's Abstract Algorithm, which is based on a beautiful model of computation, Interaction-Nets. The most important change is the fact its lambdas are affine: a lambda-bound variables can't be used more than once. At first, this sounds like an extreme limitation, but this is mitigated by FMC's boxed duplication system. It allows you to perform deep copy of arbitrary values, as long as you respect certain structural restrictions.
// Seed to generate a bounded fold over a binary tree
def tree_fold: [go] [tree]
let case_node = [a] [b] [go]
get &(go, a) = (go a)
get &(go, b) = (go b)
&(go, (Node a b))
let case_leaf = [val] [go]
&(go, (Leaf val))
(tree case_node case_leaf go)
Formality-Core is very similar to Rust. The main difference is that Rust mitigates the limitations of affine lambdas with a complex ownership system which includes borrows, lifetimes, mutable references. In FMC, you're instead encouraged to simply .clone()
structures whenever you need to. Due to the underlying interaction-net runtime, those copies are performed lazily, granularly and in parallel. They're, thus, much less expensive than a Rust-like .clone()
(and often free).
Here is an brief illustration of the process of compiling a Formality-Core term to our interaction-net runtime, reducing it in parallel, and reading the result: