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

1 名前：デフォルトの名無しさん [2020/02/10(月) 18:17:36 ID:L6eYQqyh.net] 関数型プログラミング言語 Haskell について語るスレです。 Haskell Language(公式サイト) https://www.haskell.org/ 日本Haskellユーザーグループ - Haskell-jp https://haskell.jp/ 前スレ 関数型プログラミング言語Haskell Part32 https://mevius.5ch.net/test/read.cgi/tech/1548720347/ 717 名前：デフォルトの名無しさん mailto:sage [2021/02/02(火) 22:40:39.64 ID:LQ6cge6d.net] >>707 ありがとうございます 私も多分それが原因かなと思い始めてます 一回目のcomb7 !! 1 と二回目では続く添字が! !!2 から !!1 に減ってるのですがHaskellはそんな事は勘案せずに「comb7 !! 1の展開の中にcomb7 !! 1が出てきたからアウト」と言ってるのかなと つまりはこの手の二重漸化式はHaskellはそのままズバリでは読んでくれないんでしょうね 718 名前：デフォルトの名無しさん mailto:sage [2021/02/03(水) 00:23:45.54 ID:QKvl77B6.net] comb7 !! 1 を計算するには length comb7 >= 2 のようなものが必要だぞ でも長さは1かもしれないからアウトという判断は正しい オーバーランするよりよっぽどいい 719 名前：デフォルトの名無しさん mailto:sage [2021/02/03(水) 14:08:13.61 ID:mxabq2OH.net] 求めてないかもですがこんなふうならかけますね。 module Main where import qualified Data.Array.Unboxed as AU main = do print $ comb6 !! 2000 !! 1000 print $ comb7_1 !! 1000 !! 1000 print $ comb7_2 1000 1000 AU.! ( 1000, 1000 ) comb6 = ((1 : (repeat 0)) :) $ zipWith (zipWith (+)) comb6 (map (0 :) comb6) comb7_1 = (repeat 1 :) $ ([ 1 .. ] :) $ (map (\x -> scanl (+) 1 $ tail x) $ tail comb7_1) comb7_2 :: Int -> Int -> AU.Array ( Int, Int ) Integer comb7_2 ly lx = comb7_2_table where comb7_2_table = AU.array ( ( 0, 0 ), ( ly, lx ) ) $ concatMap(\i -> map (f i) [ 0 .. lx ]) [ 0 .. ly ] f 0 x = ( ( 0, x ), 1 ) f y 0 = ( ( y, 0 ), 1 ) f y x = ( ( y, x ) , comb7_2_table AU.! ( (y - 1), x ) + comb7_2_table AU.! ( y, (x - 1) )) 720 名前：デフォルトの名無しさん [2021/02/04(木) 23:30:39.86 ID:OAJDFKMl5] サラリーマンの努力は資産にならない。 https://www.youtube.com/watch?v=3FLjm0Sn-2U ネットで稼げない残念な人の特徴 https://www.youtube.com/watch?v=sV_eyPfB7Wk 【継続＝勝利】続けているうちに、周りは勝手に消えていきます。 https://www.youtube.com/watch?v=oe8rHWFlmVc 【危険】今すぐ逃げろ！ヤバい会社の特徴10選。 https://www.youtube.com/watch?v=N0JBhysIlzc 「ろくに勉強してこなかったバカ」が今日からすべきこと。 https://www.youtube.com/watch?v=3EUDu38W1Mw バカは「必要努力量」を見誤る。 https://www.youtube.com/watch?v=RG6_qkPhCuo 721 名前：デフォルトの名無しさん mailto:sage [2021/02/04(木) 22:24:53.84 ID:w5MK0dgi.net] >>711 ありがとうございます 参考にさせていただきます そうですね もう一つ可読性が欲しい感じがします 元々の問題意識としては私は可読性の高いコードが要求されることが多いのです 例えばFibonacci数列であれば f n = ( f $ n -1 ) + ( f $ n - 2 ) に可読性においてまさるものはないのですが、もちろんこれでは遅くて使い物になりません なので実用性も多少はなりとも求めるならある程度は可読性を犠牲にせざるを得ないのですが、どういう方法がいいのだろうというのがテーマなのです でたまたまFibonacciの場合に f = 0 : 1 : ( zipWith ( + ) f $ tail f ) というのを見つけてコレ中々いいなと、dpで計算してるのに“メモ”をするための不要な手続きを書く必要がなく、Haskellの“call by need”の機能をうまく利用してdp計算させてるところにちょっと唸ったもので でどれくらいコレでいけるのかなと二重数列をやってみたらうまくいかなくて、どうしたもんかなと まぁコレはしょうがないのかもしれませんけど 722 名前：デフォルトの名無しさん mailto:sage [2021/02/05(金) 00:47:44.85 ID:hZ1aOePg.net] >>713 方向性違うかなと思いつつ書いたんですがやっぱり違いましたね。失礼しました。 今更どうでもいいですがちょっと間違えたので訂正だけさせてください。 comb7_1 = (repeat 1 :) $ (map (scanl (+) 1 . tail) $ comb7_1) 723 名前：デフォルトの名無しさん mailto:sage [2021/02/05(金) 01:12:53.20 ID:gzN36RyX.net] 読むという目的 可読性の低いコードを、読むことなく却下するという手段 この目的と手段がすぐ入れかわってしまう現象もまた深刻な問題だ 724 名前：デフォルトの名無しさん mailto:sage [2021/02/05(金) 06:11:52.56 ID:5jF91Ui3.net] 速さを求めてnconcみたいなもんだな 725 名前：デフォルトの名無しさん mailto:sage [2021/02/05(金) 19:44:21.42 ID:DBOaHn9B.net] >>713 その遅くて使い物にならない計算を、 可読性をあまり犠牲にしないで爆速にする方法に、 メモ化(memoization)というテクニックがあります。 (その代わり、当然メモリを使います) メモ化関数 memoize が用意されていれば、 n 番目のフィボナッチ数を求める関数 fib は 次のように書けます。 -- メモ化 fib :: Int -> Integer fib = fix (memoize . fib') -- フィボナッチ計算の本体 fib' :: (Int -> Integer) -> Int -> Integer fib' f 0 = 0 fib' f 1 = 1 fib' f n = f (n-1) + f (n-2) メモ化関数を提供するパッケージは色々あります。 また、メモ化の仕組みの基礎や本質を学びたいのなら、 次のごく短いブログ記事がおすすめです。 https://kseo.github.io/posts/2017-01-14-memoization-in-hasekll.html この記事の最後の fibMemo 関数について、 適当な小さな値に適用させたものを 自分でノートに展開してみるといいです。 726 名前：デフォルトの名無しさん mailto:sage [2021/02/05(金) 20:00:27.08 ID:DBOaHn9B.net] >>717 すいません。 肝腎の memoize 関数の定義を書き忘れました。 memoize :: (Int -> a) -> (Int -> a) memoize f = (map f [0 ..] !!) 先に紹介した記事にこれを導く過程や、 より速くより一般化する方法を学びたい人へ向けた URL紹介が載っています。 727 名前：デフォルトの名無しさん mailto:sage [2021/02/06(土) 09:10:00.64 ID:8eeMDweD.net] >>717 解説ありがとうございます やはりメモ化するしかないんだと思います 問題はそれがプログラマが明示的に自分でやらないといけないのか、コンパイラが自分でやってくれるのかの差なんだと思います Haskellは純粋なcall by nameではなく、call by needのシステムの中にメモ化を備えていてプログラマがメモ化するように書いてなくても勝手にメモ化できるものをメモ化してくれるのがすごいとこだと思うんですけど、例えば>>713の2番目の例で最初見た時「なんでこの定義式でメモ化が効くんだ？」とさっぱりわからなかったのが、実はHaskellのcall by needのシステムをうまく利用してるらしいとわかったのが最初なんです で二重の漸化式だとうまくいかないなと もちろん二重の全炊きでも上手くsuffixの取り方を変えたりすると同様の方法でメモ化できるんですけど、それでは結局「Haskellの機能を利用して明示的にメモ化を指定することなく高速化した」事にはなりません まぁコレはしょうがないんでしょうね どんな計算も常にメモ化して常に同じ評価式を2度扱う事を防いでたらそんなの逆に使い物になりませんからね 728 名前：デフォルトの名無しさん mailto:sage [2021/02/06(土) 20:56:07.58 ID:tGZHMqQF.net] Haskellが「ヤバそう」って偏見だけで敬遠されてるのかなしい… 同級生にも布教したい 729 名前：デフォルトの名無しさん mailto:sage [2021/02/06(土) 21:00:00.51 ID:xuEfQm7n.net] >>720 布教という言葉自体、独善的で押し付けがましく感じられる原因になってると思うよ。 相手がいやがらない程度にhaskellの良さや面白さを伝えてそれでも相手が興味をひかれないなら、それ以上はやめときな。 730 名前：デフォルトの名無しさん mailto:sage [2021/02/06(土) 21:12:54.72 ID:HlAr7yEc.net] >>719 今回の話の本質ではないので、へーそうなんだ、 程度に聞いてくれればいいのですが、 >>713 の2番目の例とは、 f = 0 : 1 : zipWith (+) f (tail f) のことでしょうか。 もしそうなら、これはメモ化ではないですよ。 (このテクニックをなんと呼ぶのかは知りませんが) メモ化というのは簡単にいえば、 関数の同じ引数に対する2度目(以降)の適用に備えて、 その引数に対する1度目の関数の値をその引数とペアにして どこかにメモしておくことです。 ポイントは、2度目以降に備えることではなく、 引数と関数値のペアをメモしておくことです。 それを踏まえて、>>713 の2番目の例において、 では何が関数で、引数と関数値のペアはどこにメモされているか、 考えてみてください。 ただ、言葉の意味は時代と共に変化していくものなので、 今はこれも広義にメモ化と言うことになっているのでしたら、すいません。 私の方が勉強不足です。 731 名前：デフォルトの名無しさん mailto:sage [2021/02/07(日) 08:28:27.99 ID:kgbg5mk/.net] >>717の方がzipwith使ったものより読みやすくて遥かにいいな こっちの書き方の方がもてはやされてほしいわ 732 名前：デフォルトの名無しさん mailto:sage [2021/02/07(日) 10:58:25.84 ID:nblMEePQ.net] 久しぶりにHaskell(Servant)触ってみたけど 相変わらず呪文のようなテンプレートマクロとかコンパイル通すためだけの幽霊型とか表に出てきているのね こういうの後ろに隠した実装がほちい(･ัω･ั) 733 名前：デフォルトの名無しさん [2021/02/07(日) 21:10:43.40 ID:B3cRggdVq] 怒る・叱る文化は、安月給＆長時間労働の証 https://www.youtube.com/watch?v=-FZ-W08t9vM&t=173s 勉強しない社員★仕事のための投資をしない人たち https://www.youtube.com/watch?v=Zg6N7a_h8AE バカが起業したんです★バカが社長になる過程 https://www.youtube.com/watch?v=WT3pvyhpazk 時給10倍差は勉強と努力だけで差がつく★最大100倍差！ https://www.youtube.com/watch?v=AHZjacip9Y4 ドリームキラー★夢の実現を応援する人、阻止する人 https://www.youtube.com/watch?v=ZoVXtIxhqTU 年収１億円は「できっこない」をやり遂げた人★10万人、銀の盾来た！ https://www.youtube.com/watch?v=3t9nQgcIzLw 734 名前：デフォルトの名無しさん mailto:sage [2021/02/07(日) 19:10:10.31 ID:Ae+USThM.net] >>724 試しに作ってみればいいのでは？ そういう気に入らない幽霊型を とりあえず1つだけ後ろに隠してみて、 使いやすいか試してみればいいと思う。 良さそうなら、ここや GitHub で提案するとか。 735 名前：デフォルトの名無しさん mailto:sage [2021/02/07(日) 21:05:48.19 ID:kgbg5mk/.net] Servant辛いから是非お願いしたい 736 名前：デフォルトの名無しさん mailto:sage [2021/02/08(月) 03:22:56.40 ID:lr3qr0Kv.net] >>708 レスが遅くなりましてすいません。 xの定義にx自身を参照していますが、それだけでは 再帰的に定義されているとは言えないということですか。 例えば次の関数 f は再帰的に定義していると皆が言います。 f n = if n == 0 then 1 else n * f (n-1) これと >>706 の x とは何が違うのでしょうか。 737 名前：デフォルトの名無しさん mailto:sage [2021/02/08(月) 07:06:31.27 ID:aZaTrcsy.net] >>728 fix x はxの定義じゃなくてfixの定義では 738 名前：デフォルトの名無しさん mailto:sage [2021/02/08(月) 09:04:48.35 ID:THE6D9/g.net] >>729 fix定義の中でlet節を使って定義されているxの話です。 739 名前：デフォルトの名無しさん mailto:sage [2021/02/08(月) 12:31:08.86 ID:hFpKnaPX.net] >>717 リスト使ったメモ化の理解にはいいんですけど、その例も実は遅いんですよね。!!がO(n)なので。 module Main where import Data.Function import qualified Data.Vector as V main = do let memo = fibMyMemo 50000 print $memo 50000 print $fibMemo 50000 fibMyMemo l = fib where fib = ((V.map f $ V.enumFromN 0 (l + 1)) V.!) f 0 = 0 :: Integer f 1 = 1 f n = fib (n -1) + fib (n -2) memoize f = (map f [0 ..] !!) fib f 0 = 0 fib f 1 = 1 fib f n = f (n - 1) + f (n - 2) fibMemo = fix (memoize . fib) 740 名前：デフォルトの名無しさん mailto:sage [2021/02/08(月) 18:33:31.66 ID:USGkiU7i.net] >>728 マジョリティとマイノリティの違いとか、合法とグレーの違いのようなものだと思えばいいだろ 再帰的な関数と再帰的な型はよく知られている 一方、関数でも型でもないケースは未知のウイルスのようなもので 既存のものと同じだとすぐ決めつけるのは判断が早過ぎる極論 741 名前：デフォルトの名無しさん mailto:sage [2021/02/08(月) 20:09:46.17 ID:xtdfQPSv.net] >>731 そうですね。 なので、実際は Trie 木でメモする MemoTrie が効率良いと思います。 742 名前：デフォルトの名無しさん [2021/02/09(火) 17:58:55.95 ID:czfvLw+x2] アスペルガー症候群と高機能自閉症 「反復運動」と「限定された物事へのこだわり・興味」 ３つの診断基準 �@人とのやり取り、関わりが難しい（社会性の障害） �Aコミュニケーションがとりにくい（コミュニケーションの障害） �B興味・行動の偏り、こだわり（限定的な行動・興味・反復行動） ASD（自閉スペクトラム症、アスペルガー症候群）の症状 細部にとらわれてしまい、最後まで物事を遂行することが出来ない 視線があいにくく、表情が乏しい 切り替えが苦手、決まったパターンと違うと癇癪を起こす、集団での活動・遊びが苦手。 743 名前：デフォルトの名無しさん mailto:sage [2021/02/10(水) 06:55:43.73 ID:w+SbAYAx.net] >>732 すいません、結局のところ、どういう事でしょう？ 744 名前：デフォルトの名無しさん mailto:sage [2021/02/10(水) 10:35:38.44 ID:tXb64EJq.net] 法律や善悪の判断の正しさを疑うのと同じレベルの懐疑的な思考が 数学やデバッグにも必要ということかな 745 名前：デフォルトの名無しさん mailto:sage [2021/02/10(水) 11:17:11.88 ID:tXb64EJq.net] 静的型は最強とかガベコレは最強とかいう考えが 疑われるようになったのは半分ぐらいHaskellが原因だよね 746 名前：デフォルトの名無しさん mailto:sage [2021/02/10(水) 13:30:33.82 ID:em7GM66H.net] >>732←こいつまだいたのか 気持ち悪すぎる 747 名前：デフォルトの名無しさん mailto:sage [2021/02/10(水) 14:18:45.17 ID:tXb64EJq.net] ここは無料だしこんなもんだろ 良いものはみんな課金される 748 名前：デフォルトの名無しさん mailto:sage [2021/02/11(木) 14:43:11.06 ID:/UgD5Hp7.net] 地獄の沙汰も金次第 だが天国への言及はない 749 名前：デフォルトの名無しさん mailto:sage [2021/02/11(木) 16:56:32.70 ID:zBw+qxbZ.net] ねえ、購入厨 ひょっとしてHaskellは、きみが同じ地獄を繰り返す毎に 強力なフリーソフトになっていったんじゃないのかい 750 名前：デフォルトの名無しさん mailto:sage [2021/02/13(土) 21:17:16.21 ID:kqsb0S1y.net] 悪役キャラには著作権等のコンプライアンスを意識させると邪気が抜けてしまう 豆知識 751 名前：デフォルトの名無しさん mailto:sage [2021/02/14(日) 18:40:01.75 .net] なぜ Haskell スレはワードサラダ bot に狙われてしまうのか 752 名前：デフォルトの名無しさん mailto:sage [2021/02/14(日) 20:59:33.34 ID:2j5v2BhK.net] >>743 ネットの差別発言を排除する努力すらやらない人がいるから ワードサラダとやらを排除する努力なんて誰もやらないのは当たり前だぞ こんな簡単なことがなぜ理解できないんだ 753 名前：デフォルトの名無しさん mailto:sage [2021/02/14(日) 21:27:29.30 ID:A1oxlP1a.net] 731はワードサラダなレスうぜぇなぁくらいの意味しかなくワードサラダなレスが存在してしまう理由を実際に疑問に思っているわけではないという簡単なことが何故わからないのか 754 名前：デフォルトの名無しさん mailto:sage [2021/02/14(日) 21:49:22.17 ID:2j5v2BhK.net] 731は、うぜぇなぁ以外何も考えてなかったというのか それは差別意識しかない絶対悪じゃないか 755 名前：デフォルトの名無しさん mailto:sage [2021/02/15(月) 01:08:13.78 ID:Qrz9kKC+.net] もっと危機感を持ったほうがいいよ 母国語の特徴までネチネチいじられたら外国語はこわくて使えないだろう 英語ができないとプログラミングもできない 756 名前：デフォルトの名無しさん mailto:sage [2021/02/15(月) 17:23:26.09 ID:Mv5LolEs.net] なんかこのスレ会話が噛み合わないよな >>744←こいつとか明らかに頭おかしいし こういう人外化け物がうじゃうじゃいるから「特技はコミュニケーション能力です」みたいなゴミ文系が社会で調子に乗り始めるんだろうな 757 名前：デフォルトの名無しさん mailto:sage [2021/02/15(月) 18:24:29.13 ID:Qrz9kKC+.net] コミュ力の悪用を止める方法で一番使えそうなのは制限時間を無くすことだ 5秒で答えさせるような問題でも時間のルールを無視してしまえば そのゴミ文系ってやつの能力を擬似的にコピーできる 758 名前：デフォルトの名無しさん mailto:sage [2021/02/15(月) 19:02:15.47 ID:3zpQr6lX.net] Haskellの話は？ 759 名前：デフォルトの名無しさん mailto:sage [2021/02/15(月) 20:58:35.44 ID:Qrz9kKC+.net] 最小不動点を定義する半順序の定義がない それと「再帰」の定義がない 760 名前：デフォルトの名無しさん mailto:sage [2021/02/16(火) 10:45:42.61 ID:AZNZAZhP.net] >>750 こういう話？ ttps://i.imgur.com/oKvfp6x.png 761 名前：デフォルトの名無しさん mailto:sage [2021/02/16(火) 12:56:19.11 ID:VICwQMLs.net] 質問なんですが, https://levelup.gitconnected.com/functional-dynamic-programming-with-haskell-top-down-and-bottom-up-7ccade222337 の一番上のコード内23-25行目の iMinusOne <- cdRecursiveTD (i-1) stArr iMinusTwo <- cdRecursiveTD (i-2) stArr writeArray stArr i ( (i-1) * ( iMinusOne + iMinusTwo ) ) の部分を添え字使って for j = 1 to 2 xs !! j <- cdRecursiveTD (i-j) stArr writeArray stArr i ( (i-1) * ( sum xs ) ) みたいに書く方法ってありませんかね？ 762 名前：デフォルトの名無しさん mailto:sage [2021/02/16(火) 15:13:16.20 ID:VICwQMLs.net] すみません自己解決しました 一応結果貼っておきます cdRecursiveTD i stArr = do ____v <- readArray stArr i ____when (v == -1) $ do ______xsm <- newSTRef [] ______forM_ [1,2] $ \j -> do ________x <- cdRecursiveTD (i-j) stArr ________modifySTRef xsm (x:) ______xs <- readSTRef xsm ______writeArray stArr i ( (i-1) * ( sum xs ) ) ____readArray stArr i 763 名前：デフォルトの名無しさん mailto:sage [2021/02/16(火) 15:27:24.80 ID:twhDC3NA.net] xs <- mapM (\j -> cdRecursiveTD (i - j) stArr) [1 .. 2] writeArray stArr i ((i - 1) * sum xs) これでよくないですかー？ 764 名前：デフォルトの名無しさん mailto:sage [2021/02/16(火) 15:32:43.34 ID:VICwQMLs.net] >>755 そっちの方が遥に良いですね… ありがとうございます 765 名前：デフォルトの名無しさん mailto:sage [2021/02/17(水) 14:02:08.57 ID:YPZ4jTJ4.net] map f [1,1,1,2]のように重複の多いリストがあったら fの実装を変える勢力とリストの構造を変える勢力の争いをどうやって解決できるか気になる 766 名前：デフォルトの名無しさん mailto:sage [2021/02/17(水) 16:20:43.74 ID:mAFPwKeZ.net] 一回Set型にしてからListに戻す 767 名前：デフォルトの名無しさん mailto:sage [2021/02/17(水) 16:22:11.25 ID:mAFPwKeZ.net] もちろんリストの要素の個数減って良い場合の話だけど 768 名前：デフォルトの名無しさん mailto:sage [2021/02/17(水) 22:40:59.85 ID:0SJ3Yct4.net] >>757 具体的な問題状況(例)が示されなければ、次のような何にでも当てはまる 至極当たり前のつまらない回答しかできないと思うが。 目的、開発リソース(時間や設備、資料、費用など)、 開発者の能力やモチベーション、メンテの容易さなどを、 優先順位を考慮したうえで出来るだけ客観的に評価し決定する。 争うということは、優先順位や評価基準が定まっていないということなので、 まずはそれらを話し合って、あるいは上の立場の者がバシッと決める。 769 名前：デフォルトの名無しさん mailto:sage [2021/02/18(木) 09:29:03.36 ID:8Wc99cSo.net] なんかしょうもない話なんですけどウチの環境で次が通ります test x = case x of _ | odd x -> 1 oyherwise -> 0 main = do print $ test 123 print $ test 456 なんか笑ってしまいました 770 名前：デフォルトの名無しさん mailto:sage [2021/02/18(木) 09:31:00.46 ID:8Wc99cSo.net] あ、イヤ違う 勘違いでした すいません 771 名前：デフォルトの名無しさん mailto:sage [2021/02/18(木) 10:58:11.75 ID:jy6gqPJ4.net] >>760 客観的な目的というのは難しすぎて誰にも分からない 例えば個人的な借金を減らすことと国の借金を減らすことはどちらが客観的目的か そうではなく、目的は主観で決めてOKというなら それは結構面白い答えであって、つまらない答えではない 772 名前：デフォルトの名無しさん mailto:sage [2021/02/18(木) 11:50:05.23 ID:6bd12mxo.net] >>763 言葉が足りず、誤解させたようで申し訳ない。 客観的に行うのは、目的を定めることではなくて、 今やろうとしている事が定めた目的に合っているのか評価すること。 fの実装を変えることが目的に合っているのか、 それともリスト構造を変える方がより合っているのか。 目的というのは様々あるよね。 見聞きした新しい技術をラフに評価するための トイプログラムを作ることが目的だったり、 次のリリースでメモリ使用量を10%削減することだったり。 客観的に評価することを意識しないと、気分や雰囲気に流されて、 メモリ使用量を抑える目標が、いつの間にか処理速度向上にすり替わってたりする。 また、目標は評価する一項目にすぎない。 リリース時期を守る方が優先順位が高い状況もある。 だから、もろもろ含めて客観的に評価する。 逆にそうじゃないと、fとリストどちらを変えるのかなんて、決めようがないと思う。 773 名前：名無しさん mailto:sage [2021/02/18(木) 15:29:22.47 ID:jy6gqPJ4.net] >>764 気分や雰囲気に流されまくるまで想定しておくのが良い作戦だよ 流されないように対策するので想定する必要はないみたいな理屈は危ない 774 名前：デフォルトの名無しさん mailto:sage [2021/02/25(木) 20:48:36.35 ID:zWeVIvWn.net] ある対象がモノイドかどうかを問う質問です。 2つのリストのうち要素の少ない方のリストをそのまま返す、 同じ要素数ならば左側のリストをそのまま返す関数 f :: [a] -> [a] -> [a] があるとします。 ここで、ある型aのリスト全体の集合[a]と、その上の二項演算fとの組([a], f)はモノイドを成すでしょうか。 私は次のように、これはモノイドではないと考えます。 このモノイド性を考えるとき、その単位元の候補として、 もし集合に無限リストを含めないのならば最大要素数のリストを、 無限リストを含めるのであれば無限リストを取ります。 他に考えようがありません。 しかし、どちらにしても単位元の一意性が証明できません。 xs、ys 共に最大要素数のリスト、あるいは無限リストであり、かつ xs /= ys を満たすものは(型aによっては)いくらでもあります。 よって、([a], f) はモノイドではないと考えますが、これは正しいでしょうか。 モノイドの定義に照らし合わせるのではなく、 モノイドならば証明できるであろう定理が証明できないことに因っているのが、 なんとも気持ち悪いのですが・・・ そもそもモノイド性を問うには ([a], f) の定義が曖昧なのでしょうか。 775 名前：デフォルトの名無しさん mailto:sage [2021/02/25(木) 21:30:50.20 ID:hQOL6Vl7.net] モノイドではないに一票 776 名前：デフォルトの名無しさん mailto:sage [2021/02/26(金) 01:35:18.34 ID:7R2bTCy0.net] リストには同じ要素が何個も入ってもいいんだから単位元になり得るのは無限リストだけでしょ ある無限リストを単位元eとするしかなさそう ここでもう1つ無限リストaを用意してf a eしたらa返さずに要素の個数比較する時点で⊥になるからモノイドにならないと思う 777 名前：デフォルトの名無しさん mailto:sage [2021/02/26(金) 02:07:21.86 ID:Drny41hT.net] 型は集合ではない 値は元ではない プログラム上の関数は数学的な意味での関数ではない Haskellは数学ではない 778 名前：デフォルトの名無しさん mailto:sage [2021/02/26(金) 10:03:43.32 ID:W2dsUZYE.net] モノイドでも集合論でも、公理が多過ぎて公理が偽になるなら 公理を減らせばいいじゃん 779 名前：デフォルトの名無しさん mailto:sage [2021/02/26(金) 10:24:37.14 ID:nFSf/y++.net] >>766 まず単位元の定義から、esが[a]の単位元であるなら、任意のxsに対して f es xs == xs f xs es == xs を満たす、というところはいいよね(ゆえにesは、任意のxsより要素数が大きくなければいけない) このことから直接非存在を言う方がこの場合は明快だと思うけど、 「ある要素が単位元ならばそれが一意である」はすぐに言えるから 背理法により単位元が存在しない、でも正しい論証だと思う もしこの演算fに対してモノイドを構成するなら、 (>>768とほぼ同じことを言うが) length es == ∞ なる要素を1つ決めて (全ての有限リスト) ∪ {es} みたいな集合の上でなら言えそう ちゃんと見てないけど結合律もそれっぽく振る舞ってそう [] [ここ壊れてます] 781 名前：デフォルトの名無しさん mailto:sage [2021/02/26(金) 11:29:42.18 ID:s/eVhYHX.net] >>768 >>771 お二方の意見を参考に、もう一度よく考えてみます。 ありがとうございました。 782 名前：デフォルトの名無しさん [2021/03/14(日) 16:53:23.31 ID:XMH1AJguA] アプリの視聴率がわかる　高専卒起業家の独創力 https://www.nikkei.com/article/DGXMZO46695580Y9A620C1000000/ １万人の若者を支援！インターンが日本を変えるかも！？　glowshipの若き創業者・足立卓也氏インタビュー https://sogyotecho.jp/glowship-adachi-interview/ 起業で成功するキャリア形成の仕方とは？ 元プロサッカー選手で起業家の鈴木啓祐氏に聞いた https://sogyotecho.jp/career-development/ 年収3,000万超え!?個人開発で儲かっている海外コミュニティサイト5選！ https://note.com/taishikato/n/n7809a8ed3ffc 自分の視野は「世の中の0.001%」と自覚せよ。ビジネスチャンスを掴む4つの習慣 https://headlines.yahoo.co.jp/hl?a=20200511-00010001-srnijugo-life 人はこうすれば“ハマる”、源流はゲーマー視点の「幸せ」 https://project.nikkeibp.co.jp/behealth/atcl/feature/00005/012100006/ 誰もがオリジナルアプリを作れる時代へ。スタートアップ支援に尽力してきた起業家の原動力とは https://fukuoka.startupnews.jp/post/nappstechnologies/ 2年間で23億円を調達。22歳の社長が語る“スタートアップ起業” https://superceo.jp/tokusyu/manga/100736 783 名前：デフォルトの名無しさん mailto:sage [2021/03/18(木) 15:12:33.23 ID:4AdjqCpZ.net] なんか最近プログラミングの情報ネットで漁ってると数学基礎論の記号らしきもの、横棒の上になんか命題らしき文字列が並んでる奴がめちゃめちゃ出てくるんですけど、完全に乗り遅れました なんかあの記号の意味解説してるいい教科書とかサイトとかありませんか？ 784 名前：デフォルトの名無しさん mailto:sage [2021/03/18(木) 19:10:51.45 ID:lKavXNN6.net] >>774 このような式ですか？ P -> Q P -------------- Q これは、横線の上の論理式(この例の場合は2つの論理式)を前提とすると、 いくつかの推論規則を使えば横線の下の論理式が導ける、 という意味です。 論理学の教科書(的な解説サイト)ならレベルの高低に関わらずどれでも載っていますが、 どれでも式自体の意味についてはこの程度の説明しか無いと思いますよ。 例えば https://abelard.flet.keio.ac.jp/person/takemura/class/2013/3-print-nk.pdf 知りたいことが違っていたらごめんなさい。 785 名前：デフォルトの名無しさん mailto:sage [2021/03/18(木) 19:28:09.20 ID:wWeTTUcP.net] >>775 ありがとうございます ギリギリその図形の意味はわかります 問題はそれとプログラミングの理論がどう関わってるかのとこなんです 多分カリーハワード対応というやつだと思うんですが コレなんか役に立つもんなんですかねぇ？ 786 名前：デフォルトの名無しさん mailto:sage [2021/03/18(木) 20:21:41.37 ID:lKavXNN6.net] >>776 めちゃめちゃ出てくるという事ですので、 そのページのURLをいくつか挙げてくれませんか。 そうすれば、もしかしたら、どう関わっているの把握できて、 説明、あるいは解説ページや書籍の紹介ができるかもしれません。 787 名前：デフォルトの名無しさん mailto:sage [2021/03/18(木) 20:27:07.75 ID:gebFut6o.net] 例えばプログラムをリファクタリングするとき、修正前後での挙動一致を証明できたりするぞ すごい🤗 (依存型のないHaskellでは出来ないからidrisの例だけど) https://keens.github.io/blog/2020/12/22/idrisdeizongatawotsukattashoumeinyuumon/ やりたいことが数学／論理学の勉強とかならcoqのほうがよさげ 788 名前：デフォルトの名無しさん mailto:sage [2021/03/18(木) 23:49:21.36 ID:wWeTTUcP.net] >>777 そうですね 例えばcall by nameとcall by needの違いを調べようと思った時に出てきた https://reader.elsevier.com/reader/sd/pii/S1571066104000222?token=1C1ACCAE69D33669B7D36179C932FC14DD80723B2FD5B3080E3B1EDED9228FC6A9A6AC347668843625B7154C276B7B4C なんかバリバリ出てきます なんのこっちゃと >>166 coqもよく聞きますよね なんかおすすめの教科書とかありますか？ 789 名前：デフォルトの名無しさん mailto:sage [2021/03/19(金) 00:48:13.30 ID:H+hZ3f68.net] カリーハワード対応って要は True => True = True True => False = False False => True = True False => False = True が {単集合->単集合}=単集合 (単集合から単集合への写像は一通りだけ) {単集合->空集合}=空集合 (単集合から空集合への写像は存在しない) {空集合->単集合}=単集合 (空集合から任意の集合への写像は一通り(空写像)) {空集合->空集合}=単集合 (上に同じ) と対応してるって感じと捉えれば良いのかな？ wikipedia読んでもあんまり理解できない 790 名前：デフォルトの名無しさん mailto:sage [2021/03/19(金) 01:58:47.96 ID:MuA020tT.net] 名前呼び出しの意味が分かりません 791 名前：デフォルトの名無しさん mailto:sage [2021/03/19(金) 02:07:37.96 ID:FHn+Zz2I.net] >>779 結局のところ知りたいことは何ですか？ カリーハワード同型対応とプログラムとの関係性ですか？ それとも、カリーハワード同型対応がプログラムの何に役立つのかですか？ それとも、call by name と call by need との違いですか。 それとも、その論文の内容ですか。 (その場合、PDFの5ページ目まで、つまり横線の式が登場する部分まではちゃんと理解できていると思っていいのですか？) それとも、全く別のことですか？ とりあえず知りたいことをピンポイントに小さく一つに絞り、 それを具体的に質問していただけると助かります。 ところで、>>781 は元の質問者さんですか？ 792 名前：768 mailto:sage [2021/03/19(金) 02:15:59.36 ID:MuA020tT.net] >>782 ごめんなさい 僕は別人で割り込みです 793 名前：デフォルトの名無しさん mailto:sage [2021/03/19(金) 03:08:33.55 ID:FHn+Zz2I.net] >>783 遅延評価を実現する評価戦略の中に、必要呼び出し(call by need)と名前呼び出し(call by name)があります。 必要呼び出しはhaskellが採っている戦略で、 一度評価した値を使い回して無駄な呼び出しを防ぐものです。 一方、名前呼び出しは同じ遅延評価でも、評価した値を記憶せず、必要なら何度でも同じ評価処理をするものです。 794 名前：デフォルトの名無しさん mailto:sage [2021/03/19(金) 09:49:18.16 ID:pEtEADGt.net] >>782 そうですね 多分対応自体はわかると思います しかし実際カリーハワード対応で基礎論の世界に持って行くことの効用がよくわかりません 基礎論の世界に持っていって基礎論でよく知られたなんかの定理が使えるとかいうわけでもなさそうですし 最初はcall by needの実装の話、すなわちcall by needでは展開された評価式に同じexpressionが出たとき、その内容を保持して同じ評価を何度も繰り返すのを防ぐらしいですが、もちろんどんな評価でも何でもかんでもメモするわけではないようなので、結局自分で手前でメモ化する必要がでたりします どういう時はcall by needのメモ化が効いてどういう場合は効かないのかよくわからないので現状は“やってみる”しかないし、やってみて上手くいかなくても、なんか上手い書き方すればやってくれるのか、はなからだめなのか、その判別もつきません 795 名前：768 mailto:sage [2021/03/19(金) 11:58:13.56 ID:f7aaFMxN.net] >>784 ありがとうございます このときの「名前」なのですが、識別子のようなものでなく、評価・簡約前の「式の字面」的な意味なのですかね 796 名前：デフォルトの名無しさん mailto:sage [2021/03/19(金) 13:27:51.17 ID:5FIf9nG9.net] 静的型のアイデアは 実行時の世界でやっていたことをコンパイル時の世界に持って行くことだから このアイデアが常識にならない限り動的型の時代は終わらないだろう 797 名前：デフォルトの名無しさん mailto:sage [2021/03/20(土) 08:58:16.14 ID:Hmrg9tvu.net] >>785 プログラムの世界において、ある事柄の性質や、事柄Aと事柄Bの間の関係を調べたいとき、 プログラムの世界の中ではなかなかうまく見えてこない場合がある。 そんなとき、 カリーハワード同型対応によって問題を論理の世界に移すと、 見通しが良くなり、調べやすくなることがある。 そういう意味では役立ちます。 質問者さんが例示した論文がまさにそれです。 一方、何かを作るためにプログラムをする(現場の)人たちにとっては、とくに役立つことは無いと思います。 役立った話を一切聞きません。 質問者さんが、名前呼び出しなどの「性質や関係」を学術的に深く知りたくて調べているのであれば、役立つと思います。 自作のプログラム言語で名前呼び出しを実装したくて調べているのであれば、役立ちませんね。 別の論文に当たった方がいいと思います。 798 名前：デフォルトの名無しさん mailto:sage [2021/03/20(土) 09:35:36.64 ID:IEpiSEKy.net] >>788 そうなんですか 難しいですね haskell の call by need のシステムがどういう具合に実装されてるか調べようとするとほぼ確実にカリーハワード対応が出てきます ボチボチ勉強するしかなさそうですね そもそもcall by needのメモ化の話はhaskell コンパイラの実装の話なのでhaskellの言語自体のレギュレーションにはひとつも載ってない(つまりghcではメモ化が効いて早いけど別のシステムでは遅いという事もありうるし文句言えない)ので効くか効かないか試してみるしかないのが不愉快なんですよねえ 799 名前：デフォルトの名無しさん mailto:sage [2021/03/20(土) 10:00:16.31 ID:1F8CRKpv.net] >>789 それなら graph reduction の実装を調べた方が良いと思います。 800 名前：デフォルトの名無しさん mailto:sage [2021/03/20(土) 10:28:51.32 ID:Hmrg9tvu.net] >>786 すいません、call by name という名称の由来は分からないです。 いままで気にしたこともなかったです。 801 名前：768 mailto:sage [2021/03/20(土) 12:05:15.57 ID:WUxvQvbt.net] >>791 ありがとうございます こちらこそ、たびたびすみません マンガのセリフのことを「ネーム」というらしいので、書いた字面をいうのかなと考えたり name を和英・英英辞典で調べても、結局しっくりきませんでした スレ汚しすみませんでした 802 名前：デフォルトの名無しさん mailto:sage [2021/03/20(土) 14:58:31.86 ID:5ytd1i+3.net] カリーハワード同型対応とかって、機械学習だのアーキテクチャだのネットワークだのアルゴリズムだのといった工学的で応用的で目的意識の定まった何かの役に立つために発明されたものというよりも、理学的で基礎的な単なる重要な事実という雰囲気ある気がする 803 名前：デフォルトの名無しさん mailto:sage [2021/03/21(日) 00:15:43.04 ID:5CEWIvha.net] 貴金属と期限つきポイントの対立煽りにたとえる 使用期限がないのは使用目的がないと言っているようなもの だが期限がない方もメリットがあるのは工学的にも否定できない事実 804 名前：デフォルトの名無しさん mailto:sage [2021/03/22(月) 13:52:42.80 ID:gNDsQT3i.net] >>790 graph refuctionですか 調べてみます しかしともかく、じゃあGHCとかではどう実装されてるのかとかいう資料はかなりの割合で結局カリーハワード対応使ってる文献しか出てこないのがなんとも 当面は“やってみる”でやり過ごすしかなさそうです 805 名前：デフォルトの名無しさん mailto:sage [2021/03/22(月) 15:09:38.98 ID:UycYSiaC.net] call by name(仮)の正式名称がgraph reductionだったら カリーハワード対応(仮)にも正式名称がありそうだけど 訂正することで利益が出せるようにならなければ正式名称の価値も分からん 806 名前：デフォルトの名無しさん mailto:sage [2021/03/22(月) 19:37:04.72 ID:TV/B7jf8.net] >>795 私にはむしろカリーハワード同型対応を陽には使っていない資料しか見当たらないです。 検索キーワードや調べ方が違うのかもしれませんね。 (カリーハワード同型対応がさす意味がお互いに違っている可能性もありますが) この資料はどうでしょうか。 遅延評価をする関数型言語一般の実装方法です。 https://www.microsoft.com/en-us/research/uploads/prod/1987/01/slpj-book-1987.pdf 807 名前：デフォルトの名無しさん mailto:sage [2021/03/22(月) 20:29:59.10 ID:UycYSiaC.net] 例えばmonomorphism restrictionとかいうアレだったら 実行時の挙動ではなく型の話になるんじゃないか 808 名前：デフォルトの名無しさん mailto:sage [2021/03/23(火) 01:01:29.12 ID:HzbeYy7B.net] >>797 ありがとうございます 十章ですね 今度時間を見つけて読んでみます そうですね やっぱり私はGHC関連の資料をあたる事が多くて、やはりそこでは数学よりの資料が多いんでしょうね でもやはりcall by needの実装方法はHaskellのレギュレーションには含まれていない実装依存のところなのでGHC userの私はどうしてもGHC関連の資料から当たりたくなってしまいます GHCでのインプリメントは最新の成果が全て反映されてるとは限らないし、あるいはあまり一般的でない手法を用いているかもしれないし、そこはGHCそのものの資料が一番頼りになります ただ一つの問題はあまりにも数学村(の計算論畑)の言葉で書かれててサッパリわからんとこorz 809 名前：デフォルトの名無しさん mailto:sage [2021/03/23(火) 03:42:25.12 ID:VKgh9sH5.net] >>799 余計なお世話だとは思いますが、どの章もその前までの章の積み重ねなので、 第10章だけを読んで理解するのは難しいと思います。 かなり古い資料を提示したのは、基礎の基礎から学んだ方が良いと思ったからです。 この資料は本当に分かりやすく基礎から説明されているので、 急がば回れの精神で、腰を据えてじっくりと学んでみることをお勧めします。 それこそ数ヶ月かけて。 なんかこう、数学で例えるなら、集合論や解析学の基礎があやふやなまま、 位相空間論の必要な部分だけを都合よく学ぼうとしているような、 そんなきらいがあるように見えます。 810 名前：デフォルトの名無しさん mailto:sage [2021/03/23(火) 05:16:41.87 ID:EMfQwUjX.net] そうですか 残念ながら当方計算論はウルマンホップクラフトや西岡先生の教科書しか読んだことないのでかなり知識が数学サイドに寄ってます 仕事もかなり数学よりで計算論はあくまで趣味なのであまり本腰入れて勉強したことはないのでもしかしたら専門に勉強されてる方から見ればそうかもしれません まぁ本職に悪影響与えない範囲で時間見つけてボチボチ勉強します 811 名前：デフォルトの名無しさん mailto:sage [2021/03/23(火) 07:32:33.02 ID:e41TIwig.net] はっきり言うと評価戦略だとか推論規則だとかカリーハワード同型対応だとかの話は、まともな情報系の学部なら習う基礎基本 大学の講義資料が易しいと思われ 812 名前：デフォルトの名無しさん mailto:sage [2021/03/23(火) 20:57:46.65 ID:zFHE0Fu5.net] 情報系とかいう言い方をする奴は言語から逃げてるね 「数学村の言葉で書かれ」た資料が存在するのも C言語で書かれたOSの話をしないのも 言語から逃げた結果じゃないかな 813 名前：デフォルトの名無しさん mailto:sage [2021/03/24(水) 19:34:45.53 ID:8SYKHDut.net] 何言ってんだコイツ… 814 名前：デフォルトの名無しさん mailto:sage [2021/03/26(金) 00:15:16.59 ID:sjuSPGcx.net] カリー・ハワード同型対応はこのスライドが分かり易かった 結局なんで上手く行くのかって良く分かってないのね https://ocw.kyoto-u.ac.jp/ja/faculty-of-lettersja/002-006/pdf/curryhoward.pdf https://ocw.kyoto-u.ac.jp/ja/faculty-of-lettersja/002-006/pdf/curryhoward2.pdf 815 名前：デフォルトの名無しさん [2021/04/03(土) 17:05:11.32 ID:K4bkjZP4q] ブログvs有料note！今稼ぐならどっちがオススメ？それぞれの特徴を紹介 https://www.youtube.com/watch?v=rFtHbM3dDXs 無名の僕が有料noteで100万円稼ぐまでの全過程【コツ3選を大公開】 https://www.youtube.com/watch?v=kLMXaMpb87A 素人でも稼げる!? 話題の「Brain」の仕組みを解説。 https://www.youtube.com/watch?v=nyelB1Gr_rE Noteを超えるか！？「Brain」の特徴と使い方を解説しました https://www.youtube.com/watch?v=GYyjfHVyAbs 有料noteやBrainで継続的に稼ぐ3つの方法【コンテンツ販売】 https://www.youtube.com/watch?v=d31w1Q5UtA4 Brainがめちゃくちゃ稼ぎやすい件について。 https://www.youtube.com/watch?v=pzRd2BEuIQU noteで47万円稼ぐまでにしたことまとめ https://www.youtube.com/watch?v=TTS6WWseUY0 816 名前：デフォルトの名無しさん mailto:sage [2021/04/05(月) 18:23:16.33 .net] 関数の名前が被るとき、このモジュールのそれだと修飾しますが、 今書いてる翻訳単位のそれだと伝えるには今書いてるモジュール名で修飾するしかないのですか？ それが長大な場合惨めな気持ちになります qualified 今書いているモジュール名 as 短い名前 にするような事はできないのですか？ 817 名前：デフォルトの名無しさん mailto:sage [2021/04/05(月) 21:28:27.96 ID:DOv0Oh8v.net] idrisを使った型駆動設計の話を聞いて、凄いなぁと思いました。 でもこの型駆動設計って、依存型が開発言語のあるのが前提の方法なんでしょうか？

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef