是否有一种将约束应用到类型应用程序的一般方法

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

可以使用G和辅助类表达F：

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