给定cons :: x -> f xs -> f (x ': xs)和nil :: f '[]
如何构建build :: forall xs . ?使得对于给定的xs ~ '[x1, x2 ... xn]、build :: x1 -> x2 -> ... -> xn -> f '[x1, x2, ..., xn]
我的想法是，我可以通过以下方式应用这样的函数($ x) . ($ y) . ($ z) $ build
{-# LANGUAGE TypeFamilies, GADTs, RankNTypes
, FlexibleInstances, MultiParamTypeClasses
, FlexibleContexts, UndecidableInstances
, DataKinds, TypeInType, TypeOperators
, AllowAmbiguousTypes, TypeApplications
, ScopedTypeVariables, UnicodeSyntax
, StandaloneDeriving #-}
import Data.Kind
import Data.HList
class Buildable (l :: [Type]) (m :: [Type]) where
type Buildup l m :: Type
build' :: (HList m -> HList l) -> Buildup l m
instance Buildable l '[] where
type Buildup l '[] = HList l
build' prep = prep HNil
instance Buildable l m => Buildable l (x ': m) where
type Buildup l (x ': m) = x -> Buildup l m
build' prep x = build' (prep . HCons x)
type Builder l = (Buildable l l) => Buildup l l
build :: ∀ l . Builder l
build = build' @l @l id
与李耀霞的基本思想相同，但用类型家庭代替了辅助MPTC的论点。优点：更清楚发生了什么，并且没有必要为build的论点提供本地签名。
*Main> build @('[Int, Bool]) 3 True
H[3,True]
以下是有效的代码。可能有太多的东西需要解释；请随时在评论中询问有关此实现的问题，我可能会扩展这个答案来回答这些问题。
为了搜索关于SO和其他地方的更多相关问题，这属于通常讨论的主题"；Haskell中的变差函数"；，即具有可变数量的自变量的函数。
需要了解的一个核心概念是类型类实例求解器是如何工作的；GHC用户指南给出了一个总结。
{-# LANGUAGE
AllowAmbiguousTypes,
DataKinds,
FlexibleInstances,
MultiParamTypeClasses,
ScopedTypeVariables,
TypeOperators,
TypeFamilies,
UndecidableInstances,
TypeApplications #-}
-- Tagless-style heterogeneous lists
class HList f where
nil :: f '[]
cons :: x -> f xs -> f (x ': xs)
class HList f => Build_ f xs r b where
build_ :: (f xs -> r) -> b
instance (HList f, xs ~ '[], f ~ g, r ~ g ys) => Build_ f xs r (g ys) where
build_ c = c nil
instance (Build_ f xs r b, xxs ~ (x ': xs)) => Build_ f xxs r (x -> b) where
build_ c x = build_ (xs -> c (cons x xs))
class Build_ f xs (f xs) b => Build f xs b
instance Build_ f xs (f xs) b => Build f xs b
build :: forall f xs b. Build f xs b => b
build = build_ @f @xs @(f xs) @b id
example :: HList f => f '[Int, Bool]
example = build (3 :: Int) True
你能解释一下为什么这里需要~等式，而不能通过直接用一种类型替换另一种类型来简化吗？
这有时被称为"；约束技巧"；。
其主要思想是，为了决定要拾取哪个实例，约束解算器只查看实例头=>的右侧。
在上面的第二个实例的head中，如果您放置(x ': xs)而不是变量xxs，则head变为Build_ f (x ': xs) r (x -> b)，那么只有当您已经知道列表以cons(':)开头时，才会拾取该实例。但是，该列表最初是未知的(除非用户显式地用列表注释build(，因此不会拾取该实例。通过使实例成为Build_ f xxs r (x -> b)，这允许仅基于build_的自变量(基于它至少还有一个(来选择实例。拾取实例后，将生成=>左侧的约束，从而允许实例的主体进行类型检查，并允许实例解算器取得更多进展。
其他实例上的相等约束也是出于类似的原因。它们是您需要对实例的主体进行类型检查的约束，但在尝试求解Build_约束时，约束求解器并不是先验的。