haskell-jp / questions #46

Hutton本2に「newtypeで宣言するデータ型も再帰的にできる」って書いてあるんですが、これは誤りですよね？ 再帰的にできるのは、data だけですよね？

GHCだと、newtype を再帰的に使えるみたいですが、どう使うんでしょうか？

こんな感じでしょうか？
newtype NewTypeRecursion a = N (Either (NewTypeRecursion a) a)

fix コンビネーターが newtype で作れるみたいです http://ilyaletre.hatenablog.com/entry/2018/03/20/224320

はるかに良い例を出されてしまった^^;

要は場合分けがないと再帰が止まらないだろうという話だったんだと思いますが、中身が場合分けを持つ型ならできるじゃんというのが私の発想で、そうでなくとも無限再帰的な型でも意味がある場合があるってことですね…

不動点オペレータの場合、結局「f」に場合分けがあることを期待している、というべきでしょうか

勉強になりました。

しかし、Hutton本2で紹介すべきか疑問ですね。Huttonさんに意図を聞いてみます。

EmptyCase拡張が無かった昔は newtype Void = Void Void みたいなのも使いましたよ．

依存型っぽいことをするためですか？

パッと思いつくのは phantom type で「型の違いを作るための目印として使うが実際には無視される型引数」に入れるのに使う、ってやつでしょうか（phantom type でぐぐると実例がでてきます）

なるほど。

一般に， type は型の計算が遅延しませんが， newtype は遅延するのが強みだと思っていました(再帰型の場合は type は無限再帰が起き停止しなくなりますが， newtype は型上は data と同じ扱いなので新しい型が作られるだけですね)

↑の Void は「値を構成できない型」を作るためで，“矛盾“に相当します．定理証明をするためですね．

勉強になります

実用的には「定理証明が必要となるような強力で厳密な依存型インターフェースを提供するため．」かな．

newtype で再帰型は割と使う人なのですが， Cofree とかは

newtype Cofree f a = Cofree (a, f (Cofree f a))

とも書けますね(やってることは同じなので， data を使うべきというのはそうですが)

Hutton本を読んだことがないので，どういうレベルの本なのか分からないですが， type と newtype ， data の大きな違いは
• type は再帰型が書けないが， newtype / data は書ける ( でも強調されてますね)
• type はインスタンスにできないが， newtype / data はインスタンスにできる
• newtype はコンストラクタが実行時に無いように振舞う
ということだと思うので，この3つは Haskell を書く上では押さえておいてほしいとは思います(特に強調するべきだとは思いませんが，入門書に書いておいてほしいとは思いますね． すごいH本には確か書いてあった気がします)

評価の違い(3点目の付帯ではあるけど)も明示はあってほしい．

(あ，主に3点目は評価の違いをさしてました．パターンマッチの意味論が違う点ですね)

Hutton本は初心者用です。

newtype で再帰ができると書いてしまうと、例を出すべきですが、例が初心者のレベルを超えていると思います。

あと、H本をぱらっと読み返してみましたが、 newtype は再帰できるという説明は見つけられませんでした。

Hutton本の訳注で、「例としては Fix だが、気にしなくていい」みたいに書くのはありだとは思います。でも「 newtype が再帰できる」とは書かない方がいいと思います。

H本をぱらっと読み返してみましたが、 newtype は再帰できるという説明は見つけられませんでした。

すいません，確かに書いてないようですね．これは僕の勘違いでした．

Hutton本2が手元にないのでどういう文脈で出てくるのか分からないですが例として

newtype Tree = Tree (Int, [Tree])

みたいなのも出せるので，一概に Fix を出す必要はないんじゃないかと(これは， Hutton本1だと type declaration で書けない例として紹介されていますね)

(Hutton本1で newtype に関する記述を見つけられなかったんですが， Hutton 本2から入ったんですかね？)

この Tree の例は素敵ですね。訳注にこれを書くのが補完し合っていていいかも。

newtype は、初版にはなく、第2版から入りました。

第2版は、大幅に書き換わっていて、訳が大変です。。。

@mod_poppo has joined the channel

@ has joined the channel

試しに print $ (unsafeCoerce True :: Int) を実行してみたら 2305843009213693952 と表示されました。64bit に変換すると 0010000000000000000000000000000000000000000000000000000000000000 になり、GHCの内部表現と関係していそうなんですけど、どうしてこうなるんですか？

https://takenobu-hs.github.io/downloads/haskell_ghc_illustrated.pdf
自己解決しました（多分）。上のスライドでの Pointer Tagging の節によると、最初の 3bit が以下のようになっているそうです。
• 000 - 未評価
• 001 - 評価済みで一番目のコンストラクタ
• 010 - 評価済みで二番目のコンストラクタ
• 011 - ...

そして、True は定数なので何も参照せず、後の 61bit が空になる……ということみたいです（これ、7個以上コンストラクタがあったときはどうするんだろう）

https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts/HaskellExecution/PointerTagging
に書かれている通り、64bitだと8個以上コンストラクタを持つ場合コンストラクタ情報はtaggingされず、evaluatedかどうかで000/001のどちらかになり、コンストラクタ情報はinfo tableを見に行くことになります

Pointer Tagging はたぶん最下位ビット側だと思うので上位が立ってるのは不思議ですね…そして True は Bool にとっては「二番目」の値のはず（deriving Ord 的に False < True なので）なので、その点でも辻褄があってない気がします

面白いですね。
pointer taggingの話題自体については解決済みと思いますが、元々のコードの出力値は妙ですね。

pointer taggingは、「ヒープ上のオブジェクト(closure)」へのポインタの下位3bitに印をつける機能なので、そのポインタの値そのものは通常、ユーザーコードからは見えないです。
（つまり、print関数では、ポインタの値自体は出力していないです。）

そしてprintが出力しているのは、データ構築子`True`のマシン上での表現を、unsafeCoerceを使ってInt型に強引に解釈させたときの値です。 なので、不整合な値が出力されているのだと思います。（例え的には、Float型のバイナリ値を、Int型に解釈させて出力させたような不整合が。）

試しに、マシン上での表現が似ているInt型をWord型へ、強引にunsafeCoerceで解釈変更させたら、以下のように値自体は矛盾しない結果になりました。（CPUやOS依存あると思います。）

ghci> import Unsafe.Coerce
ghci> print $ (unsafeCoerce (-1::Int) :: Word)
18446744073709551615

18446744073709551615 は、16進表現では、ffffffffffffffff です。（つまりInt型の-1）

unsafeCoerceは、型をごまかすだけで、実行時の表現自体は変更しないというところですね。
（勘違いあればフォローお願いします。）

解決済みと思いますが念の為です。 Haskell 2010 Language Reportでも、newtypeは再帰的使われることを想定しているようです。

"Also, unlike type synonyms, newtype may be used to define recursive types."

https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-740004.2.3

print は I# を紐解くので、そもそも表示されてるものはオブジェクトの純正の表示では無いはずですね。ついでにうちの環境(mac/GHC 8.6.3)では再現しなかったです

うちの環境で試した結果です:
https://gist.github.com/mizunashi-mana/67df53477ef464232f9e97588e099cf9

print (unsafeCoerce True :: IntOrBool) が SEGV になったのは， 5764607523051092410 をBool値のヒープを指し示すポインタだと思って飛ぼうとしたせいだと思いますね．Bool値のコンストラクタはフィールドを特に持たないので，フィールドじゃない領域をフィールドだと思って参照した結果，そういう結果が返ってくるんだと思います(主に True だと True_closure + 9 ， False だと False_closure + 8 を I64 表現だと解釈した結果こういう表示になってるようです．毎回実行するごとに結果が変わっていたので，多分空いてるヒープ領域なんだと思います)

https://github.com/Hexirp/haskell-gist/blob/1a233daa267b6647bbfede385ab9be653fd0983e/Unsafe.hs
なるほど…そう単純に考えられないみたいですね。こっちの環境は Windows 10 です。上の結果は3か月前のもので、今でも再現しました

あっ、こっちの方が重要かも。実行は ghci でやってます

……GHCiとGHCって内部表現がだいぶ異なりますよね？ 根本から勘違いしてたかも

手元のUbuntu18.04だと、以下の出力になりました。（16進で0xc800_007f_6f23_a2f0です。）

ghci> main
-4035224716524808016

runghcで実行すると、実行ごとに結果が違いますね。

$ runghc Unsafe.hs 
-4035224717148402896

$ runghc Unsafe.hs 
-4035224717726351680

いずれにしても、実メモリ上のデータ表現値を、unsafeCoerceを使って違う型として強引に解釈させるので、メモリの周辺配置状況を含めて、変な値として解釈されてしまいますね。
（例えば、ある構造体で書かれたバイナリ値を、別の構造体のフォーマットに従って読んでしまう場合のように。）

ちょっと説明がうまくなかったので補足します。

GHCは、メモリ上において、各オブジェクト(closure)を、次の内部表現で持っています。
（info ptrは、Info table(メタ情報)とEntry code(実アセンブリ命令列)へのポインタです。）

+--------+--------+--------+
|info ptr|payload1|payload2|..
+--------+--------+--------+

そして、Bool型のTrueコンストラクタと、Int型の値は、各々、次のフォーマットでメモリ上に置かれます。

Bool型のTrueコンストラクタの場合
 info ptr
+--------+
| Trueへ | (ここは無し)
+--------+

Int型の数値の場合
 info ptr  payload1
+--------+--------+
| I#へ   | Int値   |
+--------+--------+

今回、Trueコンストラクタのメモリイメージを、unsafeCoerceを使って、Int型の値として無理やり解釈しようとします。ですが、Int型の「Int値」に相当するpayloadは、Trueコンストラクタにはありません。なので、「（ここは無し）」の部分を、Int値として読みに行って、たまたまそこに書かれている無効な情報をInt値と解釈していることになります。

そういえば True / False は data section に置かれるはずなので、ヒープ領域とは限らないのですね。 True_closure + 9 の場所が Windows だと別の data section の静的データがマッピングされる(ので毎回同じ出力になる)のに対し、 Mac/Linux とかだとゴミ領域になってる(ので初期化されていないゴミデータが出力される)とかかもですね。Mac/Linux 系でも上位ビットは毎回同じなので、元々何かがいたのかもですが

各種ライブラリでhttp-client-opensslでなくてhttp-client-tlsがデフォルトなのは
なにか理由があるのでしょうか。
tlsのほうのパフォーマンスが悪いのでopensslに切り替えているのですが、
そういうのをやめたいですね。

http-client-tlsはcryptonite_gf_mul（cryptoniteのパッケージにあります） というcの関数を呼んでいるのですが、これが特に遅いです。

正確な理由は存じませんが、ビルドはhttp-client-tlsの方が楽ですね。（特にWindowsだと... :disappointed_relieved:

確かに。