类似 Haskell TypeApplication 的显式选择接口实现的方式

问题描述

我使用的是 Idris 2 v0.3。我不明白为什么编译器在

中找不到 Gaussian of Distribution 的实现

interface Distribution dist where
  mean : dist -> Double

data Gaussian : Type where
  MkGaussian : Double -> Gaussian

Distribution Gaussian where
    mean (MkGaussian mean') = mean'

KnowledgeBased : Distribution d => (d : Type) -> Type

ei : KnowledgeBased Gaussian

我收到错误

"src/Foo.idr" 12L,459C written
Error: While processing type of ei. Can't find an implementation for Distribution ?d.

.../src/Foo.idr:12:6--12:29
    |
 12 | ei : KnowledgeBased Gaussian
    |      ^^^^^^^^^^^^^^^^^^^^^^^

解决方法

你的范围是错误的；在Distribution d => (d : Type) -> Type中，Distribution d部分隐式绑定d，然后被d : Type遮蔽。

相反，您想要的是：

KnowledgeBased : (d : Type) -> Distribution d => Type

这里，第一个 d : Type 将 d 与 Pi 绑定；它解析为 (d : Type) -> (Distribution d => Type)。所以 d 中的 Distribution d 现在是绑定的，没有自动进行隐式绑定。

然而，这不是惯用的 Idris。相反，您应该使用 Distribution d 绑定的隐式参数，而不必担心使其显式的技巧：

KnowledgeBased : Distribution d => Type

ei : KnowledgeBased {d = Gaussian}