確認してみたところコーディングを支える技術には「名前的型システムと構造的型システムの違い」について書かれていなかった。これを加筆したいが媒体の都合で大幅な加筆は難しいのでここにドラフトを置く。
「名前的型システムと構造的型システムの違い」加筆案 - 西尾泰和のScrapbox
確認してみたところコーディングを支える技術には「名前的型システムと構造的型システムの違い」について書かれていなかった。これを加筆したいが媒体の都合で大幅な加筆は難しいのでここにドラフトを置く。
型システム 〜プログラムの安全性を支える数学〜 - Laborify
京都大学大学院 情報学研究科 通信情報システム専攻 修士2回生の五十嵐雄です．大学では，プログラミング言語理論，その中でも特に型システムの研究をしています． この記事では，私が特に力を入れて研究している漸進的型付けという種類の型システムについて紹介します．プログラムや型システムといった基本的な概念から解説していくので，プログラミング経験のない人も安心して読み始めてもらえたらと思います． はじめに プログラムとはコンピュータへの命令を記述したものです．2018年現在，私たちの生活は数多くのプログラムに支えられています． あなたがこの記事を Windows が入ったパソコンで見ているなら，まずその Windows がプログラムです．お家にテレビや冷蔵庫があれば，それらの中にもプログラムが内蔵されているでしょう．空いた時間にスマートフォンでゲームをするなら，遊んでいるゲームも全てプログラムです．
Go が for ループをやめるために足りないもの - methaneのブログ
ジェネリクスの話題になると常に出てくるのが、 for ループの代わりに関数型スタイルで書きたいという要望です。 for ループで書くのは、可読性が悪く、筋力がいるとまで言う人もいます。 しかし、ジェネリクスが追加されても、このスタイルのプログラミングは実用的にはなりません。ジェネリクス以外にも足りない部分がたくさんあるのです。 例えば、次のようなコードを考えてみましょう。 type PointLog struct { ID int64 UserID int64 Point int32 } // 今の書き方 func UserTotalScore(log []PointLog, userID int64) int64 { var t int64 = 0 for _, p := range log { if p.UserID == userID { t += int64(p.Point) }
F*(F Star)の複雑な型システムの何が嬉しいのか？ - Amosapientiam
マイクロソフトが開発中のF* という依存型プログラミング言語を少し触ってみました。 この言語には強力で複雑な型システムが組み込まれています。 現状、依存型言語は世間にはあまり広まっていませんので F*とは？ 複雑な型ってなんだろう？ 複雑な型システムを組み込んで何が嬉しいんだろう？ 何が嬉しくないんだろう？ と疑問をお持ちになる方も多いだろうと思います。 この記事ではF*で使われている複雑な型の一部と、複雑な型を持つことの利点・欠点の一部を述べ、それを簡単なコード例を通じて体感してみます。 疑問に対する答え F*とは？ マイクロソフトと Inria が開発中のプログラミング言語です。 依存型や monadic effect などが組み込まれており、複雑な仕様が型で表現できます。構文は OCaml や F#などのML系関数型言語に似ています。 詳しくは下記のリンクたちを参照。 F* (プログ
静的解析の限界、現実世界との境界
2018年に静的解析をとにかく強力につけまくるのは多分あんまりコストに見合わないのでよくない じゃあ静的解析を窓から投げ捨ててよいかというとそれはただの愚行 (以下、静的解析を普通に使えてる人には自明なことしか言いません) 私が最初に静的解析の限界を感じたのは多分依存型で遊んでいたとき 依存型の力はすごくて、まぁそれもそのはず命題論理から述語論理に進んで元への言及ができるので見かけ上表現力はとんでもなく上がるわけです。例えば「ある方程式を満たす解のみを受け取って何かする」みたいな関数が型として表現できるようになる。 一見すると最強に見えるんだけどこれは実質定理証明をすることなので、制限の強い型をつければつけるほど実装で苦しむ羽目になるということを割とすぐ痛感することになった。 例えば head : Vect (Suc n) a -> a で長さ1以上のvectorの先頭を安全に取り出す関数
私と型システムとポエム
最近巷では俄に型システムについての言及が増え、型システムポエマーが増えてる気がするので自分もその時流に乗りたい。 完全にポエムだけどなんかあったら随時指摘ください。直します。 TL;DR 言いたいことはまとめると次 型システムは程度問題なのでちょうどいいところを探すべき 型は万能でも強さが正義でもない(だから未だに研究されてる) よく知りもしないくせに計算機科学を侮辱するのはやめろ 予防線 あくまでポエムですので中身はないです 私は型理論専攻で学位はとったものの研究者ではないのであまり信用しすぎないように 型システムの過去 型システムは大まかに次のような利点があるとされてきた(個人的主観) 「異常」なプログラムを検出する仕組み 静的解析による分かりやすいエラーメッセージ 型そのもののドキュメント性 IDEでのcompletionに貢献 最適化に貢献 (数学に正しく裏打ちされたsemanti
Python と Ruby と typing - methaneのブログ
うーん、structural subtypingとダックタイピングは同じものなんだろうか。— Yukihiro Matsumoto (@yukihiro_matz) 2016年9月8日 https://t.co/5Rv86piThC wikipediaによると似て非なる物のようですね。 https://t.co/VwIg39h5M0— INADA Naoki (@methane) 2016年9月8日 この話題について補足しておきます。なお、僕はTAPL脱落組なのであまり正確性は期待しないでください。 背景 Ruby Kaigi で Matz が Ruby3 に向けて考え中の静的型について話されたようです。 少し前から、 Python でも Guido が Dropbox での大量のコードベースを改善していくために type hinting がほしいということで PEP 484 を始めました
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
