Ограничение аргумента функции в интерфейсе

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