関数型プログラミング言語Haskell Part32

1 ：デフォルトの名無しさん ：2019/01/29(火) 09:05:47.90 ID:gJP/u7IJ.net

関数型プログラミング言語 Haskell について語るスレです。

haskell.org (公式サイト)
https://www.haskell.org/
日本Haskellユーザーグループ
https://haskell.jp/

前スレ
関数型プログラミング言語Haskell Part31
https://mevius.5ch.net/test/read.cgi/tech/1506447188/

952 ：デフォルトの名無しさん：2020/01/19(日) 22:57:51 ID:JsYzYAKP.net

4.7. GHCi commands
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/ghci.html#ghci-commands

Prelude>:?
Prelude>:browse Data.List
scanl :: (b -> a -> b) -> b -> [a] -> [b]
GHC.List.scanl' :: (b -> a -> b) -> b -> [a] -> [b]
scanl1 :: (a -> a -> a) -> [a] -> [a]
scanr :: (a -> b -> b) -> b -> [a] -> [b]
scanr1 :: (a -> a -> a) -> [a] -> [a]

953 ：デフォルトの名無しさん：2020/01/20(月) 00:41:52.39 ID:TXkt06UM.net

Haskellの事を知れば知る程(圏論含む)、数学ってプログラミング言語だなと思う。
コンピュータが登場する遥か以前からあるプログラミング言語。
そうなると数学者はある種のプログラマーと言える。

ただ、数学はコンピュータに計算させるのではなく、自分で計算するから再帰みたいなループ構造は面倒臭い。
そこでループ構造を排除するアルゴリズム(法則や公式)を考え出して来たと考えられる節があって…。
そう考えると、コンピュータの登場で人間の効率的なアルゴリズムを考える能力が退化したかも知れん。
とか、考えてみたり。

954 ：デフォルトの名無しさん：2020/01/20(月) 13:04:34 ID:0GX6odYx.net

ΣとかΠは実質ループだが数学ではループしないで計算出来る

955 ：デフォルトの名無しさん：2020/01/20(月) 18:51:38 ID:9eVX0YAp.net

無理数や積分はほとんど計算してない
C++のtemplate実体化してないメタプログラミングと同じ

956 ：デフォルトの名無しさん：2020/01/20(月) 19:20:02.11 ID:h2nRkU1r.net

カリーハワード対応しらんのか？

957 ：デフォルトの名無しさん：2020/01/20(月) 19:35:03.18 ID:LcZgWv4y.net

普段のプログラミングでカリーハワード対応が出てくる場面ってどういうとき？
型レベルで凝ったことをするとプログラムを証明として書くことがあると思うんだけど、
その証明として書いたプログラムは実行するとどうなるの？
この辺少し勉強したいんだが書いたことも見たこともなくてさっぱり想像つかない

958 ：デフォルトの名無しさん：2020/01/20(月) 20:28:12.96 ID:9eVX0YAp.net

C++のデザインパターンとHaskellの代数的データ型の同型対応

959 ：デフォルトの名無しさん：2020/01/21(火) 08:51:19.90 ID:lxIBo8y+.net

数式の末尾再帰なfib関数を見た時、手続き型言語で書く副作用バリバリのfib関数との共通点が見えた。
(過去どこかに本の中身の画像落としたんだが、まだあるかは知らん)

そこで一つの仮説が浮かんだ。
入出力を伴わない関数であれば、副作用のある関数でも正しく動く関数は数式と相互に変換出来るのでは？
(入出力も含めるなら、相互にHaskellと変換出来る？逆に、バグがあるなら相互変換は無理？)

数学専門じゃないから、証明とか出来ないけども。

960 ：デフォルトの名無しさん：2020/01/21(火) 09:00:45 ID:Hkcle0K4.net

人に伝える努力をして欲しい
ポエムいらない

961 ：デフォルトの名無しさん：2020/01/21(火) 11:28:06 ID:d/fzPC0C.net

何か知りたいことがあるのか？
需要がないところを努力するのは意味不明だし、努力して欲しいと言うのも意味不明

962 ：デフォルトの名無しさん：2020/01/21(火) 11:52:36 ID:m86EWX9f.net

数学だけだなく国語力もないのな
努力といわれてバカにされてることに気付かない

963 ：デフォルトの名無しさん：2020/01/21(火) 13:47:51.38 ID:L/RpGA77.net

ST で検索

964 ：デフォルトの名無しさん：2020/01/21(火) 17:55:02.99 ID:sFJRAv+Q.net

表示的意味論の話かな

965 ：デフォルトの名無しさん：2020/02/04(火) 12:34:05 ID:Np8xXmTj.net

数学、糞苦手な俺
プログラムで表現出来る数学分野ってごく一部だと思ってたけどそうでもないんか？

概念操作のプロセスと計算とじゃ大きな開きがあると思うんだが
それを鬼計算量で埋められるんかね

966 ：デフォルトの名無しさん：2020/02/04(火) 13:19:01 ID:jKHkWlP0.net

オペレーションズリサーチって言った分野は数学必須だろうね
ベイズ統計とか当たり前のように使われているし
カルマンフィルタもそう

確率統計/多変量解析はコンピュータやる人間ならそれなりに必須だと思うし
現実世界に役立っている

ここでよく題材として挙がるのは圏論だけど　これは俺も必要性はあんま感じない

967 ：デフォルトの名無しさん：2020/02/04(火) 18:06:11.81 ID:6o+cJy8H.net

>>959
手続き型言語でのwhileなどの繰り返しの一回に対し、そこで用いられている変数の値の変化を、末尾再帰関数の引数の変化に置き換えれば、きれいな１重whileは、きれいな末尾再帰関数に置き換わると主張しているんだよね。

968 ：デフォルトの名無しさん：2020/02/04(火) 20:02:08 ID:+caUnTFf.net

フリーハンドで描いた線と定規で描いた線を比較するようなもの
実質的な意味は同じ
強いて言うならマナーの良さが違うだけ

969 ：デフォルトの名無しさん：2020/02/04(火) 22:57:24 ID:LyYVEub6.net

静的単一代入形式に変換して、
φ関数の出てくるところを別関数の呼び出しに変換すれば、
副作用のない状態には持ち込めるかな

970 ：デフォルトの名無しさん：2020/02/05(水) 18:14:57 ID:fFjiekZv.net

>>966
> ここでよく題材として挙がるのは圏論だけど　これは俺も必要性はあんま感じない

プログラムを書く立場ならば圏論なんて知る必要は全くないよ

そもそも仮に圏論を知らないと良いプログラムが書けないプログラミング言語があったとしたら
そんなプログラミング言語は使い物にならない

Haskellerなど一部のプログラマの間での昨今の圏論ブームは少なくとも私には単なる一種のファッションの流行にしか見えないし余り意義を認めない
他人の趣味にケチをつける気はないので、やりたければどうぞ御自由に、としか言いようがない

圏論を知る必要があるとすればプログラムを書く人間ではなくて新しいプログラミング言語の設計をする人間（の一部）だ

ただ一つだけ圏論の勉強を擁護しておくと、規模の大きなソフトウェアをメンテナンスしやすい見通しのよい構造を持つように設計する上では
抽象化と一般化という思考能力、ある事柄や概念と他のどの事柄とが対応するのかを適切に理解し判断する能力は非常に重要だ

そして数学において圏論の最も重要な効用は正にそういう一般化や抽象化といった思考法を書き表すための言葉としてだ
数学である分野での成果（例えば幾つかの定理や定義）を全く別の分野へと転用するといった数学の発展させ方が可能になったのは
正に20世紀中盤に圏論という言葉が生まれたからこそのお蔭だ

だからプログラマが圏論そのものを勉強する必要性は乏しいと思うが、圏論を勉強して理解できる能力と大規模のソフトウェアを良い構造で設計できる能力とは
間違いなく共通した部分があり、正の相関があるのは確実だと個人的には考えている

そういう意味では圏論の勉強は大規模ソフトウェアの設計に向く設計者か否かのフィルタリングに使えるかも知れないね

971 ：デフォルトの名無しさん：2020/02/05(水) 18:19:38.12 ID:hXjs1EZI.net

>>970
>そもそも仮に圏論を知らないと良いプログラムが書けないプログラミング言語があったとしたら

CPL(Categorical Programming Language)
まずは Wikipedia を参照汁

972 ：デフォルトの名無しさん：2020/02/05(水) 19:04:41 ID:2rKdW1Ec.net

圏論って知らずに使ってるんやろ
それでええやん

973 ：：2020/02/05(水) 20:36:57.76 ID:uTOW/8lH.net

圏論ってなんですか？

974 ：デフォルトの名無しさん：2020/02/05(水) 21:17:36 ID:2r8PGoiv.net

アジア文化圏

975 ：デフォルトの名無しさん：2020/02/05(水) 21:42:26.50 ID:/Jhw33Vx.net

一つ言えるのは圏論ってなんか語りたくなっちゃうものなんだということ。
プログラムにおいては全く意味はない。
計算機の動きを抽象化する道具としてそんな筋のいいものではない。
数論でも勉強するなら意味はあるだろうが。

976 ：デフォルトの名無しさん：2020/02/05(水) 23:38:47.13 ID:m+XqauaX.net

圏論はどちらかといえばポイントフリー
λとか∀とか∃とかパターンマッチとかで変数を束縛する言語
に違和感があれば圏論を語りたくなる

977 ：デフォルトの名無しさん：2020/02/06(Thu) 01:01:03 ID:OGs/tKtL.net

>>970
大規模ソフトウェアのメンテにおいて、
圏論を知らないとこのように失敗するが、
知っているとこのように成功する、
という具体例を挙げられますか？

または、具体例を挙げて説明している本やブログ、
カンファレンスなどを紹介できますか？

978 ：デフォルトの名無しさん：2020/02/06(Thu) 04:11:03 ID:7nZd7Xb0.net

>>977
圏論は、いわゆる「銀の弾丸」ではない

979 ：デフォルトの名無しさん：2020/02/06(Thu) 07:32:25 ID:OGs/tKtL.net

>>978
それは分かっています。

>>970 が圏論による成功例を知っているのなら教えてほしかったのです。

一件も挙げられず、ただ大規模ソフトウェアには大事だと言っているだけでしたら、
とても残念です。

980 ：デフォルトの名無しさん：2020/02/06(Thu) 08:35:23 ID:7WdfZf7H.net

お前が圏論理解してかつ大規模ソフトウェア開発で失敗したら反証になるじゃん
がんばれ

981 ：デフォルトの名無しさん：2020/02/06(Thu) 11:02:50 ID:OGs/tKtL.net

>>980
この件に関して反証しても、大した意味はないと思います。

具体的な成功例を一つでも知ることの方が遥かに役立つのではないでしょうか。

982 ：デフォルトの名無しさん：2020/02/06(Thu) 11:23:47 ID:gLliKWEs.net

圏論だのモナドだの相変わらずだなあ
もっと楽しい話をしようぜ
コモナドとかProfunctor Opticsとかサ

983 ：デフォルトの名無しさん：2020/02/06(Thu) 11:47:37 ID:sigCaOr9.net

横からだが
個人的に考えてる、と断ってるじゃん
単なる個人の感想
お前はそこに証拠を求めてる
何がしたいの？

984 ：デフォルトの名無しさん：2020/02/06(Thu) 12:12:18 ID:OGs/tKtL.net

>>983
個人的でもそう考える根拠が何かあると思います。
何かの記事でそう語っているのを見たとか、
自分が携わったプロジェクトで実感したとか。

記事なら出典を知りたいですし、
実感したのならもう少し具体的な話を聞きたいです。

と言うのも、今までもここで圏論を語る人はたくさんいましたが、
私の知る限り誰一人として役立った例を具体的に語った人はいませんでした。

>>970 は久しぶりに長文で熱く語っておられるので、
もしや具体例を挙げられるのではと思い聞いてみました。

985 ：デフォルトの名無しさん：2020/02/06(Thu) 13:45:00 ID:sNihMBVC.net

>>977
http://kymst.net/index.php?plugin=attach&refer=MathDocs&openfile=mjk01bt1.pdf

986 ：デフォルトの名無しさん：2020/02/06(Thu) 22:21:29 ID:AbsWoeSu.net

>>971
そりゃ学位論文レベルの言語ならあるさ
そもそもそのCPLとCSL(Categorical Specification Language)とを定義した萩野達也氏のエジンバラ大学に提出した件の学位論文は私も読んだ
そして理論的には大変に興味深い研究だと思ったよ

だが私が前の投稿で書いた「使い物にならない」の定義、つまり肯定形の「使い物になる」はソフトウェア工学的な意味で実用になるという意味だ
つまりは「多数のプログラマによって実用プロジェクトで使える言語」という意味だ、より具体的な基準が必要だと言うのならば
「最低でも100万行のソフトウェア開発をそのプログラミング言語で行える」という意味だ

君が私の主張である「使い物にならない」を否定したければ、100万行とは言わぬまでもせめて10万行のソフトウェアを
複数人で開発するのにCPLだけでやってみてくれ、もちろん必要なCPLのライブラリ類は自分達で開発してね

987 ：デフォルトの名無しさん：2020/02/06(Thu) 22:27:12 ID:sUAmWprm.net

簡単な判別法がある
デバイスドライバーが書けない言語は使い物にならない

988 ：デフォルトの名無しさん：2020/02/06(Thu) 22:27:40 ID:AbsWoeSu.net

>>977
だから能力として近いと言っているだけだよ
圏論という理論を勉強して理解できる能力と、大規模ソフトウェアを良い構造で設計する能力とはね
私がそう考えている理由は、どちらも抽象化や一般化といった思考の能力が重要だからだ

圏論を知らなければ良い設計が出来ないと言っている訳では決してない

970の最後の３行（空行はカウントしない）の意味するところは
勉強すれば圏論を理解できるようになる人は（抽象化や一般化の思考能力が高いので圏論を勉強していなくても）良い設計ができるだろう、という予想だ

989 ：デフォルトの名無しさん：2020/02/06(Thu) 23:07:57 ID:AbsWoeSu.net

>>987
> デバイスドライバーが書けない言語は使い物にならない

それは又一つ別の定義だね
私個人としてはアプリケーションしか書けないプログラミング言語でも「使い物になる」ことを認めるけれども
そういう定義をするソフトウェア技術者の立場はそれとして否定する気はない

990 ：デフォルトの名無しさん：2020/02/06(木) 23:44:41.47 ID:r1DVX1M4.net

人間の社会の役に立つ勢力の定義が存在するのか？
まずは存在を疑うのが無駄な努力をしない秘訣

991 ：デフォルトの名無しさん：2020/02/07(金) 00:02:21 ID:sQmwkFjl.net

圏論が実用言語に向いてないのと同様に、989は5chに向いてない

992 ：デフォルトの名無しさん：2020/02/07(金) 00:15:35 ID:MJwijXd8.net

そんなことないでしょ

993 ：デフォルトの名無しさん：2020/02/07(金) 01:41:24 ID:Fnc0TnWe.net

オオオオチンポ

994 ：デフォルトの名無しさん：2020/02/07(金) 08:09:04 ID:ruz5n033.net

javascriptでデバイスドライバは書けないわな
圏論とやらが必要な分野で使えばいいだけの話

995 ：デフォルトの名無しさん：2020/02/07(金) 12:13:54 ID:PWhN+bN7.net

>>990
未知のウィルスに対する検疫等の防衛が出来るのも人間に役立つ能力
いまの役人の対応観てたらあほばっかりだと思うだろ

996 ：デフォルトの名無しさん：2020/02/07(金) 13:01:46.27 ID:3L88mYwi.net

まだ定義してないのにフライングできる奴は
定義が存在しないパターンを知ってるからそれができる

997 ：デフォルトの名無しさん：2020/02/08(土) 16:14:00 ID:pTX+YoHa.net

HListのインサートとかソートとかのやり方の実装が乗ってるホームページ教えて
作ろうとしても難しくてできないから

998 ：デフォルトの名無しさん：2020/02/10(月) 18:21:44.17 ID:gQeDR86I.net

次スレ
https://mevius.5ch.net/test/read.cgi/tech/1581326256/

999 ：デフォルトの名無しさん：2020/02/10(月) 19:36:01.30 ID:gQeDR86I.net

>>997
HList パッケージのソースをみるしかないかも
https://hackage.haskell.org/package/HList-0.5.0.0/docs/src/Data-HList-HSort.html

1000 ：デフォルトの名無しさん：2020/02/10(月) 20:28:59 ID:Q/biUbUo.net

>>999
あざーす

1001 ：2ch.net投稿限界：Over 1000 Thread

2ch.netからのレス数が1000に到達しました。