将类型级别参数分配给数据结构树

Question

我有一个远程微控制器，它在树状视图中公开一些属性。这些属性都可以读取，其中一些可以写入。属性只是一个字符串，其中树的每个级别由. 分隔。

例如，属性树如下所示：

Properties.prop1 = 0
Properties.prop2.foo = 1337
Properties.prop2.bar.baz1 = "hello"
Properties.prop2.bar.baz2 = "world"

其中Properties.prop1 和Properties.prop2.foo 仅可读。 Properties.prop2.bar.baz1 和 Properties.prop2.bar.baz2 是可读可写的。无论如何，我想在 Haskell 中使用强类型对其进行编码。

data Bar = Baz1 String | Baz2 String 
data Prop2 = Foo Int | Bar Bar
data Properties = Prop1 Int | Prop2 Prop2

现在你可以很好地创建一个属性了：

p = Prop2 $ Bar $ Baz1 "hello"

但我缺少的是如何通过这些构造函数将单个“路径”关联为可读属性或读/写属性。理想情况下，我希望有一个类或类型族“ReadableProp”和“WriteableProp”，这将允许我编写如下内容：

writeProp :: WriteableProp a => a -> IO ()
writeProp = ...

readProp :: ReadableProp a => IO a
readProp = ...

我知道现在这根本行不通。但我愿意改变数据结构或使用其他东西来实现这样的目标。

有人知道吗？

感谢您的阅读！

Answer 1

作为替代方案，不要将属性树路径组件表示为代数类型“节点”和构造函数“叶子”的集合，而是将更统一的表示形式视为类型级别树，将可访问性和类型存储为树的（叶）值：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

import GHC.TypeLits
import Data.Kind

data Value = RO Type | RW Type
data Tree = Leaf Symbol Value | Node Symbol [Tree]

type Properties
  = [ Leaf "prop1" (RO Int)
    , Node "prop2" [ Leaf "foo" (RO Int)
                   , Node "bar" [ Leaf "baz1" (RW String)
                                , Leaf "baz2" (RW String)
                                ]
                   ]
    ]

如果您为属性路径编写类型级别的查找函数：

{-# LANGUAGE TypeOperators #-}

type Lookup path = Lookup1 path Properties
type family Lookup1 path props where
  Lookup1 (p:ps) (Node p props' : props) = Lookup1 ps props'
  Lookup1 '[p]   (Leaf p val : qs) = val
  Lookup1 path   (prop : props) = Lookup1 path props

这样工作：

> :kind! Lookup '["prop1"]
Lookup '["prop1"] :: Value
= 'RO Int
> :kind! Lookup '["prop2", "bar", "baz1"]
Lookup '["prop2", "bar", "baz1"] :: Value
= 'RW String

这可以满足您的大部分需求。有几个方便的类型级函数：

{-# LANGUAGE ConstraintKinds #-}
type TypeOf path = GetType (Lookup path)
type Writeable path = GetAccess (Lookup path) ~ RW
type family GetType (value :: Value) where GetType (access a) = a
type family GetAccess (value :: Value) where GetAccess (access a) = access

您可以将属性定义为：

data Property path = Property { getProperty :: TypeOf path }

让您创建新的类型安全的属性值，如下所示：

> Property @'["prop1"] 5
Property @'["prop1"] 5 :: Property '["prop1"]
> Property @'["prop2","bar","baz1"] "hello"
Property @'["prop2","bar","baz1"] "hello"
  :: Property '["prop2", "bar", "baz1"]
> Property @'["prop2","bar","baz2"] 123  --- type error

使用实用程序类从类型级路径获取值级路径：

{-# LANGUAGE ScopedTypeVariables #-}
import Data.Proxy

class KnownPath (path :: [Symbol]) where
  pathVal :: proxy path -> [String]
instance KnownPath '[] where pathVal _ = []
instance (KnownSymbol p, KnownPath ps) => KnownPath (p:ps) where
  pathVal _ = symbolVal (Proxy @p) : pathVal (Proxy @ps)

我们可以创建一个假的微控制器，作为路径/ioref 对的映射，其中 ioref 中的值是 Haskell 可打印表示，可以使用 Read/Show 编组：

{-# LANGUAGE TupleSections #-}
import Data.Map.Strict (Map, (!))
import qualified Data.Map.Strict as Map
import Data.IORef

type MicroController = Map [String] (IORef String)

newmc :: IO MicroController
newmc
  = Map.fromList <$> mapM (\(k,v) -> (k,) <$> newIORef v) defaults
  where defaults = [ (["prop1"], "0")
                   , (["prop2","foo"], "1337")
                   , (["prop2","bar","baz1"], "\"hello\"")
                   , (["prop2","bar","baz2"], "\"world\"")
                   ]

属性读/写函数可以这样写。注意Writeable path 约束对writeProp 的使用。

{-# LANGUAGE FlexibleContexts #-}

readProp :: forall path. (KnownPath path, Read (TypeOf path))
         => MicroController -> IO (Property path)
readProp mc = do
  let path = pathVal (Proxy @path)
  Property . read <$> readIORef (mc ! path)

writeProp :: forall path. (KnownPath path, Show (TypeOf path), Writeable path)
          => Property path -> MicroController -> IO ()
writeProp prop mc = do
  let path = pathVal prop
  writeIORef (mc ! path) (show (getProperty prop))

我们可以这样测试：

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
deriving instance (Show (TypeOf path)) => (Show (Property path))

main :: IO ()
main = do
  mc <- newmc
  (prop1 :: Property '["prop1"]) <- readProp mc
  print prop1
  -- writeProp prop1 mc  -- type error: couldn't match RO with RW
  (baz1 :: Property '["prop2", "bar", "baz1"]) <- readProp mc
  print baz1
  let baz2' = Property @'["prop2", "bar", "baz2"] "Steve"
  writeProp baz2' mc
  (baz2 :: Property '["prop2", "bar", "baz2"]) <- readProp mc
  print baz2

这种方法的主要优点是属性树以单一类型级“结构”的形式公开，具有直接的树状表示，KnownPath 类提供到值级属性路径的自动映射，省去了编写大量样板来将代数类型网络映射到它们的属性路径的麻烦。缺点是语法有些难看，并且需要正确组合类型应用程序、代理以及可选与强制勾选的启动器。

不管怎样，完整的代码是：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits
import Data.Kind
import Data.Proxy
import Data.Map.Strict (Map, (!))
import qualified Data.Map.Strict as Map
import Data.IORef

data Value = RO Type | RW Type
data Tree = Leaf Symbol Value | Node Symbol [Tree]

type Properties
  = [ Leaf "prop1" (RO Int)
    , Node "prop2" [ Leaf "foo" (RO Int)
                   , Node "bar" [ Leaf "baz1" (RW String)
                                , Leaf "baz2" (RW String)
                                ]
                   ]
    ]

type Lookup path = Lookup1 path Properties
type family Lookup1 path props where
  Lookup1 (p:ps) (Node p props' : props) = Lookup1 ps props'
  Lookup1 '[p]   (Leaf p val : qs) = val
  Lookup1 path   (prop : props) = Lookup1 path props
type TypeOf path = GetType (Lookup path)
type Writeable path = GetAccess (Lookup path) ~ RW
type family GetType (value :: Value) where GetType (access a) = a
type family GetAccess (value :: Value) where GetAccess (access a) = access

data Property path = Property { getProperty :: TypeOf path }
deriving instance (Show (TypeOf path)) => (Show (Property path))

class KnownPath (path :: [Symbol]) where
  pathVal :: proxy path -> [String]
instance KnownPath '[] where pathVal _ = []
instance (KnownSymbol p, KnownPath ps) => KnownPath (p:ps) where
  pathVal _ = symbolVal (Proxy @p) : pathVal (Proxy @ps)

type MicroController = Map [String] (IORef String)

newmc :: IO MicroController
newmc
  = Map.fromList <$> mapM (\(k,v) -> (k,) <$> newIORef v) defaults
  where defaults = [ (["prop1"], "0")
                   , (["prop2","foo"], "1337")
                   , (["prop2","bar","baz1"], "\"hello\"")
                   , (["prop2","bar","baz2"], "\"world\"")
                   ]

readProp :: forall path. (KnownPath path, Read (TypeOf path))
         => MicroController -> IO (Property path)
readProp mc = do
  let path = pathVal (Proxy @path)
  Property . read <$> readIORef (mc ! path)

writeProp :: forall path. (KnownPath path, Show (TypeOf path), Writeable path)
          => Property path -> MicroController -> IO ()
writeProp prop mc = do
  let path = pathVal prop
  writeIORef (mc ! path) (show (getProperty prop))

main :: IO ()
main = do
  mc <- newmc
  (prop1 :: Property '["prop1"]) <- readProp mc
  print prop1
  -- writeProp prop1 mc  -- type error: couldn't match RO with RW
  (baz1 :: Property '["prop2", "bar", "baz1"]) <- readProp mc
  print baz1
  let baz2' = Property @'["prop2", "bar", "baz2"] "Steve"
  writeProp baz2' mc
  (baz2 :: Property '["prop2", "bar", "baz2"]) <- readProp mc
  print baz2

Answer 2

扩展我的评论，一种方法可能类似于

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind (Constraint)
import Data.Type.Bool (If)
import Type.Errors (DelayError, ErrorMessage(ShowType, Text, (:<>:)))

data Bar = Baz1 String | Baz2 String deriving (Read, Show)
data Prop2 = Foo Int | Bar Bar deriving (Read, Show)

data RW = Read_ | Write_
data Props = Prop1_ | Prop2_
data Properties (a :: Props) where
  Prop1 :: Int -> Properties Prop1_
  Prop2 :: Prop2 -> Properties Prop2_
deriving instance Show (Properties a)

type family Permissions (a :: Props) :: [RW] where
  Permissions Prop1_ = '[Read_]
  Permissions Prop2_ = '[Read_, Write_]

type family Contains (x :: k) (xs :: [k]) where
  Contains _ '[] = False
  Contains x (x ': _) = True
  Contains x (_ ': xs) = Contains x xs

type HasPermission (a :: Props) (b :: RW) = 
  If
    (Contains b (Permissions a)) 
    (() :: Constraint)
    (DelayError (ShowType a :<>: Text " does not have required permission " :<>: ShowType b))

class Writeable (a :: Props)
instance (HasPermission a Write_) => Writeable a

class ReadProp (a :: Props) where
  read_ :: String -> Properties a
instance ReadProp Prop1_ where read_ = Prop1 . read
instance ReadProp Prop2_ where read_ = Prop2 . read

class ReadProp a => Readable (a :: Props)
instance (ReadProp a, HasPermission a Read_) => Readable a

设置读取实例有点额外的痛苦，因为无法保证构造（例如）Properties Prop1_ 的唯一方式，因此您必须指定使用哪个构造函数。

那么我们就可以使用它了：

writeProp :: Writeable x => Properties x -> IO ()
writeProp x = print x

readProp :: Readable x => IO (Properties x)
readProp = read_ <$> readFile "a.txt"

:t readProp @Prop1_
readProp @Prop1_ :: IO (Properties 'Prop1_)
:t readProp @Prop2_
readProp @Prop2_ :: IO (Properties 'Prop2_)

:t writeProp (Prop1 5)
* 'Prop1_ does not have required permission 'Write_
:t writeProp (Prop2 $ Bar $ Baz1 "")
writeProp (Prop2 $ Bar $ Baz1 "") :: IO ()