The typechecking rule for abilities

The general typechecking rule used for abilities is this: calls to functions requiring abilities {A1,A2} must be in a context where at least the abilities {A1,A2} are available, otherwise the typechecker will complain with an ability check failure. Abilities can be made available using a handle block (discussed below) or with a type signature: so for instance, within the body of a function Text ->{IO} Nat, {IO} is available and therefore:

  • We can call a function f : Nat ->{} Nat, since the ability requirements of f are {} which is a subset the available {IO} abilities.
  • We can also call a function g : Text ->{IO} (), since the requirements of g are {IO} which is a subset of the available {IO} abilities.

For functions accepting multiple arguments, it might seem we need a different rule, but the rule is the same: the body of the function can access the abilities attached to the corresponding function type in the signature. Here's an example that won't typecheck, since the function body must be pure according to the signature:

doesNotWork : Text ->{Exception,IO} Text ->{} Nat
doesNotWork arg1 arg2 =
  printLine "Does not work!"
  42

However, if we do the IO before returning the pure function, it typechecks just fine:

doesWork : Text ->{IO, Exception} Text -> Nat
doesWork arg1 =
  printLine "Works great!"
  arg2 -> 42

For top-level definitions which aren't contained in a function body, they are required to be pure. For instance, this doesn't typecheck:

msg = printLine "hello"

But if we say msg = '(printLine "Hello") that typechecks fine, since the printLine is now inside a function body whose requirements inferred as {IO} (try it!).

šŸ¤“ This restriction on top level definitions needing to be pure might lifted in a future version of Unison.