Puis-je écrire une fonction générique de retour à la ligne pour une interface Wrapper représentant un type qui enveloppe un autre type?

Question

L'exemple de code complet ci-dessous (qui compile avec succès) est un exemple simplifié et légèrement artificiel de mon problème.

NatPair est une paire de Nat s, et je veux « ascenseur » les opérations binaires Num à NatPair pointwise, en utilisant la fonction lift_binary_op_to_pair.

Mais je ne peux pas implémenter Num NatPair car NatPair n'est pas un constructeur de données.

Alors, je l'enveloppe dans un type WrappedNatPair, et je peux fournir une implémentation Num pour ce type, avec des versions « » correspondantes de levées + et *. Puis je veux généraliser l'idée d'un type de wrapper, avec mon interface Wrapper.

La fonction lift_natpair_bin_op_to_wrapped peut soulever une opération binaire de NatPair à WrappedNatPair, et le code de mise en œuvre est tout à fait en termes de unwrap et wrapWrapper méthodes d'interface.

Mais, si je tente de généraliser à

lift_bin_op_to_wrapped : Wrapper t => BinaryOp WrappedType -> BinaryOp t 

alors la signature de type ne sera même pas compiler, avec l'erreur:

`-- Wrapping.idr line 72 col 23: 
    When checking type of Main.lift_bin_op_to_wrapped: 
    Can't find implementation for Wrapper t 

(où l'emplacement d'erreur est l'emplacement « : 'dans la signature de type).

Je pense que le problème est que t ne figure nulle part dans la signature de type pour la méthode d'interface WrapperWrapperType, donc WrapperType ne peut être invoqué partout ailleurs qu'à l'intérieur la définition de l'interface elle-même.

(La solution consiste à écrire boilerplate lift_<wrapped>_bin_op_to_<wrapper> méthodes avec le même code de mise en œuvre op x y = wrap $ op (unwrap x) (unwrap y) chaque fois, ce qui est intolérable. Mais je voudrais avoir une compréhension claire des raisons pour lesquelles je ne peux pas écrire la méthode lift_bin_op_to_wrapped générique.)

Le code complet qui compile avec succès:

%default total 

PairedType : (t : Type) -> Type 
PairedType t = (t, t) 

NatPair : Type 
NatPair = PairedType Nat 

data WrappedNatPair : Type where 
    MkWrappedNatPair : NatPair -> WrappedNatPair 

equal_pair : t -> PairedType t 
equal_pair x = (x, x) 

BinaryOp : Type -> Type 
BinaryOp t = t -> t -> t 

lift_binary_op_to_pair : BinaryOp t -> BinaryOp (PairedType t) 
lift_binary_op_to_pair op (x1, x2) (y1, y2) = (op x1 y1, op x2 y2) 

interface Wrapper t where 
    WrappedType : Type 
    wrap : WrappedType -> t 
    unwrap : t -> WrappedType 

Wrapper WrappedNatPair where 
    WrappedType = NatPair 
    wrap x = MkWrappedNatPair x 
    unwrap (MkWrappedNatPair x) = x 

lift_natpair_bin_op_to_wrapped : BinaryOp NatPair -> BinaryOp WrappedNatPair 
lift_natpair_bin_op_to_wrapped op x y = wrap $ op (unwrap x) (unwrap y) 

Num WrappedNatPair where 
    (+) = lift_natpair_bin_op_to_wrapped (lift_binary_op_to_pair (+)) 
    (*) = lift_natpair_bin_op_to_wrapped (lift_binary_op_to_pair (*)) 
    fromInteger x = wrap $ equal_pair (fromInteger x) 

WrappedNatPair_example : the WrappedNatPair 8 = (the WrappedNatPair 2) + (the WrappedNatPair 6) 
WrappedNatPair_example = Refl 

(Plate-forme: Ubuntu 16.04 en cours d'exécution Idris 1.1.1-git:. 83b1bed)

Answer 1

I think the problem is that t doesn't appear anywhere in the type signature for the Wrapper interface WrapperType method, so WrapperType can't be invoked anywhere other than inside the interface definition itself.

Vous êtes ici. C'est pourquoi vous recevez cette erreur. Vous pouvez corriger cette erreur de compilation en spécifiant explicitement quels types est wrapper comme ceci:

lift_bin_op_to_wrapped : Wrapper w => BinaryOp (WrappedType {t=w}) -> BinaryOp w 
lift_bin_op_to_wrapped {w} op x y = ?hole 

Mais ce ne sera probablement pas vous aider, car Idris peut en quelque sorte pas en déduire la correspondance entre w et WrappedType. J'aimerais voir une explication de ce fait. Fondamentalement compilateur (j'utilise Idris 1.0) m'a dit les choses suivantes:

- + Wrap.hole [P] 
`--   w : Type 
       x : w 
       y : w 
     constraint : Wrapper w 
       op : BinaryOp WrappedType 
    ----------------------------------- 
     Wrap.hole : w 

Votre WrappedType méthode d'interface dépendamment typé implémente pattern matching sur les types d'une manière délicate. Je pense que cela pourrait être une raison pour laquelle vous avez des problèmes. Si vous êtes familier avec Haskell vous pourriez voir quelques similitudes entre votre WrappedType et -XTypeFamilies. Voir cette question: Pattern matching on Type in Idris

Bien que vous puissiez toujours implémenter la fonction d'encapsulation générale. Vous avez seulement besoin de définir votre interface différemment. J'utilise astuce décrite dans cette question: Constraining a function argument in an interface

interface Wraps (from : Type) (to : Type) | to where 
    wrap : from -> to 
    unwrap : to -> from 

Wraps NatPair WrappedNatPair where 
    wrap = MkWrappedNatPair 
    unwrap (MkWrappedNatPair x) = x 

lift_bin_op_to_wrapped : Wraps from to => BinaryOp from -> BinaryOp to 
lift_bin_op_to_wrapped op x y = wrap $ op (unwrap x) (unwrap y) 

Num WrappedNatPair where 
    (+) = lift_bin_op_to_wrapped (lift_binary_op_to_pair {t=Nat} (+)) 
    (*) = lift_bin_op_to_wrapped (lift_binary_op_to_pair {t=Nat}(*)) 
    fromInteger = wrap . equal_pair {t=Nat} . fromInteger 

Ceci compile et fonctionne parfaitement.