Quando -XAllowAmbiguousTypes é apropriado?

212

Recentemente, publiquei uma pergunta sobre sintático-2.0 com relação à definição de share. Eu tive isso trabalhando no 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

No entanto, o GHC 7.8 deseja -XAllowAmbiguousTypescompilar com essa assinatura. Como alternativa, posso substituir o fipor

(ASTF sup (Internal a) -> AST sup ((Internal a) :-> Full (Internal b)) -> ASTF sup (Internal b))

qual é o tipo implícito no fundep on SyntacticN. Isso me permite evitar a extensão. Claro que isso é

  • um tipo muito longo para adicionar a uma assinatura já grande
  • cansativo derivar manualmente
  • desnecessário devido ao fundep

Minhas perguntas são:

  1. Esse é um uso aceitável -XAllowAmbiguousTypes?
  2. Em geral, quando essa extensão deve ser usada? Uma resposta aqui sugere "quase nunca é uma boa ideia".
  3. Embora eu tenha lido os documentos , ainda estou tendo problemas para decidir se uma restrição é ambígua ou não. Especificamente, considere esta função do Data.Syntactic.Sugar:

    sugarSym :: (sub :<: AST sup, ApplySym sig fi sup, SyntacticN f fi) 
             => sub sig -> f
    sugarSym = sugarN . appSym
    

    Parece-me que fi(e possivelmente sup) deve ser ambíguo aqui, mas compila sem a extensão. Por que é sugarSyminequívoco enquanto shareé? Como shareé uma aplicação de sugarSym, sharetodas as restrições vêm diretamente sugarSym.

crockeea
fonte
4
Existe alguma razão pela qual você não pode usar apenas o tipo inferido para sugarSym Let, que é (SyntacticN f (ASTF sup a -> ASTF sup (a -> b) -> ASTF sup b), Let :<: sup) => fe não envolve variáveis ​​de tipo ambíguas?
kosmikus
3
@kosmikus Sorrt Demorou tanto tempo para responder. Esse código não é compilado com a assinatura inferida para share, mas é compilado quando qualquer uma das assinaturas mencionadas na pergunta é usada. Você pergunta também foi questionado nos comentários de um post anterior
crockeea
3
Comportamento indefinido provavelmente não é o termo mais adequado. É difícil entender apenas com base em um programa. O problema é a confiabilidade e o GHCI não conseguir provar os tipos no seu programa. Há uma longa discussão que pode lhe interessar apenas sobre esse assunto. haskell.org/pipermail/haskell-cafe/2008-April/041397.html
BlamKiwi
6
Quanto a (3), esse tipo não é ambíguo por causa das Dependências Funcionais na definição de SyntacticN (isto é, f - fi) e ApplySym (em particular fi -> sig, sup). A partir daí, você começa que fpor si só é suficiente para totalmente disambiguate sig, fie sup.
User2141650
3
@ user2141650 Desculpe, demorou muito para responder. Você está dizendo que o fundep on SyntacticNtorna fiinequívoca a entrada sugarSym, mas então por que o mesmo não é verdadeiro para a fiin share?
Crockeea

Respostas:

12

Não vejo nenhuma versão publicada do sintático cuja assinatura sugarSymuse exatamente esses nomes de tipos, portanto, usarei o ramo de desenvolvimento em commit 8cfd02 ^ , a última versão que ainda usava esses nomes.

Então, por que o GHC se queixa da fiassinatura do seu tipo, mas não a assinatura sugarSym? A documentação à qual você vinculou explica que um tipo é ambíguo se não aparecer à direita da restrição, a menos que ela esteja usando dependências funcionais para inferir o tipo ambíguo de outros tipos não ambíguos. Então, vamos comparar os contextos das duas funções e procurar dependências funcionais.

class ApplySym sig f sym | sig sym -> f, f -> sig sym
class SyntacticN f internal | f -> internal

sugarSym :: ( sub :<: AST sup
            , ApplySym sig fi sup
            , SyntacticN f fi
            ) 
         => sub sig -> f

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

Portanto sugarSym, os tipos não ambíguos são sub, sige f, dentre esses, devemos ser capazes de seguir dependências funcionais para desambiguar todos os outros tipos usados ​​no contexto, a saber, supe fi. E, de fato, a f -> internaldependência funcional SyntacticNusa nosso fpara desambiguar nossa fie, posteriormente, a f -> sig symdependência funcional ApplySymusa nosso recém-desambiguar fipara desambiguar sup(e sig, que já era não ambíguo). Então, isso explica por sugarSymque não requer a AllowAmbiguousTypesextensão.

Vamos agora olhar sugar. A primeira coisa que noto é que o compilador não está reclamando de um tipo ambíguo, mas sim de instâncias sobrepostas:

Overlapping instances for SyntacticN b fi
  arising from the ambiguity check for share
Matching givens (or their superclasses):
  (SyntacticN (a -> (a -> b) -> b) fi1)
Matching instances:
  instance [overlap ok] (Syntactic f, Domain f ~ sym,
                         fi ~ AST sym (Full (Internal f))) =>
                        SyntacticN f fi
    -- Defined in ‘Data.Syntactic.Sugar’
  instance [overlap ok] (Syntactic a, Domain a ~ sym,
                         ia ~ Internal a, SyntacticN f fi) =>
                        SyntacticN (a -> f) (AST sym (Full ia) -> fi)
    -- Defined in ‘Data.Syntactic.Sugar’
(The choice depends on the instantiation of b, fi’)
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes

Portanto, se estou lendo isso corretamente, não é que o GHC pense que seus tipos são ambíguos, mas sim, ao verificar se seus tipos são ambíguos, o GHC encontrou um problema diferente e separado. É então dizer que se você dissesse ao GHC para não executar a verificação de ambiguidade, ele não teria encontrado esse problema separado. Isso explica por que ativar o AllowAmbiguousTypes permite que seu código seja compilado.

No entanto, o problema com as instâncias sobrepostas permanece. As duas instâncias listadas pelo GHC ( SyntacticN f fie SyntacticN (a -> f) ...) se sobrepõem. Estranhamente, parece que o primeiro deles deve se sobrepor a qualquer outra instância, o que é suspeito. E o que isso [overlap ok]significa?

Suspeito que o Syntactic seja compilado com OverlappingInstances. E olhando o código , de fato ele faz.

Experimentando um pouco, parece que o GHC concorda com instâncias sobrepostas quando fica claro que uma é estritamente mais geral que a outra:

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

class Foo a where
  whichOne :: a -> String

instance Foo a where
  whichOne _ = "a"

instance Foo [a] where
  whichOne _ = "[a]"

-- |
-- >>> main
-- [a]
main :: IO ()
main = putStrLn $ whichOne (undefined :: [Int])

Mas o GHC não concorda com instâncias sobrepostas quando nenhuma delas é claramente mais adequada que a outra:

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

class Foo a where
  whichOne :: a -> String

instance Foo (f Int) where  -- this is the line which changed
  whichOne _ = "f Int"

instance Foo [a] where
  whichOne _ = "[a]"

-- |
-- >>> main
-- Error: Overlapping instances for Foo [Int]
main :: IO ()
main = putStrLn $ whichOne (undefined :: [Int])

Sua assinatura de tipo usa SyntacticN (a -> (a -> b) -> b) fi, e SyntacticN f finem SyntacticN (a -> f) (AST sym (Full ia) -> fi)é melhor que a outra. Se eu alterar essa parte da sua assinatura de tipo para SyntacticN a fiou SyntacticN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi), o GHC não reclamará mais da sobreposição.

Se eu fosse você, examinaria a definição dessas duas instâncias possíveis e determinaria se uma dessas duas implementações é a que você deseja.

gelisam
fonte
2

Eu descobri que AllowAmbiguousTypesé muito conveniente para uso TypeApplications. Considere a função natVal :: forall n proxy . KnownNat n => proxy n -> Integerde GHC.TypeLits .

Para usar esta função, eu poderia escrever natVal (Proxy::Proxy5). Um estilo alternativo é usar TypeApplications: natVal @5 Proxy. O tipo de Proxyé inferido pelo aplicativo de tipo e é irritante ter que escrevê-lo toda vez que você ligar natVal. Assim, podemos ativar AmbiguousTypese escrever:

{-# Language AllowAmbiguousTypes, ScopedTypeVariables, TypeApplications #-}

ambiguousNatVal :: forall n . (KnownNat n) => Integer
ambiguousNatVal = natVal @n Proxy

five = ambiguousNatVal @5 -- no `Proxy ` needed!

No entanto, observe que, uma vez ambíguo, você não pode voltar !

crockeea
fonte