Puis-je définir le concept général de x == y = p (x) == p (y) dans Idris?

Question

Je veux définir un constructeur de type qui incarne le concept d'utilisation d'un wrapper de type pour définir l'égalité sur un type de domaine t1 en projetant sur un type de domaine t2 avec une fonction p.

L'exemple spécifique suivant fonctionne, où t1 = ABC, t2 = Nat et p est la fonction abc_2_nat:

%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 

Mais, lorsque je tente de généraliser comme suit:

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 obtenir ce trou:

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

Cela ne fonctionne pas car il ne reconnaît pas que p est de type t1->t2 (ce que je veux). Je suppose que je demande trop de fournir la fonction de projection comme argument à un constructeur de type, et que la fonction de projection est disponible dans le cadre de la définition d'une fonction dont les paramètres appartiennent au type construit.

Y a-t-il un moyen pour que cela fonctionne?

Answer 1

C'est possible. La généralisation Projected n'est pas assez précise. Vous devez spécifier les types t1 et t2. Comme ceci:

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

Sans ce compilateur Idris ne peut pas deviner ce genre de chose sont t1 et t2 exactement. Une note de plus: pour comparer les valeurs de type t1 en comparant les projections au domaine t2, vous devez vous assurer que vous pouvez comparer les valeurs de type t2. Ainsi l'égalité de projection générale ressemble à ceci:

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

Et vous pouvez écrire Eq exemple pour elle!

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

Et cela fonctionne également. Donc, si vous définissez quelque chose comme ceci:

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 

Vous pouvez utiliser votre projection abc_2_nat pour mettre en œuvre un projecteur correspondant:

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

Je dois utiliser Main.abc_2_nat pour résoudre ambiguilty car sinon abc_2_nat peut être un paramètre de type implicite . Idris n'a aucun pouvoir pour deviner ce que vous voulez. Volontiers, compilateur m'aide avec cet avertissement:

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

Et maintenant vous pouvez vérifier dans REPL que cela fonctionne!

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

plus de bonus:

Si vous marquez abcNatProjector en implicit fonction, comme ceci:

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

Vous pouvez définir certains opérateurs de fantaisie

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

et comparer les valeurs de type e ABC avec elle sans utiliser explicitement abcNatProjector.

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