приложение типа и ограничения типа

Question

(я не совсем знаком с внутренней работой ограничения Хаскеля решателем так что это, вероятно, может быть новичком вопросом.)

При попытке использовать приложение типа на GHC 8.0.1, а показано в следующем примере кода

{-# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, ScopedTypeVariables, TypeApplications #-} 
module Test where 

import Data.Constraint 

test0 :: forall (b :: *) . (forall a . a -> Bool) -> b -> Bool 
test0 g = g @b 

test1 :: forall (c :: * -> Constraint) (b :: *) . (c b) => (forall a . c a => a -> Bool) -> b -> Bool 
test1 g = g @b 

это дает мне следующие ошибки

• Could not deduce: c0 b 
    from the context: c b 
    bound by the type signature for: 
       test1 :: c b => (forall a. c a => a -> Bool) -> b -> Bool 
    at Test.hs:9:10-101 
• In the ambiguity check for ‘test1’ 
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes 
    In the type signature: 
    test1 :: forall (c :: * -> Constraint) (b :: *). 
      (c b) => (forall a. c a => a -> Bool) -> b -> Bool 

и

• Could not deduce: c a 
    from the context: c b 
    bound by the type signature for: 
       test1 :: c b => (forall a. c a => a -> Bool) -> b -> Bool 
    at Test.hs:9:10-101 
    or from: c0 a 
    bound by the type signature for: 
       test1 :: c0 a => a -> Bool 
    at Test.hs:9:10-101 
• In the ambiguity check for ‘test1’ 
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes 
    In the type signature: 
    test1 :: forall (c :: * -> Constraint) (b :: *). 
      (c b) => (forall a. c a => a -> Bool) -> b -> Bool 

test0 Работы там, где нет ограничений, но test1 нет.

Answer 1

Если вы используете TypeApplications, вы должны включить AllowAmbiguousTypes. Если вы это сделаете, ошибка исчезнет.

ambiguity check отклоняет определения t, так что никакая t :: type аннотация может быть проверена на практике. Например:

test1 :: Show a => Int 
test1 = 0 

Если попытаться использовать test1 в другом месте в нашей программе, мы находим, что нет никакого способа, чтобы разрешить Show a ограничения путем :: аннотацию. Поэтому проверка двусмысленности отвергает само определение.

Конечно, при использовании типов приложений проверка двусмысленности становится бессмысленной (возможно, она должна быть отключена по умолчанию в этом случае), поскольку test1 @type прекрасно и полностью определяется всякий раз, когда имеется экземпляр Show type.

Обратите внимание, что это не то же самое, что и известная show . read двусмысленность. Это по-прежнему выдает ошибку, с AllowAmbiguousTypes тоже:

test2 = show . read 
-- "ambiguous type variable prevents the constraint from being solved" 

Оперативно, значения с c => t типов просто функции от c -typed экземпляров в t. Просто определение test1 прекрасно, так как мы всегда можем определить постоянную функцию. Однако в show . read нам нужно предоставить экземпляры в качестве аргумента (иначе код не будет запущен), и нет возможности их разрешить. Использование test1 без применения типа будет аналогичным образом неоднозначным.