Блог

Главная - Вопросы по программированию - RecursiveDo в Idris? (Используя значение до того, как оно определено в нотации do)

RecursiveDo в Idris? (Используя значение до того, как оно определено в нотации do)

#idris

#idris

Вопрос:

Есть ли в Idris 2 что-то похожее на Haskell RecursiveDo . У меня есть определенные значения, которые я хотел бы использовать до того, как они будут определены в IO монаде. Я пытаюсь построить циклическую сеть FRP. Они реализуют следующий интерфейс:

 interface Loop (a : Type) where
    loop : (a -> IO (b, a)) -> IO b

Однако использование loop уродливо. Есть ли лучший способ?