漸進的型付けの未来を考える

この記事はCAMPHOR- Advent Calendar 2017 11日目の記事です.

アブストラク

漸進的型付けは,ひとつの言語の中で静的型付けと動的型付けをスムーズに組み合わせるための技術です. よく知られた特徴は any 型を使った静的型付けで, TypeScript や Python といったプログラミング言語には既に実装されています. しかし,理論と実際のプログラミング言語の間には大きなギャップが存在します. 特に,漸進的型付けの理論で提案されているキャストを用いた動的型検査が実装されていないために, 静的型付けの恩恵を十分に得られていないという問題があります. この記事では,まず漸進的型付けの理論をコード例を用いて紹介し, 現状の漸進的型付き言語が抱える問題を解説します. そのあとで,漸進的型付き言語が目指すべき目標を理論的視点から論じます. それらの目標は,静的型付けを行うこと,キャストを用いた動的型検査を行うこと, 動的型検査を効率よく行うこと,型情報に基づいて最適化を行うことの4段階に分類することができます. 未だ実現されてないこれらの目標を論じることで, 多くの人に漸進的型付けの未来を考えてもらうのが本記事の目的です.

続きを読む

型クラスを含んだ型推論を概観する 〜Typing Haskell in Haskell より〜

この記事は CAMPHOR- Advent Calendar 18日目の記事です.

「Typing Haskell in Haskell (通称 thih)」から型クラスを含んだ型推論のエッセンスを紹介したいと思います. 多少専門的な内容ですが,なるべく多くの人に理解してもらえるように頑張ります.

論文のホームページは以下になります.論文本体とオリジナルの実装が利用できます.

Mark P Jones: Typing Haskell in Haskell

続きを読む

System F をHaskellとPythonで実装した

無事夏休みに突入して時間ができたので再びTaPLを読み始めました.半年触っていなくても進行,保存の証明が書けるあたり,春の自分はずいぶんしっかりと勉強していたようです.春は22章の型再構築まで読んでいたので,ひとまず23章のSystem Fから読んでサクッと実装しました.Pythonが書きたかったので,パーサーだけHaskellで書いてそれ以外をPythonで書くというよく分からない構成で実装していますが,いろいろと学びがあったのでそれを記していきます.

続きを読む

Haskellで簡単な正規表現を実装した【KMCアドベントカレンダー8日目】

KMCアドベントカレンダー8日目の記事です。

講義で正規表現とかオートマトンをちゃんと学んだので、Haskellの修行も兼ねて簡単な正規表現を実装しました。理論とか実装とかダルいと思うので、おまけだけ読むと楽しいかも知れません。 続きを読む