L'église a codé Monad libre dans F #

Question

J'essaye d'exprimer l'encodage d'église de la monade libre dans F #. Free est spécialisée dans un foncteur particulier, Effect.

Je suis capable d'écrire à la fois return_ : 'T -> Free<'T> et bind: ('T -> Free<'U>) -> Free<'T> -> Free<'U> sans aucun problème.

Une esquisse de ma mise en œuvre est donnée ci-dessous. Lorsque j'essaye d'écrire un interpréteur pour cet encodage, je rencontre un problème.

Vu le code suivant:

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') 
      ) 

je reçois une erreur de type dans le troisième argument à Free.runFree dans la fonction interpret:

... 

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

Je comprends pourquoi cela se passe (le type de résultat de la première fonction détermine 'R === string*int) et soupçonne que cela peut être résolu en utilisant une fonction de rang 2 (qui peut être codée en F # par exemple http://eiriktsarpalis.github.io/typeshape/#/33) mais je ne suis pas sûr de la façon de l'appliquer.

Tous les pointeurs seraient très appréciés.

Michael

Answer 1

Vous n'avez pas besoin de faire quoi que ce soit là, le compilateur de type suggéré est en fait correct (et en accord avec le type de runFree).

Il semble que ce que vous pensez à il y a encodage Scott (arraché à this Haskell question):

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

où F f a serait votre Effect -specialised Free<'a> et f (F f a) serait Effect<Free<'a>>, qui est ce que vous J'essaie d'utiliser.

Alors que l'Eglise encodage serait:

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

où f r est Effect<'a> - ce qui rend plus facile à exprimer en F # (ce qui est la raison pour laquelle je suppose que vous l'utilisez en premier lieu

. Voilà ce que j'avais pour interpret:

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') 
     ) 

où pureF est

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

c'est-à-dire la fonction return_. Je pense que la définition de la fonction correspondante freeF permettrait de supprimer certaines choses (par exemple, pourquoi est Effect<'a> un foncteur - vous n'utilisez pas ce fait n'importe où dans le code que vous avez collé).