records.hs

-- |
-- Types and instances of anonymous records.
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds #-}
module Record where


-- TODO:
--  1. Implement strict containers
--  2. Write rules
--  3. Implement pattern matching ?
--  4. Implement instances ?

-- Rules:
--
-- 1. Data declaration:
--      type T = {~ foo :: A, bar :: B } ===>>>  type T = Anon '[A :? "foo", B :? "bar"]
--
-- 2. Pattern matching:
--      t@{~ foo :: A, bar :: B }  ===>>>> (t :: Anon '[A :? "foo", B :? "bar"], view (fieldLens (FieldName "foo")) t, view (fieldLens (FieldName "bar")) t)
--
-- 3. Expression:
--     {~ foo :: A, bar :: B } ===>>>> (Anon $ V.fromList n [unsafeCoerce foo, unsafeCoerce bar] :: Anon [A :? "foo", B :? "bar"]

import Data.Functor.Identity
import GHC.TypeLits
import Foreign.Storable
import Foreign.Ptr (plusPtr)
import Control.Lens.Basic
import Data.Vector (Vector, (!))
import qualified Data.Vector as Vector
import GHC.Exts
import Unsafe.Coerce
import Data.Proxy

data a :? (b :: Symbol)

data FieldName (t :: Symbol) = FieldName

type family FieldType (n :: Symbol) m where
  FieldType n ((a :? n) ': z) = a
  FieldType n (b ': z)        = FieldType n z

type family FieldIndex (n::Symbol) m :: Nat where
  FieldIndex n ((a :? n) ': z) = 0
  FieldIndex n (   b     ': z) = 1 + FieldIndex n z

type family FieldTags a :: [*]

newtype Anon (m :: [*]) = Anon (Vector Any)
type instance FieldTags (Anon f) = f

vIndexProxy :: (KnownNat c, FieldIndex n m ~ c) => FieldName n -> proxy m -> Proxy c
vIndexProxy _ _ = Proxy

class HasField (n :: Symbol) f a where
  fieldIndex  :: FieldName n -> f -> Int
  updateField :: FieldName n -> f -> a -> f
  getField    :: FieldName n -> f -> a

type family Remap (n :: Symbol) z b where
  Remap n ((a :? n) ': z) b = (b :? n) ': z
  Remap n (   b     ': z) c = b ': Remap n z c

remap :: proxy1 n -> proxy2 b -> Anon z -> Anon (Remap n z b)
remap _ _ (Anon x) = Anon x

belial :: (HasField (n :: Symbol) (Anon f) a, HasField (n :: Symbol) (Anon g) b, Remap n f b ~ g)
       => proxy a -> proxy b -> (FieldName n -> Anon f -> a -> Anon f) -> (FieldName n -> Anon f -> b -> Anon g)
belial _ b z = \n f -> remap n b . z n f . unsafeCoerce

instance (KnownNat d, FieldIndex n m ~ d, FieldType n m ~ a) => HasField ( n :: Symbol) (Anon m) a where
  fieldIndex name t = fromIntegral (natVal (vIndexProxy name t))
  updateField name t@(Anon v) z = Anon $ Vector.unsafeUpd v [(fieldIndex name t,unsafeCoerce z)]
  getField name t@(Anon v) = unsafeCoerce (v ! fieldIndex name t)

fieldLens' :: (Anon m ~ z, HasField name z a, FieldType name m ~ a) => FieldName name -> Lens z z a a
fieldLens' name = \f m -> fmap (updateField  name m)
                               (f $ getField name m)

fieldLens :: (Anon m ~ z, Anon m' ~ z', HasField name z a, HasField name z' b, Remap name m b ~ m', FieldType name m' ~ b, FieldType name m ~ a) => FieldName name -> Lens z z' a b
fieldLens name = \f m -> fmap ((belial (dom f) (codom f) updateField) name m)
                              (f $ getField name m) where
    codom :: (a -> f b) -> Proxy b
    codom _ = Proxy
    dom :: (a -> f b) -> Proxy a
    dom _ = Proxy

mkT1 :: Proxy (s :: Symbol) -> Proxy k -> Anon '[k :? s]
mkT1 _ _ = Anon (Vector.replicate 1 undefined)

--------------------------------------------------------------------------------------------
-- Instances
--------------------------------------------------------------------------------------------

class ForAllT c m
instance ForAllT c '[]
instance c x => ForAllT c ((x :? t) ': xs)

class ShowT xs (f :: *) where showT :: proxy xs -> f -> String
instance ShowT '[] f where showT _ _ = ""
instance (KnownSymbol b, Show a, ShowT x f, HasField b f a, FieldType b m ~ a, f ~ Anon m) => ShowT ((a :? b) ': x) f where
  showT p f = symbolVal (pr p) ++ ":" ++ show (getField (pr p) f `asProxyTypeOf` ph p) ++ showT (ptail p) f where
    pr :: proxy ((a :? b) ': x) -> FieldName b
    pr _ = FieldName
    ph :: proxy ((a :? b) ': x) -> Proxy a
    ph _ = Proxy

instance ShowT m (Anon m) => Show (Anon m) where
  show x = "{" ++ showT x x ++ "}"

ptfn :: proxy x -> FieldName (x::Symbol)
ptfn _ = FieldName

phead :: proxy (x ': xs) -> Proxy x
phead _ = Proxy

ptail :: proxy (x ': xs) -> Proxy xs
ptail _ = Proxy

pfst :: proxy (x::k) (y::l) -> Proxy x
pfst _ = Proxy

psnd :: proxy (x::k) (y::l) -> Proxy y
psnd _ = Proxy