haskell - 将类型级别列表解构为没有标记的嵌套元组 '[]

Question

我试图将类型列表(例如 '[Int, Int] )解构为一种类型和一种通过类型运算符创建该类型的方法(与嵌套元组同构，但写起来更好)。例如:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies, FlexibleInstances #-}

import Data.Kind (Type)

data a :<> b = a :<> b
infixr 8 :<>

class Construct a where
  type Result a :: Type

instance forall a as. (Show a, Construct as) => Construct (a:as) where
  type Result (a:as) = a :<> (Result as)

instance Construct '[] where
  type Result '[] = ()

当使用这个时，我得到例如

λ  :kind! Result '[Int, Int, Int]
Result '[Int, Int, Int] :: *
= Int :<> (Int :<> (Int :<> ()))

注意 :<> ()最后我不想要的。起初，我尝试更具体地匹配列表元素的长度，例如'[a，b]:

instance forall a b. (Show a, Show b) => Construct ('[a,b]) where
  type Result '[a,b] = a :<> b

但这当然行不通:

Conflicting family instance declarations:
  Result (a : as) = a :<> Result as -- Defined at test.hs:14:8
  Result '[a, b] = a :<> b -- Defined at test.hs:22:8

我总是可以构建最多 N 个特定实例:

instance forall a. (Show a) => Construct '[a] where
  type Result '[a] = a

instance forall a b. (Show a, Show b) => Construct '[a,b] where
  type Result '[a, b] = a :<> b

instance forall a b c. (Show a, Show b, Show c) => Construct '[a,b,c] where
  type Result '[a, b, c] = a :<> b :<> c

-- etc. up to N

但这似乎非常令人不满意。

有没有办法解压到Int :<> (Int :<> Int)而不是Int :<> (Int :<> (Int :<> ())))使用递归定义？

Answer 1

使用封闭类型族。它们从上到下匹配，因此不存在冲突。

type family Construct (xs :: [Type]) :: Type where
  Construct '[x]      = x
  Construct (x ': xs) = x :<> Construct xs

现在Construct [Int, Int, Int]减少为Int :<> (Int :<> Int) .

但是，如果我对您打算如何使用它的看法大致正确，那么使用异构列表会更好，因为它们更容易使用并且具有更好的类型推断。

{-# language
  UndecidableInstances, RankNTypes, TypeOperators, TypeFamilies,
  TypeApplications, ScopedTypeVariables, GADTs, DataKinds, PolyKinds,
  ConstraintKinds, AllowAmbiguousTypes #-}

import Data.List
import Data.Kind

data HList (ts :: [Type]) :: Type where
  Nil  :: HList '[]
  (:>) :: t -> HList ts -> HList (t ': ts)
infixr 5 :>

-- example
foo :: HList [Int, String, Bool]  
foo = 0 :> "foo" :> True :> Nil

作为 HList 上的有用操作的示例，如果我们知道每个元素类型满足类约束，我们可以映射列表，要么将其收集到同构列表中，要么保留元素类型:

type family AllC c (xs :: [a]) :: Constraint where
  AllC c '[]       = ()
  AllC c (x ': xs) = (c x, AllC c xs)

hmap :: forall c ts. AllC c ts => (forall x. c x => x -> x) -> HList ts -> HList ts
hmap f Nil       = Nil
hmap f (x :> xs) = f x :> hmap @c f xs

hmap' :: forall c ts r. AllC c ts => (forall x. c x => x -> r) -> HList ts -> [r]
hmap' f Nil       = []
hmap' f (x :> xs) = f x : hmap' @c f xs

我们可以使用TypeApplications设置c限制。我们可以实现Show HList 的实例只需使用 hmap' :

instance AllC Show ts => Show (HList ts) where
  show xs = "[" ++ intercalate ", " (hmap' @Show show xs) ++ "]"

现在我们在 ghci 中有:

> foo
[0, "foo", True]

之所以有效，是因为 foo 的所有元素类型有Show实例。