实施半群在伊德里斯

Question

我试图实现Semigroup接口，用于伊德里斯简单依赖对，取决于对但这并不编译：

Semigroup (n ** Vect n f) where 
    (<+>) (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

与错误

Type mismatch between 
    ty 
and 
    Nat 

但是这样编译：

myPair:Type -> Type 
myPair f = (n ** Vect n f) 

Semigroup (myPair f) where 
    (<+>) (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

为什么？什么是完成这个最好的方法？

Answer 1

伊德里斯FAQ：

如果您在以小写字母开头，并没有施加任何参数的类型使用的名称，然后将伊德里斯把它作为一个隐含的约束参数。

一种方法来解决这一问题将是摆脱一些语法糖，并明确绑定n这样的：

Semigroup (DPair Nat (\n => Vect n f)) where 
    (<+>) = (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

另一种方法是使用一个大写字母为向量长度：

Semigroup (N ** Vect N f) where 
    (<+>) = (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

这里，N没有得到约束在Semigroup实施，这使得DPair语法糖正如我们在第一个变体中所做的一样，踢入并绑定N。

至于myPair的例子，它编译，因为这个例子基本上等于上面的例子DPair。如果你刚刚取出糖，一切都变得清晰：

myPair:Type -> Type 
myPair f = DPair Nat (\n => Vect n f)