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 whereat leastthe abilities{A1,A2}areavailable,otherwise the typechecker will complain with an ability check failure. Abilities can be made available using ahandleblock (discussed below) or with a type signature: so for instance, within the body of a functionText ->{IO} Nat,{IO}is available and therefore:

  • We can call a functionf : Nat ->{} Nat,since the ability requirements of f are{}which is a subset the available{IO}abilities.
  • We can also call a functiong : Text ->{IO} (),since the requirements ofgare{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!"

However, if we do theIObefore 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 saymsg = '(printLine "Hello")that typechecks fine, since theprintLineis 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.

Ability inference

When inferring ability requirements forf,the ability requirements become the union of all requirements for functions that can be called within the body of the function.