Haskellの型システム(+拡張)を実装して学ぶ
導入 Mark P. Jones: Typing Haskell in Haskellという論文があります。この論文は、題通りHaskellでHaskellの型チェッカを実装するというものです。詳細な解説がされており非常にわかりやすく、また型システムの体系的な知識が無くても理解できるように構成されています。 しかしながら、この論文にはソースコードを入力にとって型チェックを行うまでに必要な実装の全ては含まれておらず、プログラムを入力に取って動作させるまでにはいくつかの変換や解析が必要です。Titan Type Checkerは、これら不足している機能(+拡張)を実装し、実際にスタンドアロンに動作する型チェッカを実装したものです。本記事では、論文で解説されていない事柄を中心に振り返りたいと思います。 Typing Haskell in Haskellの動作まで 構文解析 (Parser.hs)
Introductory resources to type theory for language implementers
This post briefly tours resources that helped introduce me to type theory, because I’m frequently asked by others for resources on this subject (even though I never had a formal education in type theory). Specifically, these resources will focus more on how to implement a type checker or type inference algorithm. Also, my post will be biased against books, because I don’t tend to learn well from r
アフィン型をPrologで実装してみた - Qiita
この記事は言語実装 Advent Calendar 2020の16日目の記事です。 Prologに慣れていない人のためにPrologでの単相の型システムを示し、線形型システムであるSystem-Fo(Fポップ)およびアフィン型システムSystem-Fa(Fアフィン)を実装例を示します。 アフィン型システムというとRustのオーナーシップの型システムが近いのですが、Rustのような型システムの本質的部分を取り出して実装したものがアフィン型システムです。難解な型システムの数式は嫌がらせのように感じるかもしれませんが、Prologを使えば実際に動かせるのでより理解しやすいものになっているはずです。 1. 単相型システムとlet多相型システム まずは、Prologで単純な型推論を作ってみます: % simple.pl :- op(500,yfx,$),op(600,xfy,:),op(600,xf
ML のサブセットの型推論器を Coq で検証する - fetburner.core
この記事は言語実装 Advent Calendar 2020 の5日目の記事です． 一度でも型推論器を書いたことがあれば，そのあまりの邪悪さ，あるいはその複雑さに恐れ慄いたことでしょう． 参照を用いて単一化を実現しようものなら構文木は参照に汚染され，純粋関数型に実装しようものなら大量の型代入をどのような順序で適用したものか悩まされる． これは Hindley-Milner 型推論器を実装する上での宿命のようなものです． 本記事では，MLのサブセット——型付きλ計算をletと参照で拡張した，let多相をサポートする言語——の型推論器を Coq で実装し，その正当性を証明します． Coq で検証を行うことで我々は型推論器のバグへの恐怖とデバッグの労力から真に解放され，枕を高くして眠ることができることでしょう． もっとも、型付きλ計算を let 多相で拡張した言語の型推論器の正当性は実はすでに証
Typing Haskell in Haskellを読んでみる - Qiita
頭の中の整理も兼ねて、Haskellの型システムについて述べたM.P.Jones氏による論文Typing Haskell in Haskellについてまとめていきたいと思います。 ※少しずつ加筆しています Section 2 : Preliminaries 最初のIntroductionは省略させていただきました（興味があったらぜひ読んでみてください） ここでは早速Haskellのコードが出てきますね。 まず module TypingHaskellInHaskell import Data.List (nub,(\\),intersect,union,partition) import Control.Monad (msum)
非可述多相に触れる： GHC の ImpredicativeTypes 拡張 - Qiita
data Maybe a = Nothing | Just a -- Maybe Int や Maybe String, Maybe (Maybe Bool) などが使える double :: (a -> a) -> a -> a double f x = f (f x) -- double :: (Int -> Int) -> Int -> Int や double :: (String -> String) -> String -> String として使える forall を含む型 上記の double 関数の型における a は型変数で、任意の型を動くことができます。forall キーワードを使ってこのことを明示すると forall a. (a -> a) -> a -> a となります。（forall キーワードの利用には ExplicitForAll 拡張が必要です） さて、通常
Haskellの型システムを書く(1) - 純粋関数型技術メモ
Haskell Advent Calendar 2017 3日目の記事です． Haskellの型推論器を実装し，型システムへの理解を深める． GHC拡張には型に関するものも多いが，今回は触れず標準のHaskellに従う． Hindley-Milner 型推論 シンプルなλ式に対する多相型推論器を考える． 構文 data Expr = Var String | App Expr Expr | Lam String Expr | Let String Expr Expr | Num Int data Type = TVar TVar | TCon String | TArr Type Type type TVar = Int data Scheme = Scheme [TVar] Type 式は変数・関数適用・λ式・Let束縛・リテラル，型は型変数・型コンストラクタ・関数型から成り立つ． 型ス
Prologで様々な多相型推論 - Qiita
この記事は時空を色々遡って、2017年の言語実装技術の12日目の記事として投稿するために色々と書き換えをしたものです。 11日目、16日目、20日目、21日目と型推論のオンパレードのようになっているので、Prologの記事も合わせて載せたいと思い書き換えて投稿させてもらいます。 概要 型理論、操作的意味論などの理論では一般的に一階述語論理が広く用いられていますが、多くのプログラマにとって馴染みがなく難しい数式に思えます。 Prologを使うことでその図を簡単に理解可能になります。例えば Prolog で多相型推論を記述した TIPER 1 で示されている環境を保存し copy_term 述語によって具体化する手法を用いるとわずか十数行で多相型推論を記述可能です。(付録 A) しかしながら、一般的な言語での実装をするには飛躍があります。そこでここでは、自由型変数を求め型スキームを求めるHin
OCaml でも採用されているレベルベースの多相型型推論とは - はやくプログラムになりたい
言語実装 Advent Calendar 2017 の16日目の記事です． GoCaml という OCaml のサブセットな言語を実装していて，多相型の型推論を実装するために論文を読んだり OCaml の実装をちょっと追ったりしていたので，その知識を整理する意味でこのエントリを書いています． この記事では OCaml の型推論器のベースになっている「レベルベースの多相型型推論アルゴリズム」について概略を直感的に説明しようと思います． 理論的になぜこのアルゴリズムで正しく動作するのかについてはこの記事で概要を把握した上で論文 のほうを読んでいただければ理解が速いと思います． また，この記事では最もシンプルな単相型のHM型推論については知っている前提で書きます． ご存知でない場合は， 住井先生の MinCaml の型推論実装の解説 五十嵐先生の型推論の解説 20日目の@uint256_t さん
Javaの "? extends" や "? super" の使い方をC#やScala風に考える - Qiita
なお Comparator は java.util パッケージに含まれるインタフェースで次のように宣言されています。 ? super や ? extends （下限または上限つきワイルドカード）は Java でジェネリクスを使う上で特に難しい部分です。比較的新しい言語（ C# 、 Scala 、 Ceylon など）では同じ目的のためによりシンプルでわかりやすいアプローチがとられています。 Java が採用した方法は Use-site variance annotation と呼ばれ、 C# などが採用した方法は Declaration-site variance annotation と呼ばれます。本投稿では Declaration-site variance annotation の考え方をベースに Java でどのように ? extends や ? super を使えば良いか につい
Javaのジェネリクスは「まがい物」ではない - kmizuの日記
先日、自分が書いた kmizu.hatenablog.com に対する反応として、「Javaのようなまがい物のジェネリクスと比較するのは適切でない」「Javaのジェネリクスと比較するのは適切でない」（おそらくC#や(C++等（2017/09/24追記）)の言語と比較して）といった コメントをいくつか見かけました（はてなブックマークコメントやツイッターなどで）。しかし、ここでは、そのような言説こそが適切でない、ということを言いたいです。なお、methane氏との 対話については既に終わったものなので、それとは関係ありません。 そもそも、Javaジェネリクスは、静的型付き関数型言語で既に一般的であったパラメータ多相をJavaに追加する目的で導入されました（C++テンプレートのようなものをJavaに追加するためだと思っている人がいるかもしれませんが、それは実態にあっていません）。実際、Java
変数に型がないということの利点について考える - 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ページを開く
GitHub - msp-strath/TypOS: being an operating system for typechecking processes
GitHub - tomprimozic/type-systems: Implementations of various type systems in OCaml.