src/Symantic/Syntaxes/ADT.hs

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