{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE UndecidableInstances #-} -- | EOT (Either of Tuples) to/from ADT (Algebraic Data Type). -- to produce or consume custom ADT with @('<:>')@ and @('<+>')@. -- -- This is like what is done in @generic-sop@: -- https://hackage.haskell.org/package/generics-sop-0.5.1.0/docs/src/Generics.SOP.GGP.html#gSumFrom -- but using directly 'Either' and 'Tuples' -- instead of passing by the intermediary GADTs @NP@ and @NS@. module Symantic.Syntaxes.ADT where import Data.Either (Either (..)) import Data.Function (const, id, ($), (.)) import Data.Kind (Type) import Data.Void (Void, absurd) import GHC.Generics as Generics -- * Type family 'EoT' -- Return an 'Either' of 'Tuples' from the given 'ADT', -- matching the nesting occuring when using @('<:>')@ and ('<+>')@ -- and their associativity and precedence, -- with no parenthesis messing around. type family EoT (adt :: [[Type]]) :: Type where -- This is 'absurd' EoT '[] = Void -- There Is No Alternative EoT '[ps] = Tuples ps -- The right associativity of @('<+>')@ -- puts leaves on 'Left' and nodes on 'Right' EoT (ps ': ss) = Either (Tuples ps) (EoT ss) -- * Type family 'Tuples' -- | Return the type of 'snd'-nested 2-tuples -- from the given list of types. type family Tuples (as :: [Type]) :: (r :: Type) where Tuples '[] = () Tuples '[a] = a Tuples (a ': rest) = (a, Tuples rest) -- * Type 'ADT' -- | Normalized type-level representation of an Algebraic Data Type. type ADT (adt :: Type) = ListOfRepSums (Rep adt) '[] -- ** Type family 'ListOfRepSums' -- | Collect the alternatives in a continuation passing-style. type family ListOfRepSums (a :: Type -> Type) (ss :: [[Type]]) :: [[Type]] type instance ListOfRepSums (a :+: b) ss = ListOfRepSums a (ListOfRepSums b ss) -- | Meta-information for datatypes type instance ListOfRepSums (M1 D _c a) ss = ListOfRepSums a ss -- | Meta-information for constructors type instance ListOfRepSums (M1 C _c a) ss = ListOfRepProducts a '[] ': ss -- | Empty datatypes type instance ListOfRepSums V1 ss = ss -- ** Type family 'ListOfRepProducts' -- | Collect the records in a continuation passing-style. type family ListOfRepProducts (a :: Type -> Type) (ps :: [Type]) :: [Type] type instance ListOfRepProducts (a :*: b) ps = ListOfRepProducts a (ListOfRepProducts b ps) -- | Meta-information for record selectors type instance ListOfRepProducts (M1 S _c a) ps = TypeOfRepField a ': ps -- | Constructor without fields type instance ListOfRepProducts U1 ps = ps -- ** Type family 'TypeOfRepField' type family TypeOfRepField (a :: Type -> Type) :: Type type instance TypeOfRepField (K1 _i a) = a -- * Class 'RepOfEoT' type RepOfEoT a = RepOfEithers (Rep a) '[] -- | Morph the 'Either' of 'Tuples' corresponding to an 'ADT' -- into a constructor of this 'ADT'. -- This is the reverse of 'eotOfadt'. adtOfeot :: Generic a => RepOfEoT a => EoT (ADT a) -> a adtOfeot eot = Generics.to $ repOfEithers @_ @'[] eot id absurd -- ** Class 'RepOfEithers' class RepOfEithers (a :: Type -> Type) ss where -- | Parse the 'Either' (list-like) binary tree of 'EoT' -- into the @(':+:')@ (balanced) binary tree of 'Rep', -- using continuation passing-style for performance. repOfEithers :: EoT (ListOfRepSums a ss) -> -- the 'a' 'Rep' is the current alternative in the 'EoT' (a x -> r) -> -- the 'a' 'Rep' is a following alternative in the 'EoT' (EoT ss -> r) -> r instance (RepOfEithers a (ListOfRepSums b ss), RepOfEithers b ss) => RepOfEithers (a :+: b) ss where repOfEithers eot ok ko = -- try to parse 'a' on the current 'eot' repOfEithers @a @(ListOfRepSums b ss) eot (ok . L1) ( \next -> -- parsing 'a' failed -- try to parse 'b' on the 'Right' of the current 'eot' repOfEithers @b @ss next (ok . R1) ko -- parsing 'b' failed: backtrack ) 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 -- 'EoT' is a leaf, and 'Rep' too: parsing succeeds Left ts -> ok $ M1 $ repOfTuples @a @'[] ts const -- 'EoT' is a node, but 'Rep' is a leaf: parsing fails 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' class RepOfTuples (a :: Type -> Type) (xs :: [Type]) where -- | Parse the 'Tuples' (list-like) binary tree of 'EoT' -- into the @(':*:')@ (balanced) binary tree of 'Rep', -- using continuation passing-style for performance. 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 = -- uncons 'a' repOfTuples @a @(ListOfRepProducts b ps) ts ( \a ts' -> -- uncons 'b' 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' class RepOfField (a :: Type -> Type) where repOfField :: TypeOfRepField a -> a x instance RepOfField (K1 i a) where repOfField = K1 -- * Class 'EoTOfRep' type EoTOfRep a = EithersOfRep (Rep a) '[] -- | Morph the constructor of an 'ADT' -- into the corresponding 'Either' of 'Tuples' of this 'ADT'. -- This is the reverse of 'adtOfeot'. eotOfadt :: Generic a => EoTOfRep a => a -> EoT (ADT a) eotOfadt = eithersOfRepL @_ @'[] . Generics.from -- ** Class 'EithersOfRep' class EithersOfRep (a :: Type -> Type) 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' class TuplesOfRep (a :: Type -> Type) (ps :: [Type]) 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' class FieldOfRep (a :: Type -> Type) where fieldOfRep :: a x -> TypeOfRepField a instance FieldOfRep (K1 i a) where fieldOfRep (K1 a) = a