今日は『型、ついてますか？ - 型の本質を振り返る -』の日です
Posted on July 8, 2016
Tweet
型の本質を振り返 りに来てますので、メモをとります。
ゴリ押し抜きのマイクロソフトテクノロジー紹介 / mihochannel さん
- Windows Windows と言わなくなってきた
- OSSを重視
- azureでデプロイするためのライセンス
- 開発者特典 : MSアカウントがあれば $25 / 月 がついてくる
- 使うのであれば売りに行きます！
- .NET core も出たよ
型、ついてますか？ / 高野さん
メモは残しますが、内容に賛同するわけではありませんので悪しからず。
- 3時間で15人、1日で30人埋まってしまったので、拡充して100人
- 元ネタ「ライト、ついてますか」という本
- 問題解決の手引書らしい
- 型がどういう性質を持つのかを知る、のが型を議論するより先
- 高校からプログラミング、専攻はネットワーク、セキュリティ、言語処理、Smalltalk VM(バイト)
- 「できないことをやる」 日立、グリー、SORABITO
- 特定の言語ではなく、型、について
- 型が付いている == 静的型付けのこと
- 事前に変数の型を精査
- コンパイル、実行前のバグ発見
- 動的型付け
- 事前に変数の型を精査しない
- 評価によって型がわかる。実行時の型付け
- 静的型付け : コンパイルでは実行はしてない
- 実行ができるのは動的型付けだけ
- (原始は略)古代静的型付け : C言語。型が不明だとデータの扱い方がわからない
- 古代動的型付け : BASIC、シェルスクリプト
- システム記述の言語からユーザへの移行期
- システムコール呼べるシェルがある
- シェルを書く、という言葉に違和感(「IP」と呼ぶ違和感と一緒)
- 近代動的型付け : Perl
- sh + sed + awk + grep
- pearlは被った、shell(貝)との関連
- PCRE はperlのいい成果
- 近代静的型付け : C++
- オブジェクト指向
- PHP、Pythonも同じ時期
- 現代動的型付け Ruby、JavaScript
- 簡単にオブジェクト指向
- 現代静的型付け
- Java, Haskell, AltJS
- 強い形づけ。システム記述からの離脱。VM
- 原始動的型付け ニーモニック
a[2] == 2[a]ポインタ
- 原子静的型付け : 型ありラムダ計算
- 古代はユーザフレンドリー、近代は新しいパラダイムの上乗せ、現代はその先
- 動的型付けと静的型付けは交互に成長
- どちらも抽象化が進んでいく
- 静的な型付けと見せかけて動的な型付けとかやばい
- ミスマッチが起きると新しいもの
- ドメイン : 今はWEB
- ポートは「アプリケーション番号」と呼ばれてた
- パラダイム
- ドメインに対して有効なパラダイム
- 抽象化
- オブジェクト指向より進んだ抽象化
- 動作するUML
- リソース
- GC、OOPは昔はきつい処理と見なされてた
- 副作用を考慮したshellが欲しい
- lsは副作用がない。mkdirは副作用がある
- 作ると、エンジニアライフを豊かにする
- LLoTにて、型のセッションがあるので、そちらをお楽しみに
Linear Types / niryuu さん
- LTとかけてた(気が付かなかった)
- Linear Types : 一度しか値を得ることのできないようなもの
- 型が厳密な理由 → 規則が厳密なので
- λ計算 : 計算とは何か。論理学 : 論理とは何か
- Curry-Howard対応
- 論理の手法を型へ → LinearTypes
- 直観主義と単純型付きλ計算
- 時間、リソースの概念が抜けている
- 自然演繹がよく使われるが、シークエント計算に注目
- シークエント計算のWeakningとContractionが重要
- contractionはweakningはいつも成り立つのか？
- リソースを考えると
- Linear Logicの特徴
- 古典論理 : 正しい物を正しい物で書き換え。美しい
- 直観論理 : 証明する手続きが必要 (計算と相性がよい)
- 線形論理 : 古典と直感を合わせたもの。論理式を消費。新しい性質
- Linar Types
- !はなんどでも使えることを表す
- Clean、Rustなどで孫(の孫)みたいなものが使われている
- Wadlerが並行性や分散性に利用
- Scalaの作者など