GadtReadVariadic.hs

{-# LANGUAGE
    -- Unsurprisingly, we're going to talk about GADTs.
    GADTs,

    -- Type-level functions, data types, and polymorphism
    TypeFamilies,
    DataKinds,
    PolyKinds,

    -- Explicit type applications
    TypeApplications,
    AllowAmbiguousTypes,
    ScopedTypeVariables,

    -- Type-class programming, the bridge between types and values
    MultiParamTypeClasses,
    FlexibleContexts,
    FlexibleInstances,
    UndecidableInstances,
    QuantifiedConstraints,

    -- For higher-order functors
    RankNTypes,

    -- Applysith this extension,
    -- GHC can derive some standard instances for GADTs. Here for Show.
    StandaloneDeriving,

    -- For deriving GenericK
    TemplateHaskell,

    -- This should really be in the standard.
    TypeOperators
    #-}

module GenericParseGADTs where

import Generics.Kind         -- kind-generics
import Generics.Kind.TH      -- kind-generics-th (derive GenericK)
import Data.PolyKinded.Atom  -- kind-apply (core definitions for kind-generics)

-- base
import Data.Kind (Type, Constraint)
import Data.Type.Bool (type (&&))
import Data.Type.Equality (type (==), type (~~))
import Text.Read (readMaybe)

-- A newtype wrapper for the @(:@@:)@ family.
newtype Applys f a = Applys (f :@@: a)
deriving instance Show (f :@@: a) => Show (Applys f a)

data Ex (f :: k -> Type) where
  Ex :: f a -> Ex f

xmap :: forall f g. (forall a. f a -> g a) -> Ex f -> Ex g
xmap f (Ex x) = Ex (f x)

deriving instance (forall a. Show (f a)) => Show (Ex f)

kexToEx :: forall f. GenericK f => Ex (RepK f) -> Ex (Applys f)
kexToEx = xmap (Applys @f . toK @_ @f)

class GFromStringEx (f :: LoT k -> Type) where
  gfromStringex :: String -> Maybe (Ex f)

instance GFromStringEx f => GFromStringEx (M1 i c f) where
  gfromStringex = fmap (xmap M1) . gfromStringex

instance (GFromStringEx f, GFromStringEx g) => GFromStringEx (f :+: g) where
  gfromStringex ('0' : s) = fmap (xmap L1) (gfromStringex s)
  gfromStringex ('1' : s) = fmap (xmap R1) (gfromStringex s)
  gfromStringex _ = Nothing

instance
  ( p ~ SpineLoT p
  , Interpret c p
  , GFromString f p
  ) => GFromStringEx (c :=>: f) where
  gfromStringex s = fmap (Ex . SuchThat) (gfromString @f @p s)

instance GFromStringEx U1 where
  gfromStringex _ = Just (Ex U1)

class GFromString f p where
  gfromString :: String -> Maybe (f p)

instance GFromString U1 p where
  gfromString _ = Just U1

genericFromStringEx ::
  forall f.
  (GenericK f, GFromStringEx (RepK f)) =>
  String -> Maybe (Ex (Applys f))
genericFromStringEx = fmap kexToEx . gfromStringex @_ @(RepK f)

data Foo1 (a :: Type) where
  Bar1 :: Foo1 Int
  Baz1 :: Foo1 Bool
  Bag1 :: Foo1 a

deriving instance Show (Foo1 a)
deriveGenericK ''Foo1

data Foo2 (b :: Type) (a :: Type) where
  Bar2 :: Foo2 Int Int
  Baz2 :: Foo2 Bool Bool
  Bag2 :: Foo2 b a

deriving instance Show (Foo2 b a)
deriveGenericK ''Foo2

fromStringFoo1 :: String -> Maybe (Ex (Applys Foo1))
fromStringFoo1 = genericFromStringEx

fromStringFoo2 :: String -> Maybe (Ex (Applys Foo2))
fromStringFoo2 = genericFromStringEx

example :: [Bool]
example =
  [ show (fromStringFoo1 "0" )  == "Just (Ex (Applys Bar1))"
  , show (fromStringFoo1 "10")  == "Just (Ex (Applys Baz1))"
  , show (fromStringFoo1 "11")  == "Just (Ex (Applys Bag1))"
  , show (fromStringFoo2 "0" )  == "Just (Ex (Applys Bar2))"
  ]