Seltsame Fehlermeldung mit Idris Schnittstellen

Question

Ich versuche, eine einfache algebraische Strukturen Hierarchie mit Idris-Schnittstellen zu implementieren. Der Code lautet wie folgt:

module AlgebraicStructures 

-- definition of some algebraic structures in terms of type classes 

%access public export 

Associative : {a : Type} -> (a -> a -> a) -> Type 
Associative {a} op = (x : a) -> 
        (y : a) -> 
        (z : a) -> 
        (op x (op y z)) = (op (op x y) z) 

Identity : {a : Type} -> (a -> a -> a) -> a -> Type 
Identity op v = ((x : a) -> (op x v) = x, 
       (x : a) -> (op v x) = x)     


Commutative : {a : Type} -> (a -> a -> a) -> Type 
Commutative {a} op = (x : a) -> 
        (y : a) -> 
        (op x y) = (op y x) 


infixl 4 <**> 

interface IsMonoid a where 
    empty : a 
    (<**>) : a -> a -> a 
    assoc : Associative (<**>) 
    ident : Identity (<**>) empty 


interface IsMonoid a => IsCommutativeMonoid a where 
    comm : Commutative (<**>) 

Aber Idris schenkt diese seltsame Fehlermeldung:

When checking type of constructor of AlgebraicStructures.IsCommutativeMonoid: 
Can't find implementation for IsMonoid a 

Ich glaube, dass Idris Werke wie Haskells Typklassen-Schnittstellen. In Haskell sollte es funktionieren. Mache ich etwas Dummes?

Answer 1

Ich glaube, es beschwert werden, weil ich nicht weiß, dass es etwas gibt, das die a im Ausdruck zwingt Commutative (<**>) - so es nicht weiß, dass Sie <**> auf diese Art aufrufen kann. Explizit Angabe der a scheint für mich zu arbeiten - Commutative {a} (<**>) - ich hoffe, dass das bedeutet, dass die a von der Schnittstelle Signatur ist im Umfang und verfügbar für die explizite Weitergabe an andere Typen.