Recursive
Par has, among others, these two ambitious design choices:
- Totality, meaning preventing infinite loops by type-checking.
- A structural type system, where global type definitions are merely aliases.
When it comes to self-referential types, totality necessitates distinguishing between:
- Recursive types, those are finite.
- Corecursive types, potentially infinite. In Par, we call them iterative types.
The choice of a structural type system has led to avoiding defining self-referential types naively, and instead adding a first-class syntax for anonymous self-referential types.
Par is very radical here. If you try the usual way of defining a singly-linked list, it fails:
type IllegalList = either {
.end!,
.item(String) IllegalList, // Error! Cyclic dependency.
}
In general, cyclic dependencies between global definitions are disallowed. Instead, we have:
- Anonymous self-referential types:
recursive
anditerative
. - A single, universal recursion construct:
begin
/loop
. It’s suitable for recursive destruction, iterative construction, and imperative-style loops in process syntax.
Let’s take a look at recursive
!
Totality does not mean you can’t have a web server, or a game. While these are often implemented using infinite event loops, it doesn’t have to be done that way. Instead, we can employ corecursion, which Par supports with its iterative types.
To make it clearer, consider this Python program:
def __main__(): while True: req = next_request() if req is None: break handle_request(req)
That’s a simplified web server, handling requests one by one, using an infinite loop.
Could we switch it around and not have an infinite loop? Absolutely!
class WebServer: def close(self): pass def handle(req): handle_request(req) def __main__(): start_server(WebServer())
A small re-structuring goes a long way here. Iterative types in Par enable precisely this pattern, but with the ergonomics of the infinite loop version.
A recursive type starts with the keyword recursive
followed by a body that may contain any number
of occurrences of self
: the self-reference.
type LegalList = recursive either {
.end!,
.item(String) self, // Okay.
}
If there are nested
recursive
(oriterative
) types, it may be necessary to distinguish between them. For that, we can attach labels torecursive
andself
. That’s done with a slash:recursive/label
,self/label
. Any lower-case identifier can be used for the label.
The recursive type can be thought of as being equivalent to its expansion. That is, replacing each
self
inside the body with the recursive
type itself:
- The original definition:
recursive either { .end!, .item(String) self }
- The first expansion:
either { .end!, .item(String) recursive either { .end!, .item(String) self } }
- The second expansion:
either { .end!, .item(String) either { .end!, .item(String) recursive either { .end!, .item(String) self } } }
- And so on…
The body of a
recursive
often starts with aneither
, but doesn’t have to. Here’s an example of that: a non-empty list, which starts with a pair.type NonEmptyList<a> = recursive (a) either { .end!, .item self, }
Another example of a
recursive
type, which doesn’t start with aneither
would be a finite stream.type FiniteStream<a> = recursive choice { .close => !, .next => either { .end!, .item(a) self, } }
This one starts with a choice, which enables polling the elements on demand, or cancelling the rest of the stream. However, being recursive, a
FiniteStream<a>
is guaranteed to reach the.end!
eventually, if not cancelled.
The key features of recursive types are that their values are finite, and that we can perform recursion on them.
Construction
Recursive types don’t have any special construction syntax. Instead, we directly construct their bodies, as if they were expanded.
type Tree = recursive either {
.leaf Int,
.node(self, self)!,
}
def SmallTree: Tree = .node(
.node(
.leaf 1,
.leaf 2,
)!,
.node(
.leaf 3,
.leaf 4,
)!,
)!
Already constructed recursive values can be used in the self
-places of new ones:
def BiggerTree: Tree = .node(SmallTree, SmallTree)!
Lists are a frequently used recursive type, and so are pre-defined as:
type List<a> = recursive either {
.end!,
.item(a) self,
}
Constructing them goes like:
dec OneThroughFive : List<Int>
dec ZeroThroughFive : List<Int>
def OneThroughFive = .item(1).item(2).item(3).item(4).item(5).end!
def ZeroThroughFive = .item(0) OneThroughFive
Because lists are so ubiquitous, there is additionally a syntax sugar for constructing them more concisely:
def OneThroughFive = *(1, 2, 3, 4, 5)
However, prepending onto an existing list has no syntax sugar, so ZeroThroughFive
still has to be
done the same way.
Destruction
If we don’t need to perform recursion, it’s possible to treat recursive types as their expansions
when destructing them, too. For example, here we treat a List<String>
as its underlying either
:
type Option<a> = either {
.none!,
.some a,
}
dec Head : [List<String>] Option<String>
def Head = [list] list.case {
.end! => .none!,
.item(x) _ => .some x,
}
For a recursive reduction, we have .begin
/.loop
. Here’s how it works:
- Apply
.begin
to a value of arecursive
type. - Apply more operations to the resulting expanded value.
- Use
.loop
on a descendent recursive value, descendent meaning it was aself
in the original value we applied.begin
to.
Let’s see it in practice. Suppose we want to add up a list of integers.
- We obtain a value (
list
) of a recursive type (List<Int>
):dec SumList : [List<Int>] Int def SumList = [list]
- We apply
.begin
to it:list.begin
- We match on the possible variants:
If the list is empty, the result is.case { .end! => 0, .item(x) xs =>
0
. Otherwise, we need to add the numberx
to the sum of the rest of the list:Int.Add(x,
xs
. - Since
xs
is a descendant of the originallist
that we applied the.begin
to, and is again aList<Int>
, we can recursively obtain its sum using.loop
:
And close the braces.xs.loop),
}
All put together, it looks like this:
def SumList = [list] list.begin.case {
.end! => 0,
.item(x) xs => Int.Add(x, xs.loop),
}
You can think of .loop
as going back to the corresponding .begin
, but with the new value.
The semantics of .begin
/.loop
are best explained by expansion, just like the recursive types
themselves. In all cases, the meaning of .begin
/.loop
is unchanged, if we replace each .loop
with the entire body starting at .begin
.
Observe:
- The original code:
def SumList = [list] list.begin.case { .end! => 0, .item(x) xs => Int.Add(x, xs.loop), }
- The first expansion:
def SumList = [list] list.case { .end! => 0, .item(x) xs => Int.Add(x, xs.begin.case { .end! => 0, .item(x) xs => Int.Add(x, xs.loop), }), }
- The second expansion:
def SumList = [list] list.case { .end! => 0, .item(x) xs => Int.Add(x, xs.case { .end! => 0, .item(x) xs => Int.Add(x, xs.begin.case { .end! => 0, .item(x) xs => Int.Add(x, xs.loop), }), }), }
- And so on…
.loop
may be applied to any number of descendants. Here’s a function adding up the leafs in the Tree
type defined previously:
dec SumTree : [Tree] Int
def SumTree = [tree] tree.begin.case {
.leaf number => number,
.node(left, right)! => Int.Add(left.loop, right.loop),
}
def BiggerSum = SumTree(BiggerTree) // = 20
If there are multiple nested
.begin
/.loop
, it may be necessary to distinguish between them. Labels can be used here too, just like with the types:.begin/label
and.loop/label
does the job.TODO:
type Tree<a> = recursive List<(a) self>
Retention of local variables
Let’s consider Haskell for a moment. Say we write a simple function that increments each item in a list by a specified amount:
incBy n [] = []
incBy n (x:xs) = (x + n) : incBy n xs
This recursive function has a parameter that has to be remembered across the iterations: n
, the
increment. In Haskell, that’s achieved by explicitly passing it to the recursive call.
Now, let’s look at Par. In Par, .loop
has a neat feature:
local variables are automatically passed to the next iteration.
dec IncBy : [List<Int>, Int] List<Int>
def IncBy = [list, n] list.begin.case {
.end! => .end!,
.item(x) xs => .item(Int.Add(x, n)) xs.loop,
}
Notice, that xs.loop
makes no mention of n
, the increment. Yet, n
is available throughout the
recursion, because it is automatically passed around.
This feature is what makes begin
/loop
not just a universal recursion construct, but a sweet spot
between usual recursion and imperative loops.
If you’re confused about how or why it should work this way, try expanding the
.begin
/.loop
in the above function. Notice that when expanded,n
is in fact visible in the next iteration. It’s truly the case that expanding a.begin
/.loop
never changes its meaning.
Together with .begin
/.loop
being usable deep in expressions, local variable retention is also
very useful in avoiding the need for helper functions.
Let’s again switch to Haskell, and take a look at this list reversing function:
reverse list = reverseHelper [] list
reverseHelper acc [] = acc
reverseHelper acc (x:xs) = reverseHelper (x:acc) xs
This function uses a state: acc
, the accumulator. It prepends a new item to it in every iteration,
eventually reversing the whole list. In Haskell, this requires a helper recursive function.
In Par, it doesn’t!
dec Reverse : [type a] [List<Int>] List<Int>
def Reverse = [type a] [list]
let acc: List<a> = .end!
in list.begin.case {
.end! => acc,
.item(x) xs => let acc = .item(x) acc in xs.loop,
}
def TestReverse = Reverse(type Int)(*(1, 2, 3, 4, 5)) // = *(5, 4, 3, 2, 1)
And there we go! All we had to do was to re-assign acc
with the new value, and continue with xs.loop
.
The escape-hatch from totality: .unfounded
If the Par’s type checker refuses to accept your recursive algorithm despite you being certain it’s
total — meaning it resolves on all inputs — it’s possible to disable the totality checking by
replacing .begin
with .unfounded
.
Par’s totality checking is currently not powerful enough for some algorithms, especially divide
and conquer, and it’s also lacking when decomposing recursive algorithms into multiple functions.
In such cases, using .unfounded
is okay. We do, however, aim to make the type system stronger,
and eventually remove .unfounded
.