matthew-mojira / cicero

GNU General Public License v3.0
0 stars 0 forks source link

type hints/patterns #20

Open matthew-mojira opened 1 day ago

matthew-mojira commented 1 day ago

statically checked

if the static checker is being used, we also need to ascertain what parts of the code are not guaranteed by the static type checker

matthew-mojira commented 7 hours ago

Static checking might be difficult with the use of type patterns which are a more advanced version of type hinting. For example, we might have a function isqrt which computes the integer square root of a number n. That function (see #5) could look like

func isqrt(n) {
  ...
}

First, we should ensure that n is an integer. That could be done either by comparing n? == int (see #15), throwing an error (see #18), or do nothing and let the program fail naturally (but this would be unhelpful to the end user!). We can accomplish this through a type pattern, where we annotate the expected type of n

func isqrt(n: int) {
  ...
}

This is a simple example of a literal pattern (see #19), but we might have more complex patterns, for example if the argument is passed as a box:

func isqrt_box(n: box[int]) {
  ...
}

Without static type checking, this is just syntactic sugar for asserting the type manually (since both operations would be done at runtime). Would it be difficult to do static or gradual type checking?

A more advanced use of this could be polymorphic functions:

func dup_box(val: box[T]) {
  unbox (box val)
}

We could also do pattern matching where we write identifiers (future issue). T now becomes a constant corresponding to the value of the function which is in scope in the body expression.

Last, we can use when expressions (from pattern matching) to make additional assertions about the values in the argument:

func isqrt(n: int when n >= 0) {
  ...
}

Failures to match the types of the values would constitute a type error (where we also have to include type patterns as the expected type instead of a single type). The when expression evaluating to false would be an ArgumentError.

What about types of expressions? When should we check that the pattern in the parameter type can match to types? And when should we check that the when expression is boolean type? (Right now, would also have to be dynamic--would need to differentiate type errors that are because the type pattern when is not a bool and when that bool is false because of a successful check.)