Capture json tree structure at the type level

Admin 1
Viewed 115

I'm in the process of implementing the Fibre protocol. The way the protocol works is that you recieve a json object which represents the operations and values you can do on a remote object. Below is an example of such a json.

{
  "name": "properties",
  "type": "object",
  "members": [
    {
      "name": "foo",
      "id": 1,
      "type": "uint32",
      "access": "rw"
    },
    {
      "name": "bar",
      "id": 2,
      "type": "uint32[]",
      "access": "r"
    },
    {
      "name": "bar",
      "type": "object",
      "members": [
        {
          "name": "baz",
          "id": 3,
          "type": "float",
          "access": "rw"
        },
        {
          "name": "some_function",
          "id": 4,
          "type": "function",
          "inputs": [
            {
              "name": "param1",
              "id": 5,
              "type": "float",
              "access": "rw"
            },
            {
              "name": "param2",
              "id": 6,
              "type": "bool",
              "access": "rw"
            }
          ],
          "outputs": [
            {
              "name": "result",
              "id": 7,
              "type": "bool",
              "access": "rw"
            }
          ]
        }
      ]
    }
  ]
}

As can be seen it's essentially a tree with properties and functions of certain types. Some properties can only be read which is indicated by access being r and some can be read/written indicated by access being rw. Capturing this structure in Haskell is straightforward with some data definition:

data FibreType
   = FibreInt8  | FibreUInt8
   | FibreInt16 | FibreUInt16
   | FibreInt32 | FibreUInt32
   | FibreInt64 | FibreUInt64
   | FibreFloat
   | FibreBool
   | FibreJSON
   | FibreList FibreType
  deriving (Show, Eq, Ord)

data FibreAccess = FibreReadable | FibreReadWriteable
  deriving (Show, Eq, Ord)

data FibreObject
   = FibreValue
       { _fibreValueName     :: String
       , _fibreValueEndpoint :: Word16
       , _fibreValueType     :: FibreType
       , _fibreValueAccess   :: FibreAccess
       }
   | FibreFunction
       { _fibreFunctionName     :: String
       , _fibreFunctionEndpoint :: Word16
       , _fibreFunctionArgs     :: [FibreType]
       , _fibreFunctionResult   :: [FibreType]
       }
   | FibreObject
       { _fibreObjectName    :: String
       , _fibreObjectMembers :: [FibreObject]
       }
  deriving (Show, Eq, Ord)

getProperty :: FibreObject -> IO ByteString
getProperty FibreObject{} = error "Cannot get property of FibreObject"
getProperty FibreFunction{} = error "Cannot get property of FibreFunction"
getProperty FibreValue{} = undefined -- Implementation removed for brevity

setProperty :: FibreObject -> ByteString -> IO ByteString
setProperty FibreObject{} = error "Cannot set property of FibreObject"
setProperty FibreFunction{} = error "Cannot set property of FibreFunction"
setProperty FibreValue{_fibreValueAccess = FibreReadWriteable} = undefined -- Implementation removed for brevit
setProperty FibreValue{} = error "Cannot set property of read-only FibreValue" 

callFunction :: FibreObject -> [ByteString] -> IO [ByteString]
callFunction FibreObject{} _ = error "Cannot call function for FibreObject"
callFunction FibreValue{} _ = error "Cannot call function for FibreObject"
callFunction FibreFunction{} args = undefined -- Implementation removed for brevit

But I really don't like that once I make the function getProperty or callFunction I lose all type safety and I essentially have to hack around this by making all inputs and outputs ByteString(or I could define a sum type) and then later deserialize to certain concrete values. So I wonder if it's possible to lift this structure to the type level even though that json definition is only available at runtime.

The goal is that I would be able to write something like this:

getProperty :: FibreValue type access -> IO type
getProperty FibreValue{} = undefined -- Implementation removed for brevity

setProperty :: FibreValue type FibreReadWriteable -> IO () 
setProperty FibreValue{} = undefined

callFunction :: FibreFunction [argTys] [resTys] -> argTys -> IO [resTys]
callFunction FibreValueFunction args = undefined -- Implementation removed for brevity

This would give full type safety without having to match on a result type which really could only be a single value. I release there are problems with the function definition I have given for callFunction but it's more to illustrate the point.

Is this possible in Haskell? Any help is appreciated.

type-level-computation haskell
1 Answers

One possible API design is

data SFibreAccess :: FibreAccess -> Type where
    SFibreReadable :: SFibreAccess FibreReadable 
    SFibreReadWriteable :: SFibreAccess FibreReadWriteable
-- contructors (and record fields) should be hidden
data FibreValue s a
   = FibreValue
       { fibreValueName     :: String
       , fibreValueEndpoint :: Word16
       , fibreValueType     :: FibreType
       , fibreValueAccess   :: SFibreAccess a
       }
data FibreFunction s
   = FibreFunction
       { fibreFunctionName     :: String
       , fibreFunctionEndpoint :: Word16
       , fibreFunctionArgs     :: [FibreType]
       , fibreFunctionResult   :: [FibreType]
       }
data FibreObject s
   = FibreObject
       { fibreObjectName    :: String
       , fibreObjectMembers :: [FibreSpec s]
       }
data FibreSpec s
   = forall a. FibreSpecValue (FibreValue s a)
   | FibreSpecFunction (FibreFunction s)
   | FibreSpecObject (FibreObject s)

data FibreAPI s
   = FibreAPI
       { fibreAPISpec :: FibreSpec s
       , fibreAPIGet :: FibreValue s a -> IO ByteString
       , fibreAPISet :: FibreValue s FibreReadWriteable -> ByteString -> IO ByteString
       , fibreAPICall :: FibreFunction s -> [ByteString] -> IO [ByteString] -- further type safety for function calls possible but tedious and not done here
       }

-- internal
data SomeFibreSpec = forall s. SomeFibreSpec (FibreSpec s)
getAndParseFibreSpec :: URL -> IO SomeFibreSpec
-- exposed
withFibreAPI :: URL -> (forall s. FibreAPI s -> r) -> IO r
withFibreAPI url cont = do
    SomeFibreSpec spec <- getAndParseFibreSpec url
    return $ cont FibreAPI
        { fibreAPISpec = spec
        , fibreAPIGet = \_ -> throwIO $ userError "unimplemented"
        , fibreAPISet = \_ -> throwIO $ userError "unimplemented"
        , fibreAPICall = \_ -> throwIO $ userError "unimplemented"
        }

The phantom parameter to FibreSpec means that, under a call/within the continuation to withFibreAPI, the arguments to the get, set, and call functions are guaranteed to come from taking the fibreAPISpec object apart. (The constructors and record fields are untouchable, and mixing FibreAPIs from different calls to withFibreAPI is a type error.) This prevents creating a FibreValue or FibreFunction out of the blue and expecting the functions to work. FibreValues also come tagged with their access control. Checking whether the property passed to fibreAPISet is accessible still needs to be done by someone (you would do it by getting the fibreValueAccess and caseing it), but now, once you check it once (and gain evidence a ~ FibreReadWriteable) every call will let you through, instead of repeatedly giving you a Maybe or whatever.

EDIT: Making the functions type safe:

data SFibreType :: FibreType -> Type where
    SFibreInt8 :: SFibreType FibreInt8
    -- etc.
    -- if it isn't obvious
    SFibreList :: SFibreType a -> SFibreType (FibreList a)
-- other names: HList, Product, HMapList, etc.
-- SList is really only correct for the combined type SList s where s is a singleton family, but whatever
data SList :: (a -> Type) -> [a] -> Type where
    SNil :: SList s '[]
    SCons :: s x -> SList s xs -> SList s (x : xs)
-- replace FibreFunction, FibreSpec
data FibreFunction s args ress
   = FibreFunction
   { fibreFunctionName     :: String
   , fibreFunctionEndpoint :: Word16
   , fibreFunctionArgs     :: SList SFibreType args
   , fibreFunctionResult   :: SList SFibreType ress
   }
data FibreSpec s =
   = forall a. FibreSpecValue (FibreValue s a)
   | forall args ress. FibreSpecFunction (FibreFunction s args res)
   | FibreSpecObject (FibreObject s)

data family ValueOf (t :: FibreType) :: Type
newtype instance ValueOf FibreInt8 = MkInt8 { getInt8 :: Int8 }
-- etc.

-- modify FibreAPI
data FibreAPI s
   = FibreAPI
       { fibreAPISpec :: FibreSpec s
       , fibreAPIGet :: FibreValue s a -> IO ByteString
       , fibreAPISet :: FibreValue s FibreReadWriteable -> ByteString -> IO ByteString
       , fibreAPICall ::
            forall args ress.
            FibreFunction s args ress ->
            SList ValueOf argss ->
            IO (SList ValueOf ress)
       }

Getting type safety for properties is similar: put the FibreType into the arguments of the specification part type, put an SFibreType into the actual values in place of the FibreType, put existentials in FibreSpec and put universals in FibreAPI.

user_56842570
Related