在类型系统中模拟串行格式，如Servant [英] Model a serial format in the type system, like Servant
问题描述
我正在开发一个API集成，它忽略了XML或JSON的存在，而仅仅支持附加字符数据。 （如果感兴趣，请 Metro2 格式）
我正在简化，但想象一个人需要像这样序列化：
PERSON
YYYYMMDD
数字字段始终为右对齐和零填充。文本字段始终左对齐并填充空格。
例如：
0032PERSONDAVID WILCOX 19820711035
我可以在类型系统中表达这一点吗？像仆人一样？像这样的东西？
newtype ByteLength = ByteLength Int
newtype Age = Age Int
- etc
类型PersonMessage
=字段ByteLength'0
：|字段PERSON'5
：|字段名称'11
：|字段日期'21
：|字段时间'29
- ：|是理论类型运算符，如：>在仆人
中 - 数字是预期的偏移量
- 该字段的长度在类型
$ b中隐含
$ b
我可以静态检查我的序列化实现是否匹配类型？我可以静态检查第三个字段的偏移量名称）是 11 ？前面场的长度加起来是11？我假设不，因为这似乎需要完全依赖型支持。
这是否正确？
实例ToMetro年龄其中
- 使用类型系列获取类型系统的长度？
field =数字'3
- 表示这是如何编码的。需要使用类型家族的长度。或者如果这不起作用，把它放在构造函数中。
toMetro age =数字年龄
更新：函数我想静态验证：
personToMetro :: Person - > PersonMessage
personToMetro p = error确保我返回的是一个PersonMessage
{ - ＃LANGUAGE GADTs，DataKinds，KindSignatures，TypeOperators，ScopedTypeVariables＃ - }
模块Seriavant其中
导入GHC.TypeLits
导入Data.Proxy
导入Data.List（stripPrefix）
数据Skip（n :: Nat）=跳过导出显示
数据令牌（n :: Nat）=令牌字符串派生显示
数据亮（s ::符号）=亮导出显示
数据（：>>）ab = a：>> b导出Show
infixr：>>
类反序列化其中
deserialize :: String - > Maybe（a，String）
instance（KnownNat n）=> Deserialize（Skip n）其中
反序列化s = do
（_，s'）< - trySplit（natVal（Proxy :: Proxy n））s
return（Skip，s'）
实例（KnownNat n）=>反序列化（Token n）其中
反序列化s = do
（t，s'）< - trySplit（natVal（Proxy :: Proxy n））s
return（Token t，s' ）
实例（KnownSymbol点亮）=>反序列化（点亮）其中
反序列化s = do
s'< - stripPrefix（symbolVal（Proxy :: Proxy lit））s
return（Lit，s'）
实例（反序列化a，反序列化b）=>反序列化（a：> b）其中
反序列化s = do
（x，s'）< - 反序列化s
（y，s''）< - 反序列化s '
return（x：>> y，s''）
trySplit :: Integer - > [a] - >可能（[a]，[a]）
trySplit 0 xs = return（[]，xs）
trySplit n（x：xs）= do
（xs'，ys） - trySplit（n-1）xs
return（x：xs'，ys）
trySplit _ _ = Nothing
是的，所以这是相当简单的，但它已经允许你做
$ b $ pre $类型MyFormat =令牌4：>>点亮PERSON：>>跳过1：>>令牌4
testDeserialize :: String - >也许MyFormat
testDeserialize = fmap fst。反序列化
这样工作：
* Seriavant> testDeserialize1
Nothing
* Seriavant> testDeserialize1234PERSON Foo
Just（Token1234：>>（Lit：>>（Skip：>> TokenFoo）））
编辑：原来我完全误读了这个问题，而肖恩要求序列化，而不是反序列化......但是我们当然也可以这样做：
class Serialize a where
serialize :: a - >字符串
实例（KnownNat n）=> Serialize（Skip n）其中
serialize Skip = replicate（fromIntegral $ natVal（Proxy :: Proxy n））''
instance（KnownNat n）=> Serialize（Token n）其中
serialize（Token t）= pad（fromIntegral $ natVal（Proxy :: Proxy n））''t
实例（KnownSymbol lit）=> Serialize（点亮）其中
序列化Lit = symbolVal（Proxy :: Proxy点亮）
实例（序列化a，序列化b）=>序列化（a：>> b）其中
序列化（x：>> y）=序列化x ++序列化y
pad :: Int - > a - > [a] - > [a]
pad 0 _x0 xs = xs
pad n x0（x：xs）= x：pad（n-1）x0 xs
pad n x0 [] = replicate n x0
（当然这对于所有这些 String 串联等，但这不是重点）
* Seriavant> （（Token1234:: Token 4）：>>（Lit :: LitFOO）：>>（Skip :: Skip 2）：>>（TokenBar::令牌10））
1234FOO酒吧
当然，如果我们知道格式，我们可以避免那些烦人的类型注释：
type MyFormat = Token 4：>>点亮PERSON：>>跳过1：>>令牌4
testSerialize :: MyFormat - > String
testSerialize =序列化
* Seriavant> testSerialize（Token1234：>> Lit：>> Skip：>> TokenBar）
1234PERSON Bar
I'm working on an API integration that ignores the existence of XML or JSON in favor of just appending character data. (The Metro2 format, if interested)
I'm simplifying, but imagine that a person needs to be serialized like this:
- At pos 0, 4 chars: Number of bytes in the message
- At pos 5: 6 chars:
"PERSON"hard coded - At pos 11: 20 chars: Name, left-aligned and space-padded
- At pos 21: 8 chars: Birthday,
YYYYMMDD - At pos 29: 3 chars: Age, right-aligned and zero-padded
Numeric fields are always right-aligned and zero-padded. Text fields are always left-aligned and space padded.
For example:
"0032PERSONDAVID WILCOX 19820711035"
Can I express this in the type system? Like what servant does? Something like this?
newtype ByteLength = ByteLength Int
newtype Age = Age Int
-- etc
type PersonMessage
= Field ByteLength '0
:| Field "PERSON" '5
:| Field Name '11
:| Field Date '21
:| Field Age '29
-- :| is a theoretical type operator, like :> in servant
-- the number is the expected offset
-- the length of the field is implicit in the type
Can I statically check that my implementation of the serialization matches the type?
Can I statically check that the offset of the 3rd field (Name) is 11? That the lengths of the preceding fields add up to 11? I'm assuming no, since that seems like it would require full dependent type support.
Is this on the right track?
instance ToMetro Age where
-- get the length into the type system using a type family?
field = Numeric '3
-- express how this is encoded. Would need to use the length from the type family. Or if that doesn't work, put it in the constructor.
toMetro age = Numeric age
Update: Example of a function I would like to statically validate:
personToMetro :: Person -> PersonMessage
personToMetro p = error "Make sure that what I return is a PersonMessage"
Just to give you some inspiration, just do what Servant does and have different types for the different combinators you support:
{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, ScopedTypeVariables #-}
module Seriavant where
import GHC.TypeLits
import Data.Proxy
import Data.List (stripPrefix)
data Skip (n :: Nat) = Skip deriving Show
data Token (n :: Nat) = Token String deriving Show
data Lit (s :: Symbol) = Lit deriving Show
data (:>>) a b = a :>> b deriving Show
infixr :>>
class Deserialize a where
deserialize :: String -> Maybe (a, String)
instance (KnownNat n) => Deserialize (Skip n) where
deserialize s = do
(_, s') <- trySplit (natVal (Proxy :: Proxy n)) s
return (Skip, s')
instance (KnownNat n) => Deserialize (Token n) where
deserialize s = do
(t, s') <- trySplit (natVal (Proxy :: Proxy n)) s
return (Token t, s')
instance (KnownSymbol lit) => Deserialize (Lit lit) where
deserialize s = do
s' <- stripPrefix (symbolVal (Proxy :: Proxy lit)) s
return (Lit, s')
instance (Deserialize a, Deserialize b) => Deserialize (a :>> b) where
deserialize s = do
(x, s') <- deserialize s
(y, s'') <- deserialize s'
return (x :>> y, s'')
trySplit :: Integer -> [a] -> Maybe ([a], [a])
trySplit 0 xs = return ([], xs)
trySplit n (x:xs) = do
(xs', ys) <- trySplit (n-1) xs
return (x:xs', ys)
trySplit _ _ = Nothing
Yeah so this is quite spartan, but it already allows you to do
type MyFormat = Token 4 :>> Lit "PERSON" :>> Skip 1 :>> Token 4
testDeserialize :: String -> Maybe MyFormat
testDeserialize = fmap fst . deserialize
which works like this:
*Seriavant> testDeserialize "1" Nothing *Seriavant> testDeserialize "1234PERSON Foo " Just (Token "1234" :>> (Lit :>> (Skip :>> Token "Foo ")))
EDIT: Turns out I completely misread the question, and Sean is asking for serialization, not deserialization... But of course we can do that as well:
class Serialize a where
serialize :: a -> String
instance (KnownNat n) => Serialize (Skip n) where
serialize Skip = replicate (fromIntegral $ natVal (Proxy :: Proxy n)) ' '
instance (KnownNat n) => Serialize (Token n) where
serialize (Token t) = pad (fromIntegral $ natVal (Proxy :: Proxy n)) ' ' t
instance (KnownSymbol lit) => Serialize (Lit lit) where
serialize Lit = symbolVal (Proxy :: Proxy lit)
instance (Serialize a, Serialize b) => Serialize (a :>> b) where
serialize (x :>> y) = serialize x ++ serialize y
pad :: Int -> a -> [a] -> [a]
pad 0 _x0 xs = xs
pad n x0 (x:xs) = x : pad (n-1) x0 xs
pad n x0 [] = replicate n x0
(of course this has horrible performance with all this String concatenation etc. but that's not the point here)
*Seriavant> serialize ((Token "1234" :: Token 4) :>> (Lit :: Lit "FOO") :>> (Skip :: Skip 2) :>> (Token "Bar" :: Token 10)) "1234FOO Bar "
Of course, if we know the format, we can avoid those pesky type annotations:
type MyFormat = Token 4 :>> Lit "PERSON" :>> Skip 1 :>> Token 4
testSerialize :: MyFormat -> String
testSerialize = serialize
*Seriavant> testSerialize (Token "1234" :>> Lit :>> Skip :>> Token "Bar") "1234PERSON Bar "
这篇关于在类型系统中模拟串行格式，如Servant的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
