haskell-jp / questions #56

Control.Bifunctor ってあったっけと思ったら、 category-extras にあったんですね。今は obsolete なパッケージですが

BiFunctorは完全に私の勘違いでした＞＜

みなさん、議論、ありがとうございました。

訳語はとりあえず「脱高階関数」としました。

cabal new-buildって、UNIX系OSの伝統的なビルド方法である「一般ユーザーでconfigure&コンパイル→スーパーユーザーでmake install」みたいなフローはできるんでしょうか

デフォルトだとインストール先にシンボリックリンクを張るようになっていて、コピーするオプションがこの前追加された事は調査したのですが、これをグローバルインストールに使えるのかどうか判然としないのですね https://github.com/haskell/cabal/issues/5837

--install-method=copyでバイナリのコピーは出来ますが、sudo make install的に使うのは難しいと思います。依存ライブラリは~/.cabal/storeに書き込まれるのとバイナリ以外の例えばdata-filesなどは~/.cabal以下に入ると思うのでnew-buildとnew-installを別ユーザでやるとnew-installは新たにビルドしてインストールする動作になると思います。

本件、 cabal new-freeze で固定した依存関係を元に runhaskell Setup を実行できれば、やりたかった事は概ね実現しそうです。「ghcのバージョンに合ったfreezeファイルをリネームしてからconfigureして下さい」みたいなビルド指示になるのかな

https://kazu-yamamoto.hatenablog.jp/entry/2019/04/11/111238 こちらに関連して気になりました。
実際のところApplicative styleの「おすすめの形」は

f <$> t <*> u <*> v

だと思うのですけど、 <$> (fmap) と <*> の関係が、Applicative則に書いてないので、

pure f <*> t <*> u <*> v

から、どうやって

f <$> t <*> u <*> v

を導けばいいのかわかりません。

と、ここまで書いて「すごいH本に書いてあったような...」と思って読んでみたけど省略されてる... :disappointed: (p. 252より)

http://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Applicative.html#t:Applicative でも、

As a consequence of these laws, the Functor instance for f will satisfy
fmap f x = pure f <*> x

とまでしか書いてなかったか... :disappointed:

すごい Haskell の方は

中でも一番重要なのは pure f <*> x = fmap f x です。

と書いてあるのでこれを使えばいいのでないですか？

ああ、だからそれがどうやってほかのApplicative則やFunctor則から導かれるのかがわからないのです...。

他の則から導かれるようなものではないような？
他の則から導かれるならそれは則に含めなくてよいと思うのですが。
（何か igrep さんの主張を読みまちがってますかね

他の則から導かれるようなものではないような？

でも、さっき言及したApplicativeのドキュメントでは、

As a consequence of these laws, the Functor instance for f will satisfy
fmap f x = pure f <*> x

とあるのでさもほかの則から導かれるかのように書かれてるんですよね...

と、またここまで書いて気づいたんですが、ひょっとして :point_down: の箇所もApplicative則に含まれるのか。
だとすれば納得。

A minimal complete definition must include implementations of pure and of either <*> or liftA2. If it defines both, then they must behave the same as their default definitions:
(<*>) = liftA2 id
liftA2 f x y = f <$> x <*> y

ああー、すみません、すごいH本の「これ以外のアプリカティブ則の一覧はこちらです」の「これ以外の」を見逃してました... :bow: :cold_sweat:

ついでにですが，

[(+ 1), (+ 2)] <*> [1, 2]

みたいなのは， f <$> x <*> y の形ではないと思いますね． f <$> x <*> y の形は実用上は良くでてくる形ですが， applicative style 一般の形がそうとは限らないと思います．一応

id <$> [(+ 1), (+ 2)] <*> [1, 2]

とも書けますが

Functor がまずあって、しかる後に Applicative があります。

なので、まず <$> があって、その次に pure と <*> が出てきます。

そのときに、 <$> は実は、 f <$> x = pure f <*> x に分解できるという話です。

定義であって、Applicative 法則に含めるような規則じゃないと思います。

(<$>)は関数型(function type)の引数に適用できるので， a -> (b -> c)のような型をもつ関数にも適用できます．
たとえば， someFunc :: a -> (b -> c)という関数に (<$>)を適用した値 (<$>) someFuncの型は f (b -> c)という関数っぽい型になります．
そうすると，この関数のような値を f bという型の値に適用できるように f b -> f cという関数に変換して使いたくなるのが人情でしょう．
つまり， f (a -> b) -> (f a -> f b)という変換関数が欲しくなりますよね．それが， (<*>)というわけです．
もともとの動機を考えれば， (someFunc <$> (x :: f a)) <*> (y :: f b) ≡ (pure someFunc <*> (x :: f a)) <*> (y :: f b)を満たして欲しいですよね．

釈迦に説法ですが， $ は右結合ですが， <$> や <*> は左結合です．これでハマった方を知っています．:sweat_smile:

定義であって、Applicative 法則に含めるような規則じゃないと思います。

でも、満たさないように <*> を実装することはできる（はず）なので、すごいH本やApplicativeのドキュメントに書いてあるとおり、則の一部であると解釈していいと思います。
もちろんデフォルトの実装にしたがっていれば破られることはありませんが...

pure f <*> x = f <$> x

は法則であって，定義ではないのでは？．

ApplicativeがFunctorであるために満すべき性質(法則)かな．

<$>がメソッドから、単なる演算子に格下げされたら、法則が定義になる？

あ、 <$> は単なる演算子。 fmap との関係を調べないといけないのか。

4つの Applicative 法則が満たされれば、 fmap f x = pure f <*> x は自動的に満たされるらしい。

逆も言えますか？

直感的には、言えないような。。。

関手の単位元：

pure id <*> x = x

関手の合成法則：

pure f <*> (pure g <*> x)
= pure (.) <*> pure f <*> pure g <*> x
= pure ((.) f g) <*> x
= pure (f . g) <*> x

pure f <*> x は関手法則を満たすので、 fmap ですな。

4つのApplicative法則が満たされれば、自動的に f <$> x = pure f <*> x は満たされるので、これ自体は補題？ぐらいで、法則じゃなさそう。

私も気になったのでRedditでも質問してみました https://www.reddit.com/r/haskell/comments/bcaead/how_to_derive_pure_f_x_fmap_f_x/

補足ですが，

fmap' f x = pure f <*> x

での fmap' は， kazu さんがおっしゃるように Applicative law から Functor law を満たすことが示せます．

ただ，もし一つの型に対し， functor law を満たす fmap が複数あれば（ここでの違いとは実装の違いではなく，振る舞いの違いであることに注意してください）， fmap = fmap' と一概には言えません．しかし，実は fmap の多相性からこれらは一意であることが知られています: https://wiki.haskell.org/Typeclassopedia#Laws

なので， Functor の一意性と Applicative law から f <$> x = pure f <*> x が導けます．これは定理ですね．なお，これは Applicative law が Functor law を含んでいるからですが，もう少し明確に分離できる別の Applicative law set も知られていて，

(*) :: f a -> f b -> f (a, b)
x * y = (,) <$> x <*> y

unit :: f ()
unit = pure ()

に対して，
• naturality : fmap (f *** g) (u * v) = fmap f u * fmap g v
• left identity: fmap snd (unit * v) = v
• right identity: fmap fst (v * unit) = v
• associativity: fmap (\(x, (y, z)) -> (x, y, z)) (u * (v * w)) = fmap (\((x, y), z) -> (x, y, z)) ((u * v) * w)
で，これは元の Applicative law が fmap から独立しているのと異なり， fmap を元に law が作られています．

@kazu 記事中で気づいたのですが Monad の「交換の法則ですが、左辺は、」のところは「結合の法則」ですね。

Functor則，Pointed則と(<*>) . pure = fmap という法則？から，簡単にIdentity則とHomomorphism則は導くことができますね．

@1to100pen う。ありがとうございます。訂正しました。

@kazu「do は入れ子で書かずに、平坦な形でスッキリ書いてね」のところですが、右辺の do { x <- mx; y <- f x; g x } は左辺（と同じ意味の）の do { y <- h mx; g x }; h mx = do { x <- mx; f x } に書き換えられるように「do の中の一部分を関数に切り出しても大丈夫だよ」という解釈の方がプログラミングでは役に立つ気がします。

@1to100pen 昔、だれかが「どこで切ってもMonad」と言っていたのを思い出します。。。

@米栂 has joined the channel

@AnnPin has joined the channel

Well typedってどう訳すのが適切でしょうか。型安全？

TaPLだと「正しく型付けされている」と訳されています。

訳さない派ですが、「型がツイてる」というのはいかが

data Term = TermTrue
          | TermFalse
          | TermIf Term Term Term
          | TermZero
          | TermSucc Term
          | TermPred Term
          | TermIsZero Term
          deriving (Show) 

Term型を宣言したいのに、その中でもTermが使われていて、これどうゆうこと….

なるほど！あえて訳さないほうがいいかもね。ありがとうー

これは再帰的なデータ構造と言うもので、文字通り Term の中に Term を入れることができるようになっています。