scalazに限らずHaskellもしくはCoqなどの定理証明系の言語の文脈でもLeibniz Equalityという言葉出てくると思いますが、その話
といっても、(学生の頃少しは好きだったけど)数学とか哲学とか別にすごく詳しいわけではないので、調べたことを貼り付けるだけのなにかです。
1年数ヶ月前にこんなtweetしましたが
答えはyesですね。たぶん
ちなみに、ライプニッツというと、微分の話で出てきたり、プログラミングじゃなく哲学の方の"モナド"の文脈で出てきますね。
そもそも "Leibniz Equality" とか "Leibniz' law" あたりでググればいくらでも出てくる(ただし英語だし、プログラミングじゃなく数学の話が多い)
ので、「それらを怖がらずに読めばいいだけだろ！」と、1年数ヶ月前の自分に言ってやりたいですね。
ただし、単に"Leibniz' law"だけだと、英語版wikipediaに「(日本語版でいう)曖昧さ回避のページ？」があるように
https://en.wikipedia.org/wiki/Leibniz%27_law
微分のほうの別のlawを指す場合もあるので注意が必要です。
さて、なんとなく数学用語なのはわかるとして、なぜ「ライプニッツ」という哲学者かつ数学者*1の名前が出てくるか？あたりの話ですが、正解というか一番関連ありそうなページとして、とりあえずwikipedia貼り付けましょう
https://en.wikipedia.org/wiki/Identity_of_indiscernibles
"Identity of indiscernibles"
で、日本語に訳されてるのを探すと「不可識別者同一の原理」というのはありました。日本語版のwikipediaの「同一性」のページにも、以下のように一言だけ書いてありますね
https://ja.wikipedia.org/wiki/%E5%90%8C%E4%B8%80%E6%80%A7
ライプニッツは、識別できない2つの個体はないとする不可識別者同一の原理を立てた。この原理は、Xのもつ全ての性質をYがもち同時にYがもつ全ての性質をXがもつとき、X=Yが成り立つことを示すものと解されている。
余談として「Identity of indiscernibles」そのものについて考えだすと「量子力学では〜」みたいな話がでてきたり、どんどんプログラミングから離れて色んな方向にとんでいけるのでオススメです(ぇ
さて、このあたりそれほど自信ないのですが、どちらかというと、まず哲学の用語というか思想的にライプニッツさんがそういうこと言い出して、それが後から数学にきた*2感じでしょうか？
後はHaskell関係の話というか、プログラミング的な理論的な話としては、まずscalaz.Leibnizのソースコード中に貼ってあるHaskell cafeのリンクや
- https://github.com/scalaz/scalaz/blob/v7.2.0-M3/core/src/main/scala/scalaz/Leibniz.scala#L159
- http://osdir.com/ml/haskell-cafe@haskell.org/2010-05/msg00114.html
もう一つ貼ってある
「Typing Dynamic Typing (Baars and Swierstra, ICFP 2002)」
という論文読めばいいんじゃないでしょうか
https://github.com/scalaz/scalaz/blob/v7.2.0-M3/core/src/main/scala/scalaz/Leibniz.scala#L9
haskell-cafeの方のリンク貼ってあるところには
「Haskellだとtype familyでできることをolegさんが示してるんだけど、scalaではforce(という安全ではないcastの操作)するよ」
みたいなこと書いてありますね。
scalazを知ってから、何年もこのあたりのコメントの意味理解できなかった(なんとなくHaskellのリンク貼ってあるなーというだけの認識だった)
けど、最近になって、ようやく何割か理解できた気がします。
まとまってるのかよくわからない、(冒頭で言ったように)リンクいっぱい貼り付けただけの記事ですが、これ以上詳しく説明できることないので、このあたりにしておきます
