src/Symantic/Syntaxes/EithersOfTuples.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE ConstraintKinds #-}
   3 {-# LANGUAGE DataKinds #-}
   4 {-# LANGUAGE EmptyCase #-}
   5 {-# LANGUAGE PolyKinds #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7
   8 -- | This modules leverages @GHC.Generics@ to generate reciprocal functions
   9 -- between algebraic data type (aka. ADT) constructors
  10 -- and Eithers-of-Tuples (aka. EOT).
  11 --
  12 -- This is like what is done in @generic-sop@:
  13 -- https://hackage.haskell.org/package/generics-sop-0.5.1.0/docs/src/Generics.SOP.GGP.html#gSumFrom
  14 -- but using directly 'Either' and 'Tuples'
  15 -- instead of passing by the intermediary GADTs @NP@ and @NS@,
  16 -- enabling to produce or consume custom ADT with @('<.>')@ and @('<+>')@.
  17 module Symantic.Syntaxes.EithersOfTuples where
  18
  19 import Data.Either (Either (..))
  20 import Data.Function (const, id, ($), (.))
  21 import Data.Kind (Type)
  22 import Data.Void (Void, absurd)
  23 import GHC.Generics as Generics
  24
  25 -- * Type family 'EoT'
  26
  27 -- Return an 'Either' of 'Tuples' from the given 'ADT',
  28 -- matching the nesting occuring when using @('<.>')@ and ('<+>')@
  29 -- and their associativity and precedence,
  30 -- with no parenthesis messing around.
  31 type family EoT (adt :: [[Type]]) :: Type where
  32   -- This is 'absurd'
  33   EoT '[] = Void
  34   -- There Is No Alternative
  35   EoT '[ps] = Tuples ps
  36   -- The right associativity of @('<+>')@
  37   -- puts leaves on 'Left' and nodes on 'Right'
  38   EoT (ps ': ss) = Either (Tuples ps) (EoT ss)
  39
  40 -- * Type family 'Tuples'
  41
  42 -- | Return the type of 'snd'-nested 2-tuples
  43 -- from the given list of types.
  44 type family Tuples (as :: [Type]) :: (r :: Type) where
  45   Tuples '[] = ()
  46   Tuples '[a] = a
  47   Tuples (a ': rest) = (a, Tuples rest)
  48
  49 -- * Type 'ADT'
  50
  51 -- | Normalized type-level representation of an Algebraic Data Type.
  52 type ADT (adt :: Type) = ListOfRepSums (Rep adt) '[]
  53
  54 -- ** Type family 'ListOfRepSums'
  55
  56 -- | Collect the alternatives in a continuation passing-style.
  57 type family ListOfRepSums (a :: Type -> Type) (ss :: [[Type]]) :: [[Type]]
  58
  59 type instance ListOfRepSums (a :+: b) ss = ListOfRepSums a (ListOfRepSums b ss)
  60
  61 -- | Meta-information for datatypes
  62 type instance ListOfRepSums (M1 D _c a) ss = ListOfRepSums a ss
  63
  64 -- | Meta-information for constructors
  65 type instance ListOfRepSums (M1 C _c a) ss = ListOfRepProducts a '[] ': ss
  66
  67 -- | Empty datatypes
  68 type instance ListOfRepSums V1 ss = ss
  69
  70 -- ** Type family 'ListOfRepProducts'
  71
  72 -- | Collect the records in a continuation passing-style.
  73 type family ListOfRepProducts (a :: Type -> Type) (ps :: [Type]) :: [Type]
  74
  75 type instance ListOfRepProducts (a :*: b) ps = ListOfRepProducts a (ListOfRepProducts b ps)
  76
  77 -- | Meta-information for record selectors
  78 type instance ListOfRepProducts (M1 S _c a) ps = TypeOfRepField a ': ps
  79
  80 -- | Constructor without fields
  81 type instance ListOfRepProducts U1 ps = ps
  82
  83 -- ** Type family 'TypeOfRepField'
  84 type family TypeOfRepField (a :: Type -> Type) :: Type
  85 type instance TypeOfRepField (K1 _i a) = a
  86
  87 -- * Class 'RepOfEoT'
  88 type RepOfEoT a = RepOfEithers (Rep a) '[]
  89
  90 -- | Morph the 'Either' of 'Tuples' corresponding to an 'ADT'
  91 -- into a constructor of this 'ADT'.
  92 -- This is the reverse of 'eotOfadt'.
  93 adtOfeot :: Generic a => RepOfEoT a => EoT (ADT a) -> a
  94 adtOfeot eot = Generics.to $ repOfEithers @_ @'[] eot id absurd
  95
  96 -- ** Class 'RepOfEithers'
  97 class RepOfEithers (a :: Type -> Type) ss where
  98   -- | Parse the 'Either' (list-like) binary tree of 'EoT'
  99   -- into the @(':+:')@ (balanced) binary tree of 'Rep',
 100   -- using continuation passing-style for performance.
 101   repOfEithers ::
 102     EoT (ListOfRepSums a ss) ->
 103     -- the 'a' 'Rep' is the current alternative in the 'EoT'
 104     (a x -> r) ->
 105     -- the 'a' 'Rep' is a following alternative in the 'EoT'
 106     (EoT ss -> r) ->
 107     r
 108 instance (RepOfEithers a (ListOfRepSums b ss), RepOfEithers b ss) => RepOfEithers (a :+: b) ss where
 109   repOfEithers eot ok ko =
 110     -- try to parse 'a' on the current 'eot'
 111     repOfEithers @a @(ListOfRepSums b ss)
 112       eot
 113       (ok . L1)
 114       ( \next ->
 115           -- parsing 'a' failed
 116           -- try to parse 'b' on the 'Right' of the current 'eot'
 117           repOfEithers @b @ss
 118             next
 119             (ok . R1)
 120             ko -- parsing 'b' failed: backtrack
 121       )
 122 instance RepOfEithers a ss => RepOfEithers (M1 D c a) ss where
 123   repOfEithers eot ok = repOfEithers @a @ss eot (ok . M1)
 124 instance RepOfTuples a '[] => RepOfEithers (M1 C c a) (ps ': ss) where
 125   repOfEithers eot ok ko =
 126     case eot of
 127       -- 'EoT' is a leaf, and 'Rep' too: parsing succeeds
 128       Left ts -> ok $ M1 $ repOfTuples @a @'[] ts const
 129       -- 'EoT' is a node, but 'Rep' is a leaf: parsing fails
 130       Right ss -> ko ss
 131 instance RepOfTuples a '[] => RepOfEithers (M1 C c a) '[] where
 132   repOfEithers eot ok _ko = ok $ M1 $ repOfTuples @_ @'[] eot const
 133 instance RepOfEithers V1 ss where
 134   repOfEithers eot _ok ko = ko eot
 135
 136 -- ** Class 'RepOfTuples'
 137 class RepOfTuples (a :: Type -> Type) (xs :: [Type]) where
 138   -- | Parse the 'Tuples' (list-like) binary tree of 'EoT'
 139   -- into the @(':*:')@ (balanced) binary tree of 'Rep',
 140   -- using continuation passing-style for performance.
 141   repOfTuples ::
 142     Tuples (ListOfRepProducts a xs) ->
 143     (a x -> Tuples xs -> r) ->
 144     r
 145 instance (RepOfTuples a (ListOfRepProducts b ps), RepOfTuples b ps) => RepOfTuples (a :*: b) ps where
 146   repOfTuples ts k =
 147     -- uncons 'a'
 148     repOfTuples @a @(ListOfRepProducts b ps)
 149       ts
 150       ( \a ts' ->
 151           -- uncons 'b'
 152           repOfTuples @b @ps
 153             ts'
 154             (\b -> k (a :*: b))
 155       )
 156 instance RepOfField a => RepOfTuples (M1 S c a) (p ': ps) where
 157   repOfTuples (a, ts) k = k (M1 (repOfField a)) ts
 158 instance RepOfField a => RepOfTuples (M1 S c a) '[] where
 159   repOfTuples a k = k (M1 (repOfField a)) ()
 160 instance RepOfTuples U1 ps where
 161   repOfTuples ts k = k U1 ts
 162
 163 -- ** Class 'RepOfField'
 164 class RepOfField (a :: Type -> Type) where
 165   repOfField :: TypeOfRepField a -> a x
 166 instance RepOfField (K1 i a) where
 167   repOfField = K1
 168
 169 -- * Class 'EoTOfRep'
 170 type EoTOfRep a = EithersOfRep (Rep a) '[]
 171
 172 -- | Morph the constructor of an 'ADT'
 173 -- into the corresponding 'Either' of 'Tuples' of this 'ADT'.
 174 -- This is the reverse of 'adtOfeot'.
 175 eotOfadt :: Generic a => EoTOfRep a => a -> EoT (ADT a)
 176 eotOfadt = eithersOfRepL @_ @'[] . Generics.from
 177
 178 -- ** Class 'EithersOfRep'
 179 class EithersOfRep (a :: Type -> Type) ss where
 180   eithersOfRepL :: a x -> EoT (ListOfRepSums a ss)
 181   eithersOfRepR :: EoT ss -> EoT (ListOfRepSums a ss)
 182 instance
 183   (EithersOfRep a (ListOfRepSums b ss), EithersOfRep b ss) =>
 184   EithersOfRep (a :+: b) ss
 185   where
 186   eithersOfRepL = \case
 187     L1 a -> eithersOfRepL @a @(ListOfRepSums b ss) a
 188     R1 b -> eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepL @b @ss b)
 189   eithersOfRepR ss = eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepR @b @ss ss)
 190 instance EithersOfRep a ss => EithersOfRep (M1 D c a) ss where
 191   eithersOfRepL (M1 a) = eithersOfRepL @a @ss a
 192   eithersOfRepR = eithersOfRepR @a @ss
 193 instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) '[] where
 194   eithersOfRepL (M1 a) = tuplesOfRep @_ @'[] a ()
 195   eithersOfRepR = absurd
 196 instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) (ps ': ss) where
 197   eithersOfRepL (M1 a) = Left $ tuplesOfRep @_ @'[] a ()
 198   eithersOfRepR = Right
 199 instance EithersOfRep V1 ss where
 200   eithersOfRepL = \case {}
 201   eithersOfRepR = id
 202
 203 -- ** Class 'TuplesOfRep'
 204 class TuplesOfRep (a :: Type -> Type) (ps :: [Type]) where
 205   tuplesOfRep :: a x -> Tuples ps -> Tuples (ListOfRepProducts a ps)
 206 instance (TuplesOfRep a (ListOfRepProducts b ps), TuplesOfRep b ps) => TuplesOfRep (a :*: b) ps where
 207   tuplesOfRep (a :*: b) ps =
 208     tuplesOfRep @a @(ListOfRepProducts b ps)
 209       a
 210       (tuplesOfRep @b @ps b ps)
 211 instance TuplesOfRep U1 ps where
 212   tuplesOfRep U1 xs = xs
 213 instance FieldOfRep a => TuplesOfRep (M1 S c a) (x ': ps) where
 214   tuplesOfRep (M1 a) xs = (fieldOfRep a, xs)
 215 instance FieldOfRep a => TuplesOfRep (M1 S c a) '[] where
 216   tuplesOfRep (M1 a) _xs = fieldOfRep a
 217
 218 -- ** Class 'FieldOfRep'
 219 class FieldOfRep (a :: Type -> Type) where
 220   fieldOfRep :: a x -> TypeOfRepField a
 221 instance FieldOfRep (K1 i a) where
 222   fieldOfRep (K1 a) = a