Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Last active August 15, 2023 23:04
  • Star 2 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save Lysxia/3f6781b3a307a7e0c564920d6277bee2 to your computer and use it in GitHub Desktop.
{-# LANGUAGE
DataKinds,
DeriveGeneric,
PolyKinds,
StandaloneDeriving,
TypeFamilies,
UndecidableInstances #-}
module T where
import Data.Kind (Constraint, Type)
import Data.Void
import GHC.Generics
import GHC.TypeLits
data KeyValueX x =
KVX (X "KVX" x) String (DataX x) |
KeyValueX (X "KeyValueX" x)
deriving Generic
data DataX x =
NullX (X "NullX" x) |
IntX (X "IntX" x) Int |
NumX (X "NumX" x) Double |
BoolX (X "BoolX" x) Bool |
StringX (X "StringX" x) String |
ArrayX (X "ArrayX" x) [DataX x] |
ObjectX (X "ObjectX" x) [KeyValueX x] |
DataX (X "DataX" x)
deriving Generic
--
type family X (s :: k) (x :: l) :: Type
--
type ForAllX c x = (AllX c (CNames (DataX x)) x, AllX c (CNames (KeyValueX x)) x)
deriving instance ForAllX Eq x => Eq (DataX x)
deriving instance ForAllX Eq x => Eq (KeyValueX x)
--
data UD
type X s UD = XUD s
type family XUD (s :: Symbol) :: Type where
XUD "KeyValueX" = Void
XUD "DataX" = Void
XUD _ = ()
--
type CNames a = GCNames (Rep a)
type family GCNames (f :: Type -> Type) :: [Symbol] where
GCNames (M1 D c f) = GCNames f
GCNames (f :+: g) = GCNames f ++ GCNames g
GCNames (M1 C (MetaCons name _ _) f) = '[name]
type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)
type family AllX (c :: Type -> Constraint) (xs :: [Symbol]) (x :: l) :: Constraint where
AllX c '[] x = ()
AllX c (s ': ss) x = (c (X s x), AllX c ss x)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment