Idrisインターフェイスで関数型を制約する

Question

インターフェイスで制約された型の関数を作成したいと思います。私の目的は、VerifiedMonoidをClasses.Verifiedのcontribパッケージから定義して、単純なモノイドソルバーを構築することです。

eval : VerifiedMonoid a => Expr n -> Env a n -> a 

私は愚かな何かをするか、何かが欠けています：evalの型シグネチャのため

Monoid-prover.idr line 29 col 5: 
When checking type of MonoidProver.eval: 
Can't find implementation for VerifiedMonoid a 

：

イドリスは私に次のエラーを与えますか？そのような制約付きの型（evalの型のような）は、Haskellの型のように解釈できますか？

完全なコードを以下に示します。

module MonoidProver 

import Classes.Verified 

import Data.Fin 
import Data.Vect 

%default total 

infixl 5 :+: 

data Expr : Nat -> Type where 
    Var : Fin n -> Expr n 
    Id : Expr n 
    (:+:) : Expr n -> Expr n -> Expr n 

Env : VerifiedMonoid a => (a : Type) -> Nat -> Type 
Env a n = Vect n a 

eval : VerifiedMonoid a => Expr n -> Env a n -> a 
eval (Var i) env = index i env 
eval Id  env = neutral 
eval (e :+: e') env = eval e env <+> eval e' env 

Answer 1

@Cactusコメントで述べたように、ここでの問題は、Envのための型シグネチャが正しくないということです。具体的には、制約は引数の値に依存するため、依存型（pi）型であり、依存型は左から右へ（それらが使用される前に導入されるように）強制されます。私の理解では、基本的にコンパイラは、x : aをの省略形として見ています。ここで、は、量子の右側の型シグネチャの一部です。つまり、(a : Type)は実際には新鮮なaをバインドします。これは、暗黙的に普遍的にバインドされているVerifiedMonoid a制約で使用されていたものと同じではありません（a）。幸いにも

、イドリスはハスケル（ここで、すべてのタイプのクラス制約は型シグネチャの先頭になければならない）ではないので、これは修正するのは簡単です：ちょうどEnv : (a : Type) -> VerifiedMonoid a => Nat -> Typeにあなたの型シグネチャを変更、aは、その前にバインドされているように、使用されている！