在 Haskell 中约束类型级列表的元素答案

【问题标题】：Constrain elements of a type-level list in Haskell在 Haskell 中约束类型级列表的元素
【发布时间】：2015-09-05 22:46:44
【问题描述】：

我正在尝试编写一个类型族，我可以使用它来约束类型级别列表的元素。我有这个代码：

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, TypeFamilies #-}

import GHC.TypeLits (KnownSymbol, symbolVal)
import GHC.Exts (Constraint)
import Data.Proxy (Proxy(..))

type family AllHave (c :: k -> Constraint) (xs :: [k]) :: Constraint
type instance AllHave c '[] = ()
type instance AllHave c (x ': xs) = (c x, AllHave c xs)

type family Head (xs :: [k]) :: k where
    Head (x ': xs) = x

headProxy :: proxy xs -> Proxy (Head xs)
headProxy _ = Proxy

test :: AllHave KnownSymbol xs => proxy xs -> String
test p = symbolVal (headProxy p)

main :: IO ()
main = putStrLn $ test (Proxy :: Proxy '["a", "b"])

据我了解，这应该可以，但是当我编译 ghc 时会吐出：

Test.hs:18:10:
    Could not deduce (KnownSymbol (Head xs))
      arising from a use of ‘symbolVal’
    from the context (AllHave KnownSymbol xs)
      bound by the type signature for
                 test :: AllHave KnownSymbol xs => proxy xs -> String
      at Test.hs:17:9-52
    In the expression: symbolVal (headProxy p)
    In an equation for ‘test’: test p = symbolVal (headProxy p)

【问题讨论】：

标签： haskell

【解决方案1】：

这里的问题是Head 在test 中输入xs 时不会减少，因此Haskell 无法从AllHave KnownSymbol xs 中推断出KnownSymbol (Head xs)。它不应该：如果xs 为空应该怎么办？

要解决这个问题，你可以像这样明确xs 不是空的：

test :: AllHave KnownSymbol (x ': xs) => proxy (x ': xs) -> String

【讨论】：

谢谢！那讲得通。作为一个后续问题 - 如果我确实想为空 xs 提供一个基本案例，并在整个列表中递归地定义 test 而不仅仅是头部，这会是什么样子？

【解决方案2】：

我对类型族了解不多，因此我将向您指出 gallais's answer 以了解您的代码中出了什么问题。这是一种非常不同的方法，具有许多演示功能。可能有更好的方法；我不知道。

data CList :: (k -> Constraint) -> [k] -> * where
  CNil :: CList c '[]
  CCons :: c t => proxy t -> CList c ts -> CList c (t ': ts)

mapCSimple :: (forall a . c a => Proxy a -> b) -> CList c as -> [b]
mapCSimple f CNil = []
mapCSimple f (CCons (t :: proxy t) ts) = f (Proxy :: Proxy t) : mapCSimple f ts

toStrings :: CList KnownSymbol v -> [String]
toStrings = mapCSimple symbolVal

class KnownSymbols (xs :: [Symbol]) where
  known :: proxy xs -> CList KnownSymbol xs

instance KnownSymbols '[] where
  known _ = CNil

instance (KnownSymbol x, KnownSymbols xs) => KnownSymbols (x ': xs) where
  known _ = CCons Proxy $ known Proxy

exampleG :: KnownSymbols xs => proxy xs -> String
exampleG p = show . toStrings $ known p

这给了

> putStrLn $ exampleG (Proxy :: Proxy '["Hello", "Darkness"])
["Hello","Darkness"]

为了得到更像你想要的东西，

cHead :: CList c (a ': as) -> Dict (c a)
cHead (CCons prox _) = Dict

test :: forall x xs . CList KnownSymbol (x ': xs) -> String
test xs = case cHead xs of Dict -> symbolVal (Proxy :: Proxy x)

test2 :: (KnownSymbols xs, xs ~ (y ': ys)) => proxy xs -> String
test2 prox = test (known prox)

这得到

> putStrLn $ test2 (Proxy :: Proxy '["Hello", "Darkness"])
Hello

还有一个有趣的功能：

data HList :: (k -> *) -> [k] -> * where
  HNil :: HList f '[]
  HCons :: f a -> HList f as -> HList f (a ': as)

mapC :: (forall a . c a => Proxy a -> f a) -> CList c as -> HList f as
mapC f CNil = HNil
mapC f (CCons (t :: proxy t) ts) = HCons (f (Proxy :: Proxy t)) (mapC f ts)

【讨论】：