子程序

函數

some_func(x: T, y: U) -> V
some_func: (T, U) -> V

過程

some_proc!(x: T, y: U) => V
some_proc!: (T, U) => V

函數方法

方法類型不能用Self在外部指定

.some_method(self, x: T, y: U) => ()
# (Self, T, U) => () 擁有 self 的所有權
.some_method: (Ref(Self), T, U) => ()

過程方法(依賴)

在下文中，假設類型 T! 采用類型參數 N: Nat。要在外部指定它，請使用類型變量

K!: Nat -> Type
# ~> 表示應用前后類型參數的狀態(此時self必須是變量引用)
K!(N).some_method!: (Ref!(K! N ~> N+X), X: Nat) => ()

注意，.some_method 的類型是 | N，X: Nat| (Ref!(K! N ~> N+X), {X}) => () 對于沒有 ref! 的方法，即在應用后被剝奪所有權，不能使用類型參數轉換(~>)

如果取得所有權，則如下所示

# 如果不使用N，可以用_省略
# .some_method!: |N, X: Nat| (T!(N), {X}) => T!(N+X)
.some_method!|N, X: Nat| (self: T!(N), X: Nat) => T!(N+X)

運算符

可以通過用 ` 括起來將其定義為普通函數

中性字母運算符，例如 and 和 or 可以通過用 ` 括起來定義為中性運算符

and(x, y, z) = x and y and z
`_+_`(x: Foo, y: Foo) = x.a + y.a
`-_`(x: Foo) = Foo.new(-x.a)