{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module Symantic.Base.ADT where
import Data.Either (Either(..))
import Data.Void (Void, absurd)
import Data.Function (($), (.), id, const)
import GHC.Generics as Generics
type family EoT (adt :: [[*]]) :: * where
EoT '[] = Void
EoT '[ ps ] = Tuples ps
EoT (ps ': ss) = Either (Tuples ps) (EoT ss)
type family Tuples (as :: [*]) :: (r :: *) where
Tuples '[] = ()
Tuples '[a] = a
Tuples (a ': rest) = (a, Tuples rest)
type ADT (adt :: *) = ListOfRepSums (Rep adt) '[]
type family ListOfRepSums (a :: * -> *) (ss :: [[*]]) :: [[*]]
type instance ListOfRepSums (a:+:b) ss = ListOfRepSums a (ListOfRepSums b ss)
type instance ListOfRepSums (M1 D _c a) ss = ListOfRepSums a ss
type instance ListOfRepSums (M1 C _c a) ss = ListOfRepProducts a '[] ': ss
type instance ListOfRepSums V1 ss = ss
type family ListOfRepProducts (a :: * -> *) (ps :: [*]) :: [*]
type instance ListOfRepProducts (a:*:b) ps = ListOfRepProducts a (ListOfRepProducts b ps)
type instance ListOfRepProducts (M1 S _c a) ps = TypeOfRepField a ': ps
type instance ListOfRepProducts U1 ps = ps
type family TypeOfRepField (a :: * -> *) :: *
type instance TypeOfRepField (K1 _i a) = a
type RepOfEoT a = RepOfEithers (Rep a) '[]
adtOfeot :: Generic a => RepOfEoT a => EoT (ADT a) -> a
adtOfeot eot = Generics.to $ repOfEithers @_ @'[] eot id absurd
class RepOfEithers (a :: * -> *) ss where
repOfEithers ::
EoT (ListOfRepSums a ss) ->
(a x -> r) ->
(EoT ss -> r) ->
r
instance (RepOfEithers a (ListOfRepSums b ss), RepOfEithers b ss) => RepOfEithers (a:+:b) ss where
repOfEithers eot ok ko =
repOfEithers @a @(ListOfRepSums b ss) eot
(ok . L1)
(\next ->
repOfEithers @b @ss next
(ok . R1)
ko
)
instance RepOfEithers a ss => RepOfEithers (M1 D c a) ss where
repOfEithers eot ok = repOfEithers @a @ss eot (ok . M1)
instance RepOfTuples a '[] => RepOfEithers (M1 C c a) (ps ': ss) where
repOfEithers eot ok ko =
case eot of
Left ts -> ok $ M1 $ repOfTuples @a @'[] ts const
Right ss -> ko ss
instance RepOfTuples a '[] => RepOfEithers (M1 C c a) '[] where
repOfEithers eot ok _ko = ok $ M1 $ repOfTuples @_ @'[] eot const
instance RepOfEithers V1 ss where
repOfEithers eot _ok ko = ko eot
class RepOfTuples (a :: * -> *) (xs::[*]) where
repOfTuples ::
Tuples (ListOfRepProducts a xs) ->
(a x -> Tuples xs -> r) -> r
instance (RepOfTuples a (ListOfRepProducts b ps), RepOfTuples b ps) => RepOfTuples (a:*:b) ps where
repOfTuples ts k =
repOfTuples @a @(ListOfRepProducts b ps) ts
(\a ts' ->
repOfTuples @b @ps ts'
(\b -> k (a:*:b)))
instance RepOfField a => RepOfTuples (M1 S c a) (p ': ps) where
repOfTuples (a, ts) k = k (M1 (repOfField a)) ts
instance RepOfField a => RepOfTuples (M1 S c a) '[] where
repOfTuples a k = k (M1 (repOfField a)) ()
instance RepOfTuples U1 ps where
repOfTuples ts k = k U1 ts
class RepOfField (a :: * -> *) where
repOfField :: TypeOfRepField a -> a x
instance RepOfField (K1 i a) where
repOfField = K1
type EoTOfRep a = EithersOfRep (Rep a) '[]
eotOfadt :: Generic a => EoTOfRep a => a -> EoT (ADT a)
eotOfadt = eithersOfRepL @_ @'[] . Generics.from
class EithersOfRep (a :: * -> *) ss where
eithersOfRepL :: a x -> EoT (ListOfRepSums a ss)
eithersOfRepR :: EoT ss -> EoT (ListOfRepSums a ss)
instance (EithersOfRep a (ListOfRepSums b ss), EithersOfRep b ss) =>
EithersOfRep (a:+:b) ss where
eithersOfRepL = \case
L1 a -> eithersOfRepL @a @(ListOfRepSums b ss) a
R1 b -> eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepL @b @ss b)
eithersOfRepR ss = eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepR @b @ss ss)
instance EithersOfRep a ss => EithersOfRep (M1 D c a) ss where
eithersOfRepL (M1 a) = eithersOfRepL @a @ss a
eithersOfRepR = eithersOfRepR @a @ss
instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) '[] where
eithersOfRepL (M1 a) = tuplesOfRep @_ @'[] a ()
eithersOfRepR = absurd
instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) (ps ': ss) where
eithersOfRepL (M1 a) = Left $ tuplesOfRep @_ @'[] a ()
eithersOfRepR = Right
instance EithersOfRep V1 ss where
eithersOfRepL = \case {}
eithersOfRepR = id
class TuplesOfRep (a :: * -> *) (ps::[*]) where
tuplesOfRep :: a x -> Tuples ps -> Tuples (ListOfRepProducts a ps)
instance (TuplesOfRep a (ListOfRepProducts b ps), TuplesOfRep b ps) => TuplesOfRep (a:*:b) ps where
tuplesOfRep (a:*:b) ps =
tuplesOfRep @a @(ListOfRepProducts b ps) a
(tuplesOfRep @b @ps b ps)
instance TuplesOfRep U1 ps where
tuplesOfRep U1 xs = xs
instance FieldOfRep a => TuplesOfRep (M1 S c a) (x ': ps) where
tuplesOfRep (M1 a) xs = (fieldOfRep a, xs)
instance FieldOfRep a => TuplesOfRep (M1 S c a) '[] where
tuplesOfRep (M1 a) _xs = fieldOfRep a
class FieldOfRep (a :: * -> *) where
fieldOfRep :: a x -> TypeOfRepField a
instance FieldOfRep (K1 i a) where
fieldOfRep (K1 a) = a