Draft: Better tracking of compile-time known values

[mark-koch]

Requirements

Add a new @comptime modifier (analogous to @owned) to mark that values are known at compile-time.

The following expressions check against a @comptime annotated type:

• Literals: x: int @comptime = 42
• Comptime expressions x: int @comptime = comptime(1 + 2 + 3)
• Other variables that are annotated or inferred to as @comptime. A special case of this are comptime function arguments:

  def foo(x: int @comptime):
       y: int @comptime = x

Any other expression is invalid. For example, the following wouldn't type check:

x: int @comptime = 1 + 2 + 3  # error: value not known at comptime
xs: tuple[int, int] @comptime = (1, 2)  # Also error for MVP
ys: array[int, 3] @comptime = array(1, 2, 3)  # Also error for MVP

# For MVP we can force users to wrap more complicated datastructures into
# explicit comptime expressions
xs: tuple[int, int] @comptime = comptime((1, 2))  # Ok
ys: array[int, 3] @comptime = comptime(array(1, 2, 3))  # Ok

The compiler should automatically infer if an assignment produces a comptime value, even if not explicitly annotated. So the following should check:

x = 42  # Inferred type is `int @comptime`
y: int @comptime = x  # So this is legal

Variables that are defined in different control-flow branches are never @comptime:

if condition():
    x: int @comptime = 42
else:
    x: int @comptime = 43
# After the control-flow merge, x is no longer considered a comptime value:
y: int @comptime = x  # Error

(We could relax to allow the case where the value is the same in all paths leading to the use, but not sure if that's woth it?)

Calling a function with a comptime argument requires that the argument checks against the @comptime annotation using the rules above:

def foo(x: int @comptime): ...

def bar(y: int @comptime):
    foo(42)  # Ok
    foo(comptime(1 + 2 + 3))  # Ok
    foo(y)  # Ok
    foo(1 + 2)  # Error

Inside a comptime context, @comptime values should be available as regular Python values:

@guppy.comptime
def foo(n: int @comptime):
    assert(isinstance(n, int))  # Not a guppy tracing object!
    for i in range(n):  # So we can pass it to Python builtins like range
        ...

Hugr Lowering

TODO

[jake-arkinstall]

I love this proposal. Some small comments:

• I think it is implied, but not explicitly listed, that:

def bar(y: int @comptime):
    foo(42)  # Ok
    foo(comptime(1 + 2 + 3))  # Ok
    foo(y)  # Ok
    foo(comptime(1 + 2 + y)) # <-- Ok, too!
    foo(1 + 2)  # Error

• It would be nice to have comptime() be implicit when an expression CAN be considered comptime even if not explicitly written, i.e.

foo(1 + 2) # Sure, why not?
x: int @comptime = 10
y: int @comptime = x + 4 # Sure, why not?

• I'd be interested to see if comptime floats could work (which could be a minefield).

[mark-koch]

I think it is implied, but not explicitly listed, that:

Yes, that should also work.

It would be nice to have comptime() be implicit when an expression CAN be considered comptime even if not explicitly written

Personally, I prefer the explicit annotation. I feel like inserting comptime evaluations implicitly would make the rules harder to understand. Also, it would be tricky to implement: After type checking, arithmetic is desugared into function calls, so it's hard to decide if something can be comptime evaludated or not...

I'd be interested to see if comptime floats could work (which could be a minefield).

I think we should allow them and just use whatever semantics the Python interpreter gives us when doing float arithmetic

[jake-arkinstall]

I think we should allow them and just use whatever semantics the Python interpreter gives us when doing float arithmetic

Therein lies the minefield.

It means that compile time and runtime float math can differ depending on what system (and environment) you're compiling the guppy on and what system executes the result.

Which in general is fine but we should offer a list of caveats, such as dangers of using equalities (almost always baf anyway) and inequalities (more common) between compile time calculated and runtime calculated floats.