haskell 类型族是否可以计算为限定类型，例如`C a => T`？

kcwpcxri 于 9个月前发布在其他

关注(0)|答案(1)|浏览(72)

有没有什么方法可以写出一个类型族，它有时会计算为一个受约束的类型，比如C a => T？
这个问题是在我写下面的类型族时出现的：

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

目标是Function '[Integral a, Show b] '[String, b, a] (IO ())将评估为Integral a => Show b => String -> b -> a -> IO ()。然而，相反，我得到的错误

• Illegal qualified type: c => Function cs as r
    • In the equations for closed type family ‘Function’
      In the type family declaration for ‘Function’

我尝试使用Show c => Function cs as r来查看问题是否与裸c有关，但这似乎没有什么区别。我已经用GHC2021加上扩展ConstraintKinds、DataKinds、RankNTypes、TypeFamilies和UndecidableInstances尝试过了，但是我也很乐意添加任何其他语言扩展，如果它们会有所不同的话。
有什么办法可以做到这一点吗？如果不是，为什么不可能？

haskell

来源：https://stackoverflow.com/questions/76933811/can-type-families-evaluate-to-qualified-types-such-as-c-a-t

1条答案

按热度按时间

kyvafyod1#

这是编译。诀窍在于拆分约束部分和类型部分。

{-# 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

赞(0）回复(0）举报 9个月前

我来回答

haskell 类型族是否可以计算为限定类型，例如`C a => T`？

1条答案

相关问题

热门标签

最新问答