在接口中约束函数参数

Question

在接受函数的接口中约束函数参数的语法是什么？我试过了：

interface Num a => Color (f : a -> Type) where
     defs...

但是它说 Name a is not bound in interface...

Answer 1

你的interface实际上有两个参数：a和f。但是 f 应该足以选择一个 implementation:

interface Num a => Color (a : Type) (f : a -> Type) | f where

f这里叫一个determining parameter.

这是一个荒谬的完整示例：

import Data.Fin

interface Num a => Color (a : Type) (f : a -> Type) | f where
  foo : (x : a) -> f (1 + x)

Color Nat Fin where
  foo _ = FZ

x : Fin 6
x = foo {f = Fin} 5

在接口中约束函数参数

Constraining a function argument in an interface

idris