Effects

Declaration

Effects can be defined in one of two ways: 1. As an operation, given its signature

   effect <name>(<argument-name>:<argument-type>,<...>) -> <return-type>

for example:

   effect interact(prompt: string) -> string

defines the effect interact, which consists only of the operation interact: (string) -> string which takes a string and returns a string.

  1. As a combination of other effects kima effect <name> { <effect-name>, <effect-name>,<...> } the effect defined consists of all the operations defined by the effects specified by name inside the {}

for example:

   effect output(value: string): Unit
   effect input(): string

   effect console { output, input }

Here the console effect is defined as the sum of the output and input effects. I.e it consists of the operations output: (string) -> Unit and input: () -> String

Sub-effects

An effect e1 is a sub-effect of e2 if the set of operations of e1 is a subset of the set of operations of e2.

For example here:


effect op1(x: Int) -> Unit
effect op2(x: Int) -> String
effect op3(x: Float) -> Int

effect e1 { op1, op2 }
effect e2 { op1, op3 }
effect e3 { op1, op2, op3 }
effect e4 { e1, e2 }

e1 is not a sub-effect of e2 — or vice-versa — while both e1 and e2 are sub-effects of both e3 and e4

Effectful functions

The effect type of a function is specified as follows:

fun <function-name>(<arguments>) : <effect> -> <return-type> { <body> }

In this function, all the operations of <effect>, as well as functions with an effect type that is a sub-effect of <effect> be used inside <body> directly.

<effect> can also be given as a set of effects like so:

fun <function-name>(<arguments>)
    : { <effect1>, <effect2>, ... }
    -> <return-type> { <body> }

This is equivalent to defining an intermediate effect like effect funcEff { <effect1>, <effect2>, ...} and using that as the effect of the function.

Omitting the effect type

In function signatures, function declarations and function expressions, you can omit the : <effect> section to imply the pure effect. For example:

# Declaration
fun f(x: int) -> int { ... }

# Expression
let f = fun(x: int) -> int { ... }

# Signature
let f: (int) -> int = ...

all fs defined above refer to functions with the signature (int) : pure -> int

Using effect inference

The special effect name * can be used to invoke effect inference. When used in a function declaration or function expression it means that the function will have the smallest effect that is required to allow the function to effect-check.

For example, here the function f will have signature () : op1 -> Unit

effect op1() -> Unit
effect op2() -> Unit

fun f() : * {
   op1()
}