从异构集合中提取 Maybe

Question

我有一个项目，我定义了一个“异构列表”，如下所示。我不确定这个技巧叫什么，但我发现它很有用：

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}

import Data.Kind (Type)

data (a :: Type) :> (b :: Type) = a :> b
  deriving Show
infixr :>

有了这个，我可以编写任意长的值列表，如下所示：

val :: Int :> Bool :> String
val = 42 :> True :> "asdf"

我正在尝试编写一个函数来测试这样的值是否包含给定类型，如果是，则将其提取为

Maybe

。例如，

-- | getInt (42 :> "asdf") -> Just 42
-- | getInt (True :> "asdf") -> Nothing
getInt :: a :> b -> Maybe Int
getInt _ = ???

但是我还没有找到一种方法来编写这样的函数。我尝试使用

cast

来自

Data.Typeable

，但在尝试在类型级别解构时遇到了各种问题。

Answer 1

您可以使用

Type.Reflection

执行此操作，按照@chi的评论（见下文）。

但是，您可能会发现使用带有“cons”和“nil”构造函数以及嵌入的

Typeable

实例的更传统的列表类型会更容易：

{-# LANGUAGE DataKinds #-}

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

请注意，您可以通过一些巧妙命名的类型系列和别名来保持原始版本的大部分人体工程学：

{-# LANGUAGE UndecidableInstances #-}

type family (:>) t ts where
  t :> HList ts = HList (t ': ts)
  t :> x = TypeError (Text "(:>) type ended with " :<>: ShowType x
                     :<>: Text " instead of Nil")
type Nil = HList '[]

这允许你写：

val :: Int :> Bool :> String :> Nil
val = 42 :> True :> "asdf" :> Nil

因为类型中的

:>

和

Nil

是扩展为有效

HList

类型的类型族/别名，而表达式中的

:>

和

Nil

是相应

HList

类型的构造函数。

有了这个，就可以很容易地用

getInt

中的

cast

来定义

Data.Typeable

:

import Data.Typeable

getInt :: HList ts -> Maybe Int
getInt (x :> xs) | Just a <- cast x = Just a
                 | otherwise = getInt xs
getInt Nil = Nothing

至关重要的是，额外的

Nil

构造函数消除了在类型级别尝试区分

:>

构造函数的右侧是否为最终值或“更多列表”的需要。

以相对较小的成本（一点

:> Nil

样板），以各种方式使用通常会更加愉快。

完整示例：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module KindList2 where

import Data.Typeable
import GHC.TypeError

infixr :>
type family (:>) t ts where
  t :> HList ts = HList (t ': ts)
  t :> x = TypeError (Text "(:>) type ended with " :<>: ShowType x
                     :<>: Text " instead of Nil")
type Nil = HList '[]

data HList ts where
  (:>) :: Typeable t => t -> HList ts -> HList (t ': ts)
  Nil :: HList '[]

getInt :: HList ts -> Maybe Int
getInt (x :> xs) | Just a <- cast x = Just a
                 | otherwise = getInt xs
getInt Nil = Nothing

v1 :: Int :> Bool :> String :> Nil
v1 = 42 :> True :> "asdf" :> Nil
v2 :: String :> Int :> String :> Nil
v2 = "between" :> 2 :> "strings" :> Nil
v3 :: String :> Int :> Nil
v3 = "sweet" :> 16 :> Nil
v4 :: String :> Bool :> Nil
v4 = "contains Int = " :> False :> Nil

main = do
  print $ getInt v1
  print $ getInt v2
  print $ getInt v3
  print $ getInt v4

产生输出：

λ> main
Just 42
Just 2
Just 16
Nothing

但是，如果您想坚持仅使用

:>

的方法，那么

Data.Typeable

是不够的，因为它无法在类型级别“分解”。您可能已经发现它很容易编写：

import Data.Kind (Type)
import Data.Typeable

data (a :: Type) :> (b :: Type) = a :> b
  deriving (Show)
infixr :>

getInt :: (Typeable a, Typeable b) => a :> b -> Maybe Int
getInt (a :> b) | Just x <- cast a = Just x
                | Just x <- cast b = Just x

可以成功地从

Int

和

Int :> Bool

中提取

Bool :> Int

，但是没有直接的方法可以使用

cast

进行递归：

getInt :: (Typeable a, Typeable b) => a :> b -> Maybe Int
getInt (a :> b) | Just x <- cast a = Just x
                | Just x <- cast b = Just x
                | Just rest <- cast b = getInt rest   -- ERROR

因为即使

cast b

可以成功地将

b

转换为

c :> d

，但无法从

Typeable c

获得所需的

Typeable d

和

Typeable b

约束。

但是，如果您使用

Type.Reflection

代替，这是可能的。请注意，我在这里使用了显式导出列表，但基本上为了方便起见，我使用了来自

cast

的

Data.Typeable

，其他所有内容（包括

Typeable

类型本身）都需要来自 `Type.Reflection）。

import Data.Typeable (cast)
import Type.Reflection (Typeable, pattern App, pattern HRefl, pattern TypeRep,
                        typeOf, eqTypeRep, withTypeable,)


getInt :: (Typeable a, Typeable b) => a :> b -> Maybe Int
getInt (a :> b)

  -- handle `Int :> a`
  | Just x <- cast a = Just x

  -- handle `x :> (y :> z)`
  --   extract type (of right-hand side) as:  c `op` d
  | App (App op c) d <- typeOf b
  --   check op ~ (:>)
  , Just HRefl <- eqTypeRep op (TypeRep @(:>))
  --   extract Typeable c, Typeable d, and recurse
    = withTypeable c $ withTypeable d $ getInt b

  -- handle `x :> Int`
  | Just x <- cast b = Just x

  -- handle remaining cases
  | otherwise = Nothing

完整示例：

{-# LANGUAGE GADTs #-}            -- needed to avoid "fragile" guard bindings
{-# LANGUAGE PatternSynonyms #-}  -- only needed for import list
{-# LANGUAGE TypeOperators #-}

module KindList where

import Data.Typeable (cast)
import Type.Reflection (Typeable, pattern App, pattern HRefl, pattern TypeRep,
                        typeOf, eqTypeRep, withTypeable,)

data a :> b = a :> b deriving (Show)
infixr :>

getInt :: (Typeable a, Typeable b) => a :> b -> Maybe Int
getInt (a :> b)
  | Just x <- cast a = Just x
  | App (App op c) d <- typeOf b
  , Just HRefl <- eqTypeRep op (TypeRep @(:>))
    = withTypeable c $ withTypeable d $ getInt b
  | Just x <- cast b = Just x
  | otherwise = Nothing

v1 :: Int :> Bool :> String
v1 = 42 :> True :> "asdf"
v2 :: String :> Int :> String
v2 = "between" :> 2 :> "strings"
v3 :: String :> Int
v3 = "sweet" :> 16
v4 :: String :> Bool
v4 = "contains Int = " :> False

main = do
  print $ getInt v1
  print $ getInt v2
  print $ getInt v3
  print $ getInt v4