小编242*_*684的帖子

我有这个代码:

import Control.Lens
import Control.Monad
import Control.Arrow
import Text.Read

... IO (Maybe String) ...
    >>= \m -> case m of
        Just x -> putStrLn x
        Nothing -> putStrLn "Error"

是否有可能使它无点(摆脱\m ->)？

我正在处理一个库(ghcjs-dom),其中每个函数返回一个IO (Maybe T).

我有一个函数a返回an IO (Maybe x)和函数b,它x作为参数并返回一个IO (Maybe y).

是一个允许我做a ??? b和获得的运营商IO (Maybe y).我的Hoogle搜索没有任何结果.

我正在寻找类似的东西join,IO (Maybe (IO (Maybe t)))而不是IO (IO t)或Maybe (Maybe t).

我试图hpure通过重复相同的元素来生成一个生成hvect 的函数,直到达到所需的长度.每个元素可以具有不同的类型.例如:如果参数显示,则每个元素都是show函数的特化.

hpure show : HVect [Int -> String, String -> String, SomeRandomShowableType ->  String]

这是我的尝试:

hpure : {outs : Vect k Type} -> ({a : _} -> {auto p : Elem a outs} -> a) -> HVect outs
hpure {outs = []} _ = []
hpure {outs = _ :: _ } v = v :: hpure v

最终v发生此错误:

When checking an application of Main.hpure:
        Unifying len and S len would lead to infinite value

为什么会出现错误以及如何解决？

以下示例使用Data.Bin来自Bi包:

import Data.Bin

foo : (x, y : Bin) -> Dec (binCompare x y = LT)
foo x y = case binCompare x y of
    LT => Yes (C1 ?hole1)
    EQ => ...
    GT => ...

:t ?hole1
binCompare x y = LT

如何binCompare x y = LT在处理LT案件时获得证据？

有可能代表一些如何制作unFix总数？可能通过限制是什么f？

record Fix (f : Type -> Type) where
    constructor MkFix
    unFix : f (Fix f)

> :total unFix
Fix.unFix is possibly not total due to:
    MkFix, which is not strictly positive