Добросовестная неоднозначность при использовании PolyKinds и семейств типов - PullRequest
Новая
       40

Добросовестная неоднозначность при использовании PolyKinds и семейств типов

0 голосов
/ 13 января 2019

У меня есть два семейства типов, одно из которых сопоставляет один тип другому типу другого типа и полиморфной функции: 

{-# LANGUAGE PolyKinds, TypeFamilies, FlexibleContexts, ScopedTypeVariables #-} 

type family F (a :: k1) :: k2
type family G (a :: k2) :: *

f :: forall k1 k2 (a :: k1) (p :: k1 -> *) . p (a :: k1) -> G (F (a :: k1) :: k2)
f = undefined

Этот код не проверяет тип следующего сообщения об ошибке: 

• Couldn't match type ‘G k20 (F k20 k1 a)’ with ‘G k2 (F k2 k1 a)’
  Expected type: p a -> G k2 (F k2 k1 a)
    Actual type: p a -> G k20 (F k20 k1 a)
  NB: ‘G’ is a non-injective type family

но я не могу понять, откуда возникла неоднозначность и как я могу указать недостающие виды?

Когда я использую только одно семейство типов, оно работает: 

g :: forall k1 k2 (a :: k1) (p :: k1 -> *) (q :: k2 -> *). p (a :: k1) -> q (F (a :: k1) :: k2)
g = undefined

Ответы [ 2 ]

0 голосов
/ 14 января 2019

Проверка на неоднозначность изначально предназначалась для отклонения функций, которые никогда не могут быть вызваны из-за параметров типа и ограничений, которые не могут быть выведены из явных аргументов функции.

Однако с GHC 8.6.x таких функций не существует, потому что все можно сделать явным образом с помощью TypeApplications. Я рекомендую просто включить AllowAmbiguousTypes и TypeApplications. Предупреждение GHC о неоднозначных типах само по себе не очень информативно, так как отклоняет многие допустимые случаи использования приложений типов.

0 голосов
/ 14 января 2019 
f :: forall k1 k2 (a :: k1) (p :: k1 -> *). p a -> G (F a :: k2)

Позвольте мне попытаться сказать: 

x :: [String]
x = f (Just 'a')

Это идет и создает f с k1 ~ Type, a ~ Char и p ~ Maybe

f :: forall k2. Maybe Char -> G (F Char :: k2)

И что теперь? Что ж, мне еще нужно G (F Char :: k2) ~ [String], но G - это семейство неинъективных типов, поэтому невозможно сказать, каким должен быть какой-либо из его аргументов - k2 и F Char :: k2. Следовательно, определение x ошибочно; k2 является неоднозначным, и невозможно сделать для него экземпляр.

Тем не менее, вы можете довольно четко видеть, что нет использование f будет когда-либо сможет выводить k2. Причина заключается в том, что k2 появляется только в типе f под приложением неинъективного семейства типов (другая «плохая позиция» - это LHS =>). Он никогда не появляется в положении, в котором он может быть выведен. Следовательно, без расширения, такого как TypeApplications, f является бесполезным и никогда не может быть упомянуто без появления этой ошибки. GHC дает обнаруживает это и вызывает ошибку при определении, а не использования. Появляющееся сообщение об ошибке примерно такое же, что и при попытке: 

f0 :: forall k10 k20 (a :: k10) (p0 :: k10 -> *). p0 a0 -> G (F a0 :: k20)
f0 = f

Это приводит к тому же несоответствию типов, поскольку нет никаких причин, по которым k20 из f0 должно соответствовать k2 из f1.

Вы можете отключить ошибку в определении f, включив AllowAmbiguousTypes, что отключает проверку бесполезности для всех определений. Однако, в одиночку, это просто выдвигает ошибку при каждом использовании f. Для того, чтобы на самом деле позвонить f, вы должны включить TypeApplications: 

f0 :: forall k10 k20 (a :: k10) (p0 :: k10 -> *). p0 a0 -> G (F a0 :: k20)
f0 = f @k10 @k20 @a0 @p0

Альтернатива TypeApplications похожа на Data.Proxy.Proxy, но это в значительной степени устарело, за исключением контекстов более высокого ранга. (И даже тогда, это будет действительно без работы, когда у нас будет что-то вроде type-lambdas .)

...