柱 · 02言語
daitai-lang
ブラケット原始型を持つ、静的型付け・決定論的言語。
これは何か
daitai-lang は39以上の代数的キーワードを持ち、null、例外、暗黙の型変換が存在しない汎用言語です。 オプション値は Optional<T>、失敗可能な操作は Result<T, E> を返します。 その他はすべて、希望ではなく構造的書き換えで型検査されます。
状態はデフォルトで不変です。変更は State × Event → State 形式の明示的な遷移関数を通じて行われます。 つまり、プログラム内のすべての変化は再生可能で、推論可能で、仕様と比較可能です。 言語はブラケットリテラル — |0⟩、|1⟩、⟨ψ| — を第一級構文として提供します。 言語の下にある代数は量子状態と古典状態を同じ語彙で扱うためです。
なぜ存在するか
主流言語は「実用的」とは実行時エラーを人生の一部として受け入れることだと考えました。 Rustはメモリ安全性で、Haskellは副作用でそれに反論しました。daitai-langは次のことに反論します。 不透明な命令的トレースとしてのプログラム、です。 関数が Distribution<Int> を返すと宣言すれば、型システムはそれがdaitai代数のソートであることを知り、付随する書き換え規則を解放します。 コンパイラが最適化に使う規則も、証明器が検証に使う規則も含めて。
その結果、同じソースコードからバイナリへのコンパイル、証明義務へのエクスポート、CEAベクトルへのフィンガープリント、本番投入が、ひとつのツリーから、同じ代数に対して検証されながら行える言語が生まれます。
コード例
qubit.daitaidaitai
# A two-qubit register, prepared in a Bell state.
type Register = Tensor<Qubit, Qubit>
fn bell() -> Register {
let q0 = |0⟩
let q1 = |0⟩
let h = H(q0) # superposition
let r = CNOT(h ⊗ q1) # entangle
r
}
# Step semantics: classical observation collapses the state.
let step : Register × Measure -> Distribution<Bit × Bit> = observe