Types and values

Data types#

Faber có hệ thống kiểu tĩnh, ưu tiên kiểu. Mọi khai báo đều đặt kiểu trước tên: văn_bản tên, không phải tên: văn_bản. Hệ thống kiểu bao phủ các kiểu nguyên thủy vô hướng, tập hợp tổng quát, kiểu số có kích thước, tensor và các kiểu thanh ghi hướng đến GPU.

Các kiểu nguyên thủy#

Các kiểu số có kích thước#

Viết độ rộng ở vị trí kiểu. Đây là các kiểu số — cùng danh sách với Math in the ether:

bắt_đầu {
    hằng i32 narrow ← 7 ∷ i32
    hằng u64 wide ← 255 ∷ u64
    hằng f32 single ← 1.5 ∷ f32
}

Độ rộng trần là kiểu.

Các kiểu nullable#

Giá trị nullable sử dụng cú pháp hợp T ∪ rỗng_ty:

hàm find(văn_bản key) → số ∪ rỗng_ty {
    trả không_gì
}

hàm maybe() → văn_bản ∪ rỗng_ty {
    trả không_gì
}

Faber không có cú pháp T? hoặc Option<T>. Hợp kiểu phải được viết tường minh.

Bí danh kiểu#

kiểu_tên UserId = số

Generics#

Hàm, bí danh kiểu, kiểu và giao_ước chấp nhận tham số kiểu với cú pháp <T>:

hàm identitas<T>(T giá_trị) → T {
    trả giá_trị
}

hàm primum<T>(danh_sách<T> res) → T ∪ rỗng_ty {
    trả res.đầu_tiên()
}

Có thể chỉ rõ đối số kiểu tại vị trí gọi:

hàm identitas<T>(T giá_trị) → T {
    trả giá_trị
}

bắt_đầu {
    hằng số value ← identitas<số>(7)
}

Tập hợp#

bắt_đầu {
    hằng danh_sách<số> nums ← [1, 2, 3]
    hằng bảng<văn_bản, số> scores ← { "alice": 10, "bob": 20 }
}

Các kiểu tensor#

ten_xo<T, Figura> là bộ chứa dày có hình dạng cố định:

bắt_đầu {
    hằng ten_xo<f32, []> scalar ← tập_rỗng
    hằng ten_xo<số, [4]> row ← [1, 2, 3, 4] ↦ ten_xo<số, [4]>
    hằng số ∪ rỗng_ty first ← row[0]
}

Các kiểu lõi GPU#

Các kiểu này được lane hệ thống nhận diện để xử lý GPU và thanh ghi. Các đích gói không hỗ trợ phần cứng sẽ từ chối chúng:

hàm half(f16 x) → f16 { trả x }

hàm add(ma_trận<f32, [2, 2]> a, ma_trận<f32, [2, 2]> b) → ma_trận<f32, [2, 2]> {
    trả a.addita(b)
}

hàm swap(nguyên_tử<i32> cell, i32 value) → i32 {
    trả cell.exchange(value)
}

Marker mượn trên kiểu#

Các marker mượn (ra, vào, sở_hữu) có thể xuất hiện trên kiểu ở vị trí tham số để cho biết cách truyền một giá trị:

# shared borrow — caller retains ownership
functio imprime(de textus label) → vacuum { }

# mutable borrow — caller lends mutable access
functio duplica(in numerus value) → vacuum { }

# move — caller gives up ownership
functio consume(own textus buffer) → textus {
    redde buffer
}

Chính sách so sánh#

Variables and binding#

Faber có ba từ khóa biến và một ký hiệu gán riêng. Điểm khác biệt chính nằm giữa hằng (chỉ ghi một lần) và biến (có thể gán lại tự do), cũng như giữa ← (luồng thực thi) và = (hình dạng trường mang tính cấu trúc).

hằng — liên kết bất biến#

Các liên kết hằng chỉ được ghi một lần. Có thể khai báo chúng có hoặc không có trình khởi tạo; nếu khai báo mà không có trình khởi tạo, chúng phải được gán đúng một lần trước khi đọc. Lần gán thứ hai sẽ bị từ chối.

bắt_đầu {
    hằng số count ← 0
    hằng văn_bản name ← "Marcus"
    hằng _ inferred ← [1, 2, 3]
}

Khởi tạo trì hoãn:

bắt_đầu {
    hằng số factor
    nếu đúng {
        factor ← 10
    }
    khác {
        factor ← 100
    }
    ghi_chú factor
}

biến — liên kết khả biến#

Các liên kết biến có thể được gán lại tự do:

bắt_đầu {
    biến số count ← 0
    count ← count + 1
    count ← count * 2
}

đặt — cú pháp rút gọn cho liên kết bất biến suy luận kiểu#

đặt là cú pháp rút gọn của hằng _ — một liên kết bất biến với kiểu được suy luận:

bắt_đầu {
    hằng _ salve ← "Salve"
    hằng _ tên ← "Marcus"
    hằng _ x ← 42

    # Deferred form
    hằng _ label
    label ← "deferred"
}

Liên kết thời gian chạy và định nghĩa cấu trúc#

Faber tách biệt hai vai trò mà hầu hết các ngôn ngữ gộp chung vào =:

kiểu Point {
    hằng số x
    hằng số y
}

bắt_đầu {
    # Runtime: ← attaches a value to a name at execution time
    biến số count ← 0
    biến văn_bản label ← "ready"
    count ← count + 1

    # Structural: = defines field values inside a type literal
    hằng _ p ← Point { x = 10, y = 20 }
}

Trích xuất trường bằng từ#

từ trích xuất các trường từ một giá trị vào các liên kết cục bộ:

kiểu Persona {
    hằng văn_bản tên
    hằng số aetas
}

bắt_đầu {
    hằng _ p ← Persona { tên = "Marcus", aetas = 30 }
    hằng văn_bản tên ← p.nomen
    hằng số aetas ← p.aetas
    # prints "Marcus"
    ghi_chú tên
}

Cập nhật số khả biến#

Dùng các toán tử nhị phân + và - cùng phép gán thời gian chạy ← để cập nhật các vị trí số khả biến. Cả hai toán tử đều nhận hai toán hạng; chúng không phải câu lệnh hậu tố:

bắt_đầu {
    biến số i ← 0
    # i becomes 1
    i ← i + 1
    # i becomes 0
    i ← i - 1
}

Collections#

Faber có một số kiểu tập hợp do trình biên dịch sở hữu. Các phương thức chuẩn của chúng nằm trong trình biên dịch, không nằm trong thư viện chuẩn.

Lista — tập hợp động có thứ tự#

bắt_đầu {
    hằng danh_sách<số> empty ← tập_rỗng
    hằng _ numbers ← [1, 2, 3, 4, 5]
    hằng _ names ← ["Marcus", "Julia", "Gaius"]
    hằng _ nested ← [[1, 2], [3, 4]]
}

Trải phần tử bằng rải:

bắt_đầu {
    hằng danh_sách<số> a ← [1, 2, 3]
    hằng danh_sách<số> b ← [4, 5, 6]
    hằng _ combined ← [rải a, rải b]
    hằng _ headed ← [0, rải a, 99]
}

Các phương thức chính: longitudo, accipe, appende, tổng, primus, novissimus.

Tabula — ánh xạ khóa–giá trị#

bắt_đầu {
    hằng bảng<văn_bản, số> scores ← { "alice": 10, "bob": 20 }
}

Tensor — bộ đệm dày có hình dạng cố định#

bắt_đầu {
    hằng ten_xo<f32, []> scalar ← tập_rỗng
    hằng ten_xo<số, [4]> row ← [1, 2, 3, 4] ↦ ten_xo<số, [4]>
    hằng số ∪ rỗng_ty first ← row[0]
}

Cú pháp rút gọn cho Tensor (mã thiên về số):

bắt_đầu {
    hằng tf32[] seed ← tập_rỗng
    hằng tf32[4] lanes ← seed.dựng_từ_phẳng([1.0, 2.0, 3.0, 4.0], [4])
}

Các phương thức chính: forma, accipe, ponde, crea, structa, strue, cùng với phép tính theo từng phần tử, phép nhân ma trận (multiplicatio) và các phép rút gọn (tổng, productum).

Sparsa — bộ đệm thưa có hình dạng cố định#

bắt_đầu {
    hằng thưa<f32, [2, 3]> sparse ← tập_rỗng
    sparse.ponde([0, 1], 4.0)
    sparse.ponde([1, 2], 9.0)

    # accipe returns the stored value, here 4.0
    ghi_chú sparse.accipe([0, 1])
    # count of stored entries
    ghi_chú sparse.nonnihil()
}

Chuyển đổi giữa dạng dày và dạng thưa:

bắt_đầu {
    hằng tf32[2, 2] dense ← [[1.0, 0.0], [0.0, 2.0]] ↦ ten_xo<f32, [2, 2]>
    hằng sf32[2, 2] sparse ← dense ↦ thưa<f32, [2, 2]>
    hằng tf32[2, 2] roundtrip ← sparse ↦ ten_xo<f32, [2, 2]>
}

Cursors — luồng lười#

con_trỏ<T> là một kiểu luồng lười. Nó được tạo từ các bộ lặp của tập hợp, các view nhận hoặc các hàm sinh. Luồng được tiêu thụ bằng lặp từ:

bắt_đầu {
    hằng _ items ← [1, 2, 3]
    lặp từ items hằng item {
        ghi_chú item
    }
}

Intervallum — các khoảng#

# exclusive range: 0, 1, 2, 3, 4
lặp khoảng 0‥5 hằng i {
    ghi_chú i
}
# inclusive range: 0, 1, 2, 3, 4, 5
lặp khoảng 0…5 hằng i {
    ghi_chú i
}

‥ là điểm cuối khoảng loại trừ; … là điểm cuối khoảng bao gồm.

String and template literals#

Faber sử dụng ngữ nghĩa của các dấu phân cách — mỗi dạng dấu nháy biểu thị một dạng mã nguồn khác nhau. Chúng không phải là các từ đồng nghĩa có thể thay thế cho nhau.

Dạng literal#

Áp dụng template chuỗi#

Faber định dạng văn bản bằng phép áp dụng template chuỗi: một literal "…" hoặc «…» có các vị trí trống §, theo sau là các đối số trong ngoặc đơn:

hàm greet(văn_bản tên) → văn_bản {
    trả "Salve, §!"(tên)
}

bắt_đầu {
    hằng số pagina ← 3
    hằng số totum ← 10
    hằng văn_bản code ← "200"
    hằng văn_bản label ← "OK"
    hằng _ msg ← "Page § of §"(pagina, totum)
    hằng _ block ← "status: § (§)"(code, label)
}

Các quy tắc chính:

• § (U+00A7) là vị trí trống của template
• Vị trí trống theo thứ tự: §0, §1, … để chỉ rõ thứ tự
• Dấu ! ở cuối chọn cách định dạng hiển thị: "Salve, §!"(tên)
• Hậu tố (args) là phép áp dụng template, không phải lời gọi hàm

Chuỗi dạng khối#

Các khối nhiều dòng sử dụng dấu ngoặc kép kiểu guillemet «…»:

bắt_đầu {
    hằng _ sql ← «
        select id, email
        from accounts
    »
}

Template được thu giữ (forma)#

Template dùng dấu backtick thu giữ văn bản và tham số mà không thực hiện việc kết xuất. Phù hợp cho payload SQL/URL có liên kết tham số:

bắt_đầu {
    hằng số user_id ← 42
    hằng _ query ← `select * from users where id = §`(user_id)
}

JSON nội tuyến#

{ … } trần là JSON nội tuyến: một tài liệu json tại thời điểm biên dịch, không phải là đối tượng Faber ẩn danh. Các khóa là chuỗi được đặt trong dấu nháy và phân tách bằng ::

bắt_đầu {
    hằng _ empty ← {}
    hằng _ user ← { "name": "Marcus", "age": 30, "active": true }
    hằng _ nested ← { "meta": { "version": 1 }, "tags": ["alpha", "beta"] }
}

Để tạo một kiểu có kiểu, hãy sử dụng tên kiểu và dạng trường với =:

kiểu Point {
    hằng số x
    hằng số y
}

bắt_đầu {
    hằng _ p ← Point { x = 10, y = 20 }
}

Nullability and optionality#

Faber phân biệt sự vắng mặt trong một giá trị với việc cung cấp tùy chọn tại vị trí khai báo.

Giá trị nullable — T ∪ rỗng_ty#

Dùng T ∪ rỗng_ty khi giá trị có thể vắng mặt:

hàm find(văn_bản key) → số ∪ rỗng_ty {
    trả không_gì
}

hàm divide(số a, số b) → số ∪ rỗng_ty {
    nếu b ≡ 0 do_đó trả không_gì
    trả a / b
}

Vị trí khai báo tùy chọn — tự_nguyện#

Đặt tự_nguyện sau tên khi tham số hoặc trường có thể được lược bỏ bởi bên gọi hoặc hàm khởi tạo:

hàm connect(văn_bản host, số port tự_nguyện) → trống {
}

kiểu User {
    hằng văn_bản email tự_nguyện
}

Các dấu mượn có thể kết hợp với tham số tùy chọn:

hàm process(ra số depth tự_nguyện) → trống {
}

Khẳng định non-null — !#

Dùng !., ![, !( để khẳng định rằng một giá trị nullable không phải là rỗng_ty:

kiểu Box {
    hằng số ∪ rỗng_ty val
}

bắt_đầu {
    hằng Box ∪ rỗng_ty maybe_name ← Box { val = 7 }
    hằng _ name ← maybe_name!.val
}

Khẳng định non-null trên rỗng_ty sẽ hủy thực thi tại thời điểm chạy.

Kết hợp nullish — vel#

bắt_đầu {
    hằng văn_bản ∪ rỗng_ty provided ← không_gì
    hằng _ name ← provided hoặc_nếu_rỗng "default"
}

chưa_biết#

chưa_biết là kiểu unknown cấp cao nhất dành cho các lối thoát tạm thời và tri thức chưa hoàn chỉnh. Đây không phải là cơ chế biểu diễn tính nullable.

Conversion and construction#

Hai toán tử chuyển đổi quan trọng, một toán tử dùng khi chạy chương trình và một toán tử dùng tại thời điểm biên dịch:

# runtime chuyển
bắt_đầu {
    hằng _ parsed ← "42" ↦ số ⊥ 0
    # static ascription
    hằng số value ← 7
    hằng _ text ← value ∷ văn_bản
}

Chuyển đổi khi chạy chương trình — ↦#

Dùng ↦ để chuyển đổi khi chạy chương trình, đặc biệt là khi phân tích cú pháp hoặc ép kiểu có thể thất bại. Cung cấp xử lý phục hồi nội tuyến bằng ⊥:

bắt_đầu {
    hằng văn_bản input ← "9"
    hằng _ n ← "42" ↦ số ⊥ 0
    hằng _ safe ← input ↦ số ⊥ 0
}

Vật chất hóa theo kiểu:

bắt_đầu {
    hằng văn_bản path ← "/etc/hosts"
    hằng _ lanes ← [1.0, 2.0, 3.0, 4.0] ↦ vectơ<f32, 4>
    hằng _ body ← gọi 'solum:lege' (path) ↦ văn_bản
}

Gán kiểu tĩnh — ∷#

Dùng ∷ để gán kiểu tĩnh một cách tường minh. Toán tử này đặt ở hậu tố và được điều khiển bởi kiểu đích:

bắt_đầu {
    hằng số value ← 7
    hằng _ x ← 7 ∷ i32
    hằng _ text ← value ∷ văn_bản
}

Kết hợp giá trị null — vel#

Dùng hoặc_nếu_rỗng để kết hợp giá trị null khi một giá trị là rỗng_ty:

bắt_đầu {
    hằng văn_bản ∪ rỗng_ty provided_name ← không_gì
    hằng _ name ← provided_name hoặc_nếu_rỗng "default"
}