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 = \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       Data (IfThenElse test ok ko) ->
 118         case nor test of
 119           Data (Constant b :: Data (Constantable Bool) sem Bool) ->
 120             if b then nor ok else nor ko
 121           t -> ifThenElse (nor t) (nor ok) (nor ko)
 122       x -> x
 123
 124     whnf :: SomeData sem b -> SomeData sem b
 125     whnf = \case
 126       Data (x :@ y) -> case whnf x of
 127         Data (Lam1 f) -> whnf (f y)
 128         x' -> x' .@ y
 129       x -> x
 130
 131 -- Instantiable
 132 data instance Data Instantiable sem a where
 133   (:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Instantiable sem b
 134 instance Instantiable sem => Derivable (Data Instantiable sem) where
 135   derive = \case
 136     f :@ x -> derive f .@ derive x
 137 instance Instantiable sem => Instantiable (SomeData sem) where
 138   f .@ x = SomeData (f :@ x)
 139
 140 -- Unabstractable
 141 data instance Data Unabstractable sem a where
 142   Ap :: Data Unabstractable sem ((a -> b -> c) -> (a -> b) -> a -> c)
 143   Const :: Data Unabstractable sem (a -> b -> a)
 144   Id :: Data Unabstractable sem (a -> a)
 145   (:.) :: Data Unabstractable sem ((b -> c) -> (a -> b) -> a -> c)
 146   Flip :: Data Unabstractable sem ((a -> b -> c) -> b -> a -> c)
 147   (:$) :: Data Unabstractable sem ((a -> b) -> a -> b)
 148 instance Unabstractable sem => Derivable (Data Unabstractable sem) where
 149   derive = \case
 150     Ap -> ap
 151     Const -> const
 152     Id -> id
 153     (:.) -> (.)
 154     Flip -> flip
 155     (:$) -> ($)
 156 instance Unabstractable sem => Unabstractable (SomeData sem) where
 157   ap = SomeData Ap
 158   const = SomeData Const
 159   id = SomeData Id
 160   (.) = SomeData (:.)
 161   flip = SomeData Flip
 162   ($) = SomeData (:$)
 163
 164 -- Anythingable
 165 data instance Data Anythingable sem a where
 166   Anything :: sem a -> Data Anythingable sem a
 167 instance
 168   ( Anythingable sem
 169   ) =>
 170   Derivable (Data Anythingable sem)
 171   where
 172   derive = \case
 173     Anything x -> anything x
 174 instance Anythingable (SomeData sem)
 175 instance Anythingable (Data Anythingable sem)
 176
 177 -- Bottomable
 178 data instance Data Bottomable sem a where
 179   Bottom :: Data Bottomable sem a
 180 instance Bottomable sem => Derivable (Data Bottomable sem) where
 181   derive Bottom{} = bottom
 182
 183 -- Constantable
 184 data instance Data (Constantable c) sem a where
 185   Constant {-Typeable c =>-} :: c -> Data (Constantable c) sem c
 186 instance Constantable c sem => Derivable (Data (Constantable c) sem) where
 187   derive = \case
 188     Constant x -> constant x
 189 instance
 190   ( Constantable c sem
 191   , Typeable c
 192   ) =>
 193   Constantable c (SomeData sem)
 194   where
 195   constant c = SomeData (Constant c)
 196 instance{-Typeable c =>-} Constantable c (Data (Constantable c) sem) where
 197   constant = Constant
 198
 199 -- Eitherable
 200 data instance Data Eitherable sem a where
 201   Either :: Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
 202   Left :: Data Eitherable sem (l -> Either l r)
 203   Right :: Data Eitherable sem (r -> Either l r)
 204 instance Eitherable sem => Derivable (Data Eitherable sem) where
 205   derive = \case
 206     Either -> either
 207     Left -> left
 208     Right -> right
 209 instance Eitherable sem => Eitherable (SomeData sem) where
 210   either = SomeData Either
 211   left = SomeData Left
 212   right = SomeData Right
 213 instance Eitherable (Data Eitherable sem) where
 214   either = Either
 215   left = Left
 216   right = Right
 217
 218 -- Equalable
 219 data instance Data Equalable sem a where
 220   Equal :: Eq.Eq a => Data Equalable sem (a -> a -> Bool)
 221 instance Equalable sem => Derivable (Data Equalable sem) where
 222   derive = \case
 223     Equal -> equal
 224 instance
 225   ( Equalable sem
 226   ) =>
 227   Equalable (SomeData sem)
 228   where
 229   equal = SomeData Equal
 230 instance Equalable (Data Equalable sem) where
 231   equal = Equal
 232
 233 -- Emptyable
 234 data instance Data Emptyable sem a where
 235   Empty :: Data Emptyable sem a
 236 instance Emptyable sem => Derivable (Data Emptyable sem) where
 237   derive = \case
 238     Empty -> empty
 239 instance
 240   ( Emptyable sem
 241   ) =>
 242   Emptyable (SomeData sem)
 243   where
 244   empty = SomeData Empty
 245 instance Emptyable (Data Emptyable sem) where
 246   empty = Empty
 247
 248 -- Semigroupable
 249 data instance Data Semigroupable sem a where
 250   Concat :: Semigroup a => Data Semigroupable sem (a -> a -> a)
 251 infixr 4 `Concat`
 252 instance Semigroupable sem => Derivable (Data Semigroupable sem) where
 253   derive = \case
 254     Concat -> concat
 255 instance
 256   ( Semigroupable sem
 257   ) =>
 258   Semigroupable (SomeData sem)
 259   where
 260   concat = SomeData Concat
 261 instance Semigroupable (Data Semigroupable sem) where
 262   concat = Concat
 263
 264 -- IfThenElseable
 265 data instance Data IfThenElseable sem a where
 266   IfThenElse ::
 267     SomeData sem Bool ->
 268     SomeData sem a ->
 269     SomeData sem a ->
 270     Data IfThenElseable sem a
 271 instance IfThenElseable sem => Derivable (Data IfThenElseable sem) where
 272   derive = \case
 273     IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
 274 instance
 275   ( IfThenElseable sem
 276   ) =>
 277   IfThenElseable (SomeData sem)
 278   where
 279   ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
 280 instance IfThenElseable sem => IfThenElseable (Data IfThenElseable sem) where
 281   ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
 282
 283 -- Listable
 284 data instance Data Listable sem a where
 285   Cons :: Data Listable sem (a -> [a] -> [a])
 286   Nil :: Data Listable sem [a]
 287 infixr 4 `Cons`
 288 instance Listable sem => Derivable (Data Listable sem) where
 289   derive = \case
 290     Cons -> cons
 291     Nil -> nil
 292 instance
 293   ( Listable sem
 294   ) =>
 295   Listable (SomeData sem)
 296   where
 297   cons = SomeData Cons
 298   nil = SomeData Nil
 299 instance Listable (Data Listable sem) where
 300   cons = Cons
 301   nil = Nil
 302
 303 -- Maybeable
 304 data instance Data Maybeable sem a where
 305   Nothing :: Data Maybeable sem (Maybe a)
 306   Just :: Data Maybeable sem (a -> Maybe a)
 307 instance Maybeable sem => Derivable (Data Maybeable sem) where
 308   derive = \case
 309     Nothing -> nothing
 310     Just -> just
 311 instance
 312   ( Maybeable sem
 313   ) =>
 314   Maybeable (SomeData sem)
 315   where
 316   nothing = SomeData Nothing
 317   just = SomeData Just
 318 instance Maybeable (Data Maybeable sem) where
 319   nothing = Nothing
 320   just = Just