Почему синоним связанного типа не подразумевает ограничение

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

Например. почему не компилируется следующее:

{-# LANGUAGE TypeApplications, ScopedTypeVariables, TypeFamilies, AllowAmbiguousTypes #-}

class MyClass a where
  type AssociatedType a 
  bar :: Int

foo :: forall a. AssociatedType a -> Int
foo _ = bar @a

ghc 8.6.5 выдает следующую ошибку:

error:
    * No instance for (MyClass a) arising from a use of `bar'
      Possible fix:
        add (MyClass a) to the context of
          the type signature for:
            foo :: forall a. AssociatedType a -> Int
    * In the expression: bar @a
      In an equation for `foo': foo _ = bar @a
  |
8 | foo _ = bar @a
  |         ^^^^^^

Документация GHC, похоже, не упоминает этот аспект.


haskell type-families
person grepcake    schedule 29.08.2020    source источник

Ответы (2)


arrow_upward
4
arrow_downward

Если бы это подразумевало ограничение, то любой, кто каким-либо образом использует значения связанного значения, должен был бы иметь ограничение в области видимости. Например,

sort :: Ord a => [a] -> [a]

очевидно, ничего не знает о MyClass, но его можно использовать как sort :: [AssociatedType a] -> [AssociatedType a] при условии, что у вас есть Ord (AssociatedType a) в области вызова.

Чтобы получить поведение, похожее на то, которое вы ищете, вам нужно обернутое ограничение, а не ассоциированный тип. Этого нельзя сделать с помощью -XTypeFamilies, но можно сделать с помощью -XGADTs:

{-# LANGUAGE GADTs #-}

class MyClass a where
  bar :: Int

data MyClassWitness a where
  MyClassWitness :: MyClass a => MyClassWitness a

foo :: ∀ a. MyClassWitness a -> Int
foo MyClassWitness = bar @a

Вместо самостоятельно свернутой оболочки вы также можете использовать обертку из библиотеки constraints:

import Data.Constraint

foo :: ∀ a . Dict (MyClass a) -> Int
foo Dict = bar @a

В обоих случаях важно, чтобы вы фактически сопоставляли шаблон в конструкторе GADT, так как только это фактически приводит ограничение в область действия. Это не сработает:

foo :: ∀ a . Dict (MyClass a) -> Int
foo _ = bar @a
person leftaroundabout    schedule 29.08.2020

arrow_upward
2
arrow_downward

Потому что простое использование типа не требует ограничения типа. Например, это компилируется:

foo :: forall a. AssociatedType a -> Int
foo _ = 42

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

В вашем коде ограничение необходимо, потому что вы используете bar, а не потому, что вы используете тип.

person chi    schedule 29.08.2020