Kiedy właściwe jest ustawienie -XAllowAmbiguousTypes?

Niedawno opublikowałem pytanie dotyczące syntactic-2.0 dotyczące definicji share. Pracowałem w 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

Jednak GHC 7.8 chce -XAllowAmbiguousTypessię skompilować z tym podpisem. Ewentualnie mogę wymienić fiz

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

który jest typem sugerowanym przez fundep on SyntacticN. To pozwala mi uniknąć rozszerzenia. Oczywiście, że tak

• bardzo długi typ, który można dodać do już dużego podpisu
• męczące, aby ręcznie czerpać
• niepotrzebne ze względu na fundep

Moje pytania to:

1. Czy jest to dopuszczalne użycie -XAllowAmbiguousTypes?
2. Zasadniczo, kiedy należy użyć tego rozszerzenia? Odpowiedź tutaj sugeruje, że „prawie nigdy nie jest to dobry pomysł”.

3. Chociaż czytałem dokumenty , nadal mam problem z określeniem, czy ograniczenie jest niejednoznaczne, czy nie. W szczególności rozważ tę funkcję z Data.Syntactic.Sugar:

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

   Wydaje mi się, że fi(i być może sup) powinno być tu dwuznaczne, ale kompiluje się bez rozszerzenia. Dlaczego jest sugarSymjednoznaczny, póki sharejest? Ponieważ sharejest to zastosowanie sugarSym, sharewszystkie ograniczenia pochodzą bezpośrednio sugarSym.

Nie widzę żadnej opublikowanej wersji syntactic, której podpis dla sugarSymużywa tych dokładnych nazw typów, więc będę używał gałęzi programistycznej w commit 8cfd02 ^ , ostatniej wersji, która nadal używała tych nazw.

Dlaczego więc GHC narzeka na fipodpis w twoim typie, ale nie na ten sugarSym? Dokumentacja, z którą się łączysz, wyjaśnia, że ​​typ jest niejednoznaczny, jeśli nie wydaje się po prawej stronie ograniczenia, chyba że ograniczenie wykorzystuje zależności funkcjonalne do wnioskowania o niejednoznacznym typie z innych niejednoznacznych typów. Porównajmy więc konteksty dwóch funkcji i poszukaj zależności funkcjonalnych.

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

Tak dla sugarSym, nie-niejednoznaczne typy są sub, sigi f, i od tych, powinniśmy być w stanie śledzić zależności funkcyjnych w celu disambiguate wszystkie inne typy używanych w kontekście, a mianowicie supa fi. I faktycznie, f -> internalfunkcjonalna zależność SyntacticNużywa naszego fdo ujednoznacznienia naszego fi, a następnie f -> sig symfunkcjonalna zależność w ApplySymużywa naszego nowego ujednoznacznienia fido ujednoznacznienia sup(i sig, co już było niejednoznaczne). To wyjaśnia, dlaczego sugarSymnie wymaga AllowAmbiguousTypesrozszerzenia.

Spójrzmy teraz sugar. Pierwszą rzeczą, którą zauważam, jest to, że kompilator nie narzeka na dwuznaczny typ, ale raczej na nakładające się wystąpienia:

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

Więc jeśli dobrze to rozumiem, to nie jest tak, że GHC myśli, że twoje typy są niejednoznaczne, ale raczej, że podczas sprawdzania, czy twoje typy są niejednoznaczne, GHC napotkał inny, osobny problem. Mówi ci wtedy, że gdybyś powiedział GHC, aby nie przeprowadzał kontroli niejednoznaczności, nie napotkałby tego osobnego problemu. To wyjaśnia, dlaczego włączenie AllowAmbiguousTypes umożliwia kompilację kodu.

Pozostaje jednak problem z nakładającymi się instancjami. Dwa wystąpienia wymienione przez GHC ( SyntacticN f fii SyntacticN (a -> f) ...) pokrywają się ze sobą. O dziwo, wydaje się, że pierwszy z nich powinien nakładać się na każdy inny podejrzany przypadek. A co to [overlap ok]znaczy

Podejrzewam, że Syntactic jest kompilowany z OverlappingInstances. I patrząc na kod , rzeczywiście tak jest.

Trochę eksperymentując, wydaje się, że GHC jest w porządku z nakładającymi się instancjami, gdy jest jasne, że jedna jest bardziej ogólna niż druga:

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

Ale GHC nie jest w porządku z nakładającymi się instancjami, gdy żadna z nich nie jest wyraźnie lepsza od drugiej:

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

Podpis twojego typu używa SyntacticN (a -> (a -> b) -> b) fi, i ani SyntacticN f finie SyntacticN (a -> f) (AST sym (Full ia) -> fi)jest lepiej dopasowany niż drugi. Jeśli zmienię tę część twojego podpisu na SyntacticN a filub SyntacticN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi), GHC nie będzie już narzekać na nakładanie się.

Gdybym był tobą, spojrzałbym na definicję tych dwóch możliwych instancji i ustalił, czy jedna z tych dwóch implementacji jest tą, której chcesz.

Odkryłem, że AllowAmbiguousTypesjest to bardzo wygodne w użyciu TypeApplications. Rozważ funkcję natVal :: forall n proxy . KnownNat n => proxy n -> Integerz GHC.TypeLits .

Aby skorzystać z tej funkcji, mógłbym pisać natVal (Proxy::Proxy5). Alternatywny styl jest do stosowania TypeApplications: natVal @5 Proxy. Typ Proxyjest wywnioskować przez aplikację typu, i to jest denerwujące trzeba pisać za każdym razem, kiedy zadzwonić natVal. W ten sposób możemy włączyć AmbiguousTypesi napisać:

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

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

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

Pamiętaj jednak, że gdy przejdziesz do dwuznaczności, nie możesz wrócić !