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