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 repr a =
  24   forall able.
  25   ( Derivable (Data able repr)
  26   , Typeable able
  27   ) => SomeData (Data able repr a)
  28
  29 type instance Derived (SomeData repr) = repr
  30 instance Derivable (SomeData repr) 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 repr) = repr
  43
  44 -- | Convenient utility to pattern-match a 'SomeData'.
  45 pattern Data :: Typeable able => Data able repr a -> SomeData repr a
  46 pattern Data x <- (unSomeData -> Maybe.Just x)
  47
  48 -- | @(unSomeData c :: 'Maybe' ('Data' able repr a))@
  49 -- extract the data-constructor from the given 'SomeData'
  50 -- iif. it belongs to the @('Data' able repr a)@ data-instance.
  51 unSomeData ::
  52   forall able repr a.
  53   Typeable able =>
  54   SomeData repr a -> Maybe (Data able repr a)
  55 unSomeData (SomeData (c::Data c repr 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 repr a where
  62   (:@) :: SomeData repr (a->b) -> SomeData repr a -> Data Abstractable repr b
  63   Lam :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
  64   Lam1 :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
  65   Var :: repr a -> Data Abstractable repr a
  66   -- FIXME: add constructors
  67 instance
  68   ( Abstractable repr
  69   ) => Derivable (Data Abstractable repr) 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 repr
  77   ) => Abstractable (SomeData repr) 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 repr
  86   ) => Functionable (SomeData repr) 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 repr a where
  95   Anything :: repr a -> Data Anythingable repr a
  96 instance
  97   ( Anythingable repr
  98   ) => Derivable (Data Anythingable repr) where
  99   derive = \case
 100     Anything x -> anything x
 101 instance Anythingable (SomeData repr)
 102 instance Anythingable (Data Anythingable repr)
 103
 104 -- Bottomable
 105 data instance Data Bottomable repr a where
 106   Bottom :: Data Bottomable repr a
 107 instance Bottomable repr => Derivable (Data Bottomable repr) where
 108   derive Bottom{} = bottom
 109
 110 -- Constantable
 111 data instance Data (Constantable c) repr a where
 112   Constant :: {-Typeable c =>-} c -> Data (Constantable c) repr c
 113 instance Constantable c repr => Derivable (Data (Constantable c) repr) where
 114   derive = \case
 115     Constant x -> constant x
 116 instance
 117   ( Constantable c repr
 118   , Typeable c
 119   ) => Constantable c (SomeData repr) where
 120   constant c = SomeData (Constant c)
 121 instance {-Typeable c =>-} Constantable c (Data (Constantable c) repr) where
 122   constant = Constant
 123
 124 -- Eitherable
 125 data instance Data Eitherable repr a where
 126   Left :: Data Eitherable repr (l -> Either l r)
 127   Right :: Data Eitherable repr (r -> Either l r)
 128 instance Eitherable repr => Derivable (Data Eitherable repr) where
 129   derive = \case
 130     Left -> left
 131     Right -> right
 132 instance
 133   ( Eitherable repr
 134   ) => Eitherable (SomeData repr) where
 135   left = SomeData Left
 136   right = SomeData Right
 137 instance Eitherable (Data Eitherable repr) where
 138   left = Left
 139   right = Right
 140
 141 -- Equalable
 142 data instance Data Equalable repr a where
 143   Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
 144 instance Equalable repr => Derivable (Data Equalable repr) where
 145   derive = \case
 146     Equal -> equal
 147 instance
 148   ( Equalable repr
 149   ) => Equalable (SomeData repr) where
 150   equal = SomeData Equal
 151 instance Equalable (Data Equalable repr) where
 152   equal = Equal
 153
 154 -- Emptyable
 155 data instance Data Emptyable repr a where
 156   Empty :: Data Emptyable repr a
 157 instance Emptyable repr => Derivable (Data Emptyable repr) where
 158   derive = \case
 159     Empty -> empty
 160 instance
 161   ( Emptyable repr
 162   ) => Emptyable (SomeData repr) where
 163   empty = SomeData Empty
 164 instance Emptyable (Data Emptyable repr) where
 165   empty = Empty
 166
 167 -- Semigroupable
 168 data instance Data Semigroupable repr a where
 169   Concat :: Semigroup a => Data Semigroupable repr (a -> a -> a)
 170 infixr 4 `Concat`
 171 instance Semigroupable repr => Derivable (Data Semigroupable repr) where
 172   derive = \case
 173     Concat -> concat
 174 instance
 175   ( Semigroupable repr
 176   ) => Semigroupable (SomeData repr) where
 177   concat = SomeData Concat
 178 instance Semigroupable (Data Semigroupable repr) where
 179   concat = Concat
 180
 181 -- IfThenElseable
 182 data instance Data IfThenElseable repr a where
 183   IfThenElse ::
 184     SomeData repr Bool ->
 185     SomeData repr a ->
 186     SomeData repr a ->
 187     Data IfThenElseable repr a
 188 instance IfThenElseable repr => Derivable (Data IfThenElseable repr) where
 189   derive = \case
 190     IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
 191 instance
 192   ( IfThenElseable repr
 193   ) => IfThenElseable (SomeData repr) where
 194   ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
 195 instance IfThenElseable repr => IfThenElseable (Data IfThenElseable repr) where
 196   ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
 197
 198 -- Listable
 199 data instance Data Listable repr a where
 200   Cons :: Data Listable repr (a -> [a] -> [a])
 201   Nil :: Data Listable repr [a]
 202 infixr 4 `Cons`
 203 instance Listable repr => Derivable (Data Listable repr) where
 204   derive = \case
 205     Cons -> cons
 206     Nil -> nil
 207 instance
 208   ( Listable repr
 209   ) => Listable (SomeData repr) where
 210   cons = SomeData Cons
 211   nil = SomeData Nil
 212 instance Listable (Data Listable repr) where
 213   cons = Cons
 214   nil = Nil
 215
 216 -- Maybeable
 217 data instance Data Maybeable repr a where
 218   Nothing :: Data Maybeable repr (Maybe a)
 219   Just :: Data Maybeable repr (a -> Maybe a)
 220 instance Maybeable repr => Derivable (Data Maybeable repr) where
 221   derive = \case
 222     Nothing -> nothing
 223     Just -> just
 224 instance
 225   ( Maybeable repr
 226   ) => Maybeable (SomeData repr) where
 227   nothing = SomeData Nothing
 228   just = SomeData Just
 229 instance Maybeable (Data Maybeable repr) where
 230   nothing = Nothing
 231   just = Just