在 Idris 中对“高级”类型进行参数化答案

【问题标题】：Parametrising over "higher-kinded" types in Idris在 Idris 中对“高级”类型进行参数化
【发布时间】：2015-07-12 19:48:10
【问题描述】：

我刚开始玩 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 不匹配。所以我试着让它多态一点：

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 没有在const_auto 的定义中的任何地方使用时，为什么会提到(a, b) 的类型？我觉得AutoM 的定义本身已经有问题，但我真的不知道为什么或如何。

【问题讨论】：

标签： monads idris

【解决方案1】：

当你的直觉告诉你 m 是一个 monad 时，你是对的，它应该有 Type -> Type 类型。这里的问题是(,) is overloaded 表示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

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

const_auto : Monad m => {a : Type} -> b -> AutoM m a b

【讨论】：