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

Question

我正在尝试定义一个名为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，如 byteWidth 'a'，但不能使用 byteWidth Char。

Answer 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}