src/Symantic/Dityped/ADT.hs

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