src/Symantic/Syntaxes/Data.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-} -- For ReprKind
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE PatternSynonyms #-}
   5 {-# LANGUAGE RankNTypes #-}
   6 {-# LANGUAGE ViewPatterns #-}
   7 module Symantic.Data where
   8
   9 import Data.Bool (Bool)
  10 import Data.Either (Either)
  11 import Data.Kind (Constraint)
  12 import Data.Maybe (Maybe)
  13 import Data.Semigroup (Semigroup)
  14 import Type.Reflection (Typeable, (:~~:)(..), eqTypeRep, typeRep)
  15 import qualified Data.Eq as Eq
  16 import qualified Data.Function as Fun
  17 import qualified Data.Maybe as Maybe
  18
  19 import Symantic.Classes
  20 import Symantic.Derive
  21
  22 -- * Type 'SomeData'
  23 data SomeData sem a =
  24   forall able.
  25   ( Derivable (Data able sem)
  26   , Typeable able
  27   ) => SomeData (Data able sem a)
  28
  29 type instance Derived (SomeData sem) = sem
  30 instance Derivable (SomeData sem) where
  31   derive (SomeData x) = derive x
  32
  33 -- ** Type 'Data'
  34 -- TODO: neither data families nor data instances
  35 -- can have phantom roles with GHC-9's RoleAnnotations,
  36 -- hence 'Data.Coerce.coerce' cannot be used on them for now.
  37 -- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
  38 -- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
  39 data family Data
  40   (able :: ReprKind -> Constraint)
  41   :: ReprKind -> ReprKind
  42 type instance Derived (Data able sem) = sem
  43
  44 -- | Convenient utility to pattern-match a 'SomeData'.
  45 pattern Data :: Typeable able => Data able sem a -> SomeData sem a
  46 pattern Data x <- (unSomeData -> Maybe.Just x)
  47
  48 -- | @(unSomeData c :: 'Maybe' ('Data' able sem a))@
  49 -- extract the data-constructor from the given 'SomeData'
  50 -- iif. it belongs to the @('Data' able sem a)@ data-instance.
  51 unSomeData ::
  52   forall able sem a.
  53   Typeable able =>
  54   SomeData sem a -> Maybe (Data able sem a)
  55 unSomeData (SomeData (c::Data c sem a)) =
  56   case typeRep @able `eqTypeRep` typeRep @c of
  57     Maybe.Just HRefl -> Maybe.Just c
  58     Maybe.Nothing -> Maybe.Nothing
  59
  60 -- Abstractable
  61 data instance Data Abstractable sem a where
  62   (:@) :: SomeData sem (a->b) -> SomeData sem a -> Data Abstractable sem b
  63   Lam :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a->b)
  64   Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a->b)
  65   Var :: sem a -> Data Abstractable sem a
  66   -- FIXME: add constructors
  67 instance
  68   ( Abstractable sem
  69   ) => Derivable (Data Abstractable sem) where
  70   derive = \case
  71     f :@ x -> derive f .@ derive x
  72     Lam f -> lam (\x -> derive (f (SomeData (Var x))))
  73     Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
  74     Var x -> var x
  75 instance
  76   ( Abstractable sem
  77   ) => Abstractable (SomeData sem) where
  78   f .@ x = SomeData (f :@ x)
  79   lam f = SomeData (Lam f)
  80   lam1 f = SomeData (Lam1 f)
  81   var = Fun.id
  82
  83 -- Functionable
  84 instance
  85   ( Abstractable sem
  86   ) => Functionable (SomeData sem) where
  87   ($) = lam1 (\f -> lam1 (\x -> f .@ x))
  88   (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
  89   const = lam1 (\x -> lam1 (\_y -> x))
  90   flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
  91   id = lam1 (\x -> x)
  92
  93 -- Anythingable
  94 data instance Data Anythingable sem a where
  95   Anything :: sem a -> Data Anythingable sem a
  96 instance
  97   ( Anythingable sem
  98   ) => Derivable (Data Anythingable sem) where
  99   derive = \case
 100     Anything x -> anything x
 101 instance Anythingable (SomeData sem)
 102 instance Anythingable (Data Anythingable sem)
 103
 104 -- Bottomable
 105 data instance Data Bottomable sem a where
 106   Bottom :: Data Bottomable sem a
 107 instance Bottomable sem => Derivable (Data Bottomable sem) where
 108   derive Bottom{} = bottom
 109
 110 -- Constantable
 111 data instance Data (Constantable c) sem a where
 112   Constant :: {-Typeable c =>-} c -> Data (Constantable c) sem c
 113 instance Constantable c sem => Derivable (Data (Constantable c) sem) where
 114   derive = \case
 115     Constant x -> constant x
 116 instance
 117   ( Constantable c sem
 118   , Typeable c
 119   ) => Constantable c (SomeData sem) where
 120   constant c = SomeData (Constant c)
 121 instance {-Typeable c =>-} Constantable c (Data (Constantable c) sem) where
 122   constant = Constant
 123
 124 -- Eitherable
 125 data instance Data Eitherable sem a where
 126   Left :: Data Eitherable sem (l -> Either l r)
 127   Right :: Data Eitherable sem (r -> Either l r)
 128 instance Eitherable sem => Derivable (Data Eitherable sem) where
 129   derive = \case
 130     Left -> left
 131     Right -> right
 132 instance
 133   ( Eitherable sem
 134   ) => Eitherable (SomeData sem) where
 135   left = SomeData Left
 136   right = SomeData Right
 137 instance Eitherable (Data Eitherable sem) where
 138   left = Left
 139   right = Right
 140
 141 -- Equalable
 142 data instance Data Equalable sem a where
 143   Equal :: Eq.Eq a => Data Equalable sem (a -> a -> Bool)
 144 instance Equalable sem => Derivable (Data Equalable sem) where
 145   derive = \case
 146     Equal -> equal
 147 instance
 148   ( Equalable sem
 149   ) => Equalable (SomeData sem) where
 150   equal = SomeData Equal
 151 instance Equalable (Data Equalable sem) where
 152   equal = Equal
 153
 154 -- Emptyable
 155 data instance Data Emptyable sem a where
 156   Empty :: Data Emptyable sem a
 157 instance Emptyable sem => Derivable (Data Emptyable sem) where
 158   derive = \case
 159     Empty -> empty
 160 instance
 161   ( Emptyable sem
 162   ) => Emptyable (SomeData sem) where
 163   empty = SomeData Empty
 164 instance Emptyable (Data Emptyable sem) where
 165   empty = Empty
 166
 167 -- Semigroupable
 168 data instance Data Semigroupable sem a where
 169   Concat :: Semigroup a => Data Semigroupable sem (a -> a -> a)
 170 infixr 4 `Concat`
 171 instance Semigroupable sem => Derivable (Data Semigroupable sem) where
 172   derive = \case
 173     Concat -> concat
 174 instance
 175   ( Semigroupable sem
 176   ) => Semigroupable (SomeData sem) where
 177   concat = SomeData Concat
 178 instance Semigroupable (Data Semigroupable sem) where
 179   concat = Concat
 180
 181 -- IfThenElseable
 182 data instance Data IfThenElseable sem a where
 183   IfThenElse ::
 184     SomeData sem Bool ->
 185     SomeData sem a ->
 186     SomeData sem a ->
 187     Data IfThenElseable sem a
 188 instance IfThenElseable sem => Derivable (Data IfThenElseable sem) where
 189   derive = \case
 190     IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
 191 instance
 192   ( IfThenElseable sem
 193   ) => IfThenElseable (SomeData sem) where
 194   ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
 195 instance IfThenElseable sem => IfThenElseable (Data IfThenElseable sem) where
 196   ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
 197
 198 -- Listable
 199 data instance Data Listable sem a where
 200   Cons :: Data Listable sem (a -> [a] -> [a])
 201   Nil :: Data Listable sem [a]
 202 infixr 4 `Cons`
 203 instance Listable sem => Derivable (Data Listable sem) where
 204   derive = \case
 205     Cons -> cons
 206     Nil -> nil
 207 instance
 208   ( Listable sem
 209   ) => Listable (SomeData sem) where
 210   cons = SomeData Cons
 211   nil = SomeData Nil
 212 instance Listable (Data Listable sem) where
 213   cons = Cons
 214   nil = Nil
 215
 216 -- Maybeable
 217 data instance Data Maybeable sem a where
 218   Nothing :: Data Maybeable sem (Maybe a)
 219   Just :: Data Maybeable sem (a -> Maybe a)
 220 instance Maybeable sem => Derivable (Data Maybeable sem) where
 221   derive = \case
 222     Nothing -> nothing
 223     Just -> just
 224 instance
 225   ( Maybeable sem
 226   ) => Maybeable (SomeData sem) where
 227   nothing = SomeData Nothing
 228   just = SomeData Just
 229 instance Maybeable (Data Maybeable sem) where
 230   nothing = Nothing
 231   just = Just