Koji Miyazato

一応生きてますよ(2019/08)
すこし元気になってますよ(2020-)

趣味プログラミング専門エンジニア

[Koji Miyazato @viercc]

[私のプロフィールをこれで検証してね: openpgp4fpr:B2E1DC9AF16599BD2D873A227BABC58075EC4EE6]

[Koji Miyazato @viercc]

@luckyowlman この話だと思います
> 'return' will be removed in fabour of 'pure'

[Koji Miyazato @viercc]

@Kory__3 多分 do { _ <- ask; m } ~ m みたいな関係式も必要です、でないと`pure` と"1回は`ask`した`Free (Ask e)`"の区別をつけてもよくなってしまいそうなので

[Koji Miyazato @viercc]

@Kory__3 このMに対する"bind"は変な型になるのでgraded monadではないかもしれないですが
bind : {a : Set} {g : a -> Free f b} -> M t a -> ((x : a) -> M (g x) b) -> M (t >>= u) b

[Koji Miyazato @viercc]

@Kory__3 エフェクトの実行
send : (a : Set) -> (t : Free f a) -> M t a
とエフェクトの等式の移行
transfer : equiv t u -> M t a ~ M u a
ができるようなものとして表せたり・・・？

[SnO₂WMaN @SnO2WMaN]

現在FFLでorganizationとしてGitHub Sponsorsを開こうと思っています．ただメンテナ2人に対してGitHub側で分割する方法がおそらくないことや手数料の問題があるらしいのですが，実情をよく知らないのでOSSへの寄付に詳しい方の意見が聞きたいです．代替としてOpen Collectiveなどを考えています．

[Koji Miyazato @viercc]

@ymdfield おっと

関手[Set,Set]→Mon([Set,Set]) ですね
（Set上の自己関手をとって、モナド=Set上の自己関手が合成でなすモノイドを作る関手）

[Koji Miyazato @viercc]

@ymdfield そういえば、(普通の意味での)集合の圏Setでは関手[Set,Set]→[Set,Set]の意味でのFreeモナドは作れない(※)ので、leanでも似たようなことがあるかもしれないです

[Koji Miyazato @viercc]

@ymdfield 両辺の濃度を考えると
|T(X)| = |X| + |F(T(X))| = |X| + |B|^|A|^|T(X)|
となり、|B|と|A|が0または1でなければこれは不可能です

[Koji Miyazato @viercc]

@ymdfield ※ 関手F ∈ [Set, Set]の中には、それが生成するFreeモナドT=Free(F)が存在しないようなものがあります。例えば、A,Bを適当な集合として F(X) :=(X -> A) -> B という関手を考えます。Freeモナドは存在すれば同型を除いて一意なので、
T(X) ~ X + F(T(X))
ですが、

[Koji Miyazato @viercc]

@ymdfield あっ見切れちゃった

can'tDecompNewtype :: Coercible (Bar_R x) (Bar_R y) => Coercion x y

です

[Koji Miyazato @viercc]

@ymdfield 一応、newtypeのコンストラクタを隠せばできますよ
Bar_Rは別のモジュールで

type role Bar_R representational
newtype Bar_R a = MkBarR a

と定義してあって、MkBarRはインポートしていない状態です

[Koji Miyazato @viercc]

@ymdfield まあ、モジュールの境界で型安全性を守っているという状態なら直接unsafeCoerceを使ってもいいような気もしますが・・・

[Koji Miyazato @viercc]

@ymdfield でもclosed type family `F` が*型コンストラクタを返す*場合、つまり`F (a :: k) :: Type -> Type`のとき、`F a`に対してroleが推論できてもいいような気はしますね。

`F a x`はコンストラクタと中身の型がスコープにない`newtype F_a x = ...`と同じように扱える気がします。

[Koji Miyazato @viercc]

@ymdfield

Rolesについての論文（最初のものではなくて現時点のGHCに近いもの）を読んでみたんですが、
"decomosition rule"と呼ばれているものがこの"unlift"の性質に近いですね。

https://t.co/Dh0HRfmDBH

[Koji Miyazato @viercc]

@ymdfield

[Koji Miyazato @viercc]

@ymdfield In fact, for a `data` with nominal parameter, `Coercion` decomposes to nominal equality `(:~:)`.

[Koji Miyazato @viercc]

@ymdfield You can't lift `Coercion` over type families /at all/ unless you can reduce type families (injective or not) to other ordinary `data` or `newtype`.

[Koji Miyazato @viercc]

ここで見たように、data familyにdecomposition ruleを適用できてしまうとunsoundなので

[Koji Miyazato @viercc]

Future directionsではdata familyやtype familyにrole annotationができるように拡張できるかも？と書かれています。これは"decomposition ruleが必須"という事実とどう噛み合うのかはわかりませんが

https://t.co/PZxg1ExxYq