Dartの規格に、次のような文がある。
The static type of null is ⊥.
The decision to use ⊥ instead of Null allows null to be assigned everywhere without complaint by the static checker.
現行のドラフト規格にはbeがニ連続するtypoあり。
この⊥が何を意味するのか分からなかった。しかたがないので、IRCで人に聞いた。
私:この⊥ってやつはなんだ?
人:"bottom"
私:bottom? 何かプログラミングか数学の用語なのか?
人:lattice theoryから来てる。
人:top(本当は特別な文字があるけど)ってのがすべての上にたつ汎用的な存在で、たとえばObjectだね。
人:bottomは何よりも特殊な存在なんだ。
私:つまり、bottomであるnullからみれば、すべての型はスーパークラスのようなものだということか。
人:そういうこと。
ちなみに、topの記号は⊤で、UnicodeではU+22A4である。⊥はU+22A5である。
なぜか、昔から数学はさっぱり理解できなかった。高校生の時、理系クラスに進もうとしたら、親に反対された。特に普段、勉強しろとも言わない親ではあったが、子供の勉強を反対するというのも奇妙だ。その時の言葉が印象に残っている。
「あんたに数学は無理よ。私達にだってできなかったんだから」
まるで、なにか遺伝的、先天的に数学ができないかような物言いだったのである。私の両親はそれなりに高学歴である。これは一体どういうことか。
親の案の定、私は数学をさっぱり理解できず、高校時代は、古文、漢文、英文を読んで過ごした。なぜか、私の親と同じ道をたどっているのである。
思えば、私も変な子供だったものだ。何故か昔から読書が好きだったし、小学生の頃には、すでに古事記や論語や徒然草などを読んでいた。もちろん、これは親がそのような本を家に置いていたし、「論語のどこそこ 」とか、「徒然草の第何段」といった会話が成立するほどの教養を持っていたからということもあるのだろうが、やはり不思議なことだ。何か、遺伝的なものがあるのだろうか。
今だって、私の感じるプログラミングの面白さとは、コードを書くのではなく、プログラミング言語の文法を理解することなのだ。何故こうなってしまったのだろう。
私は理系に進みましたが, 抽象的な数学は分かりません.
ReplyDeleteしかし, 分かることは, このような型はScalaにもあるということです.
http://www.scala-lang.org/api/2.9.0/scala/Nothing.html
私はScalaの本を読んでちょこちょこっといじったあと, めんどくさくなったため放置しているのでこれ以上のことは分かりませんし, 理論的な背景も分かりませんが, リンク先の文章を読む限りでは, そのbottomというのはScalaのNothing型です. すべての型のsubtypeであると書いてありますから.
私のおぼろげな記憶では, これがあると例外がうまく扱えるなぁみたいなことでした. 今ぐぐってみると何となく私の記憶は確かそうです. bottomという文字も見えるので, 同一の概念ではないかという確信が高まります.
http://scala-programming-language.1934581.n4.nabble.com/undefined-bottom-td1988425.html
参考まで.
Haskellとかにもあるそうですね。
ReplyDeleteまあ、私が苦手だったのは計算なのかもしれませんが。
もう解決したかもしれませんが、
ReplyDelete疑問にされた記号は、数学では、
「垂直」を表す記号として使用されること
が多いかもしれません。
つまり、"a_|_b"は、「aはbに垂直である。」
という意味になります。
ただ、これ以外の意味で使われることも
ありますが....