Идиоматический способ использования конструкций Functor / Applicative / Monad в ST в Idris - PullRequest
Новая
       17

Идиоматический способ использования конструкций Functor / Applicative / Monad в ST в Idris

0 голосов
/ 24 февраля 2019

Я пытался использовать when : Applicative f => Bool -> Lazy (f ()) -> f () внутри блока ST do: 

loop : (ConsoleIO m, Draw m) =>
       (draw : Var) ->
       (state : GameState) ->
       ST m () [draw ::: SDraw {m}]
loop draw state = with ST do

  print (f state) -- works

  when True (print (f state)) -- error

  ?what

, что является ошибкой, поскольку ST, по-видимому, не является аппликативным, он просто поддерживает синтаксис do.

Я предполагаю, что есть другие полезные функции функтора / аппликатива / монады, которые также не поддерживаются из-за этого.

Есть ли какое-то идиоматическое решение для этого недостатка?

...