В Haskell, как я могу взять m-арный предикат и n-арный предикат и построить (m+n)-арный предикат?

Question

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

conjunction (>2) even

вернет предикат, который оценивается как истинное для четных чисел больше двух и

conjunction (>=) (<=)

вернется =

Хорошо, что эта часть работала, но возник вопрос, а что, если я хочу определить соединение двух предикатов как предикат, который принимает один вход для каждого входа каждого объединенного предиката? Например:

:t conjunction (>) not

вернул бы Ord a => a -> a -> Bool -> Bool. Можно ли это сделать? Если так, то как?

Answer 1

Нам понадобится TypeFamilies для этого решения.

{-# LANGUAGE TypeFamilies #-}

Идея состоит в том, чтобы определить класс Pred для n-арных предикатов:

class Pred a where
  type Arg a k :: *
  split :: a -> (Bool -> r) -> Arg a r

Проблема заключается в перестановке аргументов в предикаты, поэтому класс и стремится к этому. Связанный тип Arg должен дать доступ к аргументам n-арного предиката путем замены финального Bool с kтак что если у нас есть тип

X = arg1 -> arg2 -> ... -> argn -> Bool

затем

Arg X k = arg1 -> arg2 -> ... -> argn -> k

Это позволит нам построить правильный тип результата conjunction где все аргументы двух предикатов должны быть собраны.

Функция split принимает предикат типа a и продолжение типа Bool -> r и будет производить что-то типа Arg a r, Идея split в том, что если мы знаем, что делать с Bool мы получаем из предиката в конце концов, тогда мы можем делать другие вещи (r) между.

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

instance Pred Bool where
  type Arg Bool k = k
  split b k = k b

Bool не имеет аргументов, поэтому Arg Bool k просто возвращается k, Также для splitу нас есть Bool уже, поэтому мы можем немедленно применить продолжение.

instance Pred r => Pred (a -> r) where
  type Arg (a -> r) k = a -> Arg r k
  split f k x = split (f x) k

Если у нас есть предикат типа a -> r, затем Arg (a -> r) k должен начинаться с a ->и продолжаем звонить Arg рекурсивно на r, За splitТеперь мы можем принять три аргумента, x быть типом a, Мы можем накормить x в f а затем позвоните split на результат.

После того как мы определили Pred класс, это легко определить conjunction:

conjunction :: (Pred a, Pred b) => a -> b -> Arg a (Arg b Bool)
conjunction x y = split x (\ xb -> split y (\ yb -> xb && yb))

Функция принимает два предиката и возвращает что-то типа Arg a (Arg b Bool), Давайте посмотрим на пример:

> :t conjunction (>) not
conjunction (>) not
  :: Ord a => Arg (a -> a -> Bool) (Arg (Bool -> Bool) Bool)

GHCi не расширяет этот тип, но мы можем. Тип эквивалентен

Ord a => a -> a -> Bool -> Bool

что именно то, что мы хотим. Мы также можем протестировать несколько примеров:

> conjunction (>) not 4 2 False
True
> conjunction (>) not 4 2 True
False
> conjunction (>) not 2 2 False
False

Обратите внимание, что с помощью Pred класс, это тривиально, чтобы написать другие функции (например, disjunction), тоже.

Answer 2

{-# LANGUAGE TypeFamilies #-}

class RightConjunct b where
  rconj :: Bool -> b -> b

instance RightConjunct Bool where
  rconj = (&&)

instance RightConjunct b => RightConjunct (c -> b) where
  rconj b f = \x -> b `rconj` f x

class LeftConjunct a where
  type Ret a b
  lconj :: RightConjunct b => a -> b -> Ret a b

instance LeftConjunct Bool where
  type Ret Bool b = b
  lconj = rconj

instance LeftConjunct a => LeftConjunct (c -> a) where
  type Ret (c -> a) b = c -> Ret a b
  lconj f y = \x -> f x `lconj` y

conjunction :: (LeftConjunct a, RightConjunct b) => a -> b -> Ret a b
conjunction = lconj

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

Кроме того, вы можете объединить два класса в один, конечно, но я чувствую, что два класса проясняют идею.