Church encoded Free monad in F #

Question

F #에서 무료 모나드의 교회 인코딩을 표현하려고합니다. Free은 특정 기능자인 Effect에 특화되어 있습니다.

return_ : 'T -> Free<'T>과 bind: ('T -> Free<'U>) -> Free<'T> -> Free<'U>을 아무런 문제없이 쓸 수 있습니다.

내 구현 스케치는 아래와 같습니다.

이 인코딩을 위해 인터프리터를 작성하려고하면 문제가 발생합니다.

주어진 다음의 코드 :

module Interpret = 

    let interpretEffect = function 
     | GetStr k -> 
      let s = System.Console.ReadLine()    
      (k s , String.length s) 

     | PutStr(s,t) -> 
      do System.Console.WriteLine s 
      (t , 0) 

    let rec interpret (f: Free<string * int>) = 
     Free.runFree 
      f 
      (fun (str,len) -> (str,len)) 
      (fun (a: Effect<Free<string*int>>) -> 
       let (b,n) = interpretEffect a 
       let (c,n') = interpret b 
       (c, n + n') 
      ) 

은 내가 interpret 함수 내에서 Free.runFree에 세 번째 인수의 형식 오류 :이의 (결과 유형을 일어나는 이유

... 

(fun (a: Effect<Free<string*int>>) -> 
     ^^^^^^^^^^^^^^^^^^ ------ Expecting a Effect<string * int> but given a Effect<Free<string*int>> 

내가 이해 첫 번째 함수는 'R === string*int을 결정합니다.) 그리고 rank-2 함수 (F # # http://eiriktsarpalis.github.io/typeshape/#/33과 같이 인코딩 할 수 있음)를 사용하여 해결할 수 있다고 생각하지만 적용 방법을 잘 모르겠습니다.

모든 포인터가 많이 감사하겠습니다.

마이클

Answer 1

당신이 아무것도 할 필요가 없습니다, 컴파일러 제안 유형이 올바른 (그리고 runFree의 종류에 맞춰) 사실이다. 당신이 무엇을 어느 F f a이 될 것

runFree :: Functor f => (a -> r) -> (f (F f a) -> r) -> F f a -> r 

이 Effect이 Effect<Free<'a>>을 것 Free<'a> 및 f (F f a)을 -specialised :

당신이 생각하고하는 것은 (this Haskell question에서 찢어) 스콧 인코딩 것 같습니다 다시 사용하려고합니다. f r이 Effect<'a>입니다

runFree :: Functor f => (a -> r) -> (f r -> r) -> F f a -> r 

- 따라서 쉽게 당신이 먼저 그것을 사용하고있는 가정 이유입니다 (F #으로 표현하고

:

교회 반면 인코딩이 될 것입니다. 이것은 내가 interpret에 대해서 가지고 있던 것입니다 : pureF이

입니다

let rec interpret (f: Free<string * int>) = 
    Free.runFree 
     f 
     (fun (str,len) -> (str,len)) 
     (fun (a: Effect<_>) -> 
      let (b,n) = interpretEffect a 
      let (c,n') = interpret (Free.pureF b) 
      (c, n + n') 
     ) 

let pureF (x: 'a) : Free<'a> = 
    { new Free<'a> with member __.Apply kp _ = kp x } 

즉 return_ 기능입니다.

해당 freeF 함수를 정의하면 어떤 점이 정리 될 것이라고 생각합니다 (Effect<'a>은 왜 functor입니까? 붙여 넣은 코드에서는이 사실을 어디에도 사용하지 않고있는 것 같습니다).