なぜ型ファーストで考えるのか - 貳佰伍拾陸夜日記

How do you imagine a building? You consciously create each aspect, puzzling over it in stages. Inception 型なし言語に馴染みはあるものの型付言語をいざ使ってみたらどういう気持ちで書いたらいいのかわからなかったと同僚から相談があり, それをきっかけにして社内の勉強会で以下の話をしました. よく型なし vs. 型付の文脈では「型を書くのは面倒だ」「安全の方が大事だ」「でも面倒だ」「それは型推論を前提にしていないからだ」などの議論になりがちな気がしますが、これはあくまで「計算ありきの型」を考えているからで, 「型ありきの計算」だと全く見え方が違います. 「型はある種の仕様」とおもえば, 型ファーストであることと, 型なし言語でテスト駆動開発(TDD)するときに最初にテストを書くこととは, 同じ

[hitotakuchan]

力作。「型のついた式」の定義によるけど、一般的には Scala,TypeScript,Haskell のプログラムはその型の証明にはならないよ。>Curry-Howard

[ysync]

高級言語のことはよくわからんけど、ワークメモリを適切に配分しなきゃならないASM的には先に型を固定するのは当然なのでな…。

[REV]

"高カ""インド型"に見えた。高い力でインド人を右に？

[Songmu]

TDDと型付けの類似性僕もなんとなく感じていたけど、さすがのアウトプット力。後でもう一回読み返そう。理解しきれないとは思うけど。

[quick_past]

スクリプト言語ってたいてい型がガバガバなんだけど、そういう世界の人たちがどうして、プログラミングという行為全般において、パラダイムの大変換を唱えたり、なんでもスクリプトでやろうとしたがるのか不思議。

[Cald]

宇宙も型/形をもつシステムで、型/形が生まれたゆえに物理制約（仕様）が生まれたとかで、宇宙論まで展開する型ファースト宇宙論者と、神様はいないので仕様も後付けの計算ファースト宇宙論者と論争、まで妄想した。

[anatofuz]

めっちゃいい

[Cherenkov]

型を書くのはテストを書きながらやるのと同じてことか

[griefworker]

「型は論理式、実装は証明」

[efcl]

⊥型について

[mizdra]

良い / 前半は何故型は仕様であると言えるのかを理論的に説明し，後半では仕様としての型の表現力の限界と表現力向上の取り組みについて紹介している

[zyzy]

最近型理論系の話題があんまり上がらなくなってた所に、久々にまとめとして来た感。話題が一周しだした。

[toitoitoi2718]

“variable”

[tomomii]

エントリ中の筆者コラムが読者にやさしい。スライドのサブタイトルにウフっとなりました

[Appakun]

“「型とはメモリ上のデータの扱い方を区別するためのもの」のような説明を目にするかもしれません. しかしこれは「データ型」の側面しかとらえておらず, ALGOLの系譜に偏った見方です. ” コラムよい

[tick2tack]

全部を理解できないけどつまみ読みでもおもしろい。Scalaの話多いのでありがたい。/“型システムは自由と安全のバランスの下に発展してきた”

[chintaro3]

GJ

[maharada]

鬼滅の刃の話ではなかった

[dwarfjp]

型あり言語だとスゴく守られてる感があって安心して開発を進められるんだけど、型なし言語をメインでやってる人ってそういう感覚無いのかな？Rustなんて過保護すぎて最初はコンパイル通すのも大変だよｗｗ

[nanika-sheila]

組み込みを先にやっていたので"型がない"の意味が最初わからなかった。型なし使える分野では、型は仕様って認識がない場合もあるのか。／個人で書くときは適当だけどね！

[natu3kan]

分野やモノによっては、ある程度自動でやってくれたり、その形式しかないみたいなのがあるから意識しないのはあるかも。

[wata88]

良い

[sakuragaoka99]

ガンダムじゃないのか

[tarchan]

＞何を証明したいか決めずに証明を書くヤツはいない

[mukaken]

“型ファーストが重要な理由をつきつめていくと, Curry-Howard同型対応があるからだなぁという結論に至った”

[qawsklp]

デバッグ大変そう‥

[h3poteto]

良き

[lunastera]

“何を証明したいか決めずに証明を書くヤツはいない”

[satomi_hanten]

計算ファーストにしたいと思うコードを書くことはほとんど無いけど、そやなぁ。

[yarumato]

“型ファーストと, 型なし言語でテスト駆動開発(TDD)するとき最初にテストを書くのは同じ。型ファーストが重要な理由をつきつめていくとCurry-Howard同型対応（型は論理式で式は証明）があるからという結論”

[tettekete37564]

スクリプト言語に遅い攻撃といい、なんというか世代が数巡してるんだなあって感想

[kibitaki]

そうそうこういうことを言いたかったんだよ俺も！（すいません言語化だけじゃなくいろいろ無理です「何を証明したいか決めずに証明を書くヤツはいない」のつまみ食いだけで精一杯です）