Effect

Một hàm không có mệnh đề uses được trình biên dịch bảo đảm là thuần khiết. Đây không phải quy ước viết code và cũng không phải kết quả của một lần review — nó là hệ quả của việc phân tích effect xuyên suốt đồ thị gọi. Một hàm không khai báo gì có tập capability rỗng, và tập rỗng không bao giờ chứa được tập effect của một hàm mà nó gọi.

Chín effect

Effect	Cho phép	Trong bí danh trùm uses IO?
IO	Ghi console, đọc stdin	Có
Fs	Hệ thống tệp	Có
Clock	Đồng hồ và ngủ	Có
Args	Dòng lệnh	Có
Exit	Kết thúc tiến trình	Có
Net	DNS, socket, TLS	Không
Rand	Ngẫu nhiên	Không
Proc	Tiến trình con, biến môi trường	Không
Conc	Task, kênh, lịch trình	Không

uses IO là bí danh trùm: ở mức phân tích cú pháp nó nở ra thành {IO, Fs, Clock, Args, Exit}. Nó tồn tại để tương thích ngược với mã cũ. Nó không bao gồm Net, Rand, Proc hay Conc — bốn effect này phải được khai báo tường minh.

Viết uses Bogus là lỗi phân tích cú pháp, và trình biên dịch liệt kê đúng tập effect hợp lệ.

Khai báo một effect

fn read_config(path: str) -> str uses Fs {
    return read_file(path)
}

fn elapsed_ms() -> int uses Clock {
    return clock_ms()
}

fn program_args() -> list[str] uses Args {
    return args()
}

fn pure_compute(n: int) -> int {
    # Không có mệnh đề `uses` -> thuần khiết theo cấu trúc
    let mut s: int = 0
    let mut i: int = 0
    while i < n {
        s = s + i
        i = i + 1
    }
    return s
}

pure_compute không thể in ra, không thể đọc tệp, không thể đọc đồng hồ và không thể chạm vào mạng — và điều đó được kiểm tra, không phải hứa suông.

Điều trình biên dịch nói khi bạn khai sai

Khi thiếu khai báo, trình biên dịch không chỉ trỏ vào dòng lỗi. Nó gọi tên chuỗi gọi đã mang effect tới đó:

error: function 'load_config' calls 'read_file' which requires effect 'Fs'
not declared (declared: (none - pure); missing: Fs)

Và nếu bạn khai pure nhưng lại gọi một hàm có effect:

error: function 'f' is declared 'pure' but calls 'println' which requires
effect 'IO' (declared pure but callee chain is not pure)

pure và uses loại trừ lẫn nhau ở mức phân tích cú pháp. pure không phải món trang trí: nó là một lời tuyên bố mà checker kiểm tra xuyên suốt đồ thị gọi và gọi tên cạnh vi phạm khi lời tuyên bố sai.

Báo cáo audit

hlc --audit examples/effects_demo.hls

in ra, cho từng hàm, các capability mà nó khai báo nằm cạnh các capability mà trình biên dịch tính toán được:

  function                       declared                       computed
  ------------------------------ ------------------------------ ------
  pure_compute                   (none - pure)                  (none)
  read_config                    Fs                             Fs
  elapsed_ms                     Clock                          Clock
  program_args                   Args                           Args
  main                           IO, Fs, Clock, Args, Exit      IO, Fs, Clock, Args, Exit

Cột computed trống của pure_compute là lập luận của cả trang trong một dòng: trình biên dịch đã đi đồ thị gọi và không tìm thấy effect nào.

Lưu ý rằng cột declared của main đã hiện ra dạng nở của bí danh trùm — IO, Fs, Clock, Args, Exit — vì việc nở diễn ra ở mức phân tích cú pháp.

Token capability

Từ Stage 111, effect còn có dạng giá trị là Cap[E] — một capability token có thể được bind, truyền, trả về và lưu vào struct field. Nó chỉ có thể được cấp bởi main hoặc bởi một hàm đã khai effect đó.

Kiểm tra nhanh một lời tuyên bố

Câu hỏi	Nhìn ở đâu
Hàm này có thể in ra không?	Cột computed có chứa IO không?
Nó có thể chạm đồng hồ không?	Clock trong computed?
Nó có thể mở socket không?	Net trong computed — kể cả khi gọi qua 5 lớp hàm?
Nó có thể sinh task không?	Conc trong computed?

Danh sách đầy đủ builtin theo từng effect nằm ở trang tra cứu nhanh.