[過去ﾛｸﾞ] 次世代言語11[Rust Swift TypeScript Dart] (1002ﾚｽ)
上下前次1-新
抽出解除 必死ﾁｪｯｶｰ(本家) (べ) 自ID ﾚｽ栞 あぼーん
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
ﾘﾛｰﾄﾞ規制です｡10分ほどで解除するので､他のﾌﾞﾗｳｻﾞへ避難してください｡
611: デフォルトの名無しさん [sage] 2018/06/19(火) 01:44:59.48 ID:menX4d1R(1/2) AAS
CoqとAgdaは敬遠してるんだよね…
あの二つはプログラミング言語じゃなくて証明支援器だって聞いてるから…
オレは別にPCに証明問題を解くのを手伝ってもらいたいんじゃなくて、
従来の型システムを発展させた依存型とかを使ったより安全な
プログラミングを行うの方法が知りたいんだよって思って…
けど、学ぶ順番としてはCoqが先のほうが良かったのかな？
でも、Coqだとどうにもモチベーションが…
あと、ついでに線形型も学びたかった……
Rustの所有権・借用・ライフタイムはほぼ理解できてるんでそれほど難しくはないだろうと…
まず、依存型で躓いてるんで線形型までたどり着いていない…
んー……一度に色々やろうとし過ぎか…(´・ω・｀)
616: デフォルトの名無しさん [sage] 2018/06/19(火) 08:33:59.97 ID:menX4d1R(2/2) AAS
>>613613(1): デフォルトの名無しさん [sage] 2018/06/19(火) 04:24:16.98 ID:thfWBPV2(1) AAS
>>608
この場合呼び出しのたびに変化するものが、引数のnと「どちらの関数を呼ぶか」という
2つしかないんだから、呼び出しのたびに減る式を作ろうとしたらこれを組み合わせるしかない
後はパズルだろ
んー…１日置いたらやっと分かったような気がする…
気がしてるだけかもだけどあとは自力でどうにか理解できそう…
まあ、新しい概念を覚えるときはどうしても時間が掛かるものだし、
あとは腑に落ちるまでサンプルコードひたすら写経したりするか…
皆ありがとう
>>610610(1): デフォルトの名無しさん [sage] 2018/06/19(火) 00:28:07.36 ID:2myyjakz(1) AAS
ATSは依存型言語の中でも奇抜な方だと思うよ
Coqとソフトウェアの基礎の方が易しいと思う
ATSの依存型は奇抜なの？
他の依存型がある言語も似たようなことやるんじゃないの？
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.045s