Type annotations in Harmony

[anthonyyangdev]

Type annotations in Harmony, similar to type annotations in Python, would greatly improve the experience of implementing and testing code. A proposal for type syntax is something like the following (using Diners.hny as an example):

from synch import Lock, acquire, release

const N = 5

forks = [Lock(),] * N

def diner(which: int):
    let left, right = (which, (which + 1) % N):
        while choose({ False, True }):
            acquire(?forks[left])
            acquire(?forks[right])
            # dine
            release(?forks[left])
            release(?forks[right])
            # think

for i in {0..N-1}:
    spawn diner(i)

Ideally, there would some type inferencing to avoid excessive type annotations, such as inferencing the type of i as int, left and right as int, or forks as a list of the return type of Lock. This change would require changes to the syntax of the language, but they likely would not significantly affect the overall structure of the existing parser.