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