unsafe
unsafe
は、Leanのルールを破るような操作を許可するのに使う修飾子です。
たとえば、次のような帰納型は strictly positive 要件というLeanのルールに反するのでエラーになり、定義することができません。
/-
error: (kernel) arg #1 of 'Bad.mk' has a non positive occurrence of the datatypes being declared
-/
inductive Bad where
| mk : (Bad → Bad) → Bad
unsafe
で修飾すれば定義が通るようになります。
unsafe inductive Bad where
| mk : (Bad → Bad) → Bad
ptrAddrUnsafe
ptrAddrUnsafe
関数は、値のメモリ上での位置を返す関数ですが、unsafe
で修飾されています。
/- info: unsafe opaque ptrAddrUnsafe.{u} : {α : Type u} → α → USize -/
#print ptrAddrUnsafe
これは、ptrAddrUnsafe
が 参照透過性(referential transparency) を壊してしまうからです。参照透過性とは、「引数の値が同じならば関数の値も同じ」という性質です。ptrAddrUnsafe
は等しい引数でも異なる値を返すことがあります。
/- info: true -/
#eval show Bool from Id.run do
let u := ptrAddrUnsafe ([1, 2, 3])
let v := ptrAddrUnsafe ([1, 2] ++ [3])
-- 引数の値は同じだが
assert! [1, 2, 3] == [1, 2] ++ [3]
-- 返り値が異なる!
return u != v
Functional but in-place
unsafe
が付与されていない通常の関数は参照透過性を持ち、したがって特に Lean ではグローバル変数の値を変更することは通常できません。
-- foo という変数を定義する
def foo := "hello"
-- 再定義しようとするとエラーになる
/- error: 'foo' has already been declared -/
def foo := "hello world"
しかし、ローカル変数は破壊的に変更することができます。
/-- フィボナッチ数列を計算する -/
def fibonacci (n : Nat) : Array Nat := Id.run do
-- 可変な配列 `fib` を宣言する
let mut fib : Array Nat := Array.mkEmpty n
fib := fib.push 0
fib := fib.push 1
for i in [2:n] do
-- 更新前の配列 `fib` のメモリアドレスを取得
let old := unsafe ptrAddrUnsafe fib
-- `fib` を更新
fib := fib.push (fib[i-1]! + fib[i-2]!)
-- 更新後のメモリアドレスを取得
let new := unsafe ptrAddrUnsafe fib
-- メモリアドレスが一致する
assert! old = new
return fib
-- 値がコピーされていれば panic するはずだが...?
/- info: #[0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377] -/
#eval fibonacci 15
なぜこのようなことができるのかというと、Lean が値の不要なコピーを行わないからです。具体的には、Lean は 参照カウント がちょうど1であるような値を更新する際に、コピーして新しい値を生成する代わりに破壊的変更を行います。これを指して、Lean 言語のパラダイムのことを Functional but in-place と呼ぶことがあります。