Kann ich das allgemeine Konzept von x == y = p (x) == p (y) in Idris definieren?

Question

Ich möchte einen Typkonstruktor definieren, der das Konzept der Verwendung eines Typwrappers zum Definieren der Gleichheit in einem Domänen-Typ t1 durch Projektion auf einen Domänen-Typ t2 mit einer Funktion p verkörpert.

Das folgende spezielle Beispiel funktioniert, wo t1 = ABC, t2 = Nat und p die Funktion abc_2_nat ist:

%default total 

data ABC = A | B | C 

abc_2_nat : ABC -> Nat 
abc_2_nat A = 1 
abc_2_nat B = 1 
abc_2_nat C = 2 

data Projected_abc : Type where 
    Project_abc : ABC -> Projected_abc 

Projected_abc_equals : Projected_abc -> Projected_abc -> Bool 
Projected_abc_equals (Project_abc x) (Project_abc y) = abc_2_nat x == abc_2_nat y 

Eq Projected_abc where 
    (==) = Projected_abc_equals 

Aber, wenn ich zu verallgemeinern versuchen, wie folgt:

data Projected : t1 -> t2 -> (p: t1 -> t2) -> Type 
    where Project : t1 -> Projected t1 t2 p 

Projected_equals : Projected t1 t2 p -> Projected t1 t2 p -> Bool 
Projected_equals (Project x) (Project y) = ?hole 

I Holen Sie sich dieses Loch:

- + Main.hole [P] 
`--  phTy : Type 
      t2 : phTy 
       p : Type -> phTy 
      t1 : Type 
       x : t1 
       y : t1 
    -------------------------- 
     Main.hole : Bool 

Dies funktioniert nicht, weil es nicht erkennt, dass vom Typ t1->t2 ist (was ich will).

Ich vermute, dass ich zu viel frage, um die Projektionsfunktion als Argument für einen Typkonstruktor zu liefern, und irgendwie die Projektionsfunktion im Rahmen der Definition einer Funktion zur Verfügung haben, deren Parameter zum konstruierten Typ gehören.

Gibt es einen Weg, wie ich das zum Laufen bringen kann?

Answer 1

Es ist möglich. Sie Projected Generalisierung ist nicht genau genug. Sie sollten die Typen t1 und t2 angeben. Wie folgt aus:

data Projected : (t1: Type) -> (t2: Type) -> (p: t1 -> t2) -> Type where 
    Project : t1 -> Projected t1 t2 p 

Ohne diesen Idris Compiler kann nicht erraten, welche Art von Sache sind t1 und t2 genau. Noch eine Anmerkung: Um Werte vom Typ t1 zu vergleichen, indem Sie Projektionen mit der Domäne t2 vergleichen, sollten Sie sicher sein, dass Sie Werte vom Typ t2 vergleichen können. So allgemeine Projektion Gleichheit sieht wie folgt aus:

projected_equals : Eq t2 => Projected t1 t2 p -> Projected t1 t2 p -> Bool 
projected_equals {p} (Project x) (Project y) = p x == p y 

Und Sie können es Eq Instanz schreiben!

Eq t2 => Eq (Projected t1 t2 p) where 
    (==) = projected_equals 

Und es funktioniert auch. Also, wenn Sie so etwas wie folgt definieren:

data ABC = A | B | C 

abc_2_nat : ABC -> Nat 
abc_2_nat A = 1 
abc_2_nat B = 1 
abc_2_nat C = 2 

können Sie Ihre abc_2_nat Projektion verwenden, um entsprechende Projektor zu implementieren:

abcNatProjector : ABC -> Projected ABC Nat Main.abc_2_nat 
abcNatProjector abc = Project abc 

Ich habe Main.abc_2_nat verwenden ambiguilty zu lösen, da sonst abc_2_nat jede implizite Typparameter sein kann . Idris hat keine Macht zu erraten, was Sie wollen. Gern hilft mir der Compiler bei dieser Warnung:

Eq.idr:13:37-46:WARNING: abc_2_nat is bound as an implicit 
    Did you mean to refer to Main.abc_2_nat? 

Und jetzt können Sie in REPL einchecken, dass es funktioniert!

λΠ> abcNatProjector A == abcNatProjector B 
True : Bool 
λΠ> abcNatProjector A == abcNatProjector C 
False : Bool 

Bonus Zusatz:

Wenn Sie abcNatProjector als implicit Funktion, wie diese markieren:

implicit 
abcNatProjector : ABC -> Projected ABC Nat Main.abc_2_nat 
abcNatProjector abc = Project abc 

Sie können einige ausgefallene Operator definieren

infixr 5 ==^ 
(==^) : Eq t2 => Projected t1 t2 p -> Projected t1 t2 p -> Bool 
(==^) = projected_equals 

und Werte vergleichen von typ e ABC mit ihm ohne abcNatProjector explizit zu verwenden.

λΠ> A ==^ B 
True : Bool 
λΠ> A ==^ C 
False : Bool