Пути вокруг непредсказуемого полиморфизма - PullRequest
Новая
       24

Пути вокруг непредсказуемого полиморфизма

0 голосов
/ 29 ноября 2018

Я новичок в некоторых из более сложных конструкций типов в Haskell и бездельничал.В настоящее время я застрял, пытаясь получить функцию, которая, по моему мнению, должна работать для проверки типов.

Возьмем следующий код в качестве примера: 

{-# LANGUAGE RankNTypes   #-}
{-# LANGUAGE TypeFamilies #-}

class X a where
  data Y a
  z :: Y a -> Int

data D1 = D1
instance X D1 where
  data Y D1 = YD1
  z _ = 1

data D2 = D2
instance X D2 where
  data Y D2 = YD2
  z _ = 2

sumZ :: X a => [Y a] -> Int
sumZ = foldl' sumFn 0
  where sumFn = flip ((+) . z)

Я хочу a = sumZ [YD1, YD2] для проверки типов,Это (очевидно) не работает, так как переменная типа a фиксируется с первым YD1.

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

sumZ' :: [(forall a. X a => Y a)] -> Int
sumZ' = foldl' sumFn 0
  where sumFn = flip ((+) . z)

Но, когда я пытаюсь скомпилировать его, я сталкиваюсь с "непредсказуемым полиморфизмом": 

     • Illegal polymorphic type: forall a. X a => Y a
       GHC doesn't yet support impredicative polymorphism
     • In the type signature: sumZ' :: [(forall a. X a => Y a)] -> Int
    |
 48 | sumZ' :: [(forall a. X a => Y a)] -> Int
    |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

После небольшого прочтения я вижу, что традиционное решение заключается в переносезначение в newtype для обхода неимоверного полиморфизма. 

newtype Wrap = Wrap { unWrap :: forall a. X a => Y a }

sumZ'' :: [Wrap] -> Int
sumZ'' = foldl' sumFn 0
  where
    sumFn acc (Wrap v) = acc + (z v)

К сожалению, это тоже не работает.Компиляция завершается с этим сообщением: 

     • Ambiguous type variable ‘a0’ arising from a use of ‘z’
       prevents the constraint ‘(X a0)’ from being solved.
       Probable fix: use a type annotation to specify what ‘a0’ should be.
       These potential instances exist:
         instance X D1
           -- Defined at ...
         instance X D2
           -- Defined at ...
     • In the second argument of ‘(+)’, namely ‘(z v)’
       In the expression: acc + (z v)
       In an equation for ‘sumFn’: sumFn acc (Wrap v) = acc + (z v)
    |
 64 |     sumFn acc (Wrap v) = acc + (z v)
    |                                 ^^^

Наконец, мой вопрос (-ы):

  1. Почему в этом случае не работает стандартная техника «оборачивания»?При проверке типа v я вижу, что он имеет тип forall a. X a => Y a, мне кажется, что он должен работать.
  2. Как я могу заставить a = sumZ [YD1, YD2] работать?Я что-то не так делаю?

1 Ответ

0 голосов
/ 29 ноября 2018

Тот факт, что v :: forall a. X a => Y a - это именно то, почему применение z не работает.

То, что там forall означает, что v может быть любого типа, вы выбираете какой.Чтобы проиллюстрировать это, сравните это: 

empty :: forall a. [a]
empty = []

Там значение empty может быть любого типа, потребитель выбирает, какой тип.Вот что означает forall.Я надеюсь, что это очевидно.

И так же с вашим значением v: оно может быть любого типа, вы выбираете какой.Но в вашем коде вы не выбираете тип: вы применяете z, который сам может работать с любым типом, и поэтому тип v остается невыбранным.Это именно то, что говорит вам компилятор, когда жалуется на «переменную неоднозначного типа a0».

Чтобы это работало, вы должны поместить forall с другой стороны Wrap: 

data Wrap = forall a. X a => Wrap (Y a)

(для этого необходимо включить расширение GADTs)

Таким образом, тот, кто создает Wrap, должен выбратьопределенный тип a.А с другой стороны, когда вы делаете сопоставление с образцом, вы получаете тип a, который был выбран тем, кто построил значение.

...