some open questions

Schemas.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}


module Lib
    ( personSchema
     , main
    ) where





import Control.Applicative
import Data.Functor.Identity
import Data.Functor.Contravariant
import Data.Functor.Contravariant.Divisible
import Data.Bifunctor
import Data.List






--These are representations that allow us to talk about Sum and Product types in our schemas

type (~>) f g = forall x. f x -> g x

tuple :: Applicative f =>  (f a) -> (f b) -> (f (a, b))
tuple fa fb = (fmap (\a -> (\b -> (a,b))) fa) <*> fb


data FreeSum f a where
  SumPure :: (f a) -> FreeSum f a
  SumCons :: (f a) -> FreeSum f b -> FreeSum f (Either a b)





data FreeProduct f a where
  ProductPure :: (f a) -> FreeProduct f a
  ProductCons :: (f a) -> FreeProduct f b -> FreeProduct f (a, b)



productCovariantFold :: Applicative g => FreeProduct f a -> (f ~> g) -> (g a)
productCovariantFold (ProductPure fa ) nt =  nt fa
productCovariantFold (ProductCons fa tails) nt = tuple (nt fa) (productCovariantFold tails nt) 

productContravariantFold :: Divisible g => FreeProduct f a -> (f ~> g) -> (g a)
productContravariantFold (ProductPure fa ) nt =  nt fa
productContravariantFold (ProductCons fa tails) nt = divide id (nt fa) (productContravariantFold tails nt) 


sumCovariantFold :: Alternative g => FreeSum f a -> (f ~> g) -> (g a)
sumCovariantFold (SumPure fa) nt = (nt fa)
sumCovariantFold (SumCons fa tails) nt =  (fmap Left (nt fa)) <|> (fmap Right (sumCovariantFold tails nt))

sumContravariantFold :: Decidable g => FreeSum f a -> (f ~> g) -> (g a)
sumContravariantFold (SumPure fa) nt = nt fa
sumContravariantFold (SumCons fa tails) nt = choose id (nt fa) (sumContravariantFold tails nt)



--The covariant fold for product requires an applicative but else looks basically the same
--There are indeed also Contravariant folds requiring Decidable for Sums and Divisible for Products.



--Sum and Product Terms normally have some sort of IDs e.g. when working with json, prop names
data Term prim a a0 = Term String (Schema prim a0)




--the actual schema GADT
data Schema prim  a where
  Prim :: prim a0 -> Schema prim a0
  Opt  :: Schema prim a0 -> Schema prim (Maybe a0)
  Seq  :: Schema prim a0 -> Schema prim [a0]
  Prod :: FreeProduct (Term prim a) a0 -> (a -> a0) -> (a0 -> a) -> Schema prim a
  Sum  :: FreeSum (Term prim a) a0 -> (a -> a0) -> (a0 -> a) -> Schema prim a



--A Toy example of what we could do
data Role = User Bool | Admin [String]

data Person = Person String Role

 

data JsonPrim p where
  JString :: JsonPrim String
  JBool :: JsonPrim Bool

 

 
--these four funcitons are needed to proove equality of representation of our data and their deconstructions into the sum/prod representations
roleToEither:: Role -> (Either Bool [String])
roleToEither (User b)  = Left b
roleToEither (Admin s) = Right s

eitherToRole:: (Either Bool [String]) -> Role
eitherToRole (Left b)  = User b
eitherToRole (Right s) = Admin s


personToTuple:: Person -> (String, Role)
personToTuple (Person name role) = (name, role)

tupleToPerson:: (String, Role) -> Person
tupleToPerson (name, role) = Person name role

personSchema :: Schema JsonPrim Person
personSchema = Prod
  (ProductCons
    (Term "name" (Prim JString))
    (ProductPure
      (Term
        "role"
        (Sum
          (SumCons
            (Term "user" (Prim JBool))
            (SumPure (Term "admin" (Seq (Prim JString))))
          )
          roleToEither
          eitherToRole
        )
      )
    )
  )
  personToTuple
  tupleToPerson




--Now you could e.g. write Schema a -> (a -> JSON) by employing contravariant folds over prod and sum, and mappings for prims etc. This is all shown below. just ignore the fact that this is some
-- super ugly haskell and the json is actually not correct this is only meant to show that it works in general

--The hard part. The questions
--Can we prove duality FreeSum f x <-> FreeProduct f y where e.g x = (String, (Int, Bool)) and y = Either String (Either Int Bool)?
--Can we unify FreeSum and Free Product to one Type
--Can we unify Seq and Opt to one type by leveraging covariant functor and some sort of folding?

type JSON = String

newtype JSONSerializer f a = JSONSerializer (a -> (f JSON))
getF :: JSONSerializer f a -> (a -> (f JSON))
getF (JSONSerializer f) = f


instance Contravariant (JSONSerializer Identity) where
  contramap f (JSONSerializer ser) = JSONSerializer (\a -> ser (f (a)))

instance Divisible (JSONSerializer Identity) where 
  conquer = JSONSerializer (\a ->  mempty)
  divide f (JSONSerializer fb) (JSONSerializer fc) = JSONSerializer (\a ->combine (bimap fb fc (f a))) where
    combine (a1, a2) = mappend a1 a2

instance Decidable (JSONSerializer Identity) where 
  lose f  = JSONSerializer (\a ->  mempty)
  choose f (JSONSerializer fb) (JSONSerializer fc) = JSONSerializer (\a -> g (f a)) where
    g (Left b)  = fb b
    g (Right c) = fc c

instance Contravariant (JSONSerializer []) where
  contramap f (JSONSerializer ser) = JSONSerializer (\a -> ser (f (a)))


instance Divisible (JSONSerializer []) where 
  conquer = JSONSerializer (\a ->  mempty)
  divide f (JSONSerializer fb) (JSONSerializer fc) = JSONSerializer (\a ->combine (bimap fb fc (f a))) where
    combine (a1, a2) = mappend a1 a2


jsonPrimToJson:: JsonPrim ~> (JSONSerializer Identity) 
jsonPrimToJson (JString) = JSONSerializer(\s -> Identity s)
jsonPrimToJson (JBool) = JSONSerializer (\b -> Identity (show b))


jsonProductTerms :: (prim ~> (JSONSerializer Identity)) -> ((Term prim a ) ~> JSONSerializer [] )
jsonProductTerms prim (Term id base)  = JSONSerializer (\a0 -> [ "\"" ++  id ++ "\":" ++ (jsonSerializer base prim a0)]) 

jsonSumTerms :: (prim ~> (JSONSerializer Identity)) -> ((Term prim a ) ~> JSONSerializer Identity )
jsonSumTerms prim (Term id base) = JSONSerializer (\a0 -> Identity ("{\"" ++ id ++ "\":" ++ (jsonSerializer base prim a0) ++ "}"))


jsonSerializer :: Schema prim a -> (prim ~> (JSONSerializer Identity)) -> (a -> JSON)
jsonSerializer (Prim p) prims = \a -> runIdentity (getF (prims p) a)
jsonSerializer (Opt base) prims = \optb -> fold optb
  where 
    fold (Just b) = jsonSerializer base prims b
    fold (Nothing) = "null"
jsonSerializer (Seq base) prims = \bs -> "[" ++ (intercalate "," (fmap (jsonSerializer base prims) bs)) ++ "]"
jsonSerializer (Prod terms f g) prims = \prod -> "{" ++ (intercalate "," ( (getF (productContravariantFold terms (jsonProductTerms prims))) (f prod))) ++ "}" where  
jsonSerializer (Sum terms f g) prims = \sum ->  (\x -> (fmap runIdentity (getF (sumContravariantFold terms (jsonSumTerms prims)))) x) (f sum) where




person :: Person
person = Person "asdf" (User True)

serializer :: Person -> JSON 
serializer = jsonSerializer personSchema jsonPrimToJson

main :: IO ()
main = do
     print (serializer person)