时间戳

首页 > 解决方案 > 在签名中找不到具有约束的实现

idris - 在签名中找不到具有约束的实现

问题描述

我有一个依赖于另一个接口的接口，具有一些依赖类型，我无法让编译器在相关函数中约束一个类型

import Data.Vect

interface Distribution (0 event : Nat) (dist : Nat -> Nat -> Type) where

data Gaussian : Nat -> Nat -> Type where

Distribution e Gaussian where

interface Distribution targets marginal =>
 Model (targets : Nat) (marginal : Nat -> Nat -> Type) model where
  marginalise : model -> Vect s Double -> marginal targets s

foo : m -> Model 1 Gaussian m => Vect s Double -> Nat
foo model x = let marginal = marginalise model x in ?rhs

我明白了

While processing right hand side of foo. Can't find an implementation for Model ?targets ?marginal m.

foo model x = let marginal = marginalise model x in ?rhs  
                             ^^^^^^^^^^^^^^^^^^^

这怎么可能？

如果我使用marginalise {marginal=Gaussian} {targets=1} model x它进行类型检查，但我不明白为什么这还不是由类型签名确定的。

我不认为我问的这个关于同一领域的问题在这里适用

标签： idris

解决方案

我开始写这篇评论作为评论，并在中途意识到它可能是一个完整的答案。

Model 1 Gaussan m意味着你有一个Model接口的实现targets = 1,marginal = Gaussian和model = m。然后， let 绑定marginalrequires Model a b m，即Modelwheretargets = a和marginal = b的实现model = m。但是没有要求a = 1和b = Gaussian！

我的猜测是，一旦你阅读了确定参数，你会发现你想要这样的东西：

interface Distribution targets marginal =>
 Model (targets : Nat) (marginal : Nat -> Nat -> Type) model | model where

推荐阅读