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