Using Haskell ADT members' constructors as types-CodePudding

I have an algebraic data type like this:

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)

as my VRecord has a lot of operations on it, I need a way to define functions like:

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

but since VRecord is a data constructor, I have to define my functions like this:

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

which both reduces readability (mainly in documentation) and also forces me to deal with other cases of DBVal type. So what's the best way to deal with this situation?

CodePudding user response：

This can be done with 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

Try it here: http://goto.ucsd.edu:8090/index.html#?demo=permalink/1629647897_38731.hs

CodePudding user response：

Perhaps we could lift an auxiliary sum type using DataKinds, and turn DBVal into a GADT indexed by the auxiliary type. A simplified example:

{-# 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

Now we can write a function like

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

without having to consider the other branches. The exhaustivity checker knows that the only possible branch is VRecord and doesn't complain.

Because DBVal is now a GADT, we can't auto-derive Eq, Show, and Read. We must write the instances ourselves.

Also, we need the auxiliary SomeDBVal wrapper for when we don't want to bother with the DBType type index.

VArray and VRecord contain SomeDBVals, so we won't be able to use the more precise version of get on the sub-components.

I'm not sure I understand the motivation for this though. If you get your DBVals from an outside source, it's unlikely that they will arrive "tagged" with enough information to identify them as VRecords. So it seems that you'll need to pattern-match in any case.

CodePudding user response：

The other answers look quite complicated to me. I think it should be simple: don't take a DBVal, take the field of the constructor you know you have. So:

get :: [DBField] -> Keyword -> DBVal
get fields = ...

Define other operations on records similarly. The compiler will then enforce that callers know their DBVal is a VRecord -- because they won't have access to the [DBField] inside unless they (or their ancestor) has used a pattern-match to check that property dynamically.

If you really must, you can define a lifting operation to do this pattern match once and for all, but I probably wouldn't; in almost all cases I'd massage the callers instead, since they're going to invariably have their own ideas about what to do with values that aren't records. But, if you do want such a lift, it might look like

onRecord :: a -> ([DBField] -> a) -> (DBVal -> a)
onRecord def f val = case val of
    VRecord fields -> f vields
    _ -> def

Then you have, for example,

onRecord (error "not a record") get :: DBVal -> Keyword -> DBVal