如何在 Idris/Agda/Coq 中将类型映射到值？答案

【问题标题】：How to map Type to Value in Idris/Agda/Coq?如何在 Idris/Agda/Coq 中将类型映射到值？
【发布时间】：2023-03-06 16:43:01
【问题描述】：

我正在尝试定义一个名为byteWidth 的函数，它捕获了有关“获取特定原子类型的字节宽度”的用法。

我的第一次试用：

byteWidth : Type -> Int
byteWidth Int = 8
byteWidth Char = 1

而 Idris 编译器抱怨：“检查 byteWidth 的左侧时：左侧没有显式类型：Int”

我的第二次试用：

interface BW a where
  byteWidth : a -> Int

implementation BW Int where
  byteWidth _ = 8

implementation BW Char where
  byteWidth _ = 1

在这种情况下，我只能像byteWidth 'a' 一样使用byteWidth，但不能使用byteWidth Char。

【问题讨论】：

标签： coq agda idris dependent-type

【解决方案1】：

您的第二次尝试非常接近原则性解决方案。正如您所观察到的，问题是在实现BW a 时不能将类型a 作为参数。但您不必在意，因为您可以稍后显式设置隐式参数。

这给了我们：

interface BW a where
  byteWidth_ : Int

implementation BW Int where
  byteWidth_ = 8

implementation BW Char where
  byteWidth_= 1

然后您可以通过部分应用byteWidth_ 来恢复您想要的类型，如下所示：

byteWidth : (a : Type) -> BW a => Int
byteWidth a = byteWidth_ {a}

【讨论】：

这可行，但太棘手了...我仍然认为我的解决方案更好...
您的解决方案使用{auto pr : _}，这是一种反模式
感谢您指出这一点，但我不明白为什么它是一种反模式，还有更多细节或示例，或者一些参考资料？
这是一种让系统随机猜测一些证明（达到一定深度）的方法，并且因为它太容易使用，人们滥用它而不是证明他们的问题是可判定的或使用更有原则的搜索策略（例如，这个问题主要涉及的类型类）。
类型类本质上是一种解决问题的开放方法：您可以稍后在意识到需要它们时添加新实例。使用单例+自动的方式，只有对原库有控制权的人才能添加新的案例。它是反模块化的。

【解决方案2】：

在 Idris 中，你不能对类型进行模式匹配，假设你可以，任何人都不可能枚举所有可能的类型，所以它不可能是全部的。

您需要的唯一额外的东西是关于类型 a 的证明在某个特定集合内，我们将这个命题命名为 ByteWidthAvailable。

data ByteWidthAvailable : Type -> Type where
  IntBWA : ByteWidthAvailable Int
  ChaBWA : ByteWidthAvailable Char

total
byteWidth : (a : Type) -> {auto prf: ByteWidthAvailable a} -> Int
byteWidth _ {prf = IntBWA} = 8
byteWidth _ {prf = ChaBWA} = 1

这里唯一的技巧是 Idris 提供的 auto 命令，它有助于在调用现场自动生成证明，这样您就可以像 byteWidth Char 一样调用 byteWidth 而不是 byteWidth Char {prf = ChaBWA}。

【讨论】：