型安全性とは結局何なのか | 黒曜の吹き溜まり
この記事は 第2のドワンゴ Advent Calendar 2016 の8日目です。 日付を跨いでいる？ またまたご冗談を、DST(ドワンゴスタンダードタイム)ではまだ8日ですよ。 ちなみに前日は…なんと誰も参加登録をしていませんでした！ 結構な勢いで埋まってたんですけど、唯一の空きですね。 前々日はdaneko0123さんでした。 一昨年のアドベントカレンダー記事が「関数型プログラミングとは結局何なのか」、去年の記事が「オブジェクト指向プログラミングとは結局なんなのか」ということで、3年目ともなると記事の方向性が固まりつつある雰囲気が漂いつつ、ネタ切れの空気も漂いつつあります。 そもそも去年の時点で既にドワンゴ社員ではないのにアドベントカレンダーには参加し続けている、というのもアレな話ですが。 なにを書くか考えたのですが、最近null安全に関する記事が話題になり、その中で「型」と「安全性
型システム 〜プログラムの安全性を支える数学〜 - Laborify
京都大学大学院 情報学研究科 通信情報システム専攻 修士2回生の五十嵐雄です．大学では，プログラミング言語理論，その中でも特に型システムの研究をしています． この記事では，私が特に力を入れて研究している漸進的型付けという種類の型システムについて紹介します．プログラムや型システムといった基本的な概念から解説していくので，プログラミング経験のない人も安心して読み始めてもらえたらと思います． はじめに プログラムとはコンピュータへの命令を記述したものです．2018年現在，私たちの生活は数多くのプログラムに支えられています． あなたがこの記事を Windows が入ったパソコンで見ているなら，まずその Windows がプログラムです．お家にテレビや冷蔵庫があれば，それらの中にもプログラムが内蔵されているでしょう．空いた時間にスマートフォンでゲームをするなら，遊んでいるゲームも全てプログラムです．
静的解析の限界、現実世界との境界
2018年に静的解析をとにかく強力につけまくるのは多分あんまりコストに見合わないのでよくない じゃあ静的解析を窓から投げ捨ててよいかというとそれはただの愚行 (以下、静的解析を普通に使えてる人には自明なことしか言いません) 私が最初に静的解析の限界を感じたのは多分依存型で遊んでいたとき 依存型の力はすごくて、まぁそれもそのはず命題論理から述語論理に進んで元への言及ができるので見かけ上表現力はとんでもなく上がるわけです。例えば「ある方程式を満たす解のみを受け取って何かする」みたいな関数が型として表現できるようになる。 一見すると最強に見えるんだけどこれは実質定理証明をすることなので、制限の強い型をつければつけるほど実装で苦しむ羽目になるということを割とすぐ痛感することになった。 例えば head : Vect (Suc n) a -> a で長さ1以上のvectorの先頭を安全に取り出す関数
変数に型がないということの利点について考える - Perl入門ゼミ
Perl › 読み物 PHPやPerlやRubyやPythonなどのスクリプト言語に対して、変数に型がないということを否定的にとらえる人もいるかと思います。特にC言語やJavaなどの静的言語を使ってきた人にとっては、型がないということが不安材料として目に映ることが多いのではないかと思います。 けれども、型がないということは、本当に素晴らしいことです。型がないことによって、たくさんの面倒から解放されるからです。 どのような型の値でも代入できる まず基本的なこととして変数に型がなければどのような型の値でも代入できるということです。つまり、受け取るときに、どのような型の値を受け取るのかを意識する必要がありません。 my $str = 'Hello'; my $num = 1; my $nums = [1, 2, 3]; my $person = {age => 2, name => 'taro'
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
