Laissez-lier les résultats intermédiaires dans monade IO

Question

Dans ce contexte:

open import IO 
open import Data.String 
open import Data.Unit 
open import Coinduction 

postulate 
    A : Set 
    f : String → A 
    g₁ g₂ : A → String 

disons que je veux mettre en œuvre quelque chose comme

foo : IO ⊤ 
foo = ♯ readFiniteFile "input.txt" >>= \s → 
     ♯ (♯ putStrLn (g₁ (f s)) >> 
     ♯ putStrLn (g₂ (f s))) 

par let -binding le résultat intermédiaire f s. J'espérais cela fonctionnerait:

foo₁ : IO ⊤ 
foo₁ = ♯ readFiniteFile "input.txt" >>= \s → 
     let x = f s in 
     ♯ (♯ putStrLn (g₁ x) >> 
     ♯ putStrLn (g₂ x)) 

mais cette tentative échoue avec

Non implémenté: constructeur CoInductive dans le cadre d'un laisser lié variables

donc j'ai essayé de sortir le ♯:

foo₂ : IO ⊤ 
foo₂ = ♯ readFiniteFile "input.txt" >>= \s → 
     ♯ (let x = f s in 
     ♯ putStrLn (g₁ x) >> 
     ♯ putStrLn (g₂ x)) 

même problème que précédemment.

j'ai réussi à contourner ce il suffit de soulever le ♯ pas forcement:

_>>′_ : ∀ {a} {A B : Set a} → IO A → IO B → IO B 
m >>′ m′ = ♯ m >> ♯ m′ 

foo₂ : IO ⊤ 
foo₂ = ♯ readFiniteFile "input.txt" >>= \s → 
     ♯ let x = f s in 
     putStrLn (g₁ x) >>′ putStrLn (g₂ x) 

mais pourquoi est-ce que le travail si la version « inline » ne fonctionne pas?

Answer 1

FYI, ce problème était de longue date et comme je le regardais aujourd'hui, j'ai remarqué que it had been fixed juste quelques jours avant que vous posiez votre question. Le correctif fait partie de la version actuellement publiée (version 2.5.1.1).