Model a serial format in a type system such as Servant

Question

I am working on an API integration that ignores the existence of XML or JSON in favor of only added character data. ( Metro2 if it is interesting)

I simplify, but imagine that a person should be serialized as follows:

• In pos 0, 4 characters: the number of bytes in the message
• At position 5: 6 characters: "PERSON" hardcoded
• At 11: 20 characters: name, left justification and space
• At position 21: 8 characters: Birthday, YYYYMMDD
• In column 29: 3: age, right alignment, and null pad

Numeric fields are always right-aligned and zero. Text fields are always left-aligned and filled with a space.

For instance:

 "0032PERSONDAVID WILCOX 19820711035" 

Can this be expressed in a type system? Like what servant does? Something like that?

 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 

Is it possible to statically check if my serialization implementation matches the type?

Is it possible to statically verify that the offset of the 3rd field ( Name ) is 11 ? What are the lengths of previous fields up to 11? I guess not, because it seems like this would require full support for the dependent type.

Is it 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: An example of a function that I would like to statically test:

 personToMetro :: Person -> PersonMessage personToMetro p = error "Make sure that what I return is a PersonMessage" 

Answer 1

Just to give you some inspiration, just do what Servant does, and you have different types for the different combinators that 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 (:>>) ab = 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 

Yes, it's pretty 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 as follows:

 *Seriavant> testDeserialize "1" Nothing *Seriavant> testDeserialize "1234PERSON Foo " Just (Token "1234" :>> (Lit :>> (Skip :>> Token "Foo "))) 

EDIT . It turns out that I completely misunderstood the question, and Sean asks for serialization, not deserialization ... But, of course, we can do this:

 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 terrible performance with all this String concatenation, etc., but it’s not)

 *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 these annoying annotations like:

 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 "