Spec-Zone.ru › Haskell 9

6.11.2. Неоднозначные типы и проверка неоднозначности

AllowAmbiguousTypes
Начиная с:

7.8.1

Разрешает сигнатуры типов, которые, по-видимому, приведут к непригодной для использования привязке.

Каждая написанная пользователем сигнатура типа подвергается проверке неоднозначности. Проверка неоднозначности отклоняет функции, которые невозможно вызвать. Например:

f :: C a => Int

Идея в том, что не может существовать допустимых вызовов f, поскольку каждый вызов приведёт к неоднозначному ограничению. Действительно, единственная цель проверки неоднозначности — сообщать о функциях, которые невозможно вызвать. Мы могли бы без потери корректности полностью отказаться от проверки неоднозначности сигнатур типов, ценой того, что ошибки неоднозначности будут выявляться в местах вызова. Впрочем, языковое расширение AllowAmbiguousTypes отключает проверку неоднозначности.

Неоднозначность может быть неочевидной. Рассмотрим следующий пример с функциональными зависимостями:

class D a b | a -> b where ..
h :: D Int b => Int

Вполне возможно, что Int зафиксирует b в месте вызова, поэтому эту сигнатуру не следует отклонять. Кроме того, зависимости могут быть скрыты. Рассмотрим следующий пример:

class X a b where ...
class D a b | a -> b where ...
instance D a b => X [a] b where...
h :: X a b => a -> a

Здесь тип h кажется неоднозначным в b, но существует допустимый вызов:

...(h [True])...

Это приводит к ограничению (X [Bool] beta), а использование экземпляра означает, что нам требуется (D Bool beta), которое фиксирует beta благодаря функциональной зависимости D!

За всеми этими особыми случаями стоит простой руководящий принцип. Рассмотрим следующий пример:

f :: type
f = ...blah...

g :: type
g = f

Можно подумать, что определение g должно без проблем проходить проверку типов! Ведь f имеет точно такой же тип, и g=f. Но на самом деле тип f инстанцируется, а полученные ограничения разрешаются относительно ограничений, связанных с сигнатурой g. Поэтому, если тип неоднозначен, разрешить ограничения не удастся. Например, рассмотрим приведённое ранее определение f :: C a => Int:

f :: C a => Int
f = ...blah...

g :: C a => Int
g = f

В определении g мы инстанцируем тип до (C alpha) и пытаемся вывести (C alpha) из (C a), но терпим неудачу.

Итак, мы используем это как определение неоднозначности: тип ty является неоднозначным тогда и только тогда, когда ((undefined :: ty) :: ty) не прошёл бы проверку типов. Мы применяем очень похожую проверку к выведенным типам, чтобы гарантировать, что они также однозначны.

Отключение проверки неоднозначности. Даже если тип функции неоднозначен согласно «руководящему принципу», функцию всё же может быть возможно вызвать. Например:

class D a b where ...
instance D Bool b where ...

strange :: D a b => a -> a
strange = ...blah...

foo = strange True

Здесь тип strange неоднозначен, но вызов в foo допустим, поскольку он приводит к ограничению (D Bool beta), которое разрешается экземпляром (D Bool b).

Ещё один способ устранить неоднозначность в месте вызова — использовать расширение TypeApplications, чтобы указать типы. Например:

class D a b where
  h :: b
instance D Int Int where ...

main = print (h @Int @Int)

Здесь a неоднозначен в определении D, но позднее с помощью применения типов ему задаётся значение Int.

AllowAmbiguousTypes позволяет полностью отключить проверку неоднозначности.

Иногда AllowAmbiguousTypes плохо сочетается с RankNTypes. Например:

foo :: forall r. (forall i. (KnownNat i) => r) -> r
foo f = f @1

boo :: forall j. (KnownNat j) => Int
boo = ....

h :: Int
h = foo boo

Эта программа будет отклонена как неоднозначная, поскольку GHC не будет объединять переменные типа j и i.

В отличие от предыдущих примеров, в настоящее время невозможно вручную устранить неоднозначность с помощью TypeApplications.

Примечание

Историческая справка. Раньше GHC накладывал на сигнатуры типов более строгие и менее обоснованные ограничения. Для типа forall tv1..tvn (c1, ...,cn) => type GHC требовал:

  1. чтобы каждая универсально квантифицированная переменная типа tvi была «достижима» из type, и
  2. чтобы каждое ограничение ci упоминало хотя бы одну из универсально квантифицированных переменных типа tvi. Эти специальные ограничения полностью заменены новой проверкой неоднозначности.

© 2002–2007 The University Court of the University of Glasgow. All rights reserved.
Licensed under the Glasgow Haskell Compiler License.
https://downloads.haskell.org/~ghc/9.14.1/docs/users_guide/exts/ambiguous_types.html

Spec-Zone.ru

Настройки Оффлайн Что нового Помощь О нас
Spec-Zone .ru
спецификации, руководства, описания, API