2

我刚开始玩 Idris，并尝试在其中插入一些 Haskell 机器：

namespace works
  data Auto a b = AutoC (a -> (b, Auto a b))

  const_auto : b -> Auto a b
  const_auto b = AutoC (\_ => (b, const_auto b))

但是，我现在想概括Auto a b为AutoM m a b采用一个额外的参数，以便它可以单子生成其输出，并且m是单子。我的直觉是那m会有 type Type -> Type，但随后类型检查器抱怨那不匹配(Type, Type) -> Type。所以我试着让它多态一点：

namespace doesntwork

  data AutoM : {x : Type } -> (m : x -> Type) -> (a : Type) -> (b : Type) -> Type where
     AutoMC : (a -> m (b, AutoM m a b)) -> AutoM m a b

  data Identity a = IdentityC a

  Auto : Type -> Type -> Type
  Auto = AutoM Identity

这至少是类型检查。但是当我尝试时：

  const_auto : Monad m => {m : x -> Type } -> {a : Type} -> b -> AutoM m a b
  const_auto b = AutoMC (\_ => return (b, const_auto b))

然而，这并不好：

When elaborating right hand side of Stream.doesntwork.const_auto:
When elaborating an application of function Prelude.Monad.return:
        Can't unify
                (A, B) (Type of (a, b))
        with
                (b, AutoM m4 a b) (Expected type)

而且我无法理解类型错误。为什么在世界上会(a, b)提到类型，而a在定义的任何地方都没有使用const_auto？我觉得自己的定义AutoM已经有问题了，但我真的不知道为什么或如何。

4

1 回答 1

4

当你的直觉告诉你m作为一个 monad，它应该有 type时，你是对的Type -> Type。这里的问题(,)是重载意味着Pair类型构造函数和mkPair数据构造函数，而 Idris 的阐述者做出了错误的选择。

通过显式选择Pair，您可以修复定义：

data AutoM : (m : Type -> Type) -> (a : Type) -> (b : Type) -> Type where
   AutoMC : (a -> m (Pair b (AutoM m a b))) -> AutoM m a b

现在，如果你这样做，你会得到另一个神秘的信息：

Auto.idr:18:14:
When elaborating right hand side of Main.doesntwork.const_auto:
Can't resolve type class Monad m3
Metavariables: Main.doesntwork.const_auto

这里的问题是，您m在类型注释中引入了一个隐式，它与约束已经引入const_auto的不同，因此 Idris 找不到这个 new 的实例。解决方案是根本不引入它（约束提到足以使其在范围内），如下所示：Monad m =>Monadmm

const_auto : Monad m => {a : Type} -> b -> AutoM m a b
于 2015-07-12T21:22:13.090 回答