haskell - 从所有参数构建异构列表的构造函数

Question

给定 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) $ 构建

Answer 1

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

与 Li-yao Xia 的基本思想相同，但使用类型族而不是辅助 MPTC 参数。优点:更清楚发生了什么，并且不需要为 build 的参数提供本地签名。

*Main> build @('[Int, Bool]) 3 True
H[3,True]