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

我正在尝试定义一个名为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。

最佳答案

您的第二次尝试确实接近原则性的解决方案。如您所见，问题是实现a时不能将BW 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}

关于coq - 如何在Idris/Agda/Coq中将类型映射到值？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/48579329/