使用 Haskell ADT 成员的构造函数作为类型

Question

我有一个这样的代数数据类型：

type Keyword = Text

data DBField = (:=) Keyword DBVal
  deriving (Show, Read, Eq)

data DBVal = VNull
           | VInt Int64
           | VDouble Double
           | VBool Bool
           | VString Text
           | VUTCTime UTCTime
           | VArray [DBVal]
           | VObjId ObjectId
           | VUUID UUID
           | VRecord [DBField]
  deriving (Eq, Show, Read)

由于我VRecord有很多操作，我需要一种定义函数的方法，例如：

get :: VRecord -> Keyword -> Maybe DBVal
get r k = ...

但由于VRecord是一个数据构造函数，我必须像这样定义我的函数：

get :: DBVal -> Keyword -> Maybe DBVal
get r@(VRecord _) k = ...
get _ _ = ...

这既降低了可读性（主要在文档中），也迫使我处理其他DBVal类型的情况。那么处理这种情况的最佳方法是什么？

Answer 1

这可以通过 Liquid Haskell 完成：

module DB where

import Data.Text
import Data.Int
import Data.Time

type Keyword = Text

data DBField = (:=) Keyword DBVal
  deriving (Show, Read, Eq)

data DBVal = VNull
           | VInt Int64
           | VDouble Double
           | VBool Bool
           | VString Text
           | VUTCTime UTCTime
           | VArray [DBVal]
           | VRecord [DBField]
  deriving (Eq, Show, Read)

{-@ measure isVRecord @-}
isVRecord (VRecord _) = True
isVRecord _ = False

{-@ type VRecord = {v:DBVal | isVRecord v} @-}

{-@ get :: VRecord -> Keyword -> Maybe DBVal @-}
get :: DBVal -> Keyword -> Maybe DBVal
get (VRecord xs) k = undefined

test :: Maybe DBVal
test = get VNull (pack "test") -- error

在这里试试：http : //goto.ucsd.edu : 8090/index.html#?demo=permalink%2F1629647897_38731.hs

Answer 2

也许我们可以使用 提升一个辅助和类型DataKinds，并DBVal变成一个由辅助类型索引的 GADT。一个简化的例子：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
data DBType = TNull
            | TInt
            | TDouble
            | TBool
            | TString
            | TArray 
            | TRecord 
  deriving (Eq, Show, Read)

data DBVal (t :: DBType) where
  VNull :: DBVal TNull
  VInt :: Int -> DBVal TInt
  VDouble :: Double -> DBVal TDouble
  VBool :: Bool -> DBVal TBool
  VString :: String -> DBVal TString
  VArray :: [SomeDBVal] -> DBVal TArray
  VRecord :: [DBField] -> DBVal TRecord

data SomeDBVal where
    SomeDBVal :: DBVal t -> SomeDBVal

现在我们可以写一个函数

get :: DBVal TRecord -> Keyword -> Maybe SomeDBVal
get r@(VRecord _) k = ...

无需考虑其他分支。穷举检查器知道唯一可能的分支是VRecord并且不会抱怨。

因为DBVal现在是一个GADT，我们不能自动获得Eq，Show和Read。我们必须自己编写实例。

此外，SomeDBVal当我们不想打扰DBType类型索引时，我们需要辅助包装器。

VArray并且VRecord包含SomeDBVals，因此我们将无法get在子组件上使用更精确的版本。

我不确定我是否理解这样做的动机。如果您DBVal从外部来源获得s，则它们到达时不太可能带有足够的信息来“标记”以将它们识别为VRecords。因此，在任何情况下，您似乎都需要进行模式匹配。