elmでやってみるシリーズ3: xeyesっぽい目が動く

elmでやってみるシリーズ3: xeyesっぽい目が動く。

import Mouse

-- 目の輪郭を書く
eyeframe x y = move (x,y) <| outlined { defaultLine | width <- 5 } <| oval 40 50

-- 目玉を書く
eyeball x y = move (x,y) <| filled black <| circle 5

-- 目(=目玉+目の輪郭)を一個分書く。tは目玉の見ている方向。
eye r x y t = [eyeframe x y, eyeball ((r * (cos t))+x) ((r * (sin t))+y)]

-- 目を2つ書く
eyes t = collage 200 200 <| (eye 15 -20 0 t)++(eye 15 20 0 t)

-- 「目の座標位置を計算する(=「マウス座標の原点から見た角度」をatanで求める)」という純粋関数にマウス座標をリフト適用。シグナル化された目玉の角度が返る。
mouseDirec = let f x y = (atan2 (100-(toFloat y)) ((toFloat x)-100))
           in f <~ Mouse.x ~ Mouse.y

-- 目を2つ書く、という純粋関数に、シグナル化された目玉の角度(mouseDirec)をリフト適用する。
main = eyes <~ mouseDirec

この簡潔さよ! ブラボー。Elm ブラボー。(さぼってますけどね。)

ブラウザ内で編集したり実行したい場合はこちらからどうぞ。

気づいたこと

• SignalはElmのFRPのキモである。Signalを制するものはElmを制する。
• mainの直下にSignalを使うReactive Codeを固めて、他はなるべくピュアにしたい、と思うじゃない。でもそれはたぶん無理な相談である。いや、やれるところはそうすれば良いと思うけど、「Signalを返す関数」はElmプログラミングにとって中核的であり最重要。それをどう組むべきかという問題からは逃げられない。
• 「なるべくピュアにしたい」という理由は、liftの適用は演算子<~,~があろうともやっぱり可読性に難があるから。今のElmにはセクションがないし、演算子関数をliftすると演算子っぽくなくなるし、flip駆使しても限界がある。もっと言えばSignalはモナドではないし*1、仮にモナドであってもElmにDo記法は無い。で、考えたのですが、ベストプラクティスとしてのコーディングパターンは、上でもしているように、lift一発でできないところは以下のように関数ごとに純粋部とリアクテイブ部に分けることではないかと今のところ思っております*2。なお今のElmはwhere句は使えません。

func = let f x y ... = 純粋コード
      in  f <~ Signal X ~ Singal Y ... -- 必要なSignalを使用するリアクティブコード

• 「{ defaultLine | width <- 5 } 」の記法は、指定したフィールドを更新した新しいレコードを返すというものである。Elmのレコードはすごく強力である。ちなみにレコードの拡張で型クラスを実現することも狙っているらしい。

関連エントリ

「Elmでやってみる」シリーズのまとめエントリ - uehaj's blog

*1:Signalがモナドでなくアプリカティブなのは理由があって、「SignalのSignal」を禁止するためだそうな。つまりSignalにjoinは定義できない・してはならない。bind/flatMapも然り。

*2:fは無名関数でも良いかもしれない。letのセマンティクスが無名関数とその適用に差があるのか、たとえばElmにlet多相があるかどうかは不明。

elmでやってみるシリーズ1: ●を動かす

elmでやってみるシリーズ1: ●を動かす。

import Window

pos : Signal Int
pos =let f = \tmp -> (tmp `mod` 30) - 10
        in f <~ foldp (\it acc-> acc + 1) 0 (fps 50)

drawCircle : Float -> Float -> Form
drawCircle x y = move (x,y) <| filled red (circle 20)

drawMatrix : [Form]
drawMatrix = map (\x -> drawLine <| x*10) [-10..10]

drawLine : Float -> Form
drawLine x = traced (solid blue) ( segment (x,-100) (x,100) )

main : Signal Element
main=let f = \w h p-> collage w h ([drawCircle ((toFloat p)*10) 10]++drawMatrix)
     in f <~ Window.width ~ Window.height ~ pos

続く。

感想

• foldpは好き。
• inputに対応するSignalってグローバル変数じゃね?まあ「マウスがクリックされる」とか「時間が経過する」という事実はグローバルなんだが、それによって引き起こされるイベントもそうなる…。プログラムからその値を能動的に制御できないから変数とは呼べない…のかな。でもユーザがフィールドに値を入力したり、ラジオボタンをクリックしたり、という操作によって設定項目をリアクティブに変更したその結果の、Signalである設定項目って、どう見てもグローバル変数だよね。まだよくわからない。

関連エントリ

「プログラムでシダを描画する」をelmで描画する

やや乗り遅れているネタとして、シダを描くというのを、elm言語でやってみました。
(追記： 改良版も作りました)

elm言語は、基本はHaskellライク文法(サブセット方向)に、F#とOCaml風味の演算子・文法を振り掛けた、ヒンドリーミルナー型推論・純粋関数型・正格評価の言語で、repl上もしくは主にJSにコンパイルしてブラウザ内で実行します*1。特徴はFRP,ファンクショナルリアクティブプログラミングをサポートする言語だということです。

以下がシダを描画するelmコード。もっといい書き方あると思うので気付いたらご指摘お願いします。

import Mouse
import Generator
import Generator.Standard

sida_width=500
sida_height=500

randomSeed = 12346789
gen = Generator.Standard.generator randomSeed
main = collage (sida_width*2) (sida_height*2) <~ ((f0 13 0 0 gen) <~ (flip (/) sida_width <~ (toFloat <~ Mouse.x)))

-- Original: w1x x y = 0.836 * x + 0.044 * y
w1x x y n = n * x + (1-n) * y
w1y x y = -0.044 * x + 0.836 * y + 0.169
w2x x y = -0.141 * x + 0.302 * y
w2y x y = 0.302 * x + 0.141 * y + 0.127
w3x x y = 0.141 * x - 0.302 * y
w3y x y = 0.302 * x + 0.141 * y + 0.169
w4x x y = 0
w4y x y = 0.175337 * y

f0 k x y gen0 n =
     let (seq, _)=f k x y gen0 n
     in [(move (0,0)) (filled black <| rect (sida_width*2) (sida_height*2))
     ]++seq

f k x y gen0 n =
    if (0 < k) then
      let (rnd1, gen1) = Generator.int32 gen0
          (seq1, gen2) = (f (k - 1) (w1x x y n) (w1y x y) gen1 n)
          (seq2, gen3) = if (rnd1 `mod` 3 == 0) then (f (k - 1) (w2x x y) (w2y x y) gen2 n) else ([], gen2)
          (seq3, gen4) = if (rnd1 `mod` 3 == 1) then (f (k - 1) (w3x x y) (w3y x y) gen3 n) else ([], gen3)
          (seq4, gen5) = if (rnd1 `mod` 3 == 2) then (f (k - 1) (w4x x y) (w4y x y) gen4 n) else ([], gen4)
      in
          (seq1 ++ seq2 ++ seq3 ++ seq4, gen5)
    else
        ((plot (x * sida_width * 0.98)
               (y * sida_height * 0.98)), gen0)

plot x y = [move (x,y) (filled green <| rect 1 1)]

リアクティブプログラミングというのは、私の理解では、時間経過とかマウスクリックとか、なんらかの(外部/外部)イベントに刻々と反応することの記述を容易にできるってことです(雑すぎる説明)。それがファンクショナルなのは、関数型ってことで、elmはさらにピュア・ファンクショナルなので副作用は記述できません。Signalというのが「変化する値」を表わしていて、これはHaskellのIOアクションが副作用を一手に背負っているようなものです。SignalはしかしモナドではなくArrowで、これでFRPを実現しているのを Arrowized FRPと呼ぶとか。ただそこらへんの詳しいことはわからなくても書けます*2。

上記のコードは、マウスのx座標で反応するようにしました。FRPなのはmainだけであとは全部ピュアな関数です。x座標に対応して、シダの図のどのパラメータをどう動かすかは、適当にやったので動きは不自然です。あと再帰の深さを深くすると非常に遅くなります。Canvasに書き捨ててるんじゃなくて、描画命令(Form,形状)をリストで持ってるからです。

以下にはコンパイル結果のJSを登録しましたので、ブラウザ上で実際に動かして試すことができます。マウスを左右に動くとなんか動くわけです。

• http://js.do/uehaj/40320

以下は、静止画像のスナップショットです(なので動きません)。

枝ぶりが貧弱なのは、速度上の問題ですorz。

以下はelm_dependencies.jsonの内容。標準関数以外には、random generatorというのを使っています。

{
    "version": "0.1",
    "summary": "concise, helpful summary of your project",
    "description": "full description of this project, describe your use case",
    "license": "BSD3",
    "exposed-modules": [],
    "elm-version": "0.12.3",
    "dependencies": {
        "jcollard/generator": "0.3"
    },
    "repository": "https://github.com/USER/PROJECT.git"
}

elmについては別途紹介記事を書くつもり。

「Elmでやってみる」シリーズのまとめエントリ - uehaj's blog

*1:elmをAltJS、すなわちJSの他の選択肢(オルタネティブ)と言うべきなのかはわからない。言うならばJS+CSS+HTML+DOM全体のオルタネティブな気がする。

*2:ちなみにdo記法もproc記法もelmにはありません。lift(n)もしくはアプリカティブスタイルを使って書きます。Haskellの<$>は<~、<*>は~に対応。

オブジェクト指向だけじゃない開発宣言

Manifesto for Not Only Object-Oriented Development、オブジェクト指向だけじゃない開発宣言、というのが出てましたのでごにょと訳してみました*1。

オブジェクト指向だけじゃない開発宣言

私たちは、ソフトウェア開発の実践
あるいは実践を手助けをする活動を通じて、
よりよい開発方法を見つけだそうとしている。
この活動を通して、私たちは以下の価値に至った。

クラスよりも、関数と型を、
可変性よりも、純粋性を、
継承よりも、コンポジションを、
メソッドディスパッチよりも、高階関数を、
nullよりも、Optionを、

価値とする。すなわち、左記のことがらに価値があることを認めながらも(但しnullは除くが)、私たちは右記のことがらにより価値をおく。

内容は、「今どきのオブジェクト指向開発宣言」と名乗ってもあんまり違和感ないっす。
ただし、null、おめーは別だ。

追加希望
正格評価よりも、非正格評価を、
チューリングマシンではなく、SKコンビネータを、

追記：この翻訳が本家の日本語訳に採用されました。

*1:元ネタがアジャイル開発宣言のパロなので、訳も借用させてもらいました。

Hindley-Milner型推論アルゴリズムをGroovyで書いてみた

こないだ「Haskellのforallについて理解したことを書いておく(ランクN多相限定)」の記事を書いたときにHindley-Milner型推論アルゴリズム*1を調査するにあたって、こちらにある「Scala by Example」の16章にあるScalaでの実装例をGroovyに書きなおしたので晒しておきます。

以下のような型検査・推論ができます。実行はできません。

def listLenTest = LetRec('len',
                         Lam('xs',
                             App(App(App(Var('if'),
                                         App(Var('isEmpty'), Var('xs'))),
                                     Var('zero')),
                                 App(Var('succ'),
                                     App(Var('len'),
                                         App(Var('tail'),
                                             Var('xs'))))
                                )),
                         App(Var('len'),
                             App(
                                 App(Var('cons'),
                                     Var('zero')),
                                 Var('nil'))
                            )
                        );
assert listLenTest.toString() == 'letrec len = λ xs . (((if (isEmpty xs)) zero) (succ (len (tail xs)))) in (len ((cons zero) nil))'
assert typeInfer.showType(listLenTest) == "Int[]"

型理論としてのHMを理論的に(型付ラムダ計算の定理の集合として)理解して実装しているわけではないのですが、先の「Scala By Example」の著者はScala開発者にしてJava Genericsの開発者、著名なる型理論学者Martin Odersky先生様その人ですので、プログラムの動作としてはまあ間違いはないと思っています。

コードから読み取ったことについて、多数のコメントを追記してあります。また、テストコードも追加したフルバージョンはこちらのgistにのせました。

Hindley-Milner型推論の特徴は、

• 双方向性。左辺・右辺の型、仮引数と実引数、宣言の型と使用側が期待する型、リターンしている型と返り値宣言の型、など、どっちかが決まれば、どっちかが決まるのだが、HMでは前後関係も関係なく、双方向で決まる。ここはScalaとかJava7/8とかGroovyの「型推論」と大きく異なる*2。
• 上の結果でもあるが、明示的な型宣言が(多くの場合?)不要*3。リテラルの型さえ決まっていれば、波及して型が決まる。矛盾があれば、エラーになる。字面上、明示された型指定が全く無いのに、例外無くすべて宣言されているのと同じように扱われる。もし決まらなければ(「\a->a」など)、自動的に多相型になる。
• 多相型に対応。つまり以下のコードはGenericsに対応している。こんな簡潔なコードなのに!!
• 多相型の解決と型推論の統合。つまり「型推論の開始時に未知の型」は、「多相型の型変数」と同じ枠組みで扱われて解決しようとする。
• 多相型の解決は識別子の使用を契機とするが、let変数とlambda変数では多相型解決についての意味上の違いがある。詳細はコメント参照。

でしょうかね。
Hindleyによって論文が書かれたのが1969年とのこと。なんかもう。

で、Groovy 2.1のカスタムタイプチェッカとしてHMを実装してみる野望(ゴゴゴゴ)*4

import groovy.transform.*
import static TypeInfer.typeInfer

@InheritConstructors
class TypeError extends Exception {}

/**
 * 構文木や式木をnewキーワード無しでオブジェクトを生成するために、
 * @Newify AST変換を適用するアノテーション@ApplyNewifyを定義する。
 *  @AnnotationCollectorは、Groovyの合成アノテーション作成機能。
 *  [annotations]* @AnnocationCollector @interface 新規アノテーション {}
 * で、[annotations]*を指定したのと等価な新規アノテーションを作成する。
 */
@Newify([Var,Lam,App,Let,LetRec,Tyvar,Arrow,Tycon])
@AnnotationCollector @interface ApplyNewify {}

/**
 * Termおよびそのサブクラスによって構文木を構成する項を定義する。
 * 項とは以下のいずれか。
 *   - 変数(Var)
 *   - λ抽象(Lambda)
 *   - 関数適用(App)
 *   - let式(Let)
 *   - letrec式(LetRec)
 * @Immutable AST変換を適用するとTupleConstructorと同様に、
 * メンバーを引数で初期化するコンストラクタが生成される。
 */
interface Term {}
@Immutable class Var implements Term { String x
    @Override String toString(){ x } }
@Immutable class Lam implements Term { String x; Term e
    @Override String toString(){ "λ $x . $e" } }
@Immutable class App implements Term { Term f; Term e
    @Override String toString(){ "($f $e)" } }
@Immutable class Let implements Term { String x; Term e; Term f
    @Override String toString(){ "let $x = $e in $f" } }
@Immutable class LetRec implements Term { String x; Term e; Term f
    @Override String toString(){ "letrec $x = $e in $f" } }

/**
 * Typeおよびそのサブクラスによって式木の構成要素を定義する。
 * 型とは以下のいずれか。
 *  - 型変数(Tyvar)
 *  - 関数型(Arrow)
 *  - 型コンストラクタ呼び出し(Tycon)(具体型)
 * 型変数を含む型を多相型と呼ぶ。
 */
interface Type {}
@Immutable class Tyvar implements Type { String a
    @Override String toString(){ a } }
@Immutable class Arrow implements Type { Type t1; Type t2
    @Override String toString(){ "($t1 -> $t2)" } }
@Immutable class Tycon implements Type { String k; List<Type> ts = []
    @Override String toString(){ k + "[${ts.join(',')}]" } }

/**
 * Substは「型に含まれる型変数の置換処理」を表わす。
 * Subst represent a step of substitution of type variables of polymorphic type.
 *
 * Substはcallメソッドが定義されているので、Subst(のサブクラス)のイ
 * ンスタンスに対して関数のように呼び出すことができる(Groovyの機能)。
 * 例えばx = new Subst(); x(..)と呼べるということ。
 * 2種類の引数の型に対してcallが定義されている。
 * 
 *  - call(Type)
 *    型中に含まれる型変数を置換する。
 *  - call(Env)
 *    Envに含まれるすべての型スキーマに含まれる型変数を置換したEnvを返す。
 * 
 * 実装機構としては、Substのサブクラスのインスタンス1つは、「Innerクラ
 * ス→内部クラスを含むOuterクラスのインスタンス」、それをまた含む
 * Outerクラス…というチェインを構成する。そのチェインは複数の置換処理
 * を連鎖である。callはOuterクラスのcallを呼び、という再帰処理が行なわ
 * れるので、複数の置換が適用できる。Innerクラスのインスタンスを作成す
 * るには、extendを呼ぶ。
 */
@ApplyNewify
abstract class Subst {
    /**
     * 指定した型変数の置換結果を返す。
     * SubstのOuter/Innerクラス関係から構成されるチェインを辿って探す。
     */
    protected abstract Type lookup(Tyvar x)
    abstract String toString()

    /**
     * 型Type t中に含まれる型変数を置換した結果の型を返す。
     * 型に含まれる型変数(つまり多相型の型変数)の変数を、変化しなく
     * なるまでひたすら置換する。置換の結果がさらに置換可能であれば、
     * 置換がなされなくなるまで置換を繰り返す。(循環参照の対処はさ
     * れてないので現実装は置換がループしてないことが前提)。
     */
    Type call(Type t) {
        switch (t) {
        case Tyvar: def u = lookup(t); return (t == u) ? t : call(u)
            // TODO: this code could throw stack overflow in the case of cyclick substitution.
        case Arrow: return Arrow(call(t.t1), call(t.t2))
        case Tycon: return Tycon(t.k, t.ts.collect{owner.call(it)})
        }
    }

    /**
     * 環境Env eに含まれるすべての型スキーマに含まれる型変数を置換した
     * Envを返す。
     */
    Env call(Env env) {
        env.collectEntries { String x, TypeScheme ts ->
            // assumes tyvars don't occur in this substitution
            def tmp = new TypeScheme(ts.tyvars, owner.call(ts.tpe))
            [x, tmp]
        }
    }

    /**
     * Innerクラスのインスタンスを生成する操作がextend()であり、「1つの
     * 型変数を一つの型へ置換」に対応するインスタンス1つを返す。ただし
     * extendで生成されたインスタンスは、extendを呼び出した元のオブジェ
     * クト(extendにとってのthisオブジェクト) =Outerクラスのインスタン
     * スとチェインしており、さらにcallにおいて、Outerクラスを呼び出し
     * て実行した置換の結果に対して追加的に置換を行うので、元の置換に対
     * して「拡張された置換」になる。
     */
    Subst extend(Tyvar x, Type t) {
        new Subst() {
            Type lookup(Tyvar y) {
                if (x == y) t else Subst.this.lookup(y)
            }
            String toString() {
                Subst.this.toString() + "\n$x = $t"
            }
        }
    }

    /**
     * 初期値としての空の置換を返す。
     * 任意のSubstインスタンスについて、OuterクラスのOuterクラスの…
     * という連鎖の最終端となる。
     */
    static final Subst emptySubst =  new Subst() {
        Type lookup(Tyvar t) { t }
        String toString() { "(empty)" }
    }
}

/**
 * TypeSchemeは、型抽象(∀X.T)を表わす。
 * 型抽象とは、「型引数」を引数に取り、型変数を含むテンプレートのよう
 * なものを本体とするような、λ式のようなもの。
 *
 * TypeSchemeはTypeを継承していない。その結果、Typeの構造の途中に
 * TypeSchemeが表われることもない。
 *
 * Haskellの「forall.」は型スキーマ(型抽象)に対応しているが、このHMアル
 * ゴリズムでは型スキーマ(抽象)はトップレベルの環境における識別子に直接
 * 結びつく形でしか存在しない。つまりランクN多相を許していない。
 *
 * もしTypeSchemeが型の一種であり、型構造の任意の部分に表われ得るなら
 * (つまりmgu()やtp()の型推定の解決対象の型コンストラクタなら)、ランク
 * N多相が実現されることになる。
 */
@Canonical
class TypeScheme {
    /**
     * tyvarsは型抽象において全称量化された型変数の集合を表す。
     * tyvars are set of universally quantified types in the type scheme.
     *
     * tyvarsは「その外側に対して名前が衝突しないことの保証」を持った型
     * 変数である。なぜなら型スキーマの使用に際してnewInstance()するこ
     * とでtpe中でのtyvars変数の使用がリネームされるからである。
     *
     * 具体的には、プログラム中にVar(x)の形で識別子xが使用されるとき、
     * 識別子xの型を得るために、環境に登録された「xに対応する型スキーマ」
     * を取得した上で、Type型に変換する処理(TypeScheme.newInstance())が
     * 行なわれる。newInstance()は、type中のtyvarsと同じ名前を持った変数
     * を、すべて重ならない新規の名前にリネーム置換したバージョンのtpe
     * を返す。
     */
    List<Tyvar> tyvars
    
    /**
     * 型のテンプレートを表わす。全称量化されている型変数と同じ型変数を
     * 含んでいれば、その型変数は、型スキーマがインスタンス化されるとき
     * に重ならない別名に置換される。
     */
    Type tpe

    /**
     * 型スキーマ(型抽象)を型に具体化する操作。
     *
     *    newInstance: TypeSchema → Type
     *
     * ちなみにgen()は反対に型から型スキーマを生み出す操作である。
     *
     *    gen: Type → TypeSchema
     * 
     * newInstance()は、全称限量指定された変数およびそれに束縛された変
     * 数(つまりフリー型変数を除いた全ての型変数)の使用を、新規の変数名
     * にリネームする。この操作の結果は、環境には左右されず、
     * TypeSchemeインスタンスのみの情報によって確定される。(変数名のシー
     * ドとなるtypeInfer.nの値には依存するが)
     * 
     * newInstance()の結果として得られる型には全称限量で指定されていた
     * 型変数は含まれない。たとえば、型スキーマ
     * 
     *    TypeSchema s = ∀ a,b . (a,b型を含む型)
     * 
     * に対して、newInstanceした結果は、
     * 
     *      s.newInstance() = (a',b'型を含む型)
     * 
     * であり、a,bは、a'b'に置換されるので、結果の型には決して現われな
     * い。
    */
    Type newInstance() {        
        tyvars.inject(Subst.emptySubst){ s, tv -> s.extend(tv, TypeInfer.instance.newTyvar())} (tpe)
    }
    String toString() { "∀ (${tyvars.join(',')}) . ($tpe)" }
}

/**
 * 環境Envは、プログラムのある位置における、識別子と型情報(型スキー
 * マ)の対応表である。
 * Env is map of identifier to type schema.
 * 環境Envは、意味的には型変数を含む制約の集合と見做すことができる。
 * Env can be regarded as set of constraints of relationships concerning
 * types include type variables. So HM type checker is constraints solver for it.
 * 環境は、tp()が解くべき、型方程式の制約条件を表現している。
 *     Env: 「プログラム中の識別子→型スキーマ」の対応の集合
 * 
 * ちなみに、Substもある種の対応表であるが、型変数の書き換えルールの
 * 集合。
 * 
 *     Subst: 「型変数→型(型変数|Arrow|Tycon)」という書き換え規則の集合
 * 
 * なお、明かにこの実装は空間効率が悪い。Scalaではタプルのリスト(連想リ
 * スト)で実現されていたところをGroovy化する際に、安易にMapにしてコピー
 * して受け渡すようにしたが、実用的には連想リストにすべき。
 */
@InheritConstructors
@ApplyNewify
class Env extends LinkedHashMap<String, TypeScheme> {
}

/**
 * TypeInferはHM型推論の全体を含む。Scalaではオブジェクトだったので、
 * @Singletonとして定義してある。サービスメソッドを呼び出すための静的
 * import可能な変数として、static typeInferを容易してある。
 * 型チェックの全体の流れは、
 *
 * showType ->  predefinedEnv
 *          ->  typeOf         ->    tp  ->  mgu
 *
 * である。
 */
@ApplyNewify
@Singleton
class TypeInfer {

    int n = 0
    def reset() {
        n = 0
    }
    
    /**
     * 名前が重ならない新規の型変数を作成する。
     */
    Type newTyvar() { Tyvar("a${n++}") }

    /**
     * 環境中にで定義された識別子xに対応する型スキーマを取得する。
     */
    TypeScheme lookup(Env e, String x) {
        return e.get(x)
    }

    /**
     * 型tに含まれているすべての型変数の集合(A)から、この環境に登録され
     * ているすべての型スキーマの「全称量化に関するフリー型変数の集合
     * (※1)」=(B)を除外したもの((A)-(B))を全称量化することで型スキーマ
     * を生成する。
     *
     * (※1)λx.yのとき変数xに束縛されていることを「λ束縛」と呼び、
     *     「λ束縛されていない変数」をフリー変数と呼ぶが、それと同様に、
     *     型変数に関する∀y...のとき型変数yに束縛されていることを「全
     *     称量化束縛」と呼び、「全称量化束縛」されていない型変数を「全
     *     称量化に関するフリー型変数」とする(ここで作った言葉)。
     *
     * 環境において「全称量化に関するフリー型変数」が発生するケースとい
     * うのは、具体的にはラムダ式
     *
     *    λ x . y
     *
     * において、識別子xに対応する型は、新規の型変数として環境に登録さ
     * れ、そのもとでyが型推論されるが、y解析中でのxの登場はスキーマ内
     * で全称量化されていない、という状態である。
     */
    TypeScheme gen(Env env, Type t) {
        new TypeScheme(tyvars(t) - tyvars(env), t)
    }

    /**
     * 型に対するtyvars()は、指定した型Type t中に含まれる型変数のリスト
     * を返す。
     */
    List<Tyvar> tyvars(Type t) {
        switch (t) {
        case Tyvar: return [t]
        case Arrow: return tyvars(t.t1) + tyvars(t.t2)
        // 型コンストラクタ T[a,b]のとき、Tは型変数ではない。
        case Tycon: return t.ts.inject([]) { List<Tyvar> tvs, Type elem -> tvs + tyvars(elem) }
        }
    }

    /**
     * 型スキーマに対するtyvars()は、指定した型スキーマTypeSchema tsの
     * 型テンプレート(ts.tpe)が使用している型変数から、全称量化された変
     * 数(ts.tyvars)を除外したものを返す。これは、何かというと、型スキー
     * マの型テンプレート(TypeSchema.tpe)が含む「全称量化に関するフリー
     * 型変数)の集合」である。
     */
    List<Tyvar> tyvars(TypeScheme ts) {
      tyvars(ts.tpe) - ts.tyvars
    }

    /**
     * 環境Envに対するtyvarsは、その環境に登録されているすべての型スキー
     * マに対するtvarsの値全体を返す。
     * つまり、環境全体が含む「全称量化に関するフリー変数の集合」を返す。
     */
    List<Tyvar> tyvars(Env env) {
        env.values().inject([]){ acc, it -> acc+tyvars(it)}
    }

    /**
     * 型tと型uのユニフィケーション。
     * 型tと型uに対してs'(t) s'(u)が一致するような、sを拡張した置換s'
     * を返す。
     */
    Subst mgu(Type t, Type u, Subst s) {
        def (st, su) = [s(t), s(u)]
        if (st instanceof Tyvar && su instanceof Tyvar && st.a == su.a) { return s } // 等しい型変数
        else if (st instanceof Tyvar) { return s.extend(st, su) } // 左辺が型変数
        else if (su instanceof Tyvar) { return mgu(u, t, s) } // 右辺が型変数
        else if (st instanceof Arrow && su instanceof Arrow) { // Arrow同士
            return mgu(su.t1, st.t1, mgu(su.t2, st.t2, s))
        }
        else if (st instanceof Tycon && su instanceof Tycon && st.k == su.k) {
            return zip(st.ts, su.ts).inject(s) { acc, it -> mgu(it[0], it[1], acc) }
        }
        throw new TypeError("cannot unify $st with $su")
    }

    /**
     * 二つのリストxs=[x1,x2,x3..], ys=[y1,y2,y3]のとき、
     * [[x1,y1],[x2,y2],[x3,y3]..]を返す。
     */
    static zip(xs, ys) {
        if (xs.size() != ys.size()) {
            throw new TypeError("cannot unify $xs with $ys, number of type arguments are different")
        }
        Iterator itor = ys.iterator()
        xs.collect { [it, itor.next()] }
    }

    /**
     * エラーメッセージに含めるための、処理中の項への参照。
     */
    Term current = null

    /**  
     * envのもとで、eの型がt型に一致するためのsを拡張した置換s'を返す。
     * 数式で書くと以下のとおり。
     *
     *    s'(env) ├ ∈ e:s'(t)
     *  
     * つまり、型の間の関係制約式(型変数を含む)の集合envのもとで、「s'(env)の
     * 型はs'(t)である」を満たすような、sを拡張した置換s'を値を返す。
     */
    Subst tp(Env env, Term e, Type t, Subst s) {
        current = e
        switch (e) {
        case Var:
            // 変数参照eの型は、eの識別子e.xとして登録された型スキーマを実体化(全称量
            // 化された変数のリネーム)をした型である。
            TypeScheme u = lookup(env, e.x)
            if (u == null) throw new TypeError("undefined: "+e.x)
            return mgu(u.newInstance(), t, s)
        case Lam:
        
            // λで束縛される変数とletで束縛される変数の扱いの違いにつ
            // いて。
            // 変数(識別子)は、HMの多相型の解決において、キーとなる存在
            // である。型スキーマは変数(識別子)にのみ結びつく。変数を介
            // 在して得た型スキーマを基軸に、インスタンス化=全称量化=型
            // 変数置換が実行される。
            //
            // 識別子x,yに束縛される式が多相型であるとき、型変数の解決
            // の扱いに関して両者には違いがある。
            //
            // λx.eの場合、xに対応して環境に登録されるのは、xの型を表
            // わす新規の型変数(a = newTyvar())を型テンプレートとする型
            // スキーマ(型抽象)であり、かつaについては全称限量されない。
            // つまり「全称量化に関するフリー型変数を含む型スキーマ」に
            // なっている。
            //
            // let y=e1 in e2の場合、yに対応して環境に登録されるのは、
            // e1の型を元にして、e1中の型変数群
            // 
            // 「e1.tyvars-tyvars(e1.e)」…(*)
            // 
            // を全称限量した型スキーマ(型抽象)。例えば「new
            // TypeScheme(tyvars(e1), e1)」が登録される。
            // なお、(*)における、tyvars(e1.e)は、e1中のフリー型変数だ
            // が、これが生じるのは、λ束縛の本体の型検査の場合である。
            // つまり
            //
            //   \ x -> let y=e1 in e2
            //
            // のように、λ本体の中にlet式が出現するときに、let束縛され
            // る識別子yのために登録される型スキーマでは、xに対応する型
            // スキーマで使用されている型変数がフリーなので全称限量対象
            // から除外される。
            // 
            // [ここでのλとletの違いがどのような動作の違いとして現われるか?]
            // 
            // Haskellで確認する。
            // 
            // ghci> let x=length in x [1,2,3]+x "abc"
            // 6
            // ghci> (\ x -> x [1,2,3]+x "abc") length
            //         <interactive>:5:12:
            //     No instance for (Num Char)
            //       arising from the literal `1'
            //     Possible fix: add an instance declaration for (Num Char)
            //     In the expression: 1
            //     In the first argument of `x', namely `[1, 2, 3]'
            //     In the first argument of `(+)', namely `x [1, 2, 3]'
            //
            // letでのxに束縛された多相関数lengthの型(a->a)における型変
            // 数aは全称限量される(Haskell流に書くとforall a.a->a)ので、
            // 「x [1,2,3]」と「x "abc"」それぞれにおけるxの出現それぞ
            // れでaがリネームされ(1回目はa',二回目はa''など)、別の型変
            // 数扱いになる。そのため、a'とa''がそれぞれのIntとCharに実
            // 体化されても、型エラーにならない。
            // 
            // λの場合、xの型は全称限量されない(a->a)なので、a=Intと
            // a=Charの型制約が解決できず型エラーとなる。この動作はテス
            // トケースtestTpLamP2()、testTpLetP1() で確認する。
            def (Tyvar a, Tyvar b) = [newTyvar(), newTyvar()]
            Subst s1 = mgu(t, Arrow(a, b), s)
            return tp(new Env(env)+[(e.x):new TypeScheme([], a)], e.e, b, s1)
        case App:
            Tyvar a = newTyvar()
            Subst s1 = tp(env, e.f, Arrow(a, t), s)
            return tp(env, e.e, a, s1)
        case Let:
            // λ x ...で束縛される変数とlet x= ..in..で束縛され
            // る変数の違いについては前述の通り。
            Tyvar a = newTyvar()
            Subst s1 = tp(env, e.e, a, s)
            return tp(new Env(env) + [(e.x):gen(s1(env), s1(a))], e.f, t, s1)
         case LetRec:
             def (Tyvar a, Tyvar b) = [newTyvar(), newTyvar()]
             def s1 = tp(new Env(env) + [(e.x):new TypeScheme([], a)], e.e, b, s)
             def s2 = mgu(a, b, s1)
             return tp(new Env(env) + [(e.x):gen(s2(env), s2(a))], e.f, t, s2)
         }
    }

    /**
     * 環境envにおいてTerm eの型として推定される型を返す。
     */
    Type typeOf(Env env, Term e) {
      def a = newTyvar()
      tp(env, e, a, Subst.emptySubst)(a)
    }

    /**
     * 既定義の識別子(処理系の組み込み関数もしくはライブラリ関数を想定)を
     * いくつか定義した型環境を返す。型のみの情報でありそれらに対する構
     * 文木の情報はない。
     */
    Env predefinedEnv() {
        Type booleanType = Tycon("Boolean", [])
        Type intType = Tycon("Int", [])
        Closure<Type> listType = { Type t -> Tycon("List", [t]) }
        Closure<TypeScheme> gen = { Type t -> gen(new Env(), t) }

        def a = newTyvar()
        return new Env(['true':gen(booleanType),
                       'false':gen(booleanType),
                       'if':gen(Arrow(booleanType, Arrow(a, Arrow(a, a)))),
                       'zero':gen(intType),
                       'succ':gen(Arrow(intType, intType)),
                       'nil':gen(listType(a)),
                       'cons':gen(Arrow(a, Arrow(listType(a), listType(a)))),
                       'isEmpty':gen(Arrow(listType(a), booleanType)),
                       'head':gen(Arrow(listType(a), a)),
                       'tail':gen(Arrow(listType(a), listType(a))),
                       'fix':gen(Arrow(Arrow(a, a), a))]) 
    }

    /**
     * 項の型を返す。
     */
    String showType(Term e) {
        try {
            typeOf(predefinedEnv(), e).toString()
        } catch (TypeError ex) {
            "\n cannot type: $current"+
                "\n reason: ${ex.message}"
        }
    }

    /**
     * @Singleton宣言したクラスのシングルトンはTypeInfer.instanceで保持
     * されており、クラス外からも取得できる。しかし、
     * 「TypeInfer.instance」が少し冗長なのと、Scala版に合せるため、シ
     * ングルトンを以下で定義する静的変数TypeInfer.typeInferで取得でき
     * るようにする。ただしSingletonの初期化タイミングの都合上か、遅延
     * 設定のAST変換@Lazyを指定しないとうまくいかないようである。
     */
    @Lazy static typeInfer = TypeInfer.instance
}

テストコードつきはこちら。

上記は元コード同様関数型っぽい作りになってる(Substによる実現とか)が、書き換えを許す前提でならもっと簡潔になりそう。型変数の一意性保証のために「型変数名」とかの置き換えにたよらず、型変数オブジェクトを単にシェアすればいいんじゃないかな…。

*1:もしくはDamas–Milner or Damas–Hindley–Milnerとしても知られているとのこと。

*2:HMと比べると果してそれらが「推論」と呼べるのかどうか…。

*3:実言語では、常にはそうならないケースもあると思われる。ランクN多相とかにとどまらず。あと、実用上は宣言しないと、人間がついていけない(デバッグできない。)という問題もあり、適宜宣言するのだろう。

*4:型に継承関係があると難しそうだ。

HaskellにおけるIOモナドとSTモナドの関係

HaskellにおけるIOモナド(IO a型)とSTモナド(ST s a型)について整理してみました。

IOの定義から知るST

IOモナドの考え方についての原論文に相当する「Lazy Functional State Threads」においては、IOの定義は

newtype IO a = ST RealWorld a

のようにST型を直接使用して定義されるものとして説明されています。ただ、「IO inside」によれば、GHCのライブラリ実装においてIO aの定義は

newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))

だそうで直接STを使ってはいません。後者のは正格タプル非ボックス化タプルを使ってます(知らん!)。

まあ、Haskell仕様ではIO aと関数仕様が定義されているだけで=の右側は実装依存というわけなのでしょう。

IOモナドとSTモナドとの機能的関係

直接的な利用関係があるかどうかはともかく、記事「第7回 入出力と遅延評価の間を取り持つIOモナド - ITpro」からすると

STモナドは、「状態」を参照型などのより効率の良い仕組みで利用できるようにするため、IOモナドと同じ技術を使って実装されています

とのことです。

まず、IOモナドの機能を整理しよう

上記を踏まえて私の理解した限りでは、まずIOモナドには以下(1),(2)の2つの役割りがあります。

• (1) 副作用コードを分離する
  • (1-1)純粋コードから副作用コードを呼べなくする。
    • 静的型チェックおよびランタイムがmainを経由してからしかIOアクションを起動できないことによって
  • (1-2)更新状態を外に持ち出せなくする。
    • 静的型(多相型)チェックでコンパイル時に保証(ランクN多相によって)。ただし、IOでは(1-1)があるので(1-2)は試みることもできず、IO利用者からは(1-1)と一体的に認識される役割りである。
• (2) 副作用を有するコードの実行順序を保証する
  • 副作用は以下の二種類に分けて考えることができるが、実行順序の保証はいずれに対しても必須。
    • (2-1)外部から観測可能なもの→入出力
    • (2-2)外部から観測不能なもの→変数更新(IORef,newIORef,...)

おさらいでした。

そして、STモナドは?

STモナドは、機能的に前述の青字の(1-2)と(2-2)を得るものです。つまり、入出力を行なわず、変数更新(STRef,newSTRef..)だけを行なう用途に使用できます。STモナドには、入出力を行なえない、という制限がありますが、実行順序は保証されるので変数更新はでき、さらに有用なことに(1-1),(2-1)が無いので純粋関数からも呼べるという利点が得られます。

もうちょっと詳しく言うと、

• 「変数更新」のみを実行するコードは、そのコードがもはやコードの見た目としても実質としても状態更新バリバリの命令型(=評価順序が結果に影響を与える)であったとしても、呼び出し側から見たときの参照透過性さえ保てれば、純粋コードから呼んでも大丈夫だ問題ない(呼ぶ側のコードは純粋なので、呼ばれるかどうか、呼ばれる順序などはわからないが、一旦呼ばれたならその呼ばれるコード内なら順序が保たれる)。なぜなら、プログラムの外部から見て検知不能だからである。プログラムの最適化と同じである。ばれなきゃイカサマじゃないんだぜby承太郎である。
  • ここで言う「変数更新」は、Stateモナドによる「状態から異なる新規状態を作り、次々と置き換えていくことで「状態の更新」をエミュレーションする」ということとは違い、特定アドレスのバイト値の書き換えが発生するような、真のメモリ更新の意味。ここで問おうとしているのは、アルゴリズムの特性によって「実際のメモリ書き換えでのみ、期待される高い実行効率が達成できるようなアルゴリズム」が実際にあり、それを直接的に記述・実装するような用途に使える、ということ。
• しかし「入出力(=プログラム外とのインタラクション)」を行うコードは、たとえそれが「呼び出し側から見て参照透過(引数のみによって返り値が定まる)」としても、純粋コードから呼ばれるわけにはいかない。純粋コード自身が遅延評価によって、呼ばれるかよばれないか、あるいは呼び出し順序について保証がないからで、その状況下では外部から見ておかしなこと(起きて欲しい副作用が起きない・順序が変、など)が検出でき都合が悪いからである*1。だから純粋コードのような恐ろしいものから呼ばれないようにIOで守り、mainにつらなる「見えないバトン*2」の唯一の連鎖(the chain)に繋げる必要がある。
• IOは、入出力も変数更新も両方行なうことができる。しかし、入出力を行なわず、変数更新だけを行うコードをIOにするのは、純粋コードから呼べなくなるので嫌である。STモナドは、その目的のためにある。STモナドは入出力はできないが変数更新は行うことができる(ただし更新中の状態を外に持ち出せないように工夫がしてある)。そして、純粋コードからも(IOからも)任意に呼び出すことができる。

表にすると

	入出力	起動方法	純粋関数から	変数更新	順序の保証	相互に呼べるか
STモナド	できない	runST	呼べる	できる	ある	IOを呼べない(純粋関数と同様)
IOモナド	できる	mainで起動	呼べない	できる	ある	ST,State含め純粋関数を呼べる
Stateモナド	できない	runState	呼べる	できない	ある	IOを呼べない(純粋関数と同様)

まとめ

• STモナドはIOモナドへの接続性を意図的に除去したIOモナドのようなものである。
• STモナドはメモリ更新の可否が重要なアルゴリズムを命令型で効率良く実装できる(ただし入出力を行わず、参照透過である場合に限る)
• STモナドは純粋コードからも純粋コードであるかのように呼べる。

*1:時系列に沿った因果律に支配された哀れな人間はそういう状態をバグと呼ぶかもしれない。

*2:バトンはIO Insideの表現。実行順序を保証するためにうけわたしていく状態値を意味する。

Haskellのforallについて理解したことを書いておく(ランクN多相限定)。

Haskellのforallについて理解したことを書いておくyo!(ランクN多相限定*1 )。

前提知識のおさらい: 型・多相型・型検査・型推論…

最初に基本概念を整理しておきます。

• IntやInt->Intは単相型、aやa->aは多相型である。ここでaを型変数と呼ぶ。型変数を含む型が多相型ってわけです。

• 言語処理系の実装上、型という概念は型変数や型コンストラクタのツリー構造として表現される。Int,Char,[],->,(,),(,,,),IO aなどが型コンストラクタ。 a,bが型変数。組合せて(a->[Int])->[b]->(a,b)とか。::の右に書くやつです。

• 型は、プログラムの字面上に直接的実体がある関数や変数だけではなく、値を生じさせる部分式すべてに付随し、コンパイル時に決定されるべき情報である(値あるところに型がある。*2 )。それを決定しようというのが(静的)型検査である。Haskellでは基本としてhindley-milner(以降、HMと記載するときもある)と呼ばれる型推論機構をベースにして多々拡張したもので型推論を行なう。この記事はhindley-milnerのロジック(こちらにscalaのコードがある)を読んで理解したことのみをベースにしHaskellに対して類推したものである*3。hindley-milnerでは型検査は型推論と一体化しているような気がするのでこの記事では「型検査」には「型推論」が含んでいるというつもりで「型検査」という用語を用いる。なお、Hindley-milner型推論の実装については、こちらの記事「Hindley-Milner型推論アルゴリズムをGroovyで書いてみた」もどうぞ。

• 多相型は、1個以上の型変数を含んだ型であり、多相型を解決するための仕組み(後述)を「型スキーマ」もしくは「型抽象」と呼ぶ。型スキーマ中の特定型変数を置換し(結果、単相型が得られるかもしくは単相型に近づく)、その結果を得る操作を型スキーマのインスタンス化と呼ぶ。これは、λ抽象に引数の値を与えると、具体的な結果の値が得られるのと同じ。値の世界のλ抽象は、値を与えると値が返るが、型の世界の型抽象は、型を与えて型が返るような型の世界の関数である。多相型というのは「パラメタを持った型」であり「パラメタに具体値をあてはめることで初めて利用できるような型」なわけです。まあ直感的にそれはそうでしょう。(Javaのジェネリクスも同じだと言える)

HM型検査器の構造と実行

• 「環境」という概念を導入する。環境は識別子*4から型スキーマへの対応表であり型検査に使用する(コンパイル一般のためには、環境は他の情報も含むのかもしれない。ASTとか)。環境は、処理開始時のトップレベルは「組み込み定義」情報だけを含んでいるところから始まり、関数を定義したり、あるいは他モジュールから識別子をインポートすることによって、あるいはラムダ束縛やlet束縛で識別子が定義されるたびに、エントリが拡張されそれぞれのネストレベルで使用される。

• オリジナルhindley-milnerではトップレベルの関数のみ*5に型スキーマを明示的に付与できる*6。
  例: func :: a-> Int。これはfunc :: forall a. a -> Intの略記法である。

forallと型スキーマ・型抽象、インスタンス化のタイミング

• forallは型スキーマ(型抽象)を表わし、型の世界のλである。forallをλに機械的に置換してみると良い。先の例func :: λa.(a->Int)について
  • (λa.(a->Int)) Int の返り値は、Int -> Int、
  • (λa.(a->Int)) [String]の返り値は、[String] -> Int
  みたいな。ただ、値の世界のλとは異なり、型抽象をプログラムから直接的に明示的に呼ぶものではない。構文木上の型検査や型推論の処理中で暗黙的に呼び出される。型検査・推論の中で型スキーマがどう扱われるか、どういうタイミングでインスタンス化されるかがforallの意味を決めている。

• 型検査の過程において、プログラム字面上の「識別子の出現」が型スキーマのインスタンス化のタイミングである。なおインスタンス化一発ですべての型変数が消去できるわけではない。構文木をツリーとして再帰的に辿るhindley-milner型検査過程の各ステップで、型変数を媒介として双方向的・全体的に型がきまっていく*7。こんなことが可能なのはある意味驚きであるが、決まるそうなのである。これがHindley-milnerの凄いところである。処理対象プログラム中に識別子が現われたら、環境から型スキーマを引っぱってきてインスタンス化して、構文木構造(関数適用、let、lambda..)ごとに決められたルールで双方向パターンマッチ(ユニフィケーション、単一化)して型を決めていく。

ちなみに型検査器を外部から見て一言で言うと

• 外部から見ると、hindley-milner型検査器は、型変数を含んだ連立程式を解く、制約問題ソルバとみなせる。

ランクN多相は型スキーマを一級市民の型として扱うこと

• forallが型スキーマのトップレベルにしかあらわれないのがHindley-milner。これに対し、forall. .(.(.. (forall..)..).)という途中レベルで表われてよいのがランクN多相(SystemFに相当？良くわかってない)。これは、λ計算で言えば、「トップレベルの識別子に=で代入する右辺の最左でしかλが使えない」のがhindley-milnerであり、λ抽象を引数や関数の戻り値に使える高階λ計算がランクN多相に相当する。つまり関数を一級市民として扱える(高階操作)ような感じで型抽象を一級市民として扱えるのがランクN多相である。

forallの機能

• 型スキーマのインスタンス化について機能面で言及すべきことがあって、それは型変数名をリネームすることによる衝突回避機能を持つということである(これもλ抽象でできるのと同じ話だが)。型変数に単相型をマッチさせる、という行為に関して、型変数はそれを媒介とした型の一致・不一致の判別の一意性を判定するものであるからして、一致させないためにリネームしたり、リネームの効果がおよぶ特定の範囲では一致させる、というようなコントロールができる。これを利用しているのがかの有名なST Monadで、詳しくはこちら「Lazy Functional State Threads 」(って原論文を読むしかないのか…。しかしweb上では他に理解可能な情報を見付けられませんでした。)。

HMの限界

• hindley-milnerの型検査には双方向性があるため、「ある範囲」を対象とした「型変数の連立方程式」というか制約問題を解く必要があるのだが、そしてGHCはおそらくそれを「トップレベルに定義した関数」という単位でやる*8のだが、hindley-milnerオリジナルでは関数引数の型のインスタンス化について、「関数そのものに付随する型スキーマの実体化」1回分の中で決定しようとするため、識別子の複数回の使用それぞれで異なるインスタンス化ができない。このことは、多相関数を引数にとる関数を定義する際に多相性が1回限りしか発揮できないということなので不便なときがある。例えば、[a]->Intを引数にとる関数([a]->Int)->Intがあったとする。

  func:: ([a]->Int)->Int
  func f = f [1,2,3] + f["a","b","c"]

  これは型エラーになる。なぜならf[Int]、f[ [Char] ]というfの出現2つにそれぞれ対応してインスタンス化されることで生成された、f::[Int]->Intとf::[ [ Char ] ] -> Intというボトムアップで定まる2つの型制約を、引数としての識別子fの型が同時に満せないからである。

ランクN多相の意義と動作例

• これを回避するために、「型スキーマを取ってきてインスタンス化する」という行為を、1つの関数の中で何回も行なえるようするための拡張が、GHCのランクN多相(XRankNTypes)である。その実装はたぶん、型スキーマ(型変数を含む型)を型の一種として扱い(型スキーマ型、forallつきの型として表現)、型スキーマを、関数トップレベルだけではなく、関数引数部分などに登場可能にした上で、λ変数が型スキーマ型にマッチしたとき、そのλ変数の使用(出現)それぞれでインスタンス化してマッチを継続するのである*9。

• GHCiでの書き方としてはオプション-XRankNTypesを指定して、

  func:: (forall a. [a]->Int)->Int
  func f = f [1,2,3] + f["a","b","c"]

  こう。これでコンパイルも通って

  GHCi> func length
  6

  のように実行できる。ここで、fの出現ごとに「forall a.[a]->Int」という型スキーマがインスタンス化される様子が心に浮びますでしょうか。

名前が悪いぞforall

あとは非生産的な話。

• プログラミング言語としてのHakellにおける、forallというキーワードで起動される言語機構を理解するのに、全称量化を理解する必要はないし形式論理学の知識は不要である。「全称量化」という単語を知る必要すら一切ない。それは理解に寄与しない。ていうか理解の妨げになるだけだッ。名称としてそれしかないので「全称量化子」とか「全称量化された」とか呼ぶしかないので、しょうがない面もあるのだろうが、ミスリーディングなだけである。forallというキーワードから「all(全ての)」という含意を読みとる必要すらない。必要があるってのなら値に関して同型であるλについてもどういう意味でallなのか、allを付けないのかプログラミングレベルでの説明を聞かせてほしい。 ∀が型抽象の型表記で慣例的に使われてるのを敬意を表してなのか論理学者は慣れてるからなのか、結果的には無批判に導入しただけだろ、っていう。最終的にはカリー・ハワード同型対応で、そういう方面に応用できるのだとは思うが、Haskellをプログラミングのみに使いたいプログラマにとっては不要なことである。迷惑なことである。

型システム入門 −プログラミング言語と型の理論−

posted with amazlet at 14.01.23

Benjamin C. Pierce
オーム社
売り上げランキング: 220,470

Amazon.co.jpで詳細を見る

*1:ここを読むと、ランクN多相を実現する以外に2つぐらい意味があると。ExistentialQuantificationについてはきちんと理解してないが理解したら何か書くかも。

*2:加えて、値が無いところにもたまに型がある。

*3:本当は「型システム入門」とかにさぞ詳しく書いてあるであろう。でも読めてません。ごめんなさい。

*4:環境のキーとなる「識別子」はプログラム本体で使われる識別子である。型側でのみ使われる「型変数」の名前ではない。混同しないこと。両者は混在することは決してない。

*5:Haskellでは::でlambda変数とかにも他にも付与できる

*6:例のscalaのコードから読む限りでだが、letで定義する識別子には暗黙に形成された型スキーマが付与される。なのでletを介入させるとランクN多相を導入しなくても型スキーマを複数回インスタンス化できそう(未確認)(2014.01.26追記できない)。この意味でletはlambda+関数適用のシンタックスシュガーではない。haskellもそうなってるようだ。不思議。

*7:最終的にもすべてが単相型に落ちずに、型変数が残ることもあるだろう。つまり多相関数はそれである。

*8:これも予想でしかない。前述のScalaのコードでは、任意の構文木の枝に対して型チェック(tp() )を起動可能だが、それは正しい環境を引数に渡せる前提である。正しい環境を構築するためには、上の方から解析を結局していかなければならないよね。だから関数単位だろうと予想しました。遅延評価とかを使って全然違う単位・順序で解析するのかもしれませんが。

*9:この動作は裏をとってない。SystemFなりHaskellのランクN拡張でどう実装しているかは不明。「私だったらそう実装したい」というレベルの話である。