我有一個這樣的代數資料型別：
我有一個這樣的代數資料型別。
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 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型別的情況。那么，處理這種情況的最好方法是什么呢？
uj5u.com熱心網友回復：
這可以用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/1629647897_38731.hs
uj5u.com熱心網友回復：
也許我們可以使用DataKinds提升一個輔助的和型別，并將DBVal變成一個由輔助型別索引的GADT。一個簡化的例子：
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
data DBType = TNull
|TInt
| TDouble
| TBool | TBool
| TString TString
| TArray | TArray
| TRecord TRecord
deriving (Eq, Show, Read)
data DBVal (t : : DBType) where
VNull :: DBVal TNull VNull :.
VInt :: Int -> DBVal TInt
VDouble :: Double -> DBVal TDouble
VBool :: Bool -> DBVal TBool
VString :: String -> DBVal TStringVArray :: [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，那么它們不可能在到達時被 "標記 "為足夠的資訊來識別它們是 VRecord。因此，在任何情況下，你都需要進行模式匹配。
uj5u.com熱心網友回復：
其他的答案在我看來相當復雜。我認為這應該很簡單：不要取一個DBVal，取你知道的建構式的欄位。所以：
get :: [DBField] -> Keyword -> DBVal
get fields = ...。
以類似的方式定義對記錄的其他操作。編譯器將強制要求呼叫者知道他們的DBVal是一個VRecord--因為他們將無法訪問里面的[DBField]，除非他們（或他們的祖先）使用模式匹配來動態地檢查該屬性。
如果你真的需要，你可以定義一個提升操作來一勞永逸地進行這種模式匹配，但我可能不會這樣做；幾乎在所有情況下，我都會對呼叫者進行按摩，因為他們對于如何處理不是記錄的值會有自己的想法。但是，如果你確實需要這樣的提升，它可能會像
一樣onRecord :: a -> ([DBField] -> a) -> （DBVal -> a
onRecord def f val = case val of >。
VRecord fields -> f vields
_ -> def
那么你就有，例如，
onRecord (error "not a record"/span>) get : : DBVal -> Keyword -> DBVal >。
轉載請註明出處，本文鏈接：https://www.uj5u.com/shujuku/316970.html
標籤：
上一篇：實體約束比較型別-家族約束