kakkun61
@kakkun61 has joined the channel
Free を使ったEffectの定理証明を試みるも、そのままでは停止性チェックに引っかかってしまうため、
class Container c where
type Shape c :: Type
type Pos c :: Shape c -> Type
-- Concrete instance of a container
data Ext c a = Ext (s :: Shape c) (Pos c s -> a)
data Free c a = Pure a | Impure (Ext c (Free c a))
Writer みたいなMonadについてどうするか、って話もあったけど理解できずTYPE (a :: RuntimeRep (FunRep 2)) というような新たなポリモーフィズムが--fno-do-lambda-eta-expansion してるコードを見たことがあるんだけど、積極的にしたいケースってどんなだろう。TExp ）において、splice時に型引数がどう具体化されたか（Context）をどうやって保存するか、という話。