newtype ContT r m a = ContT {runContT :: (a -> m r) -> m r}
newtype ContT m a = ContT {runContT :: forall r. (a -> m r) -> m r}
ContT m a 는 RankNTypes extension 켜야됨
둘이 별로 다를거 없다고 생각했는데
instance MonadReader r m => MonadReader r (ContT m) where
reader = lift . reader
local f m = lift $ local f (runContT m return)
이런건 후자만 되네..
ContT m a 도 쓸 가치가 있는건가..?
m이 모나드이면 후자는 m a랑 동치 아님? - dc App
Monad m, ma :: m a |- ContT (ma >>= ) :: ContT m a이고 Monad m, c :: ContT m a |- (runContT c) return :: m a이니까 Monad m => m a ~ ContT m a이다. - dc App
원래 forall r. ContT r m a 이 m a 랑 동치 맞음.
근데 전자는 forall r.을 타입 쓰는데서 붙이는거고 후자는 이미 forall r. 이 안에 달려있는게 다름
근디 전자 처럼 하면 Monad (ContT r m) 을 각 r에 대해 정의하는거라서 후자처럼 r을 polymorphic 하게 쓰는걸 못함
1. Monad m일 때 동치이지 않음? 2. 근데 왜 동치임? - dc App
더 일반화시킬 수는 없을까? - dc App
from :: (forall r. ContT r m a) -> m a from m = runContT m return to :: m a -> (forall r. ContT r m a) to m = ContT (\k -> m >>= k) 원래 이건데, forall r. 을 바깥으로 꺼내서 Rank 1 으로 만들 수 있지
내꺼랑 증명이 같네 ㅎㅎ - dc App
님 증명에 쓴 기호 몰라서 사실 못알아들음 ㅋㅋ
hyps |- conc의 뜻은 hyps를 가정했을 때 conc가 결론임을 증명할 수 있다임. 예를 들어 f :: a → b, x :: a |- (f x) :: b임. - dc App
근데 더 일반화된 결론을 얻을 수 없을까? - dc App
더 일반화된 결론이 뭐 말하는거임?
Monad m => m (Either a b) ~ forall r. (a → m r) → (b → m r) → m r 같은 거 - dc App
또는 Monad의 정의를 새롭게 내리는 거 - dc App
그런건 수학자 성님들이 해주실거야.. ㅠㅠ
야 너라면 가능해 - dc App