haskell-jp / random #26

@ has joined the channel
hfmtがTemplateHaskellのトップレベルな関数呼び出しに対応してなさそうで泣いてる
foo bar ''Baz
対応してた:two_hearts:
ちまたで話題の pixe.la のクライアントを土曜日から書き始めた
Pixela使って何か作るんですか?
$ の感覚でいると infixl 4 <$> で引っかかってしまう……
とりあえずデジカメの写真がいっぱいあるのでそれから日付情報取ってこれば撮影枚数で草生やせるなーと考えてます
なるほどそういう使いみちもあるんですね :memo:
hfmt……っていうか多分その内部のstylish-haskell?
パースエラー起こすと変なフォーマットがかかったコードを落としていく気がするので、なかなかつらくなってきた。
設定の問題?
GHCがPhabricatorからGitLabに移行するかもしれない話
https://mail.haskell.org/pipermail/ghc-devs/2018-October/016425.html
https://ghc.haskell.org/trac/ghc/wiki/WhyNotPhabricator

私もPhabricatorが嫌いなので実現したら嬉しい
登録 :done:

Haskell-jp Blog への寄稿も大歓迎です!(寄稿方法はこちら)
……って書いちゃってもいいですかね :eyes:
もうできたんだw
もちろんOKだ!
https://github.com/haskell-jp/blog/blob/master/README.md のご案内も忘れずに!
もしかしてstackage-ltsのお知らせ機能停止してます??
ほんとだ2日前に 12.16 出てるね
https://www.stackage.org
情報源がRSSだから、先方にお願いしないといけないかな?
これってどうやってるんでしたっけ?
誰かのプログラムだっけ?
いや、 questions-feed とかと同じように、SlackのRSS配信機能を使っています。
なるほど
なのでどこかで聞いてみないとな。。。止まっていると言うより、1日に連続して出たことによってなんかバグったんだろうか。。。
元のfeedが入ったXMLファイルがこれらしい https://www.stackage.org/feed/lts
ページ内検索した限り普通に12.16もヒットしますね。。。
どちらかというとSlack側の問題なんじゃないかという気がしてきました。
https://twitter.com/slackhq/status/506655984979546113 で言ってるように、5分間隔でRSSの更新を確認して、さらに、RSSのフィードとしての要件として、各レコードは正しい日付を持っていることとなっていますので、同じ日付の更新だとRSSの更新とは見られないのかもしれませんね。
http://fumieval.hatenablog.com/entry/2018/10/31/150056 最近の議論を受け、取り急ぎ「束縛」という言葉の使い方についての記事を執筆しました。なるべく正確を期したつもりですが、もし不適当な記述があればご教示ください
ちなみに、 x = 42 のように Haskell で = を使った場合は何て読むのが正しいのでしょう?定義とかですかね?
(関数|変数)定義が一番無難だと思います。
なるほど :+1:
読ませていただきました.うまく理解できないところがありましたのでコメントします.

>これは**あくまで変数とそれを導入する抽象の関係**であり、**変数と実体の関係ではない**ことだ。

「自由な」とか「束縛された」が修飾するのは構文上の**位置**なので,λ変数とそれを導入する抽象の関係を「束縛」といえることは確かだと思います.しかし,λ変数は後続の構文中での出現によって,どの位置がどの抽象で束縛されているか示すため方法の1つにすぎません.どの位置がどの抽象で束縛されているか示せれば,変数が存在しなくてもよいわけです.そうだとすると**変数と実体の関係ではない**というためにはさらに説明が必要な気がします.

>Haskellは、x = 42のような定義を与えることによって、変数で値を参照できる。だからといって「Haskellでは変数を値にバインドする」と言い切ってしまうことには大きな問題がある。理由は簡単で、変数に対して値以外もバインドできるからだ。例えばy = x + 1という宣言を考えてみよう。この宣言はyをバインドするが、その対象はx + 1という計算であり、式を評価した結果の値ではない。

>定義がインライン化(その名前が使われている場所に展開)されず、メモリ上に領域を確保すべきものと処理系が判断した場合、初めて値に関する議論が始まる――これが「代入」である。代入は、オブジェクトをヒープ(実行時に確保されるメモリ領域)上の場所にセットする。ここで言うオブジェクトは大きく分けて2種類ある。

私には,式``42``と式``6 * 7``とでは,一方は値で一方は計算であるという区別をする理由がよく判らないです.どちらの式も,「よんじゅうに」という同じ値を表わ(denote)すと考えたとき,どのような不都合がありますでしょうか?
一般にはHaskellで書かれたプログラムの意味は,数学的な関数モデルで考えるのが判りやすいと思われています.関数モデルは**構文**と**意味**で二元的に構成されている体系だとすると,**式**と**値**がその2つに相当すると考えてよいでしょう.そこに3つめの**計算**という元素を入れて,さらにメモリ,関数モデルではないモデルで説明する理由が示されていると判りやすいのかもしれません.

>この混乱は言語仕様ですらやらかしてしまっている。Haskell 2010 Language Reportの3.17.2 Informal Semantics of Pattern Matchingを見ると、"Binding does not imply evaluation"と注記しているにもかかわらず、本来オブジェクトに対するものであるパターンマッチを値に対するものと宣言してしまい、変数を値に束縛するという旨の表現を二箇所で使ってしまっている。学習者は言語仕様を読むだけでなく、case undefined + undefined of _ -> 42のような式を手元で評価し、実際の意味論を把握することを推奨する。

私としては「パターンマッチは値に対するものではなく,オブジェクトに対するものである」ことがうまく理解できません.「パターンマッチは値に対するもの」では,どのような不都合があるのでしょうか?
また``case undefined + undefined of _ -> 42``はなにを説明する例なのでしょうか.

>以下のような主張はすべて**誤り**である.

定義が明示されていないので,すこし判りにく気がします.「定義によるんじゃないの」というひねくれものが出そう(相手にしなければいいだけかもしれないですが).

bindがどのような意味で使われているかに注意を払うべき,という主張は,肝に銘じます.
> **変数と実体の関係ではない**というためにはさらに説明が必要な気がします.

この部分はよく理解できませんでした。変数が存在しなくても良いというのは例えばde-Bruijn indexのようなものを指しているのでしょうか?また、どのような説明が必要だとお考えですか?

> さらにメモリ,関数モデルではないモデルで説明する理由が示されていると判りやすいのかもしれません.

「関数モデル」(私は使わない言葉ですが)は崩していません。「式」と「値」ではなく、「式」と「オブジェクト」がより正確であると主張しています。

> 「パターンマッチは値に対するもの」

今まで述べたことに沿って考えると、もし値に対するものとした場合、サンクのような値でないオブジェクトに対してパターンマッチできないことになります。すると、`case undefined + undefined of _ -> 42`の結果はundefinedになってしまいます(実際の処理系は42を返します)。

> 定義が明示されていないので

主張が正しくなってしまうような定義でないことは本文で示唆したつもりでしたが、どのあたりが不十分とお考えでしょうか?
これは嬉しいやら悲しいやらですね。 それだけHaskellが浸透してきている証拠(なんて堅苦しいものじゃないですけど)でもあるだろうし、 ゴキブリを不浄の比喩ともとらえられるし。。。
JasperのいるFugueはHaskellを使っている会社なので、自虐的なジョークなのでしょう :bug:
@tanashin has joined the channel
型理論や圏論について、なんかちょっと難しい議論が始まると、とたんに「みんなHaskellを知ってる前提で書くけど……」モードに突入するあるある
はい,変数がないというのは de Bruijin インデックスを想定しました.
>...さらに説明が必要な気がします.
しかし,ここまでの部分は自分でもなにを言いたかったのかわかりません.撤回させてください.すみません.

>「式」と「オブジェクト」がより正確であると主張しています。

ここが要点だと思っていますが,動機というか「こころ」が良く理解できません.

サンクに対するパターンマッチするとは,どういう状況でしょう?サンクの値は⊥とみなせばよく,変数パターンはすべての値にマッチするので case undefined + undefined of _ -> 42 は42です.

>定義が明示されてないので,

これも完全に私の惚けでした.すみません.撤回させてください.誤った主張をしている側が誤った定義を使っているので,そもそも主張に意味がないことに気づいていませんでした.
雑なコメントで申し訳けありません.
@ysatoshi has joined the channel
@autotaker has joined the channel
蛇足かもしれませんがde-Bruijn indexはあくまで文字列の代わりに自然数を変数の表現に用いる仕組みで、変数が存在しないわけではありません(変数の存在しないコンビネータ論理の場合、当然束縛も存在しません)。
> ここが要点だと思っていますが,動機というか「こころ」が良く理解できません.
それが実際に使われているモデルだから、というのは十分な動機になると思います。
> サンクに対するパターンマッチするとは,どういう状況でしょう?サンクの値は⊥とみなせばよく,変数パターンはすべての値にマッチするので case undefined + undefined of _ -> 42 は42です.
サンクの値をボトムとみなしていいというのはまったく聞いたことがありません。代わりに`case 1+2+3+4+...100000 of`とかを考えてもらってもいいです。パターンマッチの話はコーナーケースといえばコーナーケースですが、Informalと前置きしているにせよ一貫性のない説明だったため、それを本文で指摘しました。
変数とは何か?も難しいですね.私は変数と構文上位置を指示する名前とを同一視して話していました.de Bruijnインデックスはその位置を束縛する抽象の位置を指示する指標ですから,変数とは別の機能なので,変数とは言わないかな.と思うしだいです.もちろん,どちらも,抽象とそれが束縛する位置を特定するために使うので目的は同じですね.

それが実際に使われているモデルだから、というのは十分な動機になると思います。

Haskellのモデルで使われているのなら十分な動機だと思います.興味としては,単純な式と値のモデルではなく,そのモデルが採用されたモチベーションは何か,ということです.
その位置を束縛する抽象の位置を指示する指標ですから,変数とは別の機能
これは同意しかねます…私ならそれこそが束縛変数の定義だと言います。

そのモデルが採用されたモチベーションは何か
これはまさに遅延評価の動機、つまり「使わない計算は評価しない」「評価した結果である値を共有する」()であると言えると思います
評価しようとしまいと,1+2 が表示(denote)する値は「さん」と考えています.これは評価戦略にかかわらずです.
それこそが束縛変数の定義だと言います。
はい,それは同意です.私の方が変数と変数名,あるいは変数と変数の出現を混同しています.
サンクの値をボトムとみなしていいというのはまったく聞いたことがありません。
⊥値の導入の動機は,「Well-formedな式は例外なく値を表示(denote)する」と単純に考えるために特定の型の特定の値として定義されない⊥値があれば都合がよい,というものです.inf :: Integer; inf = inf + 1とあれば,infの表示(denote)する値は確定できない値⊥です.評価機計算中は表示(denote)する値は確定できないので,そのことを⊥とみなしても不都合はないように思います.
user name と token は基本的に変わらないから毎回渡すのバカらしいのどうしようかな
あんまり議論を追えてないのですが,値自体の定義を https://www.haskell.org/onlinereport/haskell2010/haskellch1.html#dx6-12001
An expression evaluates to a value and has a static type.
に則って考えた場合,Haskellでは let x = 1 2 はxに(1 2を計算した)値を束縛しているのではなく,言うとしたら(call by name的には)1 2という式自体への束縛,または(call by need的には)1 2という計算自体への束縛というのが正しいと思います(なので記事の値への束縛というのが誤った使用法というのはHaskellでは誤りというのに同意です).なお,Haskellではcaseも(Formal Semanticsに則れば)まず対象の式を変数に束縛する変換がなされるので同じ議論を適用できると思います(これもつまり記事と同意見です): https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-610003.17.3

また,一般的なdenotational semanticsは明るくないので分かりませんが,Haskellでは https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-230003.1 に述べられているように⊥とは,計算するとエラーになるまたは計算が止まらないような式に対する表示値のことであり,(一般的な)サンクに対する表示値ではありません.これは当然(仕様上明示されていませんが)Haskellのdenotational semanticsに合わせた定義だと思われるので, @nobsun の用法はHaskellにおいてはあまり一般的ではないと思います.

それからここからは個人的な意見ですが,(取り急ぎと言うことなので続編があるのかもしれませんが)正しい言い方に対する言及がないのが色々疑問を招いているのではないかと感じました.