在接口中約束函數參數

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