Назначьте параметр уровня типа дереву структуры данных - PullRequest
Новая
       24

Назначьте параметр уровня типа дереву структуры данных

2 голосов
/ 28 мая 2020

У меня есть удаленный микроконтроллер, который предоставляет некоторые свойства в виде дерева. Все эти свойства можно читать, и в некоторые из них можно записывать. Свойство - это просто строка, в которой каждый уровень дерева разделен символом ..

В качестве примера дерево свойств выглядит примерно так: 

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 = ...

Я знаю, что сейчас это вообще не работает. Но я открыт для изменения структуры данных или использования чего-то еще для достижения чего-то подобного.

Есть у кого-нибудь идеи?

Спасибо, что прочитали!

Ответы [ 2 ]

2 голосов
/ 29 мая 2020

В качестве альтернативы, вместо того, чтобы представлять компоненты пути вашего дерева свойств в виде набора алгебраических c «узлов» типа и «листьев» конструктора, рассмотрите более единообразное представление в виде дерева уровня типа, в котором хранятся доступность и тип в качестве значений (листьев) дерева: 

{-# 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, где значения в iorefs являются 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 обеспечивает автоматическое c сопоставление с путями свойств на уровне значений, избавляя вас от необходимости писать много шаблонов в сопоставьте сеть алгебраических c типов с их путями свойств. К недостаткам можно отнести несколько уродливый синтаксис и необходимость подобрать правильное сочетание типов приложений, прокси и необязательных и обязательных промоутеров с галочкой.

В любом случае полный код: 

{-# 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
1 голос
/ 29 мая 2020

Расширяя мой комментарий, один из подходов может быть примерно таким: 

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

Настройка экземпляров чтения немного сложнее, потому что нет гарантии уникального способа создания (например) 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 ()
Добро пожаловать на сайт PullRequest, где вы можете задавать вопросы и получать ответы от других членов сообщества.

Похожие темы

...