Количественное равенство типов связанных семейств типов

У меня есть связанное семейство типов Bar в классе типов Foo. Foo' требует Bar f ~ Bar (f a) для всех a, но в другой функции test получаю ошибку Couldn't match type 'Bar f' with 'Bar (f a)', хотя она зависит от Foo' f. Код:

{-# LANGUAGE TypeFamilies, PolyKinds, QuantifiedConstraints #-}

import Data.Proxy

class Foo f where
  type Bar f

class (Foo f, forall a. Foo (f a), forall a. Bar f ~ Bar (f a)) => Foo' f where

test :: Foo' f => Proxy (f a) -> Bar (f a) -> Bar f
test _ = id

Почему GHC не может определить это равенство типов и есть ли способ помочь программе проверки типов, не утверждая конкретное равенство в test?


haskell type-families quantified-constraints
person Greg C    schedule 15.07.2020    source источник
comment
Я думаю, что это неинъективность семейства типов: в test GHC хочет Bar (f a) ~ Bar f, где a — аргумент для test. Он имеет forall b. Bar (f b) ~ Bar f. Ему нужно создать экземпляр этого равенства, чтобы получить конкретное, поэтому я думаю, что он пытается найти экземпляр, создавая переменную объединения _b, создавая экземпляр b := _b, а затем объединяя полученные Bar (f _b) с Bar (f a) для решения для _b. Однако он не может уменьшить Bar (f _b) ~ Bar (f a) до f _b ~ f a, а затем _b ~ a, потому что первый шаг требует, чтобы Bar было инъективным. Не знаю, как решить это автоматически.   -  person HTNW    schedule 15.07.2020
comment
Это странно. Я даже не могу загрузить определение класса для Foo', не говоря уже о самом test (он говорит мне о недопустимом приложении семейства синонимов типа «Bar f», например: Bar f ~ Bar (f a)). Какую версию GHC вы используете? Я пробовал 8.8 и 8.10, и они оба дают ту же ошибку.   -  person Daniel Wagner    schedule 15.07.2020
comment
@DanielWagner Я использовал версию 8.6. Это странно. Я получил такое же поведение в более новых версиях ghc, добавив оболочку newtype Wrap f = Wrap (Bar f) и используя ее в определении класса. Если я также использую его в test, ошибка изменится на cannot construct the infinite type: f ~ f a.   -  person Greg C    schedule 15.07.2020

Ответы (1)


arrow_upward
2
arrow_downward

Семейства типов и количественные ограничения не смешиваются. Тем более с равенствами типов . Но есть способ разделить их для достижения более или менее одинакового результата.

Количественное ограничение фактически ограничено способами его использования. Недостаточно знать, что ограничение действует для всех типов, вам также нужен способ узнать, на каких типах вам нужно его специализировать. GHC достигает этого, представляя количественные ограничения в виде своего рода локального экземпляра, на который распространяется общие правила разрешения экземпляров. Я не уверен, что количественные равенства типов вообще что-то значат. Таким образом, недостаточно, чтобы квантифицированное ограничение можно быть создано для того, чтобы делать то, что мы хотим; эта инстанцирация должна происходить в обычном порядке разрешения экземпляра, и это накладывает ограничения на разрешенные формы количественных ограничений.

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

class    (Bar f ~ Bar (f a)) => EBar f a
instance (Bar f ~ Bar (f a)) => EBar f a

Таким образом, мы можем переписать количественное ограничение как forall x. EBar f x, семейств типов не видно:

class (Foo f, forall a. Foo (f a), forall x. EBar f x) => Foo' f where

Чтобы использовать этот класс, нам нужна явная функция для специализации количественного ограничения (проблема в том, что если мы используем равенство Bar f ~ Bar (f a) напрямую, средство проверки типов не сможет связать его с количественным ограничением forall x. EBar f x, которое на него не похоже):

-- Morally a function on constraints `(forall x. EBar f x) => EBar f a`
-- in continuation-passing style: (x => y) is isomorphic to forall r. (y => r) -> (x => r)
ebar :: forall f a r. (EBar f a => Proxy (f a) -> r) -> (forall x. EBar f x) => Proxy (f a) -> r
ebar f = f

test :: Foo' f => Proxy (f a) -> Bar (f a) -> Bar f
test = ebar (\_ -> id)

{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FlexibleInstances, TypeFamilies, PolyKinds, QuantifiedConstraints #-}

import Data.Proxy

class Foo f where
  type Bar f

class (Foo f, forall a. Foo (f a), forall a. EBar f a) => Foo' f where

class    (Bar f ~ Bar (f a)) => EBar f a
instance (Bar f ~ Bar (f a)) => EBar f a

ebar :: forall f a r. (EBar f a => Proxy (f a) -> r) -> (forall x. EBar f x) => Proxy (f a) -> r
ebar f = f

test :: Foo' f => Proxy (f a) -> Bar (f a) -> Bar f
test = ebar (\_ -> id)
person Li-yao Xia    schedule 15.07.2020