gtag.hs

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TypeOperators       #-}

{-

The package for generic programming, @generics-sop@, feels like a sledgehammer.

Sometimes you are so lazy, so you don't even write types do derive `Generic`
instance for, but directly work with generic representation, sums of products
`NS (NP I) xss`, or parts of it.

Nowadays the GHC support is reasonably good. You have to hold horses, but a lot
of stuff is possible!

-}

import           Data.Aeson
import           Data.Type.Equality
import           Generics.SOP
import qualified GHC.Generics       as GHC

data Tag a where
    TagBool :: Tag Bool
    TagInt  :: Tag Int

{-

If we try add `deriving (Eq, Show)` clause we get:

```
Gen.hs:22:13: error:
    • Can't make a derived instance of ‘Eq (Tag a)’:
        Constructor ‘TagBool’ has existentials or constraints in its type
        Constructor ‘TagInt’ has existentials or constraints in its type
        Possible fix: use a standalone deriving declaration instead
    • In the data declaration for ‘Tag’
```

That is easy to fix:
-}

deriving instance Eq (Tag a)
deriving instance Show (Tag a)

{-

```hs
deriving instance GHC.Generic (Tag a)
```

```
Gen.hs:43:1: error:
    • Can't make a derived instance of ‘GHC.Generic (Tag a)’:
        TagBool must be a vanilla data constructor, and
        TagInt must be a vanilla data constructor
```

-}

{-
However, say we want to write `aeson` instances for `Tag`. For simplicity
we'd like to encode `TagBool` as zero: `0`; and `TagInt` as one: `1`.
After all, `Tag` is just an enumeration.

Without too much explaining, let's just see the code!
-}



nsToInt :: NS f xs -> Int
nsToInt (Z _) = 0
nsToInt (S n) = 1 + nsToInt n

intToNS :: forall f xs. SListI xs => (forall a. f a) -> Int -> Maybe (NS f xs)
intToNS x 0 = case sList :: SList xs of
    SNil -> Nothing
    SCons -> Just (Z x)
intToNS x n = case sList :: SList xs of
    SNil -> Nothing
    SCons -> S <$> intToNS x (n - 1)

{-
λ *Main > nsToInt (S (S (Z Proxy)) :: NS Proxy '[Int, Bool, Char])
2
λ *Main > nsToInt (S (S (Z Proxy)) :: NS Proxy '[Int, Bool, Char, String, Maybe Integer])
2
λ *Main > intToNS Proxy 2 :: NS Proxy '[]

<interactive>:16:1: error:
    • Couldn't match expected type ‘NS Proxy '[]’
                  with actual type ‘Maybe (NS Proxy xs0)’
    • In the expression: intToNS Proxy 2 :: NS Proxy '[]
      In an equation for ‘it’: it = intToNS Proxy 2 :: NS Proxy '[]
λ *Main > intToNS Proxy 2 :: Just (NS Proxy '[])

<interactive>:17:20: error:
    • Expected a type, but ‘'Just (NS Proxy '[])’ has kind ‘Maybe *’
    • In an expression type signature: Just (NS Proxy '[])
      In the expression: intToNS Proxy 2 :: Just (NS Proxy '[])
      In an equation for ‘it’:
          it = intToNS Proxy 2 :: Just (NS Proxy '[])
λ *Main > intToNS Proxy 2 :: Maybe (NS Proxy '[])
Nothing
λ *Main > intToNS Proxy 2 :: Maybe (NS Proxy '[Int])
Nothing
λ *Main > intToNS Proxy 2 :: Maybe (NS Proxy '[Int, Bool])
Nothing
λ *Main > intToNS Proxy 2 :: Maybe (NS Proxy '[Int, Bool, Char])
Just (S (S (Z Proxy)))
λ *Main > intToNS Proxy 2 :: Maybe (NS Proxy '[Int, Bool, Char, String, Maybe Integer])
Just (S (S (Z Proxy)))
-}

type Is = (:~:)

{-
λ *Main > nsToInt (S (S (Z Refl)) :: NS (Is Char) '[Int, Bool, Char, String, Maybe Integer])
2
-}

data SomeRep xs where
    MkSomeRep :: NS (Is a) xs -> SomeRep xs

succSomeRep :: SomeRep xs -> SomeRep (x ': xs)
succSomeRep (MkSomeRep ns) = MkSomeRep (S ns)

intToSomeRep :: forall xs. SListI xs => Int -> Maybe (SomeRep xs)
intToSomeRep n = case sList :: SList xs of
    SNil  -> Nothing
    SCons -> case n of
        0 -> Just (MkSomeRep (Z Refl))
        _ -> succSomeRep <$> intToSomeRep (n - 1)

type TagCode = '[Bool, Int]
type TagRep a = NS (Is a) TagCode

fromTag :: Tag a -> TagRep a
fromTag TagBool = Z Refl
fromTag TagInt  = S (Z Refl)

toTag :: TagRep a -> Tag a
toTag (Z Refl)     = TagBool
toTag (S (Z Refl)) = TagInt
toTag (S (S x))    = case x of {} -- error "ghc, try harder!"

toSomeTag :: SomeRep TagCode -> SomeTag
toSomeTag (MkSomeRep r) = MkSomeTag (toTag r)

{-
λ *Main > toTag . fromTag  $ TagBool
TagBool
λ *Main > toTag . fromTag  $ TagInt
TagInt
-}

instance ToJSON (SomeRep xs) where
    toJSON (MkSomeRep ns) = toJSON (nsToInt ns)

instance SListI xs => FromJSON (SomeRep xs) where
    parseJSON v = do
        i <- parseJSON v
        maybe (fail "index out-of-bounds") pure (intToSomeRep i)


data SomeTag where
    MkSomeTag :: Tag a -> SomeTag

deriving instance Show SomeTag

instance ToJSON (Tag a) where
    toJSON = toJSON . MkSomeRep . fromTag

instance ToJSON SomeTag where
    toJSON (MkSomeTag t) = toJSON t

instance FromJSON SomeTag where
    parseJSON = fmap toSomeTag . parseJSON

{-
λ *Main > decode $ encode TagBool :: Maybe SomeTag
Just (MkSomeTag TagBool)
-}

-------------------------------------------------------------------------------
-- Existentials
-------------------------------------------------------------------------------

-- | phantom type request
newtype Req a = Req String
    deriving (Eq, Show, GHC.Generic)

instance ToJSON (Req a)
instance FromJSON (Req a)

data SomeReq where
  MkSomeReq :: Tag a -> Req a -> SomeReq

deriving instance Show SomeReq

instance ToJSON SomeReq where
    toJSON (MkSomeReq t r) = object
        [ "tag" .= t
        , "req" .= r
        ]

instance FromJSON SomeReq where
    parseJSON = withObject "SomeReq" $ \obj -> do
        MkSomeTag t <- obj .: "tag"
        r <- obj .: "req"
        pure (MkSomeReq t r)

{-
λ > decode $ encode $ MkSomeReq TagBool $ Req "example" :: Maybe SomeReq
Just (MkSomeReq TagBool (Req "example"))
-}