src/Symantic/Syntaxes/Data.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 -- For Semantic
   3 {-# LANGUAGE DataKinds #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# LANGUAGE PatternSynonyms #-}
   6 {-# LANGUAGE RankNTypes #-}
   7 {-# LANGUAGE ViewPatterns #-}
   8
   9 module Symantic.Syntaxes.Data where
  10
  11 import Data.Bool (Bool)
  12 import Data.Either (Either)
  13 import Data.Eq qualified as Eq
  14 import Data.Function qualified as Fun
  15 import Data.Maybe (Maybe)
  16 import Data.Maybe qualified as Maybe
  17 import Data.Semigroup (Semigroup)
  18 import Type.Reflection (Typeable, eqTypeRep, typeRep, (:~~:) (..))
  19
  20 import Symantic.Syntaxes.Classes
  21 import Symantic.Syntaxes.Derive
  22
  23 -- * Type 'SomeData'
  24 data SomeData sem a
  25   = forall syn.
  26     ( Derivable (Data syn sem)
  27     , Typeable syn
  28     ) =>
  29     SomeData (Data syn sem a)
  30
  31 type instance Derived (SomeData sem) = sem
  32 instance Derivable (SomeData sem) where
  33   derive (SomeData x) = derive x
  34
  35 -- ** Type 'Data'
  36
  37 -- TODO: neither data families nor data instances
  38 -- can have phantom roles with GHC-9's RoleAnnotations,
  39 -- hence 'Data.Coerce.coerce' cannot be used on them for now.
  40 -- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
  41 -- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
  42 data family Data (syn :: Syntax) :: Semantic -> Semantic
  43 type instance Derived (Data syn sem) = sem
  44
  45 -- | Convenient utility to pattern-match a 'SomeData'.
  46 pattern Data :: Typeable syn => Data syn sem a -> SomeData sem a
  47 pattern Data x <- (unSomeData -> Maybe.Just x)
  48
  49 -- | @(unSomeData sd :: 'Maybe' ('Data' syn sem a))@
  50 -- extract the data-constructor from the given 'SomeData' @(sd)@
  51 -- iif. it belongs to the @('Data' syn sem a)@ data-instance.
  52 unSomeData ::
  53   forall syn sem a.
  54   Typeable syn =>
  55   SomeData sem a ->
  56   Maybe (Data syn sem a)
  57 unSomeData (SomeData (constr :: Data actualSyn sem a)) =
  58   case typeRep @syn `eqTypeRep` typeRep @actualSyn of
  59     Maybe.Just HRefl -> Maybe.Just constr
  60     Maybe.Nothing -> Maybe.Nothing
  61
  62 -- Abstractable
  63 data instance Data Abstractable sem a where
  64   Lam :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
  65 instance (Abstractable sem, Varable sem) => Derivable (Data Abstractable sem) where
  66   derive = \case
  67     Lam f -> lam (\x -> derive (f (SomeData (Var x))))
  68 instance (Abstractable sem, Varable sem) => Abstractable (SomeData sem) where
  69   lam f = SomeData (Lam f)
  70
  71 -- Abstractable1
  72 data instance Data Abstractable1 sem a where
  73   Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable1 sem (a -> b)
  74 instance (Abstractable1 sem, Varable sem) => Derivable (Data Abstractable1 sem) where
  75   derive = \case
  76     Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
  77 instance (Abstractable1 sem, Varable sem) => Abstractable1 (SomeData sem) where
  78   lam1 f = SomeData (Lam1 f)
  79
  80 -- Varable
  81 data instance Data Varable sem a where
  82   Var :: sem a -> Data Varable sem a
  83 instance Varable sem => Derivable (Data Varable sem) where
  84   derive = \case
  85     Var x -> var x
  86 instance Varable sem => Varable (SomeData sem) where
  87   var = Fun.id
  88
  89 -- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
  90 -- but to avoid duplication of work, only those manually marked
  91 -- as using their variable at most once.
  92 --
  93 -- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
  94 -- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
  95 normalOrderReduction ::
  96   forall sem a.
  97   Abstractable sem =>
  98   Abstractable1 sem =>
  99   Unabstractable sem =>
 100   Varable sem =>
 101   IfThenElseable sem =>
 102   SomeData sem a ->
 103   SomeData sem a
 104 normalOrderReduction = nor
 105   where
 106     nor :: SomeData sem b -> SomeData sem b
 107     nor = \case
 108       Data (Lam f) -> lam (nor Fun.. f)
 109       Data (Lam1 f) -> lam1 (nor Fun.. f)
 110       Data (x :@ y) -> case whnf x of
 111         Data (Lam1 f) -> nor (f y)
 112         x' -> nor x' .@ nor y
 113       Data (IfThenElse test ok ko) ->
 114         case nor test of
 115           Data (Constant b :: Data (Constantable Bool) sem Bool) ->
 116             if b then nor ok else nor ko
 117           t -> ifThenElse (nor t) (nor ok) (nor ko)
 118       x -> x
 119
 120     whnf :: SomeData sem b -> SomeData sem b
 121     whnf = \case
 122       Data (x :@ y) -> case whnf x of
 123         Data (Lam1 f) -> whnf (f y)
 124         x' -> x' .@ y
 125       x -> x
 126
 127 -- Unabstractable
 128 data instance Data Unabstractable sem a where
 129   (:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Unabstractable sem b
 130 instance Unabstractable sem => Derivable (Data Unabstractable sem) where
 131   derive = \case
 132     f :@ x -> derive f .@ derive x
 133 instance Unabstractable sem => Unabstractable (SomeData sem) where
 134   f .@ x = SomeData (f :@ x)
 135
 136 -- Functionable
 137 instance
 138   ( Abstractable sem
 139   , Unabstractable sem
 140   , Varable sem
 141   ) =>
 142   Functionable (SomeData sem)
 143   where
 144   ($) = lam (\f -> lam (\x -> f .@ x))
 145   (.) = lam (\f -> lam (\g -> lam (\x -> f .@ (g .@ x))))
 146   const = lam (\x -> lam (\_y -> x))
 147   flip = lam (\f -> lam (\x -> lam (\y -> f .@ y .@ x)))
 148   id = lam (\x -> x)
 149
 150 -- Anythingable
 151 data instance Data Anythingable sem a where
 152   Anything :: sem a -> Data Anythingable sem a
 153 instance
 154   ( Anythingable sem
 155   ) =>
 156   Derivable (Data Anythingable sem)
 157   where
 158   derive = \case
 159     Anything x -> anything x
 160 instance Anythingable (SomeData sem)
 161 instance Anythingable (Data Anythingable sem)
 162
 163 -- Bottomable
 164 data instance Data Bottomable sem a where
 165   Bottom :: Data Bottomable sem a
 166 instance Bottomable sem => Derivable (Data Bottomable sem) where
 167   derive Bottom{} = bottom
 168
 169 -- Constantable
 170 data instance Data (Constantable c) sem a where
 171   Constant {-Typeable c =>-} :: c -> Data (Constantable c) sem c
 172 instance Constantable c sem => Derivable (Data (Constantable c) sem) where
 173   derive = \case
 174     Constant x -> constant x
 175 instance
 176   ( Constantable c sem
 177   , Typeable c
 178   ) =>
 179   Constantable c (SomeData sem)
 180   where
 181   constant c = SomeData (Constant c)
 182 instance{-Typeable c =>-} Constantable c (Data (Constantable c) sem) where
 183   constant = Constant
 184
 185 -- Eitherable
 186 data instance Data Eitherable sem a where
 187   Either :: Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
 188   Left :: Data Eitherable sem (l -> Either l r)
 189   Right :: Data Eitherable sem (r -> Either l r)
 190 instance Eitherable sem => Derivable (Data Eitherable sem) where
 191   derive = \case
 192     Either -> either
 193     Left -> left
 194     Right -> right
 195 instance Eitherable sem => Eitherable (SomeData sem) where
 196   either = SomeData Either
 197   left = SomeData Left
 198   right = SomeData Right
 199 instance Eitherable (Data Eitherable sem) where
 200   either = Either
 201   left = Left
 202   right = Right
 203
 204 -- Equalable
 205 data instance Data Equalable sem a where
 206   Equal :: Eq.Eq a => Data Equalable sem (a -> a -> Bool)
 207 instance Equalable sem => Derivable (Data Equalable sem) where
 208   derive = \case
 209     Equal -> equal
 210 instance
 211   ( Equalable sem
 212   ) =>
 213   Equalable (SomeData sem)
 214   where
 215   equal = SomeData Equal
 216 instance Equalable (Data Equalable sem) where
 217   equal = Equal
 218
 219 -- Emptyable
 220 data instance Data Emptyable sem a where
 221   Empty :: Data Emptyable sem a
 222 instance Emptyable sem => Derivable (Data Emptyable sem) where
 223   derive = \case
 224     Empty -> empty
 225 instance
 226   ( Emptyable sem
 227   ) =>
 228   Emptyable (SomeData sem)
 229   where
 230   empty = SomeData Empty
 231 instance Emptyable (Data Emptyable sem) where
 232   empty = Empty
 233
 234 -- Semigroupable
 235 data instance Data Semigroupable sem a where
 236   Concat :: Semigroup a => Data Semigroupable sem (a -> a -> a)
 237 infixr 4 `Concat`
 238 instance Semigroupable sem => Derivable (Data Semigroupable sem) where
 239   derive = \case
 240     Concat -> concat
 241 instance
 242   ( Semigroupable sem
 243   ) =>
 244   Semigroupable (SomeData sem)
 245   where
 246   concat = SomeData Concat
 247 instance Semigroupable (Data Semigroupable sem) where
 248   concat = Concat
 249
 250 -- IfThenElseable
 251 data instance Data IfThenElseable sem a where
 252   IfThenElse ::
 253     SomeData sem Bool ->
 254     SomeData sem a ->
 255     SomeData sem a ->
 256     Data IfThenElseable sem a
 257 instance IfThenElseable sem => Derivable (Data IfThenElseable sem) where
 258   derive = \case
 259     IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
 260 instance
 261   ( IfThenElseable sem
 262   ) =>
 263   IfThenElseable (SomeData sem)
 264   where
 265   ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
 266 instance IfThenElseable sem => IfThenElseable (Data IfThenElseable sem) where
 267   ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
 268
 269 -- Listable
 270 data instance Data Listable sem a where
 271   Cons :: Data Listable sem (a -> [a] -> [a])
 272   Nil :: Data Listable sem [a]
 273 infixr 4 `Cons`
 274 instance Listable sem => Derivable (Data Listable sem) where
 275   derive = \case
 276     Cons -> cons
 277     Nil -> nil
 278 instance
 279   ( Listable sem
 280   ) =>
 281   Listable (SomeData sem)
 282   where
 283   cons = SomeData Cons
 284   nil = SomeData Nil
 285 instance Listable (Data Listable sem) where
 286   cons = Cons
 287   nil = Nil
 288
 289 -- Maybeable
 290 data instance Data Maybeable sem a where
 291   Nothing :: Data Maybeable sem (Maybe a)
 292   Just :: Data Maybeable sem (a -> Maybe a)
 293 instance Maybeable sem => Derivable (Data Maybeable sem) where
 294   derive = \case
 295     Nothing -> nothing
 296     Just -> just
 297 instance
 298   ( Maybeable sem
 299   ) =>
 300   Maybeable (SomeData sem)
 301   where
 302   nothing = SomeData Nothing
 303   just = SomeData Just
 304 instance Maybeable (Data Maybeable sem) where
 305   nothing = Nothing
 306   just = Just