J'ai récemment posté une question sur syntactic-2.0 concernant la définition de share
. J'ai eu ce travail dans GHC 7.6 :
{-# LANGUAGE GADTs, TypeOperators, FlexibleContexts #-}
import Data.Syntactic
import Data.Syntactic.Sugar.BindingT
data Let a where
Let :: Let (a :-> (a -> b) :-> Full b)
share :: (Let :<: sup,
sup ~ Domain b, sup ~ Domain a,
Syntactic a, Syntactic b,
Syntactic (a -> b),
SyntacticN (a -> (a -> b) -> b)
fi)
=> a -> (a -> b) -> b
share = sugarSym Let
Cependant, GHC 7.8 veut -XAllowAmbiguousTypes
compiler avec cette signature. Alternativement, je peux remplacer le fi
par
(ASTF sup (Internal a) -> AST sup ((Internal a) :-> Full (Internal b)) -> ASTF sup (Internal b))
qui est le type impliqué par le fundep on SyntacticN
. Cela me permet d'éviter l'extension. Bien sûr, c'est
- un type très long à ajouter à une signature déjà volumineuse
- fastidieux à dériver manuellement
- inutile en raison du fundep
Mes questions sont:
- Est-ce une utilisation acceptable de
-XAllowAmbiguousTypes
? - En général, quand utiliser cette extension? Une réponse ici suggère "ce n'est presque jamais une bonne idée".
Bien que j'aie lu les documents , j'ai toujours du mal à décider si une contrainte est ambiguë ou non. En particulier, considérez cette fonction de Data.Syntactic.Sugar:
sugarSym :: (sub :<: AST sup, ApplySym sig fi sup, SyntacticN f fi) => sub sig -> f sugarSym = sugarN . appSym
Il me semble que
fi
(et peut-êtresup
) devrait être ambigu ici, mais il compile sans l'extension. Pourquoi est-ilsugarSym
sans ambiguïtéshare
? Puisqueshare
c'est une application desugarSym
, lesshare
contraintes viennent toutes directementsugarSym
.
sugarSym Let
, qui est(SyntacticN f (ASTF sup a -> ASTF sup (a -> b) -> ASTF sup b), Let :<: sup) => f
et n'implique pas de variables de type ambiguë?share
, mais ne compile lorsque l'une des signatures mentionnées dans la question est utilisée. Votre question a également été posée dans les commentaires d'un post précédentf
seul est suffisant pour pleinement désambiguïsersig
,fi
etsup
.SyntacticN
rendfi
sans ambiguïté ensugarSym
, mais alors pourquoi est-ce pas la même chose pourfi
enshare
?Réponses:
Je ne vois aucune version publiée de syntaxique dont la signature
sugarSym
utilise ces noms de type exacts, donc j'utiliserai la branche de développement à commit 8cfd02 ^ , la dernière version qui utilisait toujours ces noms.Alors, pourquoi GHC se plaint-il de la
fi
signature de votre type mais pas de celle poursugarSym
? La documentation à laquelle vous avez lié explique qu'un type est ambigu s'il n'apparaît pas à droite de la contrainte, sauf si la contrainte utilise des dépendances fonctionnelles pour déduire le type par ailleurs ambigu à partir d'autres types non ambigus. Comparons donc les contextes des deux fonctions et recherchons les dépendances fonctionnelles.Donc pour
sugarSym
, les types non ambigus sontsub
,sig
etf
, à partir de ceux-ci, nous devrions pouvoir suivre les dépendances fonctionnelles afin de lever l'ambiguïté de tous les autres types utilisés dans le contexte, à savoirsup
etfi
. Et en effet, laf -> internal
dépendance fonctionnelle dansSyntacticN
utilise notref
pour lever l'ambiguïtéfi
, et par la suite laf -> sig sym
dépendance fonctionnelle dansApplySym
utilise notre nouvellement désambiguïséfi
pour lever l' ambiguïtésup
(etsig
, ce qui était déjà non ambigu). Cela explique pourquoisugarSym
ne nécessite pas l'AllowAmbiguousTypes
extension.Regardons maintenant
sugar
. La première chose que je remarque est que le compilateur ne se plaint pas d'un type ambigu, mais plutôt de superpositions d'instances:Donc, si je lis bien, ce n'est pas que GHC pense que vos types sont ambigus, mais plutôt, qu'en vérifiant si vos types sont ambigus, GHC a rencontré un problème différent et distinct. Il vous indique ensuite que si vous aviez demandé à GHC de ne pas effectuer la vérification d'ambiguïté, il n'aurait pas rencontré ce problème distinct. Cela explique pourquoi l'activation de AllowAmbiguousTypes permet à votre code de se compiler.
Cependant, le problème avec les instances qui se chevauchent reste. Les deux instances répertoriées par GHC (
SyntacticN f fi
etSyntacticN (a -> f) ...
) se chevauchent. Curieusement, il semble que le premier d'entre eux devrait se chevaucher avec toute autre instance, ce qui est suspect. Et qu'est-ce que cela[overlap ok]
signifie?Je soupçonne que Syntactic est compilé avec OverlappingInstances. Et en regardant le code , c'est le cas.
En expérimentant un peu, il semble que GHC accepte les instances qui se chevauchent lorsqu'il est clair que l'une est strictement plus générale que l'autre:
Mais GHC n'est pas d'accord avec des instances qui se chevauchent lorsque ni l'une ni l'autre n'est clairement mieux adaptée que l'autre:
Votre signature de type utilise
SyntacticN (a -> (a -> b) -> b) fi
, et ni l'unSyntacticN f fi
ni l' autre neSyntacticN (a -> f) (AST sym (Full ia) -> fi)
convient mieux que l'autre. Si je change cette partie de votre signature de type enSyntacticN a fi
ouSyntacticN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi)
, GHC ne se plaint plus du chevauchement.Si j'étais vous, je regarderais la définition de ces deux instances possibles et déterminer si l'une de ces deux implémentations est celle que vous voulez.
la source
J'ai découvert que
AllowAmbiguousTypes
c'est très pratique à utiliser avecTypeApplications
. Considérez la fonctionnatVal :: forall n proxy . KnownNat n => proxy n -> Integer
de GHC.TypeLits .Pour utiliser cette fonction, je pouvais écrire
natVal (Proxy::Proxy5)
. Un autre style est d'utiliserTypeApplications
:natVal @5 Proxy
. Le type deProxy
est déduit par l'application de type, et c'est ennuyeux de devoir l'écrire à chaque fois que vous appeleznatVal
. Ainsi, nous pouvons activerAmbiguousTypes
et écrire:Cependant, notez qu'une fois que vous devenez ambigu, vous ne pouvez pas revenir en arrière !
la source