Есть ли общий способ применения ограничений к типу приложений?

Question

Комментарий пользователя 2426021684 побудил меня выяснить, возможно ли придумать функцию типа F такой, что F c1 c2 fa демонстрирует, что для некоторых f а также a:

1. fa ~ f a
2. c1 f
3. c2 a

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

Answer 1

Во-первых, несколько шаблонов:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

module ConstrainApplications where

import GHC.Exts (Constraint)
import Data.Type.Equality

Теперь введите семейства для деконструкции приложений произвольных видов.

type family GetFun a where
  GetFun (f _) = f
type family GetArg a where
  GetArg (_ a) = a

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

type G (cfa :: (j -> k) -> j -> Constraint) (fa :: k)
  = ( fa ~ (GetFun fa :: j -> k) (GetArg fa :: j)
    , cfa (GetFun fa) (GetArg fa))

Мне не нравится предлагать функции ограничения без классов, поэтому вот первоклассная версия G,

class G cfa fa => GC cfa fa
instance G cfa fa => GC cfa fa

Можно выразить F с помощью G и вспомогательный класс:

class (cf f, ca a) => Q cf ca f a
instance (cf f, ca a) => Q cf ca f a

type F cf ca fa = G (Q cf ca) fa

class F cf ca fa => FC cf ca fa
instance F cf ca fa => FC cf ca fa

Вот несколько примеров использования F:

t1 :: FC ((~) Maybe) Eq a => a -> a -> Bool
t1 = (==)

-- In this case, we deconstruct the type *twice*:
-- we separate `a` into `e y`, and then separate
-- `e` into `Either x`.
t2 :: FC (FC ((~) Either) Show) Show a => a -> String
t2 x = case x of Left p -> show p
                 Right p -> show p

t3 :: FC Applicative Eq a => a -> a -> GetFun a Bool
t3 x y = (==) <$> x <*> y