- 1 名前：デフォルトの名無しさん [2024/03/16(土) 19:41:45.98 ID:nuwGv9us.net]
- たとえば、プログラミングで
π/4 = 1 - 1/3 + 1/5 - 1/7 + ...
を近似ではなく厳密に確かめるにはどうしたらいいの
人間が証明できるってことは、有限なアルゴリズムに書き換えられると思うんだけど
- 795 名前：デフォルトの名無しさん mailto:sage [2024/12/27(金) 23:43:23.45 ID:QY/IdYVY.net]
- 単一継承ならせいぜい親と子の対立しかない
多重継承なら親と親の対立もありえる
ドメインとドメインの対立
- 796 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 17:37:12.88 ID:1/gaPmQa.net]
- 命題⇔型
理論⇔ライブラリ
- 797 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 17:42:01.70 ID:0n60WVz7.net]
- 物理とプログラミングは対立構造か
- 798 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 17:51:31.87 ID:R/JuY1We.net]
- 言葉に酔ってるだけだろ
- 799 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 18:41:16.54 ID:1/gaPmQa.net]
- 自分が理解できないからと言って難癖をつけるのはやめましょう
- 800 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 19:34:52.40 ID:0n60WVz7.net]
- 国語を勉強してくれ
- 801 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 23:31:21.70 ID:Ettja4KR.net]
- 正しい言葉遣いをしたら綺麗事しか言わなくなると思うよ
オールドメディアを超越することと可読性は両立しない
- 802 名前：デフォルトの名無しさん mailto:sage [2024/12/30(月) 06:05:18.87 ID:AFoxKaw/.net]
- オールドメディアガー
- 803 名前：デフォルトの名無しさん mailto:sage [2024/12/30(月) 07:54:23.09 ID:AFoxKaw/.net]
- SNSで炎上商売
- 804 名前：デフォルトの名無しさん mailto:sage [2024/12/30(月) 23:30:57.09 ID:djpp6m1u.net]
- 商売なら買い手に責任がある
商品や作品の側に罪はないという理屈で変な物が作られる
買い手の方は責任を果たすために優れた物を買い、自然淘汰されるべき物には不買運動をする
- 805 名前：デフォルトの名無しさん [2025/01/09(木) 12:47:55.94 ID:iZ6OsWgm.net]
- 炎上商売にエンジョイ
- 806 名前：デフォルトの名無しさん mailto:sage [2025/01/12(日) 02:01:35.37 ID:8Ab7i+tr.net]
- 型に対してプログラミングすべき
- 807 名前：デフォルトの名無しさん mailto:sage [2025/01/12(日) 07:50:15.14 ID:aNPLoHWH.net]
- それやってもすぐ人間の能力限界にぶつかるから
- 808 名前：デフォルトの名無しさん [2025/01/12(日) 10:12:06.95 ID:l8rSJlAD.net]
- バリアントで統一
- 809 名前：デフォルトの名無しさん mailto:sage [2025/01/12(日) 10:51:45.53 ID:iqj2UdGG.net]
- 空手型
- 810 名前：デフォルトの名無しさん [2025/01/12(日) 15:49:20.69 ID:DO5vWwuf.net]
- 科学をプログラミングするのは難しいが
プログラミングを科学するのは可能では？
- 811 名前：デフォルトの名無しさん mailto:sage [2025/01/12(日) 16:35:24.05 ID:iqj2UdGG.net]
- 主語がでかい
- 812 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 02:34:19.05 ID:scTw5na7.net]
- オブジェクト指向って、コンピュータサイエンスじゃないんだよな
単に（一部の）人間にとって理解しやすくモジュール化しようってだけのことで、それで技術的に出来ることが増えるわけじゃないから
- 813 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 02:37:56.75 ID:scTw5na7.net]
- 構造化プログラミングや、関数プログラミングは、それ以前より高レベルの抽象化をもたらしたけど、オブジェクト指向は単に書き方の問題
科学論文で例えれば、構造化プログラミングや関数プログラミングは理論の内容に相当するが、オブジェクト指向は論文の体裁のこと
- 814 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 02:40:56.25 ID:XXChvl3U.net]
- そして、科学論文の体裁は重要だが、オブジェクト指向はいまや重要ではない
- 815 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 05:24:15.88 ID:elRKgauc.net]
- 型
並行性
最適化
この3つだよ
今求められてんのは
- 816 名前：デフォルトの名無しさん [2025/01/13(月) 09:04:54.93 ID:PzkYuqRH.net]
- 求めてないよ
- 817 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 09:12:00.23 ID:J7wtrzSF.net]
- 俺が大学生だった20年前はオブジェクト指向もCSの一部だったが
教授はカプセル化が一番重要だといってた
研究はされてたけど、アスペクト指向は流行らなかったなー
- 818 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 09:12:18.64 ID:6+/RYvQh.net]
- で、出ｗｗｗｗインターネットあまのじゃく君ｗｗｗｗｗｗｗ
- 819 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 09:13:20.48 ID:wtvPYUbh.net]
- >>809
君、勉強できなそうだね
- 820 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 09:42:56.67 ID:94WYo5Du.net]
- >>809
たった三行でここまで頭悪そうな文章書けるのってある意味才能だな
- 821 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 10:20:57.19 ID:Ymx2LteG.net]
- オブジェクト志向の次はデザインパターンだろ
- 822 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 10:42:06.79 ID:LSOaiCCa.net]
- カプセル化も全否定されてるけど
いまだにアンダースコアの変数はモヤモヤする
- 823 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 10:43:00.59 ID:P3ktA6B0.net]
- それも宗教
振り子が逆に振れてるだけ
- 824 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 11:39:54.56 ID:J7wtrzSF.net]
- デザインパターン20数個のうち10数個ぐらいはただの高階関数でかけるという研究もある
- 825 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 11:55:37.97 ID:Ymx2LteG.net]
- 魔法はなかった
- 826 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 13:02:05.46 ID:DTY38xVU.net]
- >>816
そして残りの10個はただのアンチパターン
- 827 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 17:18:23.47 ID:Ymx2LteG.net]
- 岩波講座 ソフトウェア科学 [基礎]1
計算システム入門
著者 所真理雄 著
刊行日 1988/10/06
ソフトウェアの作成は人間的な作業で，信頼性や生産性の点でいまだに手工業の域にある．こうした現状をふまえ，ソフトウェア作成の方法を示すとともに，その理論と知識を整理し，新しい学問体系として提示する
- 828 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 00:54:16.56 ID:eoA7bUR4.net]
- なぜ高階関数を使わないのか
εδ論法はなぜεの関数を具体的に構成しないのか
こういうのを体系的に整理したら特定の勢力だけが得をして他は損するんじゃないか
だから整理しない
- 829 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 08:02:07.96 ID:WvheYWow.net]
- Foo = Bar | Baz
- 830 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 08:15:31.11 ID:BEZztBwJ.net]
- 型⊂クロージャ
- 831 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 12:10:31.19 ID:ygjj3afU.net]
- 型なんて特別なものじゃない
0や1はInt型のオブジェクト、IntはType型のオブジェクト
- 832 名前：デフォルトの名無しさん [2025/01/14(火) 12:50:51.03 ID:1hGtsoWq.net]
- 水の呼吸、壱の型
- 833 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 13:27:13.44 ID:2ZQOZttA.net]
- >>824
咄嗟にアニメの話出せるとか
おまえすげえ最先端行ってるな
才能の塊かよ
- 834 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 13:30:47.33 ID:5ok8hMJ2.net]
- >>824
それ知ってるわ
煉獄さんの映画のやつだろ
お前マジでおもしれーな
- 835 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 13:58:17.70 ID:L1ZxvYgu.net]
- 型が第一級オブジェクトなら、クロージャを使えば状態つきの型を作れるわけか
- 836 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 14:18:33.81 ID:x8Aql6YT.net]
- 有理数型や小数型も作れるのか？
- 837 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 14:29:34.08 ID:S4iOQtDV.net]
- >>827
わざわざ型情報を実行時に変化させてどうすんだ
- 838 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 14:29:54.43 ID:S4iOQtDV.net]
- >>828
お前は低レベルすぎ
- 839 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 20:10:44.55 ID:6b3bLxyH.net]
- 有理数型はHaskellやMathematicaにもうある
状態付きの型、考えただけで恐ろしい
- 840 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 20:32:44.91 ID:A8xCzIhU.net]
- そうやって進化していくものよ
- 841 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 21:00:24.45 ID:6b3bLxyH.net]
- 状態付きの計算を行う手順を持った型なら純粋だから許せるけど
状態付きの型なんていらないよ
- 842 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 21:07:31.89 ID:KUHcAlDi.net]
- 君に要るかどうかは関係ない
- 843 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 00:39:06.33 ID:v8xz0BVe.net]
- `f1 = Foo 1`なら、f1の型は`Foo 1`
基本的にはこれでいい
`Foo 1`は `{n: Nat} Foo n`のサブタイプ
`f1`を`Bar :: t -> s`に渡せるのは、`Foo 1`に変換する規則が存在するとき
型検査はそれをコンパイラがチェックすればいい
- 844 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 00:39:55.88 ID:v8xz0BVe.net]
- `f1 = Foo 1`なら、`f1`の型は`Foo 1`
基本的にはこれでいい
`Foo 1`は `{n: Nat} Foo n`のサブタイプ
`f1`を`Bar :: t -> s`に渡せるのは、`Foo 1`を`t`に変換する規則が存在するとき
型検査はそれをコンパイラがチェックすればいい
- 845 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 00:45:33.23 ID:2eRf9tIs.net]
- ユーザー定義関数から値返せないじゃん
- 846 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 00:50:21.44 ID:LknHRWOL.net]
- 型は実体ではなく注釈か
- 847 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 01:13:53.96 ID:xsuF+zK/.net]
- 型っつっても所詮は構造体に名前がついただけ
計算の過程や性質に型付けをしたいんだ
「関数fを抜けたタイミングで、ポインタpは必ず指定の条件をみたす場所を指していなければならない」
こういうのを型で保証したいんだ
- 848 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 01:33:23.91 ID:Yf+/cXFX.net]
- ぬるぽは実行前に排除する
- 849 名前：デフォルトの名無しさん [2025/01/15(水) 03:48:57.84 ID:y+Z6DxpET]
- 大企業資本家階級のために政治やってる自民公明か゛クソなのは分かりきってるが野党も公平もクソもない主張ばかりで入れたい党か゛ねえよな
郵便料金超絶値上げで年収一千萬超ゴ囗ゴロの連中やらに児童手当た゛なんだと税金くれてやってる上に完全教育無償化だのとトチ狂ったこと
ほさ゛いて税金泥棒に追い銭とか主張する党だらけ貧乏人か゛孑を産み落としたら遺棄罪で逮捕懲役，日当5千円で塀の中から子に送金させるのか゛
筋だし金を出す者が子を育てる権利を得るのも筋、子はダメな親なんて平気で見限るものだし孑がほしい金持ちに子を斡旋する制度を作る
のが国の仕事、カンコーテロでJＡLANAテロリストに莫大な温室効果ガスまき散らさせてるのが原因の自称被災者に億の資産持っていようが
税金くれてやれた゛のほざいてる党まであるしナマポ制度があるのになぜ追い銭が必要なのか捕捉率云々なら何万人も寄生蟲公務員使って
桐生市みたくはじきまくってないで無条件に最低所得保障やって相続税で回収すれは゛いいわな
まともな主張は消費税廃止と内部留保課税むしろ社會の寄生虫である大企業に毎年外形課税して自民公明による不公平政治の巻戻しが必要
(ref.) TTрs://www.call4.jp/info.php?tｙpe=iｔems&id=I0000062
ttps://haneda-projeCТ.jimdofree.Ｃom/ , ttps:/／flight-route.com／
tｔps://n-souonhigaisosyoudan.amebaownd.com/
- 850 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 06:39:48.90 ID:xj5qHVfP.net]
- >>839
理解浅すぎ
数学勉強してないでしょ
- 851 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 08:07:10.18 ID:ogU0rXVD.net]
- >>842
君が数学で研究職に就いているのでなければ、まず間違いなく君よりは理解してるよ
- 852 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 08:10:12.30 ID:zm/Y+w4S.net]
- >>839
実行時のアサーションで書けることは、型にできる
- 853 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 08:19:11.22 ID:Uf2ceum5.net]
- 二分探索やクイックソートのロジックが正しいことを型で証明できるか
- 854 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 08:32:18.93 ID:nE+pEHV1.net]
- 数学的帰納法で証明できる
（長さ1の配列に対しては自明
長さ1, 2, ..., k-1に対して正しいと仮定して、長さkに対して証明する）
そのような構造はF代数で定式化できる
- 855 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 08:56:17.03 ID:3W/U+R8x.net]
- アキュームレータを再帰的に更新していくようなのはF代数に抽象化できる
- 856 名前：デフォルトの名無しさん mailto:sage [2025/01/15(水) 19:07:44.03 ID:8y1isLBr.net]
- オブジェクト指向はオワコン
- 857 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 02:12:12.85 ID:hp6XExKo.net]
- 抽象データ型、凝集度、関心の分離などの既存の概念だけで簡潔かつ正確に説明できることをわざわざバズワードに言い換えただけのクソ概念
- 858 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 03:23:35.34 ID:DBY13IoQ.net]
- 形式論理とかまじで役に立たんからな
- 859 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 08:27:28.13 ID:L1OHI3Vu.net]
- 実は当たり前にやっていること。関数適用はmodus ponensに相当する
- 860 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 18:56:00.70 ID:DBY13IoQ.net]
- でも役に立たないでしょ
少しは文章読めよガイジ
- 861 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 20:35:27.89 ID:FAOk1woG.net]
- 型情報からあまり使ったことない関数でも使い方にあたりがつくのは便利だと思うけどお前はそうではないんだな
- 862 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 20:51:11.29 ID:Wo2SWLBc.net]
- 複素数型も四元数型も定義可能だし、GPUに組み込んで高速で並列演算できるようにしてやれば科学界に革命を起こせるな
- 863 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 21:51:56.76 ID:zFtBKiS0.net]
- 処理系がcall/ccをサポートすることは、直観主義論理に背理法を加えることに相当する
- 864 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 22:19:04.03 ID:FAOk1woG.net]
- 研究者の名前がなかなか思い出せなかったがGriffinだな POPL 1990
- 865 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 22:28:22.29 ID:l7++KB1R.net]
- イマドキ型のない言語なんて、即席のスクリプトくらいにしか使わんでしょ
- 866 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 22:31:22.46 ID:IceLMl7e.net]
- 代数的データ型やパラメータ多相を使えばプログラムのかなり多くの性質をコンパイラが保証できるのに、わざわざ型検査なしで注意してコード書くとか馬鹿のすること
- 867 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 22:36:34.50 ID:IceLMl7e.net]
- 人類未曾有のソフトウェアを書くならともかく、巷のプログラムの9割近くのコードはただデータを整形してマッピングしてるだけ
あとの一割は既存のライブラリの呼び出し
現代のプログラミング言語の型システムがあれば、IDEの入力補完に従ってるだけでバグの無いコードが書ける
画面にらみつけてロジック確認なんかしてんのはただのアホ
- 868 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 22:51:04.55 ID:fgdrajER.net]
- しかし、それができるなら動的型付けの言語でもエディタが構文から型推論すれば同じことができるのでは？
- 869 名前：デフォルトの名無しさん mailto:sage [2025/01/16(木) 23:35:14.70 ID:N/7GMQUm.net]
- ところがどっこい
型注釈無しでは型推論ができない、あるいはエラーにすべきか型チェッカが判定できないケースが存在する
まず簡単なのは、ユニオン型だ
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]
という使われ方をしていても、チェックに通ってしまうことになる
リフレクションやメタプログラミングをしている場合も勿論、コードだけから型推論するのは困難だ
逆に言えば、このようなケースに適切に型注釈をつければ、その他の部分は推論できるようになるので、生産性が格段に上がる
- 870 名前：デフォルトの名無しさん mailto:sage [2025/01/17(金) 04:10:24.01 ID:VwDpqJJw.net]
- なんかグダグダ言ってるけどそれ形式論理なしでできるよね
この話の発端は形式論理が役に立たないってことであって，型が役に立たないって話じゃないよ
- 871 名前：デフォルトの名無しさん mailto:sage [2025/01/17(金) 06:49:41.95 ID:b1HMrou3.net]
- 単純に、お前の話に誰も興味ないから話題が変わっただけでは
- 872 名前：デフォルトの名無しさん mailto:sage [2025/01/17(金) 09:10:34.70 ID:qO2eRSGs.net]
- ocamlなんかは型推論の健全性と完全性を備えているから
どんな式でも型がつくし、型エラーがでなければ正しいプログラムになるというのが保証されてる
健全性と完全性をどちらか捨てるとしたら完全性なので、そういう言語は型注釈が必要になる
- 873 名前：デフォルトの名無しさん mailto:sage [2025/01/17(金) 16:31:58.98 ID:tFlne/Xr.net]
- まぁ形式論理も時相論理もプログラミングには何の恩恵もないわな
- 874 名前：デフォルトの名無しさん [2025/01/17(金) 16:59:57.91 ID:GO6/DX25.net]
- CSは数学を一部利用するが
数学はCSなんて知らんがな状態
- 875 名前：デフォルトの名無しさん mailto:sage [2025/01/17(金) 18:01:24.36 ID:7aS9Z/2O.net]
- 学問にコンプレックス持ってる人って、みっともないね。
- 876 名前：デフォルトの名無しさん mailto:sage [2025/01/17(金) 20:14:27.37 ID:b0CV3tPB.net]
- >>858
パラメータ多相のジェネリックな型は特に制約を指定しなければ任意の型がOK何でもありだけど
何の型でもありということは使える範囲も極めて狭いというか
言語によってはprintすることすら任意の型が可能派と必ずしも可能とは限らない派もあり曖昧で
何らかの制約を指定しないと何の処理もできないためその型の値をそのまま返すことしかできなくなってしまう
つまりジェネリック型パラメータに対する制約記述がカギとなる
- 877 名前：デフォルトの名無しさん mailto:sage [2025/01/18(土) 08:09:37.99 ID:eX+b185R.net]
- >>867
多分コンプレックスとかじゃなくて無駄なものを持ち込まずにシンプルにしておきたいってだけじゃない
- 878 名前：デフォルトの名無しさん mailto:sage [2025/01/18(土) 08:45:22.05 ID:BE7PGd83.net]
- >>866 数学が専門の人がどんどんCSに入ってきて内容が高度化してるって聞いたぞ俺は
- 879 名前：デフォルトの名無しさん [2025/01/18(土) 10:15:15.14 ID:ERaUWL8N.net]
- シンプレックスでコンプレックス
- 880 名前：デフォルトの名無しさん [2025/01/18(土) 11:19:59.28 ID:7Jaib8zo.net]
- なんでコンプレックスの話が出て来てるのかさっぱり判らん
>>870
それこそ >>866 の説を補強してるだけじゃないの
- 881 名前：デフォルトの名無しさん mailto:sage [2025/01/18(土) 11:57:14.53 ID:xEXW43By.net]
- >>869
イミフ
- 882 名前：デフォルトの名無しさん mailto:sage [2025/01/18(土) 12:09:19.43 ID:pstj5VhN.net]
- >>869
数学やCSを持ち込んで対象が複雑になると思ってるのは、
自分が理解できないものにコンプレックス持ってるからだよ
理論を作って対象が複雑になることはあり得ない
- 883 名前：デフォルトの名無しさん mailto:sage [2025/01/18(土) 12:14:10.21 ID:pstj5VhN.net]
- >>874
一筆書きして最初の場所に戻ってこられるか、は複雑な問題
グラフのすべての頂点から出ている辺の数が偶数、というのは単純な問題
グラフ理論を持ち込んで問題が複雑になったというのは、
頂点・辺・偶数・奇数などの概念が理解できないから
それは数学に対するコンプレックスにほかならない
- 884 名前：デフォルトの名無しさん mailto:sage [2025/01/18(土) 12:39:38.25 ID:84F6tYk8.net]
- >>872 P=NP予想とかCSの問題も数学で扱われてるんだから知らんがな状態ではないと思う
- 885 名前：デフォルトの名無しさん mailto:sage [2025/01/18(土) 15:06:03.89 ID:2/LPmLwt.net]
- プログラミングに必要な数学は数値計算で使う数学くらいか？
微積と線形
圏論がプログラミングで無意味なのは誰でもわかるか
- 886 名前：デフォルトの名無しさん mailto:sage [2025/01/18(土) 15:34:34.81 ID:28NAL8Fg.net]
- >>877
プログラミングと数学を分けてる時点で、Qiitaのブログのサンプルコピペしてる雑魚と同レベル
- 887 名前：デフォルトの名無しさん mailto:sage [2025/01/18(土) 15:41:30.33 ID:Zj1ghav+.net]
- 反論になってないなぁ
- 888 名前：デフォルトの名無しさん mailto:sage [2025/01/18(土) 16:26:51.31 ID:xuSYONRy.net]
- プログラミングに数学はいくらでも使うことができる
プログラミングに使う数学とか言ってんのは、ただ単に自分が数学を学びたくないだけ
- 889 名前：デフォルトの名無しさん mailto:sage [2025/01/19(日) 12:35:56.76 ID:fNMlPpUq.net]
- Felleisen 30年研究して「プログラミングには型が必要なことがわかった」←これ好き
- 890 名前：デフォルトの名無しさん mailto:sage [2025/01/20(月) 01:24:19.62 ID:8nHIoBfi.net]
- 型＝命題
項＝証明
この対応は、通常のプログラミングでも同様
そう思えないってことは、型の使い方が大雑把すぎるってこと
- 891 名前：デフォルトの名無しさん mailto:sage [2025/01/20(月) 06:41:50.30 ID:qtJTpWnY.net]
- >>882
お前のソースコード見せてくれよ
どんだけ立派なのか拝ませてくれ
- 892 名前：デフォルトの名無しさん mailto:sage [2025/01/20(月) 08:41:47.10 ID:jEcxLOMX.net]
- 立派とは？
- 893 名前：デフォルトの名無しさん mailto:sage [2025/01/20(月) 08:45:50.71 ID:VdwKz6kz.net]
- int i=10;
char c='a';
printf("%d\n",i+c);
こんなのがかけるC++ではカリーハワード同型対応なりたたなさそう
- 894 名前：デフォルトの名無しさん mailto:sage [2025/01/20(月) 09:06:44.29 ID:3GFrNXKp.net]
- C/C++の型付けは、メモリをなんぼ確保するかの目印でしかないからな
- 895 名前：デフォルトの名無しさん mailto:sage [2025/01/23(木) 23:15:16.69 ID:gkeqtoks.net]
- Rustの型はトレイト属性があって
マルチスレッドでも同期が保証される型など
抽象度の高い表現が型システムで扱えるようになってるね
それによりデータ競合が起きないことを型システムで保証してしまってるところが凄いと思った
|
 |
