src/Symantic/Syntaxes/ADT.hs

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