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

**デフォルトの名無しさん** · 2020/02/10(月) 18:17:36.49

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

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

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

**デフォルトの名無しさん** · 2021/02/02(火) 22:40:39.64

>>698
ありがとうございます
私も多分それが原因かなと思い始めてます
一回目のcomb7 !! 1 と二回目では続く添字が! !!2 から !!1 に減ってるのですがHaskellはそんな事は勘案せずに「comb7 !! 1の展開の中にcomb7 !! 1が出てきたからアウト」と言ってるのかなと
つまりはこの手の二重漸化式はHaskellはそのままズバリでは読んでくれないんでしょうね

**デフォルトの名無しさん** · 2021/02/03(水) 00:23:45.54

comb7 !! 1 を計算するには length comb7 >= 2 のようなものが必要だぞ
でも長さは1かもしれないからアウトという判断は正しい
オーバーランするよりよっぽどいい

**デフォルトの名無しさん** · 2021/02/03(水) 14:08:13.61

求めてないかもですがこんなふうならかけますね。
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) ))

**デフォルトの名無しさん** · 2021/02/04(木) 22:24:53.84

>>702
ありがとうございます
参考にさせていただきます
そうですね
もう一つ可読性が欲しい感じがします
元々の問題意識としては私は可読性の高いコードが要求されることが多いのです
例えばFibonacci数列であれば

f n = ( f $ n -1 ) + ( f $ n - 2 )

に可読性においてまさるものはないのですが、もちろんこれでは遅くて使い物になりません
なので実用性も多少はなりとも求めるならある程度は可読性を犠牲にせざるを得ないのですが、どういう方法がいいのだろうというのがテーマなのです
でたまたまFibonacciの場合に
f = 0 : 1 : ( zipWith ( + ) f $ tail f )
というのを見つけてコレ中々いいなと、dpで計算してるのに“メモ”をするための不要な手続きを書く必要がなく、Haskellの“call by need”の機能をうまく利用してdp計算させてるところにちょっと唸ったもので
でどれくらいコレでいけるのかなと二重数列をやってみたらうまくいかなくて、どうしたもんかなと
まぁコレはしょうがないのかもしれませんけど

**デフォルトの名無しさん** · 2021/02/05(金) 00:47:44.85

>>703
方向性違うかなと思いつつ書いたんですがやっぱり違いましたね。失礼しました。
今更どうでもいいですがちょっと間違えたので訂正だけさせてください。
comb7_1 = (repeat 1 :) $ (map (scanl (+) 1 . tail) $ comb7_1)

**デフォルトの名無しさん** · 2021/02/05(金) 01:12:53.20

読むという目的
可読性の低いコードを、読むことなく却下するという手段

この目的と手段がすぐ入れかわってしまう現象もまた深刻な問題だ

**デフォルトの名無しさん** · 2021/02/05(金) 06:11:52.56

速さを求めてnconcみたいなもんだな

**デフォルトの名無しさん** · 2021/02/05(金) 19:44:21.42

>>703
その遅くて使い物にならない計算を、
可読性をあまり犠牲にしないで爆速にする方法に、
メモ化(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 関数について、
適当な小さな値に適用させたものを
自分でノートに展開してみるといいです。

**デフォルトの名無しさん** · 2021/02/05(金) 20:00:27.08

>>707
すいません。
肝腎の memoize 関数の定義を書き忘れました。

memoize :: (Int -> a) -> (Int -> a)
memoize f = (map f [0 ..] !!)

先に紹介した記事にこれを導く過程や、
より速くより一般化する方法を学びたい人へ向けた
URL紹介が載っています。

**デフォルトの名無しさん** · 2021/02/06(土) 09:10:00.64

>>707
解説ありがとうございます
やはりメモ化するしかないんだと思います
問題はそれがプログラマが明示的に自分でやらないといけないのか、コンパイラが自分でやってくれるのかの差なんだと思います
Haskellは純粋なcall by nameではなく、call by needのシステムの中にメモ化を備えていてプログラマがメモ化するように書いてなくても勝手にメモ化できるものをメモ化してくれるのがすごいとこだと思うんですけど、例えば>>703の2番目の例で最初見た時「なんでこの定義式でメモ化が効くんだ？」とさっぱりわからなかったのが、実はHaskellのcall by needのシステムをうまく利用してるらしいとわかったのが最初なんです
で二重の漸化式だとうまくいかないなと
もちろん二重の全炊きでも上手くsuffixの取り方を変えたりすると同様の方法でメモ化できるんですけど、それでは結局「Haskellの機能を利用して明示的にメモ化を指定することなく高速化した」事にはなりません
まぁコレはしょうがないんでしょうね
どんな計算も常にメモ化して常に同じ評価式を2度扱う事を防いでたらそんなの逆に使い物になりませんからね

**デフォルトの名無しさん** · 2021/02/06(土) 20:56:07.58

Haskellが「ヤバそう」って偏見だけで敬遠されてるのかなしい…
同級生にも布教したい

**デフォルトの名無しさん** · 2021/02/06(土) 21:00:00.51

>>710
布教という言葉自体、独善的で押し付けがましく感じられる原因になってると思うよ。
相手がいやがらない程度にhaskellの良さや面白さを伝えてそれでも相手が興味をひかれないなら、それ以上はやめときな。

**デフォルトの名無しさん** · 2021/02/06(土) 21:12:54.72

>>709
今回の話の本質ではないので、へーそうなんだ、
程度に聞いてくれればいいのですが、

>>703 の2番目の例とは、

f = 0 : 1 : zipWith (+) f (tail f)

のことでしょうか。
もしそうなら、これはメモ化ではないですよ。
(このテクニックをなんと呼ぶのかは知りませんが)

メモ化というのは簡単にいえば、
関数の同じ引数に対する2度目(以降)の適用に備えて、
その引数に対する1度目の関数の値をその引数とペアにして
どこかにメモしておくことです。

ポイントは、2度目以降に備えることではなく、
引数と関数値のペアをメモしておくことです。

それを踏まえて、>>703 の2番目の例において、
では何が関数で、引数と関数値のペアはどこにメモされているか、
考えてみてください。

ただ、言葉の意味は時代と共に変化していくものなので、
今はこれも広義にメモ化と言うことになっているのでしたら、すいません。
私の方が勉強不足です。

**デフォルトの名無しさん** · 2021/02/07(日) 08:28:27.99

>>707の方がzipwith使ったものより読みやすくて遥かにいいな
こっちの書き方の方がもてはやされてほしいわ

**デフォルトの名無しさん** · 2021/02/07(日) 10:58:25.84

久しぶりにHaskell(Servant)触ってみたけど
相変わらず呪文のようなテンプレートマクロとかコンパイル通すためだけの幽霊型とか表に出てきているのね
こういうの後ろに隠した実装がほちい(･ัω･ั)

**デフォルトの名無しさん** · 2021/02/07(日) 19:10:10.31

>>714
試しに作ってみればいいのでは？

そういう気に入らない幽霊型を
とりあえず1つだけ後ろに隠してみて、
使いやすいか試してみればいいと思う。

良さそうなら、ここや GitHub で提案するとか。

**デフォルトの名無しさん** · 2021/02/07(日) 21:05:48.19

Servant辛いから是非お願いしたい

**デフォルトの名無しさん** · 2021/02/08(月) 03:22:56.40

>>699
レスが遅くなりましてすいません。
xの定義にx自身を参照していますが、それだけでは
再帰的に定義されているとは言えないということですか。

例えば次の関数 f は再帰的に定義していると皆が言います。
f n = if n == 0 then 1 else n * f (n-1)

これと >>697 の x とは何が違うのでしょうか。

**デフォルトの名無しさん** · 2021/02/08(月) 07:06:31.27

>>717
fix x はxの定義じゃなくてfixの定義では

**デフォルトの名無しさん** · 2021/02/08(月) 09:04:48.35

>>718
fix定義の中でlet節を使って定義されているxの話です。

**デフォルトの名無しさん** · 2021/02/08(月) 12:31:08.86

>>707
リスト使ったメモ化の理解にはいいんですけど、その例も実は遅いんですよね。!!が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)

**デフォルトの名無しさん** · 2021/02/08(月) 18:33:31.66

>>717
マジョリティとマイノリティの違いとか、合法とグレーの違いのようなものだと思えばいいだろ

再帰的な関数と再帰的な型はよく知られている
一方、関数でも型でもないケースは未知のウイルスのようなもので
既存のものと同じだとすぐ決めつけるのは判断が早過ぎる極論

**デフォルトの名無しさん** · 2021/02/08(月) 20:09:46.17

>>720
そうですね。

なので、実際は Trie 木でメモする MemoTrie が効率良いと思います。

**デフォルトの名無しさん** · 2021/02/10(水) 06:55:43.73

>>721
すいません、結局のところ、どういう事でしょう？

**デフォルトの名無しさん** · 2021/02/10(水) 10:35:38.44

法律や善悪の判断の正しさを疑うのと同じレベルの懐疑的な思考が
数学やデバッグにも必要ということかな

**デフォルトの名無しさん** · 2021/02/10(水) 11:17:11.88

静的型は最強とかガベコレは最強とかいう考えが
疑われるようになったのは半分ぐらいHaskellが原因だよね

**デフォルトの名無しさん** · 2021/02/10(水) 13:30:33.82

>>721←こいつまだいたのか
気持ち悪すぎる

**デフォルトの名無しさん** · 2021/02/10(水) 14:18:45.17

ここは無料だしこんなもんだろ
良いものはみんな課金される

**デフォルトの名無しさん** · 2021/02/11(木) 14:43:11.06

地獄の沙汰も金次第
だが天国への言及はない

**デフォルトの名無しさん** · 2021/02/11(木) 16:56:32.70

ねえ、購入厨
ひょっとしてHaskellは、きみが同じ地獄を繰り返す毎に
強力なフリーソフトになっていったんじゃないのかい

**デフォルトの名無しさん** · 2021/02/13(土) 21:17:16.21

悪役キャラには著作権等のコンプライアンスを意識させると邪気が抜けてしまう
豆知識

**デフォルトの名無しさん** · 2021/02/14(日) 18:40:01.75

なぜ Haskell スレはワードサラダ bot に狙われてしまうのか

**デフォルトの名無しさん** · 2021/02/14(日) 20:59:33.34

>>731
ネットの差別発言を排除する努力すらやらない人がいるから
ワードサラダとやらを排除する努力なんて誰もやらないのは当たり前だぞ
こんな簡単なことがなぜ理解できないんだ

**デフォルトの名無しさん** · 2021/02/14(日) 21:27:29.30

731はワードサラダなレスうぜぇなぁくらいの意味しかなくワードサラダなレスが存在してしまう理由を実際に疑問に思っているわけではないという簡単なことが何故わからないのか

**デフォルトの名無しさん** · 2021/02/14(日) 21:49:22.17

731は、うぜぇなぁ以外何も考えてなかったというのか
それは差別意識しかない絶対悪じゃないか

**デフォルトの名無しさん** · 2021/02/15(月) 01:08:13.78

もっと危機感を持ったほうがいいよ
母国語の特徴までネチネチいじられたら外国語はこわくて使えないだろう
英語ができないとプログラミングもできない

**デフォルトの名無しさん** · 2021/02/15(月) 17:23:26.09

なんかこのスレ会話が噛み合わないよな
>>732←こいつとか明らかに頭おかしいし
こういう人外化け物がうじゃうじゃいるから「特技はコミュニケーション能力です」みたいなゴミ文系が社会で調子に乗り始めるんだろうな

**デフォルトの名無しさん** · 2021/02/15(月) 18:24:29.13

コミュ力の悪用を止める方法で一番使えそうなのは制限時間を無くすことだ
5秒で答えさせるような問題でも時間のルールを無視してしまえば
そのゴミ文系ってやつの能力を擬似的にコピーできる

**デフォルトの名無しさん** · 2021/02/15(月) 19:02:15.47

Haskellの話は？

**デフォルトの名無しさん** · 2021/02/15(月) 20:58:35.44

最小不動点を定義する半順序の定義がない
それと「再帰」の定義がない

**デフォルトの名無しさん** · 2021/02/16(火) 10:45:42.61

>>738
こういう話？
ttps://i.imgur.com/oKvfp6x.png

**デフォルトの名無しさん** · 2021/02/16(火) 12:56:19.11

質問なんですが,
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 ) )
みたいに書く方法ってありませんかね？

**デフォルトの名無しさん** · 2021/02/16(火) 15:13:16.20

すみません自己解決しました
一応結果貼っておきます
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

**デフォルトの名無しさん** · 2021/02/16(火) 15:27:24.80

xs <- mapM (\j -> cdRecursiveTD (i - j) stArr) [1 .. 2]
writeArray stArr i ((i - 1) * sum xs)
これでよくないですかー？

**デフォルトの名無しさん** · 2021/02/16(火) 15:32:43.34

>>743
そっちの方が遥に良いですね…
ありがとうございます

**デフォルトの名無しさん** · 2021/02/17(水) 14:02:08.57

map f [1,1,1,2]のように重複の多いリストがあったら
fの実装を変える勢力とリストの構造を変える勢力の争いをどうやって解決できるか気になる

**デフォルトの名無しさん** · 2021/02/17(水) 16:20:43.74

一回Set型にしてからListに戻す

**デフォルトの名無しさん** · 2021/02/17(水) 16:22:11.25

もちろんリストの要素の個数減って良い場合の話だけど

**デフォルトの名無しさん** · 2021/02/17(水) 22:40:59.85

>>745
具体的な問題状況(例)が示されなければ、次のような何にでも当てはまる
至極当たり前のつまらない回答しかできないと思うが。

目的、開発リソース(時間や設備、資料、費用など)、
開発者の能力やモチベーション、メンテの容易さなどを、
優先順位を考慮したうえで出来るだけ客観的に評価し決定する。

争うということは、優先順位や評価基準が定まっていないということなので、
まずはそれらを話し合って、あるいは上の立場の者がバシッと決める。

**デフォルトの名無しさん** · 2021/02/18(木) 09:29:03.36

なんかしょうもない話なんですけどウチの環境で次が通ります

test x = case x of
_ | odd x -> 1
oyherwise -> 0

main = do
print $ test 123
print $ test 456

なんか笑ってしまいました

**デフォルトの名無しさん** · 2021/02/18(木) 09:31:00.46

あ、イヤ違う
勘違いでした
すいません

**デフォルトの名無しさん** · 2021/02/18(木) 10:58:11.75

>>748
客観的な目的というのは難しすぎて誰にも分からない
例えば個人的な借金を減らすことと国の借金を減らすことはどちらが客観的目的か

そうではなく、目的は主観で決めてOKというなら
それは結構面白い答えであって、つまらない答えではない

**デフォルトの名無しさん** · 2021/02/18(木) 11:50:05.23

>>751
言葉が足りず、誤解させたようで申し訳ない。

客観的に行うのは、目的を定めることではなくて、
今やろうとしている事が定めた目的に合っているのか評価すること。

fの実装を変えることが目的に合っているのか、
それともリスト構造を変える方がより合っているのか。

目的というのは様々あるよね。
見聞きした新しい技術をラフに評価するための
トイプログラムを作ることが目的だったり、
次のリリースでメモリ使用量を10%削減することだったり。

客観的に評価することを意識しないと、気分や雰囲気に流されて、
メモリ使用量を抑える目標が、いつの間にか処理速度向上にすり替わってたりする。

また、目標は評価する一項目にすぎない。
リリース時期を守る方が優先順位が高い状況もある。
だから、もろもろ含めて客観的に評価する。

逆にそうじゃないと、fとリストどちらを変えるのかなんて、決めようがないと思う。

**デフォルトの名無しさん** · 2021/02/18(木) 15:29:22.47

>>752
気分や雰囲気に流されまくるまで想定しておくのが良い作戦だよ
流されないように対策するので想定する必要はないみたいな理屈は危ない

**デフォルトの名無しさん** · 2021/02/25(木) 20:48:36.35

ある対象がモノイドかどうかを問う質問です。

2つのリストのうち要素の少ない方のリストをそのまま返す、
同じ要素数ならば左側のリストをそのまま返す関数 f :: [a] -> [a] -> [a] があるとします。
ここで、ある型aのリスト全体の集合[a]と、その上の二項演算fとの組([a], f)はモノイドを成すでしょうか。

私は次のように、これはモノイドではないと考えます。

このモノイド性を考えるとき、その単位元の候補として、
もし集合に無限リストを含めないのならば最大要素数のリストを、
無限リストを含めるのであれば無限リストを取ります。
他に考えようがありません。

しかし、どちらにしても単位元の一意性が証明できません。
xs、ys 共に最大要素数のリスト、あるいは無限リストであり、かつ xs /= ys を満たすものは(型aによっては)いくらでもあります。

よって、([a], f) はモノイドではないと考えますが、これは正しいでしょうか。

モノイドの定義に照らし合わせるのではなく、
モノイドならば証明できるであろう定理が証明できないことに因っているのが、
なんとも気持ち悪いのですが・・・

そもそもモノイド性を問うには ([a], f) の定義が曖昧なのでしょうか。

**デフォルトの名無しさん** · 2021/02/25(木) 21:30:50.20

モノイドではないに一票

**デフォルトの名無しさん** · 2021/02/26(金) 01:35:18.34

リストには同じ要素が何個も入ってもいいんだから単位元になり得るのは無限リストだけでしょ
ある無限リストを単位元eとするしかなさそう
ここでもう1つ無限リストaを用意してf a eしたらa返さずに要素の個数比較する時点で⊥になるからモノイドにならないと思う

**デフォルトの名無しさん** · 2021/02/26(金) 02:07:21.86

型は集合ではない
値は元ではない
プログラム上の関数は数学的な意味での関数ではない

Haskellは数学ではない

**デフォルトの名無しさん** · 2021/02/26(金) 10:03:43.32

モノイドでも集合論でも、公理が多過ぎて公理が偽になるなら
公理を減らせばいいじゃん

**デフォルトの名無しさん** · 2021/02/26(金) 10:24:37.14

>>754
まず単位元の定義から、esが[a]の単位元であるなら、任意のxsに対して
f es xs == xs
f xs es == xs
を満たす、というところはいいよね(ゆえにesは、任意のxsより要素数が大きくなければいけない)

このことから直接非存在を言う方がこの場合は明快だと思うけど、
「ある要素が単位元ならばそれが一意である」はすぐに言えるから
背理法により単位元が存在しない、でも正しい論証だと思う

もしこの演算fに対してモノイドを構成するなら、
(>>756とほぼ同じことを言うが) length es == ∞ なる要素を1つ決めて
(全ての有限リスト) ∪ {es}
みたいな集合の上でなら言えそう
ちゃんと見てないけど結合律もそれっぽく振る舞ってそう

**デフォルトの名無しさん** · 2021/02/26(金) 11:29:42.18

>>756
>>759
お二方の意見を参考に、もう一度よく考えてみます。
ありがとうございました。

**デフォルトの名無しさん** · 2021/03/18(木) 15:12:33.23

なんか最近プログラミングの情報ネットで漁ってると数学基礎論の記号らしきもの、横棒の上になんか命題らしき文字列が並んでる奴がめちゃめちゃ出てくるんですけど、完全に乗り遅れました
なんかあの記号の意味解説してるいい教科書とかサイトとかありませんか？

**デフォルトの名無しさん** · 2021/03/18(木) 19:10:51.45

>>761
このような式ですか？

P -> Q P
--------------
Q

これは、横線の上の論理式(この例の場合は2つの論理式)を前提とすると、
いくつかの推論規則を使えば横線の下の論理式が導ける、
という意味です。

論理学の教科書(的な解説サイト)ならレベルの高低に関わらずどれでも載っていますが、
どれでも式自体の意味についてはこの程度の説明しか無いと思いますよ。
例えば
https://abelard.flet.keio.ac.jp/person/takemura/class/2013/3-print-nk.pdf

知りたいことが違っていたらごめんなさい。

**デフォルトの名無しさん** · 2021/03/18(木) 19:28:09.20

>>762
ありがとうございます
ギリギリその図形の意味はわかります
問題はそれとプログラミングの理論がどう関わってるかのとこなんです
多分カリーハワード対応というやつだと思うんですが
コレなんか役に立つもんなんですかねぇ？

**デフォルトの名無しさん** · 2021/03/18(木) 20:21:41.37

>>763
めちゃめちゃ出てくるという事ですので、
そのページのURLをいくつか挙げてくれませんか。

そうすれば、もしかしたら、どう関わっているの把握できて、
説明、あるいは解説ページや書籍の紹介ができるかもしれません。

**デフォルトの名無しさん** · 2021/03/18(木) 20:27:07.75

例えばプログラムをリファクタリングするとき、修正前後での挙動一致を証明できたりするぞ
すごい🤗
(依存型のないHaskellでは出来ないからidrisの例だけど)

https://keens.github.io/blog/2020/12/22/idrisdeizongatawotsukattashoumeinyuumon/

やりたいことが数学／論理学の勉強とかならcoqのほうがよさげ

**デフォルトの名無しさん** · 2021/03/18(木) 23:49:21.36

>>764
そうですね
例えばcall by nameとcall by needの違いを調べようと思った時に出てきた

https://reader.elsevier.com/reader/sd/pii/S1571066104000222?token=1C1ACCAE69D33669B7D36179C932FC14DD80723B2FD5B3080E3B1EDED9228FC6A9A6AC347668843625B7154C276B7B4C

なんかバリバリ出てきます
なんのこっちゃと

>>165
coqもよく聞きますよね
なんかおすすめの教科書とかありますか？

**デフォルトの名無しさん** · 2021/03/19(金) 00:48:13.30

カリーハワード対応って要は
True => True = True
True => False = False
False => True = True
False => False = True
が
{単集合->単集合}=単集合 (単集合から単集合への写像は一通りだけ)
{単集合->空集合}=空集合 (単集合から空集合への写像は存在しない)
{空集合->単集合}=単集合 (空集合から任意の集合への写像は一通り(空写像))
{空集合->空集合}=単集合 (上に同じ)
と対応してるって感じと捉えれば良いのかな？
wikipedia読んでもあんまり理解できない

**デフォルトの名無しさん** · 2021/03/19(金) 01:58:47.96

名前呼び出しの意味が分かりません

**デフォルトの名無しさん** · 2021/03/19(金) 02:07:37.96

>>766
結局のところ知りたいことは何ですか？

カリーハワード同型対応とプログラムとの関係性ですか？
それとも、カリーハワード同型対応がプログラムの何に役立つのかですか？
それとも、call by name と call by need との違いですか。
それとも、その論文の内容ですか。
(その場合、PDFの5ページ目まで、つまり横線の式が登場する部分まではちゃんと理解できていると思っていいのですか？)

それとも、全く別のことですか？

とりあえず知りたいことをピンポイントに小さく一つに絞り、
それを具体的に質問していただけると助かります。

ところで、>>768 は元の質問者さんですか？

**768** · 2021/03/19(金) 02:15:59.36

>>769
ごめんなさい
僕は別人で割り込みです

**デフォルトの名無しさん** · 2021/03/19(金) 03:08:33.55

>>770
遅延評価を実現する評価戦略の中に、必要呼び出し(call by need)と名前呼び出し(call by name)があります。

必要呼び出しはhaskellが採っている戦略で、
一度評価した値を使い回して無駄な呼び出しを防ぐものです。

一方、名前呼び出しは同じ遅延評価でも、評価した値を記憶せず、必要なら何度でも同じ評価処理をするものです。

**デフォルトの名無しさん** · 2021/03/19(金) 09:49:18.16

>>769
そうですね
多分対応自体はわかると思います
しかし実際カリーハワード対応で基礎論の世界に持って行くことの効用がよくわかりません
基礎論の世界に持っていって基礎論でよく知られたなんかの定理が使えるとかいうわけでもなさそうですし
最初はcall by needの実装の話、すなわちcall by needでは展開された評価式に同じexpressionが出たとき、その内容を保持して同じ評価を何度も繰り返すのを防ぐらしいですが、もちろんどんな評価でも何でもかんでもメモするわけではないようなので、結局自分で手前でメモ化する必要がでたりします
どういう時はcall by needのメモ化が効いてどういう場合は効かないのかよくわからないので現状は“やってみる”しかないし、やってみて上手くいかなくても、なんか上手い書き方すればやってくれるのか、はなからだめなのか、その判別もつきません

**768** · 2021/03/19(金) 11:58:13.56

>>771
ありがとうございます

このときの「名前」なのですが、識別子のようなものでなく、評価・簡約前の「式の字面」的な意味なのですかね

**デフォルトの名無しさん** · 2021/03/19(金) 13:27:51.17

静的型のアイデアは
実行時の世界でやっていたことをコンパイル時の世界に持って行くことだから
このアイデアが常識にならない限り動的型の時代は終わらないだろう

**デフォルトの名無しさん** · 2021/03/20(土) 08:58:16.14

>>772
プログラムの世界において、ある事柄の性質や、事柄Aと事柄Bの間の関係を調べたいとき、
プログラムの世界の中ではなかなかうまく見えてこない場合がある。
そんなとき、カリーハワード同型対応によって問題を論理の世界に移すと、
見通しが良くなり、調べやすくなることがある。
そういう意味では役立ちます。
質問者さんが例示した論文がまさにそれです。

一方、何かを作るためにプログラムをする(現場の)人たちにとっては、とくに役立つことは無いと思います。
役立った話を一切聞きません。

質問者さんが、名前呼び出しなどの「性質や関係」を学術的に深く知りたくて調べているのであれば、役立つと思います。

自作のプログラム言語で名前呼び出しを実装したくて調べているのであれば、役立ちませんね。
別の論文に当たった方がいいと思います。

**デフォルトの名無しさん** · 2021/03/20(土) 09:35:36.64

>>775
そうなんですか
難しいですね
haskell の call by need のシステムがどういう具合に実装されてるか調べようとするとほぼ確実にカリーハワード対応が出てきます
ボチボチ勉強するしかなさそうですね
そもそもcall by needのメモ化の話はhaskell コンパイラの実装の話なのでhaskellの言語自体のレギュレーションにはひとつも載ってない(つまりghcではメモ化が効いて早いけど別のシステムでは遅いという事もありうるし文句言えない)ので効くか効かないか試してみるしかないのが不愉快なんですよねえ

**デフォルトの名無しさん** · 2021/03/20(土) 10:00:16.31

>>776
それなら graph reduction の実装を調べた方が良いと思います。

**デフォルトの名無しさん** · 2021/03/20(土) 10:28:51.32

>>773
すいません、call by name という名称の由来は分からないです。
いままで気にしたこともなかったです。

**768** · 2021/03/20(土) 12:05:15.57

>>778
ありがとうございます
こちらこそ、たびたびすみません

マンガのセリフのことを「ネーム」というらしいので、書いた字面をいうのかなと考えたり
name を和英・英英辞典で調べても、結局しっくりきませんでした

スレ汚しすみませんでした

**デフォルトの名無しさん** · 2021/03/20(土) 14:58:31.86

カリーハワード同型対応とかって、機械学習だのアーキテクチャだのネットワークだのアルゴリズムだのといった工学的で応用的で目的意識の定まった何かの役に立つために発明されたものというよりも、理学的で基礎的な単なる重要な事実という雰囲気ある気がする

**デフォルトの名無しさん** · 2021/03/21(日) 00:15:43.04

貴金属と期限つきポイントの対立煽りにたとえる
使用期限がないのは使用目的がないと言っているようなもの
だが期限がない方もメリットがあるのは工学的にも否定できない事実

**デフォルトの名無しさん** · 2021/03/22(月) 13:52:42.80

>>777
graph refuctionですか
調べてみます
しかしともかく、じゃあGHCとかではどう実装されてるのかとかいう資料はかなりの割合で結局カリーハワード対応使ってる文献しか出てこないのがなんとも
当面は“やってみる”でやり過ごすしかなさそうです

**デフォルトの名無しさん** · 2021/03/22(月) 15:09:38.98

call by name(仮)の正式名称がgraph reductionだったら
カリーハワード対応(仮)にも正式名称がありそうだけど
訂正することで利益が出せるようにならなければ正式名称の価値も分からん

**デフォルトの名無しさん** · 2021/03/22(月) 19:37:04.72

>>782
私にはむしろカリーハワード同型対応を陽には使っていない資料しか見当たらないです。
検索キーワードや調べ方が違うのかもしれませんね。
(カリーハワード同型対応がさす意味がお互いに違っている可能性もありますが)

この資料はどうでしょうか。
遅延評価をする関数型言語一般の実装方法です。
https://www.microsoft.com/en-us/research/uploads/prod/1987/01/slpj-book-1987.pdf

**デフォルトの名無しさん** · 2021/03/22(月) 20:29:59.10

例えばmonomorphism restrictionとかいうアレだったら
実行時の挙動ではなく型の話になるんじゃないか

**デフォルトの名無しさん** · 2021/03/23(火) 01:01:29.12

>>784
ありがとうございます
十章ですね
今度時間を見つけて読んでみます
そうですね
やっぱり私はGHC関連の資料をあたる事が多くて、やはりそこでは数学よりの資料が多いんでしょうね
でもやはりcall by needの実装方法はHaskellのレギュレーションには含まれていない実装依存のところなのでGHC userの私はどうしてもGHC関連の資料から当たりたくなってしまいます
GHCでのインプリメントは最新の成果が全て反映されてるとは限らないし、あるいはあまり一般的でない手法を用いているかもしれないし、そこはGHCそのものの資料が一番頼りになります
ただ一つの問題はあまりにも数学村(の計算論畑)の言葉で書かれててサッパリわからんとこorz

**デフォルトの名無しさん** · 2021/03/23(火) 03:42:25.12

>>786
余計なお世話だとは思いますが、どの章もその前までの章の積み重ねなので、
第10章だけを読んで理解するのは難しいと思います。

かなり古い資料を提示したのは、基礎の基礎から学んだ方が良いと思ったからです。
この資料は本当に分かりやすく基礎から説明されているので、
急がば回れの精神で、腰を据えてじっくりと学んでみることをお勧めします。
それこそ数ヶ月かけて。

なんかこう、数学で例えるなら、集合論や解析学の基礎があやふやなまま、
位相空間論の必要な部分だけを都合よく学ぼうとしているような、
そんなきらいがあるように見えます。

**デフォルトの名無しさん** · 2021/03/23(火) 05:16:41.87

そうですか
残念ながら当方計算論はウルマンホップクラフトや西岡先生の教科書しか読んだことないのでかなり知識が数学サイドに寄ってます
仕事もかなり数学よりで計算論はあくまで趣味なのであまり本腰入れて勉強したことはないのでもしかしたら専門に勉強されてる方から見ればそうかもしれません
まぁ本職に悪影響与えない範囲で時間見つけてボチボチ勉強します

**デフォルトの名無しさん** · 2021/03/23(火) 07:32:33.02

はっきり言うと評価戦略だとか推論規則だとかカリーハワード同型対応だとかの話は、まともな情報系の学部なら習う基礎基本
大学の講義資料が易しいと思われ

**デフォルトの名無しさん** · 2021/03/23(火) 20:57:46.65

情報系とかいう言い方をする奴は言語から逃げてるね
「数学村の言葉で書かれ」た資料が存在するのも
C言語で書かれたOSの話をしないのも
言語から逃げた結果じゃないかな

**デフォルトの名無しさん** · 2021/03/24(水) 19:34:45.53

何言ってんだコイツ…

**デフォルトの名無しさん** · 2021/03/26(金) 00:15:16.59

カリー・ハワード同型対応はこのスライドが分かり易かった
結局なんで上手く行くのかって良く分かってないのね
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

**デフォルトの名無しさん** · 2021/04/05(月) 18:23:16.33

関数の名前が被るとき、このモジュールのそれだと修飾しますが、
今書いてる翻訳単位のそれだと伝えるには今書いてるモジュール名で修飾するしかないのですか？
それが長大な場合惨めな気持ちになります

qualified 今書いているモジュール名 as 短い名前
にするような事はできないのですか？

**デフォルトの名無しさん** · 2021/04/05(月) 21:28:27.96

idrisを使った型駆動設計の話を聞いて、凄いなぁと思いました。
でもこの型駆動設計って、依存型が開発言語のあるのが前提の方法なんでしょうか？

**デフォルトの名無しさん** · 2021/04/05(月) 22:48:33.31

>>793
今書いている翻訳単位で import しているモジュールを qualified で装飾すれば、
今書いている翻訳単位内で定義している同名の関数は修飾せずとも使えると思うのですが、どうですか？

module Main where

import qualifued Data.List as L

transpose :: (Int, Int) -> (Int, Int)
transpose (x, y) = (y, x)

main :: IO ()
main = do
let a = L.transpose [[1, 2], [3, 4]]
let b = transpose (1, 2)
putStrLn $ show a ++ " / " ++ show b

**デフォルトの名無しさん** · 2021/04/06(火) 12:32:00.21

>>795
値コンストラクタ名に被りがあった場合、それができないようなのです
import モジュールの側の同名値コンストラクタを、qualifiedして修飾しましたので今書いてるモジュールの方を修飾なしで書いたのですが
それはAmbiguousだと怒られます

**デフォルトの名無しさん** · 2021/04/06(火) 20:13:47.61

ホントだ
怒られた

import qualified Data.Bool as B

data MyBool = True | False

instance Show MyBool where
show Main.True = "MyTrue"
show Main.False = "MyFalse"

main = do
print B.True
print Main.True
--print True ←ダメだって

**デフォルトの名無しさん** · 2021/04/06(火) 20:14:29.60

そりゃそうでしょうよ・・

**デフォルトの名無しさん** · 2021/04/06(火) 20:30:15.84

曖昧さ無く無い？なんでダメなんだっけ

**デフォルトの名無しさん** · 2021/04/06(火) 20:31:09.67

Prelude が暗黙的に居るから？