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

【问题标题】：Haskell TypeApplication-like way of explicitly picking an implementation of an interface显式选择接口实现的类似 Haskell TypeApplication 的方式
【发布时间】：2021-08-08 03:53:17
【问题描述】：

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

中找不到Gaussian 的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
    |      ^^^^^^^^^^^^^^^^^^^^^^^

【问题讨论】：

标签： interface idris implements

【解决方案1】：

你的范围是错误的；在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)。所以Distribution d中的d现在被绑定了，没有自动的隐式绑定。

但是，这不是惯用的 Idris。相反，您应该使用Distribution d-bound 隐式参数，而不用担心使其显式化的技巧：

KnowledgeBased : Distribution d => Type

ei : KnowledgeBased {d = Gaussian}

【讨论】：

我更改了标题，因为我认为它会帮助其他人更容易地找到这个问题——很多人去 Idris 时都有 Haskell 经验。我认为惯用的版本是Knowledgebased {d = Gaussian}。