インターフェイスの関数引数を制限する

Question

関数を引数とするインターフェイスの関数引数を制約する構文は何ですか？

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

をしかし、それはあなたのinterfaceName a is not bound in interface...

Answer 1

は、実際には2つのパラメータを持っていると言う：私が試したaとfを。 determining parameterと呼ばれ、ここで

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

f：しかしfはimplementationを選ぶのに十分でなければなりません。

ここでは無意味な完全な例です：

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