record.hs

-- | Unsorted Records based on HashMaps
--
-- Instead of ensuring type safety by construction we create a coincidence
-- between value and type level. This is less save but allows us to work with
-- HashMaps instead of linked lists

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}

module Record where

import           Data.Aeson
import qualified Data.ByteString.Lazy     as BSL
import           Data.HashMap.Strict      (HashMap)
import qualified Data.HashMap.Strict      as HMap
import           Data.Monoid              ((<>))
import           Data.Singletons
import           Data.Singletons.TypeLits
import           Data.Text                (Text)
import qualified Data.Text                as Text
import           GHC.Exts
import           GHC.TypeLits

import           Unsafe.Coerce            (unsafeCoerce)

import           Prelude                  hiding (lookup, map)

data AnyVal = forall a. AnyVal a

-- | Allows us to create Records of any type. We restrict the functions that can
-- create these to ensure type safety
newtype Record (fields :: [(Symbol,*)]) :: * where
  Record :: (HashMap Text AnyVal) -> Record a

-- We hope to create a coincidence between 'At' and 'lookup' so unsaefeCoerce is
-- actually safe

-- | Lookup the type of a certain field
type family At (record :: [(Symbol, *)]) (name :: Symbol) :: * where
  At ('(field, a):_) field = a
  At (_:record') field = record' `At` field
  At record field = TypeError ('Text "Record does not contain field " ':<>: 'ShowType field )

-- | Type-safe lookup.
lookup :: forall field record. Sing field -> Record record -> record `At` field
lookup name (Record m) =
  case HMap.lookup (Text.pack $ fromSing name) m of
    Nothing -> error "Record lookup: value not found. This is a bug"
    -- The basic assumption of all this is that this is safe:
    Just (AnyVal x) -> unsafeCoerce x

type family Without (record :: [(Symbol, *)]) (name :: Symbol) :: [(Symbol, *)] where
  Without '[] _ = '[]
  Without ('(field, _):fields) field = Without fields field
  Without (field' : fields) field = field' : Without fields field

delete :: Sing field -> Record fields -> Record (fields `Without` field)
delete s (Record hmap) = Record $ HMap.delete (Text.pack $ fromSing s) hmap

type family With (record :: [(Symbol, *)]) (field :: (Symbol, *)) :: [(Symbol, *)] where
  With record '(name, a) = '(name, a) : (Without record name)

-- | Insertion when the field is not present yet
insertSimpl :: (fields `Without` field ~ fields)
            => Sing field
            -> a
            -> Record fields
            -> Record ('(field, a) : fields)
insertSimpl s a (Record r) =
  Record $ HMap.insert (Text.pack $ fromSing s) (AnyVal a) r

insert :: Sing name -> a -> Record fields -> Record (fields `With` '(name, a))
insert name x (Record m) = Record $ HMap.insert (Text.pack $ fromSing name) (AnyVal x) m

-- | Because of injectivity of "With" we don't need to pass a singleton.
--
-- Can be called with -XTypeApplications
--
-- > insert @"foo" True empty
insert' :: forall name fields a. KnownSymbol name
        => a
        -> Record fields
        -> Record (fields `With` '(name, a))
insert' = insert sing

-- | Left-biased merge
type family (<++>) (record1 :: [(Symbol, *)]) (record2 :: [(Symbol, *)])  :: [(Symbol, *)] where
  '[] <++> fieldsr = fieldsr
  ('(field, a): fieldsl) <++> fieldsr = (fieldsl <++> fieldsr) `With` '(field, a)
    -- '(field, a) : (fieldsl <++> fieldsr `Without` field )

-- -- | Left-biased union
union :: Record recordl -> Record recordr -> Record (recordl <++> recordr)
-- No unsafeCoerce necessary because Record is not type-safe
union (Record r1) (Record r2) = Record $ HMap.union r1 r2

type family Subset (subset :: [(Symbol,*)]) (superset :: [(Symbol,*)]) :: Constraint where
  Subset '[] _ = ()
  Subset ('(field, a) : fields) superset = ( superset `At` field ~ a, Subset fields superset)

cast :: forall record1 record2. (record1 `Subset` record2) => Record record2 -> Record record1
cast (Record m) = Record m

class All (c :: * -> Constraint) (record :: [(Symbol,*)]) where
  toHashMap :: proxy c
            -> (forall a. c a => a -> r)
            -> Record record
            -> HashMap Text r
  fromHashMap :: forall r proxy.
                 proxy c
              -> (forall a. c a => r -> Either Text a)
              -> HashMap Text r
              -> Either Text (Record record)

instance All c '[] where
  toHashMap _ _ _ = HMap.empty
  fromHashMap _ _ _ = Right $ empty

instance ( Subset fields ('(field, a) : fields)
         , All c fields
         , KnownSymbol field
         , fields `Without` field ~ fields
         , c a
         ) => All c ('(field, a) : fields) where
  toHashMap prx f record =
    let record' = cast @fields record
        hmap = toHashMap prx f record'
        s = sing :: Sing field
    in HMap.insert (Text.pack $ fromSing s) (f (lookup s record)) hmap
  fromHashMap prx f hmap =
    let mbRecord = fromHashMap prx f hmap
        s = sing :: Sing field
        name = Text.pack $ fromSing s
    in case mbRecord of
         Left e -> Left e
         Right record ->
           case HMap.lookup name hmap of
             Nothing -> Left $ "Field not found: " <> name
             Just r -> case f r of
                         Left e -> Left e
                         Right r -> Right $ insertSimpl s r record

empty :: Record '[]
empty = Record HMap.empty

data Showable = forall a. Show a => Showable a

instance Show Showable where
  show (Showable s) = show s

-- | That's not quite right, the values are shown twice.
instance (All Show fields ) => Show (Record fields) where
  show  = show . toHashMap (Proxy :: Proxy Show) Showable

instance Eq (Record '[]) where
  (==) _ _ = True

instance ( Eq a
         , Eq (Record fields)
         , KnownSymbol field
         , Subset fields ('(field, a): fields)
         ) => Eq (Record ('(field, a): fields)) where
  (==) r1 r2 =
    let s = sing :: Sing field
        a = lookup s r1
        b = lookup s r2
        r1' = cast r1 :: Record fields
        r2' = cast r2 :: Record fields
    in a == b && r1' == r2'


-- instance Show (Record '[]) where
--   show _ = ""

-- instance ( Show a
--          , Show (Record as)
--          , KnownSymbol field
--          , Subset as ('(field, a) : as)
--          ) => Show ( Record ('(field, a) : as)) where
--   show map =
--     let name = fromSing (sing :: Sing field)
--     in show name ++ ": " ++ (show $ lookup @field sing map)
--        ++"; " ++ show (cast map :: Record as)

--------------------------------------------------------------------------------
-- Aeson -----------------------------------------------------------------------
--------------------------------------------------------------------------------

instance (All ToJSON fields) => ToJSON (Record fields) where
  toJSON map = Object $ toHashMap (Proxy :: Proxy ToJSON) toJSON map

instance (All FromJSON fields) => FromJSON (Record fields) where
  parseJSON = withObject "record" $ \o -> do
    case fromHashMap (Proxy :: Proxy FromJSON) fromJSON' o of
      Left e -> fail $ Text.unpack e
      Right r -> return r
    where
      fromJSON' x = case fromJSON x of
                      Success r -> Right r
                      Error e -> Left $ Text.pack e

--------------------------------------------------------------------------------
-- Examples --------------------------------------------------------------------
--------------------------------------------------------------------------------

infixl 1 &
(&) :: a -> (a -> b) -> b
(&) = flip ($)


example1 :: Record ['("abc", Bool), '("def", Integer)]
example1 = insert' @"abc" True . insert' @"def" (3 :: Integer) $ empty

example2 :: Record ['("foo", [Double]), '("def", Maybe Int)]
example2 = insert' @"foo" [4 :: Double, 5]
         . insert' @"def" (Nothing :: Maybe Int) $ empty


-- exampleOverwrite :: Record ['("foo", [Char]), '("def", Maybe Int)]
exampleOverwrite :: Record ['("foo", String), '("def", Maybe Int)]
exampleOverwrite = example2 & insert' @"foo" ("12345" :: String)

exampleUnion :: Record ['("abc", Bool), '("def", Integer), '("foo", [Double])]
exampleUnion = example1 `union` example2


exampleUnionValues :: (Bool, Integer, [Double])
exampleUnionValues = ( lookup @"abc" sing exampleUnion
                     , lookup @"def" sing exampleUnion
                     , lookup @"foo" sing exampleUnion
                     )

exampleSubset :: Record ['("abc", Bool), '("foo", [Double])]
exampleSubset = cast exampleUnion

exampleSubsetValues :: (Bool, [Double])
exampleSubsetValues = ( lookup @"abc" sing exampleUnion
                      , lookup @"foo" sing exampleUnion
                      )

--------------------------------------------------------------------------------
-- Usage Example ---------------------------------------------------------------
--------------------------------------------------------------------------------

type field := value = '(field, value)

type family (//) (record :: *) (field ::  Symbol) :: * where
  (Record fields) // field = Record (fields `Without` field)

type User = Record [ "name"  := Text
                   , "email" := Text
                   , "age"   := Integer
                   , "ID"    := Text
                   ]

-- Use cast to fix order of fields
exampleUser :: User
exampleUser = cast $ empty & insert' @"name" "Robert"
                           & insert' @"email" "no@spam.please"
                           & insert' @"age" 32
                           & insert' @"ID" "12345"

exampleUser2 :: User // "ID"
exampleUser2 = cast $ empty & insert' @"name" "Kathrin"
                            & insert' @"email" "bla@blub.foo"
                            & insert' @"age" 29


exampleUser2Encode :: BSL.ByteString
exampleUser2Encode = encode exampleUser2

-- "{\"email\":\"bla@blub.foo\",\"age\":29,\"name\":\"Kathrin\"}"

testAeson :: Bool
testAeson = decode exampleUser2Encode == Just exampleUser2