类型族可以评估为限定类型，例如“C a => T”吗？

Question

有没有办法编写一个有时评估为受约束类型的类型系列，例如C a => T？

\n

当我编写以下类型系列时出现了这个问题：

\n

type family Function (cs :: [Constraint]) (as :: [Type]) (r :: Type) :: Type where\n  Function (c ': cs) as        r = c => Function cs  as r\n  Function '[]       (a ': as) r = a -> Function '[] as r\n  Function '[]       '[]       r = r\n

\n

目标是Function '[Integral a, Show b] '[String, b, a] (IO ())评估为Integral a => Show b => String -> b -> a -> IO (). 但是，相反，我收到错误

\n

    \xe2\x80\xa2 Illegal qualified type: c => Function cs as r\n    \xe2\x80\xa2 In the equations for closed type family \xe2\x80\x98Function\xe2\x80\x99\n      In the type family declaration for \xe2\x80\x98Function\xe2\x80\x99\n

\n

我尝试使用Show c => Function cs as r看看问题是否出在 bare 上c，但这似乎没有什么区别。我已经尝试过加上GHC2021扩展名ConstraintKinds、DataKinds、RankNTypes、TypeFamilies和UndecidableInstances，但我也很乐意添加任何其他语言扩展，如果它们会有所作为的话。

\n

有什么办法可以做到这一点吗？如果不是，为什么不可能呢？

\n

Answer 1

这样就可以编译了。诀窍是将约束部分和类型部分分开。

{-# LANGUAGE TypeFamilies, DataKinds #-}

import Data.Kind

-- Handle the list of constraints.
type family Context (cs :: [Constraint]) :: Constraint where
  Context (c ': cs) = (c, Context cs)
  Context '[]       = ()    

-- Handle the list of argument types.
type family Fun (as :: [Type]) (r :: Type) :: Type where
  Fun (a ': as) r = a -> Fun as r
  Fun '[]       r = r

-- Combine both.
type Function (cs :: [Constraint]) (as :: [Type]) (r :: Type)
  = (Context cs) => Fun as r