haskell - online - ¿Cuándo es apropiado-XAllowAmbiguousTypes?

haskell core download

Question

Recientemente publiqué una question sobre syntactic-2.0 respecto a la definición de share . He tenido este trabajo en 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

Sin embargo, GHC 7.8 quiere que -XAllowAmbiguousTypes compile con esa firma. Alternativamente, puedo reemplazar la fi con

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

que es el tipo implícito por el fundep en SyntacticN . Esto me permite evitar la extensión. Por supuesto esto es

• un tipo muy largo para agregar a una firma ya grande
• cansado de derivar manualmente
• innecesario debido al fundep

Mis preguntas son:

1. ¿Es este un uso aceptable de -XAllowAmbiguousTypes ?
2. En general, ¿cuándo debería usarse esta extensión? Una respuesta here sugiere que "casi nunca es una buena idea".

3. Aunque he leído los documentos , todavía tengo problemas para decidir si una restricción es ambigua o no. Específicamente, considere esta función de Data.Syntactic.Sugar:

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

   Me parece que fi (y posiblemente sup ) debería ser ambiguo aquí, pero compila sin la extensión. ¿Por qué es sugarSym unívoco mientras que share es? Dado que share es una aplicación de sugarSym , las restricciones de share provienen directamente de sugarSym .

Answer 1

Descubrí que AllowAmbiguousTypes es muy conveniente para usar con TypeApplications . Considere la función natVal :: forall n proxy . KnownNat n => proxy n -> Integer natVal :: forall n proxy . KnownNat n => proxy n -> Integer from GHC.TypeLits .

Para usar esta función, podría escribir natVal (Proxy::Proxy5) . Un estilo alternativo es usar TypeApplications : natVal @5 Proxy . El tipo de Proxy es inferido por la aplicación de tipo, y es molesto tener que escribirlo cada vez que llamas natVal . Así podemos habilitar AmbiguousTypes y escribir:

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

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

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

Sin embargo, tenga en cuenta que una vez que va ambiguo, ¡no puede volver !

Answer 2

No veo ninguna versión publicada de syntactic cuya firma para sugarSym use esos nombres de tipo exactos, así que usaré la rama de desarrollo en commit 8cfd02 ^ , la última versión que todavía usó esos nombres.

Entonces, ¿por qué GHC se queja sobre el fi en su firma de tipo pero no el de sugarSym ? La documentación a la que se ha vinculado explica que un tipo es ambiguo si no aparece a la derecha de la restricción, a menos que la restricción esté usando dependencias funcionales para inferir el tipo ambiguo de otra manera de otros tipos no ambiguos. Entonces, comparemos los contextos de las dos funciones y busquemos dependencias funcionales.

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

Entonces, para sugarSym , los tipos no ambiguos son sub , sig y f , y a partir de ellos deberíamos poder seguir las dependencias funcionales para desambiguar todos los otros tipos utilizados en el contexto, es decir, sup y fi . Y, de hecho, la dependencia funcional f -> internal en SyntacticN utiliza nuestra f para desambiguar nuestra fi , y, a partir de entonces, la dependencia funcional ApplySym f -> sig sym en ApplySym usa nuestra fi recientemente desambiguada para desambiguar sup (y sig , que ya no era ambiguo). Entonces, eso explica por qué sugarSym no requiere la extensión AllowAmbiguousTypes .

Veamos ahora el sugar . Lo primero que noté es que el compilador no se queja de un tipo ambiguo, sino de instancias superpuestas:

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

Entonces, si estoy leyendo esto correctamente, no es que GHC piense que sus tipos son ambiguos, sino que, al verificar si sus tipos son ambiguos, GHC encontró un problema diferente y diferente. Entonces le está diciendo que si le hubiera dicho a GHC que no realizara la verificación de ambigüedad, no habría encontrado ese problema por separado. Esto explica por qué habilitar AllowAmbiguousTypes permite que su código se compile.

Sin embargo, el problema con las instancias superpuestas permanece. Las dos instancias enumeradas por GHC ( SyntacticN f fi y SyntacticN (a -> f) ... ) se superponen entre sí. Por extraño que parezca, parece que el primero de estos debería superponerse con cualquier otra instancia, lo cual es sospechoso. ¿Y qué significa [overlap ok] ?

Sospecho que Syntactic está compilado con OverlappingInstances. Y mirando el código , de hecho lo hace.

Experimentando un poco, parece que GHC está bien con los casos que se superponen cuando está claro que uno es estrictamente más general que el otro:

{-# 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])

Pero GHC no está de acuerdo con los casos que se superponen cuando ninguno de ellos es claramente mejor que el otro:

{-# 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])

La firma de su tipo utiliza SyntacticN (a -> (a -> b) -> b) fi , y ni SyntacticN f fi ni SyntacticN (a -> f) (AST sym (Full ia) -> fi) se ajusta mejor que el otro. Si cambio esa parte de su firma de tipo a SyntacticN a fi o SyntacticN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi) , GHC ya no se queja de la superposición.

Si fuera usted, vería la definición de esas dos posibles instancias y determinaría si una de esas dos implementaciones es la que usted desea.