Einschränken eines Funktionsarguments in einer Schnittstelle

Question

Wie lautet die Syntax zum Einschränken eines Funktionsarguments in einer Schnittstelle, die eine Funktion übernimmt? Ich habe versucht:

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

Aber es sagt der Name a is not bound in interface...

Answer 1

Ihre interface tatsächlich hat zwei Parameter: a und f. Aber f sollte genug sein implementation ein holen:

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

f hier genannt wird, ein determining parameter.

Hier ist eine unsinnige Voll Beispiel:

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