개발을 코드로 표현

develop :: Coffee -> IO Code develop fuel = burn fuel . forever $ do w <- popWork s <- solve w case s of Solved s -> report s YakShaving w1 w2 -> do pushWork w1 pushWork w2


했다가 말 되게 할 수 있을것 같아서 진짜로 짜봄

https://gist.github.com/damhiya/614c4f178096c75fe6cba9070fe8f63a


data DevF :: Type -> Type where PopWork :: DevF Work PushWork :: Work -> DevF () Solve :: Work -> DevF Result Report :: Solution -> DevF () data Dev :: Type -> Type where Vis :: DevF e -> (e -> Dev a) -> Dev a Ret :: a -> Dev a popWork :: Dev Work popWork = Vis PopWork Ret pushWork :: Work -> Dev () pushWork w = Vis (PushWork w) Ret solve :: Work -> Dev Result solve w = Vis (Solve w) Ret report :: Solution -> Dev () report s = Vis (Report s) Ret instance Functor Dev where fmap f (Vis e k) = Vis e (fmap f . k) fmap f (Ret a) = Ret (f a) instance Applicative Dev where pure = Ret (<*>) = ap instance Monad Dev where (Vis e k1) >>= k2 = Vis e (k1 >=> k2) (Ret x) >>= k = k x

이부분이 핵심인데, Dev라는 freer monad로 일종의 명령형 DSL을 만들었음.

PopWork, PushWork, Solve, Report 같은것들은 이 DSL이 발생시킬수 있는 event들의 목록인데, event라는건 이 DSL로 정의한 기계가 외부세계(혹은 Oracle?)와 할 수 있는 상호작용을 표현한거임.

PopWork :: DevF Work는 외부세계로부터 Work를 받아오는 이벤트고

Solve :: Work -> DevF Result는 외부세계에 어떤 Work를 해결해달라고 요청하고 그 결과인 Result를 받아오는 이벤트임.

popWork, pushWork, solve, report는 이 이벤트들을 사용하기 편하게 감싸둔거고.


이 이벤트들은 인터페이스만 정의된것일 뿐이라서 실제로 어떻게 동작을 할지는 인터프리터인 "burn" 함수에 달려있음.

burn 함수는 Dev DSL로 작성된 프로그램을 입력으로 받아서 하스켈이 실제로 실행할수 있는 IO로 번역함.

각각의 이벤트를 어떻게 IO로 번역할지는 burn에 달린거지.


free/freer monad로 명령형 언어나 side-effect를 모델링 하는게 엄청 유용해서 2019년에도 이걸로 interaction tree라는 논문이 나왔음.

https://github.com/DeepSpec/InteractionTrees

간략하게 소개하자면 Coq에서 free monad로 실제 C같은 프로그래밍 언어를 모델링 할 수 있는 프레임워크임.