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 able.
  26     ( Derivable (Data able sem)
  27     , Typeable able
  28     ) =>
  29     SomeData (Data able 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 (able :: Syntax) :: Semantic -> Semantic
  43 type instance Derived (Data able sem) = sem
  44
  45 -- | Convenient utility to pattern-match a 'SomeData'.
  46 pattern Data :: Typeable able => Data able sem a -> SomeData sem a
  47 pattern Data x <- (unSomeData -> Maybe.Just x)
  48
  49 -- | @(unSomeData c :: 'Maybe' ('Data' able sem a))@
  50 -- extract the data-constructor from the given 'SomeData'
  51 -- iif. it belongs to the @('Data' able sem a)@ data-instance.
  52 unSomeData ::
  53   forall able sem a.
  54   Typeable able =>
  55   SomeData sem a ->
  56   Maybe (Data able sem a)
  57 unSomeData (SomeData (c :: Data c sem a)) =
  58   case typeRep @able `eqTypeRep` typeRep @c of
  59     Maybe.Just HRefl -> Maybe.Just c
  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   Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
  66   Var :: sem a -> Data Abstractable sem a
  67 instance Abstractable sem => Derivable (Data Abstractable sem) where
  68   derive = \case
  69     Lam f -> lam (\x -> derive (f (SomeData (Var x))))
  70     Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
  71     Var x -> var x
  72 instance Abstractable sem => Abstractable (SomeData sem) where
  73   lam f = SomeData (Lam f)
  74   lam1 f = SomeData (Lam1 f)
  75   var = Fun.id
  76
  77 -- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
  78 -- but to avoid duplication of work, only those manually marked
  79 -- as using their variable at most once.
  80 --
  81 -- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
  82 -- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
  83 normalOrderReduction ::
  84   forall sem a.
  85   Abstractable sem =>
  86   IfThenElseable sem =>
  87   SomeData sem a ->
  88   SomeData sem a
  89 normalOrderReduction = nor
  90   where
  91     nor :: SomeData sem b -> SomeData sem b
  92     nor = \case
  93       Data (Lam f) -> lam (nor Fun.. f)
  94       Data (Lam1 f) -> lam1 (nor Fun.. f)
  95       Data (x :@ y) -> case whnf x of
  96         Data (Lam1 f) -> nor (f y)
  97         x' -> nor x' .@ nor y
  98       Data (IfThenElse test ok ko) ->
  99         case nor test of
 100           Data (Constant b :: Data (Constantable Bool) sem Bool) ->
 101             if b then nor ok else nor ko
 102           t -> ifThenElse (nor t) (nor ok) (nor ko)
 103       x -> x
 104
 105     whnf :: SomeData sem b -> SomeData sem b
 106     whnf = \case
 107       Data (x :@ y) -> case whnf x of
 108         Data (Lam1 f) -> whnf (f y)
 109         x' -> x' .@ y
 110       x -> x
 111
 112 -- Unabstractable
 113 data instance Data Unabstractable sem a where
 114   (:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Unabstractable sem b
 115 instance Unabstractable sem => Derivable (Data Unabstractable sem) where
 116   derive = \case
 117     f :@ x -> derive f .@ derive x
 118 instance Unabstractable sem => Unabstractable (SomeData sem) where
 119   f .@ x = SomeData (f :@ x)
 120
 121 -- Functionable
 122 instance
 123   ( Abstractable sem
 124   ) =>
 125   Functionable (SomeData sem)
 126   where
 127   ($) = lam1 (\f -> lam1 (\x -> f .@ x))
 128   (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
 129   const = lam1 (\x -> lam1 (\_y -> x))
 130   flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
 131   id = lam1 (\x -> x)
 132
 133 -- Anythingable
 134 data instance Data Anythingable sem a where
 135   Anything :: sem a -> Data Anythingable sem a
 136 instance
 137   ( Anythingable sem
 138   ) =>
 139   Derivable (Data Anythingable sem)
 140   where
 141   derive = \case
 142     Anything x -> anything x
 143 instance Anythingable (SomeData sem)
 144 instance Anythingable (Data Anythingable sem)
 145
 146 -- Bottomable
 147 data instance Data Bottomable sem a where
 148   Bottom :: Data Bottomable sem a
 149 instance Bottomable sem => Derivable (Data Bottomable sem) where
 150   derive Bottom{} = bottom
 151
 152 -- Constantable
 153 data instance Data (Constantable c) sem a where
 154   Constant {-Typeable c =>-} :: c -> Data (Constantable c) sem c
 155 instance Constantable c sem => Derivable (Data (Constantable c) sem) where
 156   derive = \case
 157     Constant x -> constant x
 158 instance
 159   ( Constantable c sem
 160   , Typeable c
 161   ) =>
 162   Constantable c (SomeData sem)
 163   where
 164   constant c = SomeData (Constant c)
 165 instance{-Typeable c =>-} Constantable c (Data (Constantable c) sem) where
 166   constant = Constant
 167
 168 -- Eitherable
 169 data instance Data Eitherable sem a where
 170   Either :: Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
 171   Left :: Data Eitherable sem (l -> Either l r)
 172   Right :: Data Eitherable sem (r -> Either l r)
 173 instance Eitherable sem => Derivable (Data Eitherable sem) where
 174   derive = \case
 175     Either -> either
 176     Left -> left
 177     Right -> right
 178 instance Eitherable sem => Eitherable (SomeData sem) where
 179   either = SomeData Either
 180   left = SomeData Left
 181   right = SomeData Right
 182 instance Eitherable (Data Eitherable sem) where
 183   either = Either
 184   left = Left
 185   right = Right
 186
 187 -- Equalable
 188 data instance Data Equalable sem a where
 189   Equal :: Eq.Eq a => Data Equalable sem (a -> a -> Bool)
 190 instance Equalable sem => Derivable (Data Equalable sem) where
 191   derive = \case
 192     Equal -> equal
 193 instance
 194   ( Equalable sem
 195   ) =>
 196   Equalable (SomeData sem)
 197   where
 198   equal = SomeData Equal
 199 instance Equalable (Data Equalable sem) where
 200   equal = Equal
 201
 202 -- Emptyable
 203 data instance Data Emptyable sem a where
 204   Empty :: Data Emptyable sem a
 205 instance Emptyable sem => Derivable (Data Emptyable sem) where
 206   derive = \case
 207     Empty -> empty
 208 instance
 209   ( Emptyable sem
 210   ) =>
 211   Emptyable (SomeData sem)
 212   where
 213   empty = SomeData Empty
 214 instance Emptyable (Data Emptyable sem) where
 215   empty = Empty
 216
 217 -- Semigroupable
 218 data instance Data Semigroupable sem a where
 219   Concat :: Semigroup a => Data Semigroupable sem (a -> a -> a)
 220 infixr 4 `Concat`
 221 instance Semigroupable sem => Derivable (Data Semigroupable sem) where
 222   derive = \case
 223     Concat -> concat
 224 instance
 225   ( Semigroupable sem
 226   ) =>
 227   Semigroupable (SomeData sem)
 228   where
 229   concat = SomeData Concat
 230 instance Semigroupable (Data Semigroupable sem) where
 231   concat = Concat
 232
 233 -- IfThenElseable
 234 data instance Data IfThenElseable sem a where
 235   IfThenElse ::
 236     SomeData sem Bool ->
 237     SomeData sem a ->
 238     SomeData sem a ->
 239     Data IfThenElseable sem a
 240 instance IfThenElseable sem => Derivable (Data IfThenElseable sem) where
 241   derive = \case
 242     IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
 243 instance
 244   ( IfThenElseable sem
 245   ) =>
 246   IfThenElseable (SomeData sem)
 247   where
 248   ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
 249 instance IfThenElseable sem => IfThenElseable (Data IfThenElseable sem) where
 250   ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
 251
 252 -- Listable
 253 data instance Data Listable sem a where
 254   Cons :: Data Listable sem (a -> [a] -> [a])
 255   Nil :: Data Listable sem [a]
 256 infixr 4 `Cons`
 257 instance Listable sem => Derivable (Data Listable sem) where
 258   derive = \case
 259     Cons -> cons
 260     Nil -> nil
 261 instance
 262   ( Listable sem
 263   ) =>
 264   Listable (SomeData sem)
 265   where
 266   cons = SomeData Cons
 267   nil = SomeData Nil
 268 instance Listable (Data Listable sem) where
 269   cons = Cons
 270   nil = Nil
 271
 272 -- Maybeable
 273 data instance Data Maybeable sem a where
 274   Nothing :: Data Maybeable sem (Maybe a)
 275   Just :: Data Maybeable sem (a -> Maybe a)
 276 instance Maybeable sem => Derivable (Data Maybeable sem) where
 277   derive = \case
 278     Nothing -> nothing
 279     Just -> just
 280 instance
 281   ( Maybeable sem
 282   ) =>
 283   Maybeable (SomeData sem)
 284   where
 285   nothing = SomeData Nothing
 286   just = SomeData Just
 287 instance Maybeable (Data Maybeable sem) where
 288   nothing = Nothing
 289   just = Just