2

在 Idris 中，这有效：

appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String
appShow s x = s x

tAppShow : String
tAppShow = appShow show 5

但是，有些不同的版本没有。这编译：

specializeMonad : ({m : _} -> Monad m => m Int) -> IO Int
specializeMonad f = f

但如果我尝试使用它：

tSpecializeMonad1 : IO Int
tSpecializeMonad1 = specializeMonad (return 5)

-- Or trying harder to keep it polymorphic
tSpecializeMonad2 : IO Int
tSpecializeMonad2 = specializeMonad (the ({m : _} -> Monad m => m Int) (return 5))

然后我得到Can't find implementation for Monad m第一个并且：

                Type mismatch between
                        m Integer (Type of return 5)
                and
                        m2 Int (Expected type)

对于第二个。

我注意到即使只有return 5. 例如，如果我在 repl 中尝试：

> return 5
Can't find implementation for Monad m

有没有办法获得具有接口多态类型的值？我对 Idris 类型检查背后的原则有什么误解吗？（我来自 Haskell，这可能已经很明显了。）

4

0 回答 0