Неинъективная семья закрытого типа - PullRequest
Новая
       43

Неинъективная семья закрытого типа

0 голосов
/ 28 сентября 2018

У меня есть этот заведомо надуманный кусок кода 

{-# LANGUAGE DataKinds, TypeFamilies #-}

data Foo = Foo

type family Id (n :: Foo) a where
    Id 'Foo a = a

data Bar (n :: Foo) = Bar

class Dispatch (n :: Foo) where
    consume :: Id n a -> Bar n -> a

consume' :: Dispatch n => Id n [Bool] -> Bar n -> [Bool]
consume' = consume

consume'' :: Dispatch n => Id n [Bool] -> Bar n -> Bool
consume'' g x = and (consume' g x)

Это компилируется и работает отлично.Однако, если я заменю окончательное определение consume'' на 

consume'' :: Dispatch n => Id n [Bool] -> Bar n -> Bool
consume'' g x = and (consume g x)

(обратите внимание на consume вместо consume'), то я получу ошибку 

noinject.hs:17:30: error:
    • Couldn't match expected type ‘Id n (t0 Bool)’
                  with actual type ‘Id n [Bool]’
      NB: ‘Id’ is a non-injective type family
      The type variable ‘t0’ is ambiguous
    • In the first argument of ‘consume’, namely ‘g’
      In the first argument of ‘and’, namely ‘(consume g x)’
      In the expression: and (consume g x)
    • Relevant bindings include
        x :: Bar n (bound at noinject.hs:17:13)
        g :: Id n [Bool] (bound at noinject.hs:17:11)
        consume'' :: Id n [Bool] -> Bar n -> Bool
          (bound at noinject.hs:17:1)
   |
17 | consume'' g x = and (consume g x)
   |                              ^
Failed, no modules loaded.

Если мыПредположим, что Id неинъективен, тогда ошибка возникает потому, что consume может реально специализироваться на consume :: Id n (t0 Bool) -> Bar n -> t0 Bool, для некоторого складного t0, который не [].Я так много понимаю.Мой вопрос: почему Id не на самом деле инъективен.Он принимает два аргумента: для первого аргумента есть только одно допустимое значение, и Id довольно явно инъективен во втором аргументе, так почему же GHC считает, что это неинъективное семейство?

1 Ответ

0 голосов
/ 28 сентября 2018

Инъективные семейства типов являются отдельным расширением поверх семейств типов, и вам необходим специальный синтаксис для объявления семейства типов как одного.Инъективность не выводится.

...