时间戳

首页 > 解决方案 > 使用 Haskell ADT 成员的构造函数作为类型

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

问题描述

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

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类型的情况。那么处理这种情况的最佳方法是什么？

标签： haskelladt

解决方案

这可以通过 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

推荐阅读