読者です 読者をやめる 読者になる 読者になる

mastodon運用していく

mastodon

IDでアイデンティティを確保してきた人間的には、OStatus準拠のサービスをやっていくうえで、独自ドメインとらないと気分になれないというのが動機としてあった。流行っているというのもあるし、railsだしpostgresだしsidekiqだし、自分の持っている技術スタックでいい感じやっていけそうな気分になったということで、ある程度まともな感じで運用してみることにした。

方針というか、どういうコミュニティがというポリシーは一切無いし、強いて言うなら自分の好きなことをやっていくつもり。 例えばHEADをガンガンデバッグしつつchankoとか使ってこのインスタンスだけの機能みたいなのを実装していくとか。 あとは、外部の人間の登録をどうするかとか、そういうのも考えないといけない気がするけど、自由にしてもらっていいんじゃないですかね。

mstdn.everysick.com

specifications

サービスはAWSだと高いのでさくらのクラウドで、dockerとかfigとか使わずにsystemd使いつつ単一のサーバー内で全てを簡潔させる感じに構築した。SSLが必須というわけではないけど、パスワードを収集するマストドンになるつもりもないので、CloudFlare使ってSSL化している。こんな感じ。

[Browser]---(HTTPS)---[CloudFlare]---(HTTPS)---[mstdn.everysick.com]

あとは、mailgunではなくSendGridとかで置き換えてみようかなと思ったりしている。 当初はSendGridでやろうと思っていたけど審査結果がまだらしい。来たらやっていこう。

Follow me

mstdn.everysick.com

また何か進捗があったら書くぞ。

Region based mini ml - unification and implementation

変換前言語・変換後定義、Regionの概要については初回の記事を読んでください。
また、Region推論についての定義・説明は2回目の記事を読んでください。
この記事ではRegion推論精度の話・Region推論実装の話について書いています。
個人的な解釈が含まれているため、記事の内容が全て正しいとは限りません。何か問題点・不明点等があれば連絡してください。

Region推論精度の話

Region推論によって決定されるRegionの配置は、型推論中にあるEffectの単一化のアルゴリズムに依存することが知られています。 例えば、Effectに対して適当な単一化を行ってしまうと、letregion によるRegionの生存期間の同定が非効率的になったり、不正なRegion割当てがされてしまったりします。 そもそもEffectは集合で、他のEffectへの参照も含ますので、比較のコストなどは結構厳しいです*1。 参考論文では単一化についての話題に触れているものの、そのアルゴリズムについての説明は皆無でした。 そのため、introでも紹介した別論文*2を参考にし実装にはそのアルゴリズムを採用しました。

内容として参考・実装したのはMLkitで実際に採用されている単一化の方法です。

例として、以下のArrowEffect1, ArrowEffect2を単一化によって代入規則を導きたいとします。

ArrowEffect1 = (eps1, { get(r1), put(r1), eps2 })
ArrowEffetc2 = (eps3, { get(r2), put(r2), eps4 })

上記のArrowEffectの単一化は以下のステップによって行われます。

  • もしArrowEffect1のEffectVariable(この場合はeps1)とArrowEffect2のEffectVariable(この場合はeps3)が等しい
    • 代入規則は空
  • それ以外の場合
    • ArrowEffect1のEffectとArrowEffect2のEffectの和集合 effect' を定義
    • 代入規則 { eps1 -> (eps2, effect'), eps2 -> (eps2, effect')}を返す

以上のアルゴリズムで真っ当な精度のRegion割り当てを行うことができます。 また、この内容については記事の興味範囲を外れるため、詳細・証明は元論文に任せることにします。

実装について

論文中の実装全てを行う体力は残っていなかったためことは本来の目的ではないため、以下のSExpからTExpへRegion推論を行うプログラムを作成しました。 実装においては今回のサーベイで得た知見、他の方が別言語で実装されたもの、A Region Inference Algorithm 内で使用されていたサンプルコードを参考にしています。 また、letregion規則の導入に関して、少々正しく動作していない部分があるので、実装はあくまで参考として信用しないでください。

  • SExp
e := c 
     | x 
     | (lambda x. e)
     | e1 e2
  • TExp
e := c at r
     | x 
     | (lambda x. e) at r
     | e1 e2
     | letregion r in e end

簡単な実行例

入力として以下のような式の構文で実行します。

(lambda x. x) 1

構文木に直したものはこちら

SrcExp.Call((SrcExp.Lam("x", SrcExp.Var("x"))), SrcExp.IntLit(1))

出力結果として出るものとそれを意訳したものを以下に示します。 Effectの中身は煩雑長くなっているため、省略して出力しています。

RCall((RLetReg('r0, ), (RLam(x, (RVarX(x, (TVar('t0) at 'r0), effects)), 'r1, ((TVar('t0) at 'r0)-{'e0, effects}-(TVar('t0) at 'r0)), effects )), ((TInt at 'r2)-{'e0, effects}-(TInt at 'r2)), effects), (RInt(1, 'r2, (TInt at 'r2), effects), (TInt at 'r1), effects))

意訳したものはこちら

letregion 'r0 in
  (lambda x:(('t0, 'r0), effects). x):('t0 at 'r0)->{'e0, effects}->('t0 at 'r0), effects)
end:((TInt at 'r2)-{'e0, effects}-(TInt at 'r2), effects)
1:((TInt, 'r2), effects)

前述の通り、letregion句において、本来は結果の式全体を囲む

letregion 'r2 in ... end

の式が必要ですが、結果には現れていないため、首をかしげます。

Repository

実装のリポジトリはこちらです。気が向かないと修正はする気がおきない気がするので[WIP]は永遠にある気がします。

github.com

あとがき

アドベントカレンダー駆動で書いていた記事ですが、記事の分割をしてしまったせいで大幅に遅れて続きを書くことになりました。 個人的な多忙期や実装のバグなどに追われたこともありますが、遅れてしまってすみませんでした。

Region推論に関しての完全な説明はしきれていない、というよりふんわりとした概要を説明する記事となったため、 それ以上の理解や疑問などは参考論文をあたるか、自分に質問していただければお答えできる範囲でお教えします。

また、内容に関して間違っているなどの指摘はコメント・Twitter・mailなどにお送りしていただければ確認のうえ修正します。

Region based mini ml - translation

変換前言語・変換後定義、Regionの概要については前回の記事を読んでください。
この記事ではtranslationに必要な表現・変数の定義を先に説明し、参考論文の規則に則って詳細を説明していきます。
個人的な解釈が含まれているため、記事の内容が全て正しいとは限りません。何か問題点・不明点等があれば連絡してください。

Translation

結論から説明すると、SExpからTExpへのTranslationはRegion注釈付きの型推論と言い換えることができます。 ではまずそれぞれ変数・表現を元論文より抜粋して定義します。シンプルなものであるため、定義を列挙します。 例示・詳細については参考論文を参照してください(P21 5.1 Semantic object)。

Variable

  • {
\alpha \in TyVar
}

  • {
p \ or \ \rho \in RegVar
}

  • {
\epsilon \in EffectVar
}

それぞれ型変数・Region変数・Effect変数を示します。

Effect

  • {
\psi \in Effect  = Fin(AtomicEffect)
}

  • {
AtomicEffect = EffectVar \cup PutEffect \cup GetEffect
}

  • {
put(\rho) \in PutEffect = RegVar
}

  • {
get(\rho) \in GetEffect = RegVar
}

Effectは各Token(厳密には定義していないがExpressionの各項)について、その項を評価した際の副作用を示します。 また、EffectはRegionに対する操作・参照によるRegionへの副作用を示すものです。 PutEffectは 変数 {\rho}のRegionに対するWriteの操作を、GetEffectは変数 {\rho}のRegionに対するReadの操作を示します。これらの作用に関しては実行時に評価されるため、意味についての説明はこの程度にしておきます。

Type, TypeScheme

  • {
\tau \in Type = TyVar \cup ConsType \cup FunType
}

  • {
SimpleTypeScheme = Type
}

  • {
CompoundTypeScheme = \cup_{k \geq 0} RegVar^{k} \times \cup_{n \geq 0} TyVar^{n} \times \cup_{m \geq 0} EffectVar^{m}
}

  • {
\sigma \in TypeScheme = SimpleTypeScheme \cup CompoundTypeScheme
}

  • {
ConsType = { int }
}

  • {
\mu     \rightarrow^{\epsilon . \psi} \mu \in FunType = TypeWithPlace \times ArrowEffect \times TypeWithPlace
}

  • {
\epsilon . \psi \in ArrowEffect = EffectVar \times Effect
}

  • {
\mu \in TypeWithPlace = Type \times RegVar
}

前回の記事で後ほど紹介すると言っていたTExpに対するType schemeを含みます。これらを書き下すと

{
\sigma ::= \forall().\tau
}

{
\sigma ::= \forall \rho_1 \cdots \rho_k \alpha_1 \cdots \alpha_n \epsilon_1 \cdots \epsilon_m . \tau
}

となり、これらは任意のEffectVar, TypeVar, RegVarを含む多相を表現できると言えます。

他、特に説明しなければいけないのはFunTypeについてです。SExpでは純粋なArrowTypeであったに対し、 上記ではTypeWithPlaceからTypeWithPlaceへArrowEffectを伴う型と定義されており、 これはRegion {\rho_1}に紐づく型 {\tau_1}を持つ項を評価した際、 ArrowEffect  {\epsilon . \psi}を副作用とし、 Region {\rho_2}に紐づく型 {\tau_2}を持つ項を結果とすると言えます。

また、ArrowEffect  {\epsilon . \psi} にある  {\epsilon} はEffectVarであり、他のEffectから参照されるための識別子として使われ、  {\psi} はEffectの有限集合を示します。

Environment

  • {
TE \in TyEnv = Var \rightarrow^{fin} (TypeScheme \times RegVar)
}

評価を行う際の型環境TEの定義です。 プログラム中の変数を元として、型を示すTypeと紐付いているRegionを示すRegVarを対応させます。

Inference rule

推論は以下の形式で与えられます。

{
TE \vdash e \Rightarrow e' : \mu, \psi
}

これは 型環境TE上で、 {e}を評価した際、TypeWithPlace  {\mu}, Effect  {\psi} を持つ  {e'} へと変換される と読みます。 これに則り、P26 5.2 The inference system の各ruleを適用することでSExpからTExpへの変換を含めた型推論を行うことができます。 各ruleについての説明は、Variable, Effect, Type, TypeScheme, TEの定義、また多相型の推論をベースにした簡単なものであるため省略します。


ここまででRegion推論についての概要を説明しました。 まとめるとRegion推論(SExpからTExpへのtranslation)はRegion注釈付きの型推論であり、 多相型を拡張した型スキームに則り、型推論を行うことでRegionを推論することが可能であるという点です。 初期に考えていた記事のボリュームよりかなりやっつけになってしまいましたが、 とりあえずRegion推論に関する概要の説明はここまでとして、次回は推論の詳細の話と実装について書きます。