[過去ﾛｸﾞ] 「数学」をプログラミングするには (1002ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
843: デフォルトの名無しさん [sage] 2025/01/15(水) 08:10:12.30 ID:zm/Y+w4S(1) AAS
>>839839(2): デフォルトの名無しさん [sage] 2025/01/15(水) 01:13:53.96 ID:xsuF+zK/(1) AAS
型っつっても所詮は構造体に名前がついただけ
計算の過程や性質に型付けをしたいんだ
「関数fを抜けたタイミングで、ポインタpは必ず指定の条件をみたす場所を指していなければならない」
こういうのを型で保証したいんだ
実行時のアサーションで書けることは、型にできる
844: デフォルトの名無しさん [sage] 2025/01/15(水) 08:19:11.22 ID:Uf2ceum5(1) AAS
二分探索やクイックソートのロジックが正しいことを型で証明できるか
845: デフォルトの名無しさん [sage] 2025/01/15(水) 08:32:18.93 ID:nE+pEHV1(1) AAS
数学的帰納法で証明できる
（長さ1の配列に対しては自明
長さ1, 2, ..., k-1に対して正しいと仮定して、長さkに対して証明する）
そのような構造はF代数で定式化できる
846: デフォルトの名無しさん [sage] 2025/01/15(水) 08:56:17.03 ID:3W/U+R8x(1) AAS
アキュームレータを再帰的に更新していくようなのはF代数に抽象化できる
847: デフォルトの名無しさん [sage] 2025/01/15(水) 19:07:44.03 ID:8y1isLBr(1) AAS
オブジェクト指向はオワコン
848: デフォルトの名無しさん [sage] 2025/01/16(木) 02:12:12.85 ID:hp6XExKo(1) AAS
抽象データ型、凝集度、関心の分離などの既存の概念だけで簡潔かつ正確に説明できることをわざわざバズワードに言い換えただけのクソ概念
849: デフォルトの名無しさん [sage] 2025/01/16(木) 03:23:35.34 ID:DBY13IoQ(1/2) AAS
形式論理とかまじで役に立たんからな
850: デフォルトの名無しさん [sage] 2025/01/16(木) 08:27:28.13 ID:L1OHI3Vu(1) AAS
実は当たり前にやっていること。関数適用はmodus ponensに相当する
851: デフォルトの名無しさん [sage] 2025/01/16(木) 18:56:00.70 ID:DBY13IoQ(2/2) AAS
でも役に立たないでしょ
少しは文章読めよガイジ
852: デフォルトの名無しさん [sage] 2025/01/16(木) 20:35:27.89 ID:FAOk1woG(1/2) AAS
型情報からあまり使ったことない関数でも使い方にあたりがつくのは便利だと思うけどお前はそうではないんだな
853: デフォルトの名無しさん [sage] 2025/01/16(木) 20:51:11.29 ID:Wo2SWLBc(1) AAS
複素数型も四元数型も定義可能だし、GPUに組み込んで高速で並列演算できるようにしてやれば科学界に革命を起こせるな
854: デフォルトの名無しさん [sage] 2025/01/16(木) 21:51:56.76 ID:zFtBKiS0(1) AAS
処理系がcall/ccをサポートすることは、直観主義論理に背理法を加えることに相当する
855: デフォルトの名無しさん [sage] 2025/01/16(木) 22:19:04.03 ID:FAOk1woG(2/2) AAS
研究者の名前がなかなか思い出せなかったがGriffinだな POPL 1990
856: デフォルトの名無しさん [sage] 2025/01/16(木) 22:28:22.29 ID:l7++KB1R(1) AAS
イマドキ型のない言語なんて、即席のスクリプトくらいにしか使わんでしょ
857(1): デフォルトの名無しさん [sage] 2025/01/16(木) 22:31:22.46 ID:IceLMl7e(1/2) AAS
代数的データ型やパラメータ多相を使えばプログラムのかなり多くの性質をコンパイラが保証できるのに、わざわざ型検査なしで注意してコード書くとか馬鹿のすること
858: デフォルトの名無しさん [sage] 2025/01/16(木) 22:36:34.50 ID:IceLMl7e(2/2) AAS
人類未曾有のソフトウェアを書くならともかく、巷のプログラムの9割近くのコードはただデータを整形してマッピングしてるだけ
あとの一割は既存のライブラリの呼び出し
現代のプログラミング言語の型システムがあれば、IDEの入力補完に従ってるだけでバグの無いコードが書ける
画面にらみつけてロジック確認なんかしてんのはただのアホ
859: デフォルトの名無しさん [sage] 2025/01/16(木) 22:51:04.55 ID:fgdrajER(1) AAS
しかし、それができるなら動的型付けの言語でもエディタが構文から型推論すれば同じことができるのでは？
860: デフォルトの名無しさん [sage] 2025/01/16(木) 23:35:14.70 ID:N/7GMQUm(1) AAS
ところがどっこい
型注釈無しでは型推論ができない、あるいはエラーにすべきか型チェッカが判定できないケースが存在する
まず簡単なのは、ユニオン型だ
f:: () -> Int | Str
みたいな関数は注釈なしでは、ふたつの箇所で異なる型を返してるのが間違いなのかどうか型チェッカには判定できない
パラメータ多相を使う高階関数も型推論が困難だ
map :: (a -> b) -> [a] -> [b]
これがたとえば二カ所で
map :: (Str -> Int) -> [Str] -> [Int]
map :: (Str -> Str) -> [Str] -> [Str]
と使われていたら、型チェッカは
map :: (Str -> Int|Str) -> [Str] ->[Int]|[Str]
だと推論するかも知れない。もしそうなると、
map :: (Str -> Str) -> [Str] -> [Int]
という使われ方をしていても、チェックに通ってしまうことになる
リフレクションやメタプログラミングをしている場合も勿論、コードだけから型推論するのは困難だ
逆に言えば、このようなケースに適切に型注釈をつければ、その他の部分は推論できるようになるので、生産性が格段に上がる
861: デフォルトの名無しさん [sage] 2025/01/17(金) 04:10:24.01 ID:VwDpqJJw(1) AAS
なんかグダグダ言ってるけどそれ形式論理なしでできるよね
この話の発端は形式論理が役に立たないってことであって，型が役に立たないって話じゃないよ
862: デフォルトの名無しさん [sage] 2025/01/17(金) 06:49:41.95 ID:b1HMrou3(1) AAS
単純に、お前の話に誰も興味ないから話題が変わっただけでは
863: デフォルトの名無しさん [sage] 2025/01/17(金) 09:10:34.70 ID:qO2eRSGs(1) AAS
ocamlなんかは型推論の健全性と完全性を備えているから
どんな式でも型がつくし、型エラーがでなければ正しいプログラムになるというのが保証されてる
健全性と完全性をどちらか捨てるとしたら完全性なので、そういう言語は型注釈が必要になる
864: デフォルトの名無しさん [sage] 2025/01/17(金) 16:31:58.98 ID:tFlne/Xr(1) AAS
まぁ形式論理も時相論理もプログラミングには何の恩恵もないわな
865(2): デフォルトの名無しさん [] 2025/01/17(金) 16:59:57.91 ID:GO6/DX25(1) AAS
CSは数学を一部利用するが
数学はCSなんて知らんがな状態
866(1): デフォルトの名無しさん [sage] 2025/01/17(金) 18:01:24.36 ID:7aS9Z/2O(1) AAS
学問にコンプレックス持ってる人って、みっともないね。
867: デフォルトの名無しさん [sage] 2025/01/17(金) 20:14:27.37 ID:b0CV3tPB(1) AAS
>>857
パラメータ多相のジェネリックな型は特に制約を指定しなければ任意の型がOK何でもありだけど
何の型でもありということは使える範囲も極めて狭いというか
言語によってはprintすることすら任意の型が可能派と必ずしも可能とは限らない派もあり曖昧で
何らかの制約を指定しないと何の処理もできないためその型の値をそのまま返すことしかできなくなってしまう
つまりジェネリック型パラメータに対する制約記述がカギとなる
上下前次1-新書関写板覧索設栞歴
あと 135 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.015s