如何在Idris/Agda/Coq中映射Type到Value？

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

您的第二次尝试非常接近原则解决方案.正如您所观察到的那样,问题在于您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}