Объединение ограничений с fundeps

У меня есть функция foo со множеством ограничений. Конечно, эти ограничения должны появляться в сигнатурах функций, использующих foo, поэтому я пытаюсь обернуть ограничения foo синонимом типа FooCtx a b ... :: Constraint. Например,

foo :: (A a, B b, C c, ...) => a -> b -> c

bar :: (A a, B b, C c, ...) ...
bar = ... foo ...

станет

type FooCtx a b c ... = (A a, B b, C c, ...)
foo :: (FooCtx a b c) => a -> b -> c
bar :: (FooCtx a b c) => ...

Это прекрасно работает, если все типы выставлены. Однако я использую функциональные зависимости для создания некоторых типов в списке ограничений, и эти типы не отображаются в сигнатуре foo. Например:

class Bar a b | a -> b

foo (Bar a b, ...) => a -> a

GHC не примет type FooCtx a = (Bar a b), потому что b не привязан к LHS. Я также не могу использовать type FooCtx a b = (Bar a b), потому что b не входит в область действия подписи foo. Подпись foo будет foo :: (FooCtx a ?) => a -> a.

Одно из неудовлетворительных решений — поместить одно из ограничений в подпись foo с FooCtx, чтобы ввести тип fundep в область видимости:

class Bar a b | a -> b

type FooCtx a b = ...

foo (Bar a b, FooCtx a b) => a -> a

но это противоречит цели группировки ограничений:

Пока я не столкнулся с этим случаем, я предполагал, что синонимы ограничений можно слепо заменять произвольными списками ограничений. Единственный известный мне способ инкапсулировать такие ограничения — с помощью класса, но он страдает от той же проблемы: class (A a, B b, C c, ...) => FooCtx a b c не может иметь никаких скрытых типов в LHS. Есть ли какой-то другой способ, которым я мог бы полностью собрать все эти ограничения?


functional-dependencies type-constraints haskell ghc
person crockeea    schedule 03.03.2015    source источник
comment
Что не так с type FooCtx a b = ... - это всего на 2 символа длиннее, чем type FooCtx a = ....   -  person user2407038    schedule 03.03.2015
comment
Как я упоминал выше, GHC принимает вашу подпись, но для меня это бесполезно в LHS foo, потому что b не входит в область действия подписи foo.   -  person crockeea    schedule 03.03.2015
comment
Есть ли причина, по которой вы не можете использовать TypeFamilies вместо FunctionalDependencies?   -  person Cirdec    schedule 03.03.2015
comment
@Cirdec Теперь, когда вы упомянули об этом, есть ли причина? Разве они не изоморфны? Это позволило бы мне ввести эти новые типы в область видимости...   -  person crockeea    schedule 03.03.2015

Ответы (2)


arrow_upward
5
arrow_downward

Вы неправильно понимаете, как связаны переменные типа. Они не связаны типом тау (a -> a в вашем примере), а неявным связующим, основанным на полном типе фи ((Bar a b) => a -> a). Эту привязку можно сделать явной с помощью языкового расширения ExplicitForAll GHC.

В вашем примере, когда вы пишете что-то вроде

foo :: (Bar a b) => a -> a

то полный сигма-тип, с прописанной явной привязкой тиваров, следующий (поскольку в неявном случае сюда привязываются все тивары из фи-типа)

foo :: forall a b. (Bar a b) => a -> a

Это означает, что нет проблем с использованием псевдонима ограничения таким же образом: если у вас есть, например.

type FooCtx a b = (Bar a b, Num a, Eq a)

тогда следующая сигнатура допустимого типа:

foo' :: forall a b. (FooCtx a b) => a -> a

и, таким образом, следующее сокращение также допустимо:

foo' :: (FooCtx a b) => a -> a
person Cactus    schedule 03.03.2015
comment
Как интересно! Спасибо. - person crockeea; 03.03.2015

arrow_upward
1
arrow_downward

Эту проблему можно решить с помощью TypeFamilies и FlexibleContexts.

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}

У нас есть три класса: A, B и C и ваша исходная функция foo.

class A a
class B a
class C a

foo :: (A a, B b, C c) => a -> b -> c
foo = undefined

Класс Bar использует семейство типов, чтобы выяснить, что B сочетается с a. Я добавил к нему дополнительную функцию только для того, чтобы написать пример foo'.

class Bar a where
    type BofA a :: *
    aToB :: a -> BofA a

foo' — это функция, которая не имеет ни входных, ни выходных данных, равных B, но все же использует в своей реализации foo. Требуется, чтобы тип BofA, связанный с a, удовлетворял ограничению B. Эта подпись требует гибких контекстов.

foo' :: (A a, Bar a, B (BofA a), C c) => a -> a -> c
foo' x y = foo x (aToB y)
person Cirdec    schedule 03.03.2015