Koji Miyazato

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

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

AIがいきなりHaskellのreturnはpureに置き換えられる方向で議論が進んでると言ってたが本当か…？ってなってる

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

Freer (Ask e) を do { r1 ← ask; r2 ← ask; f r1 r2 } = ask >>= (r → f r r) で「割る」とちゃんと Reader e になるのかな〜、って気はします（今考える余裕は無い）（ならなかったらびっくりする）

@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

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

Hoare State Monad みたいなアイデアはあるので、モナド側を作り込めばワンチャン…というのは全然あり、IndexedState みたいな機構を持ってくれば get/set 等式くらいは依存型理論の内部で実現できると思うんですが、そこを動かすというのは実はあんまりやられていないのかもしれない

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

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

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

Freeモナドトランスフォーマーがleanと絶望的に相性が悪いかもしれないという状況になってきている chatgpt.com/s/t_68c2d117a5…

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

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

@ymdfield あっ見切れちゃった can'tDecompNewtype :: Coercible (Bar_R x) (Bar_R y) => Coercion x y です

@ymdfield 一応、newtypeのコンストラクタを隠せばできますよ Bar_Rは別のモジュールで type role Bar_R representational newtype Bar_R a = MkBarR a と定義してあって、MkBarRはインポートしていない状態です

newtypeにはdecomposition rule適用されないならdataをnewtypeで包めばunsoundにならないのでは？と思ったけど、正確には適用されないんじゃなくて、newtype先のdataがそのまま展開されているような形でdecompositionが適用されるだけだから結果は同じだった

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

@ymdfield でもclosed type family `F` が*型コンストラクタを返す*場合、つまり`F (a :: k) :: Type -> Type`のとき、`F a`に対してroleが推論できてもいいような気はしますね。 `F a x`はコンストラクタと中身の型がスコープにない`newtype F_a x = ...`と同じように扱える気がします。

@viercc あざます、最初はGHCがあんま賢くなくて利用したい性質が言語内で利用できない…って気持ちだったんですけど、実際はそれunsoundだし、しかもこのdecompositionのルールも合わせるとむしろ逆方向も言えるという意味で本来利用できる性質が全部言語内で利用できるなーと感心です

@ymdfield Rolesについての論文（最初のものではなくて現時点のGHCに近いもの）を読んでみたんですが、 "decomosition rule"と呼ばれているものがこの"unlift"の性質に近いですね。 #subsection.2.7" target="_blank" rel="nofollow noopener">seas.upenn.edu/~sweirich/pape…

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

@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`.

Haskellers, please help me out. Here is an Either indexed by a type-level Bool. When 'i' is False it is guaranteed to be Left, and when 'i' is True it is guaranteed to be Right. Is there a way to keep the type parameters 'a' and 'b' representational while also being able to ...

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

Future directionsではdata familyやtype familyにrole annotationができるように拡張できるかも？と書かれています。これは"decomposition ruleが必須"という事実とどう噛み合うのかはわかりませんが #subsection.8.4" target="_blank" rel="nofollow noopener">seas.upenn.edu/~sweirich/pape…