src/Symantic/Data.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-} -- For ReprKind
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE PatternSynonyms #-}
   5 {-# LANGUAGE RankNTypes #-}
   6 {-# LANGUAGE StandaloneDeriving #-}
   7 {-# LANGUAGE ViewPatterns #-}
   8 module Symantic.Data where
   9
  10 import Data.Bool (Bool)
  11 import Data.Either (Either)
  12 import Data.Kind (Constraint)
  13 import Data.Maybe (Maybe)
  14 import Type.Reflection (Typeable, (:~~:)(..), eqTypeRep, typeRep)
  15 import qualified Data.Eq as Eq
  16 import qualified Data.Maybe as Maybe
  17 import qualified Data.Function as Fun
  18
  19 import Symantic.Lang
  20 import Symantic.Derive
  21
  22 -- * Type 'SomeData'
  23 data SomeData repr a =
  24   forall able.
  25   ( Derivable (Data able repr)
  26   , Typeable able
  27   ) => SomeData (Data able repr a)
  28
  29 type instance Derived (SomeData repr) = repr
  30 instance Derivable (SomeData repr) where
  31   derive (SomeData x) = derive x
  32
  33 -- ** Type 'Data'
  34 -- TODO: neither data families nor data instances
  35 -- can have phantom roles with GHC-9's RoleAnnotations,
  36 -- hence 'Data.Coerce.coerce' cannot be used on them for now.
  37 -- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
  38 -- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
  39 data family Data
  40   (able :: ReprKind -> Constraint)
  41   :: ReprKind -> ReprKind
  42 type instance Derived (Data able repr) = repr
  43
  44 -- | Convenient utility to pattern-match a 'SomeData'.
  45 pattern Data :: Typeable able => Data able repr a -> SomeData repr a
  46 pattern Data x <- (unSomeData -> Maybe.Just x)
  47
  48 -- | @(unSomeData c :: 'Maybe' ('Data' able repr a))@
  49 -- extract the data-constructor from the given 'SomeData'
  50 -- iif. it belongs to the @('Data' able repr a)@ data-instance.
  51 unSomeData ::
  52   forall able repr a.
  53   Typeable able =>
  54   SomeData repr a -> Maybe (Data able repr a)
  55 unSomeData (SomeData (c::Data c repr a)) =
  56   case typeRep @able `eqTypeRep` typeRep @c of
  57     Maybe.Just HRefl -> Maybe.Just c
  58     Maybe.Nothing -> Maybe.Nothing
  59
  60 -- Abstractable
  61 data instance Data Abstractable repr a where
  62   (:@) :: SomeData repr (a->b) -> SomeData repr a -> Data Abstractable repr b
  63   Lam :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
  64   Lam1 :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
  65   Var :: repr a -> Data Abstractable repr a
  66   -- FIXME: add constructors
  67 instance
  68   ( Abstractable repr
  69   ) => Derivable (Data Abstractable repr) where
  70   derive = \case
  71     f :@ x -> derive f .@ derive x
  72     Lam f -> lam (\x -> derive (f (SomeData (Var x))))
  73     Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
  74     Var x -> var x
  75 instance
  76   ( Abstractable repr
  77   ) => Abstractable (SomeData repr) where
  78   f .@ x = SomeData (f :@ x)
  79   lam f = SomeData (Lam f)
  80   lam1 f = SomeData (Lam1 f)
  81   var = Fun.id
  82   ($) = lam1 (\f -> lam1 (\x -> f .@ x))
  83   (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
  84   const = lam1 (\x -> lam1 (\_y -> x))
  85   flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
  86   id = lam1 (\x -> x)
  87
  88 -- Anythingable
  89 data instance Data Anythingable repr a where
  90   Anything :: repr a -> Data Anythingable repr a
  91 instance
  92   ( Anythingable repr
  93   ) =>
  94   Derivable (Data Anythingable repr) where
  95   derive = \case
  96     Anything x -> anything x
  97 instance Anythingable (SomeData repr)
  98 instance Anythingable (Data Anythingable repr)
  99
 100 -- Bottomable
 101 data instance Data Bottomable repr a where
 102   Bottom :: Data Bottomable repr a
 103 instance Bottomable repr => Derivable (Data Bottomable repr) where
 104   derive Bottom{} = bottom
 105
 106 -- Constantable
 107 data instance Data (Constantable c) repr a where
 108   Constant :: {-Typeable c =>-} c -> Data (Constantable c) repr c
 109 instance Constantable c repr => Derivable (Data (Constantable c) repr) where
 110   derive = \case
 111     Constant x -> constant x
 112 instance
 113   ( Constantable c repr
 114   , Typeable c
 115   ) => Constantable c (SomeData repr) where
 116   constant c = SomeData (Constant c)
 117 instance {-Typeable c =>-} Constantable c (Data (Constantable c) repr) where
 118   constant = Constant
 119
 120 -- Eitherable
 121 data instance Data Eitherable repr a where
 122   Left :: Data Eitherable repr (l -> Either l r)
 123   Right :: Data Eitherable repr (r -> Either l r)
 124 instance Eitherable repr => Derivable (Data Eitherable repr) where
 125   derive = \case
 126     Left -> left
 127     Right -> right
 128 instance
 129   ( Eitherable repr
 130   ) => Eitherable (SomeData repr) where
 131   left = SomeData Left
 132   right = SomeData Right
 133 instance Eitherable (Data Eitherable repr) where
 134   left = Left
 135   right = Right
 136
 137 -- Equalable
 138 data instance Data Equalable repr a where
 139   Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
 140 instance Equalable repr => Derivable (Data Equalable repr) where
 141   derive = \case
 142     Equal -> equal
 143 instance
 144   ( Equalable repr
 145   ) => Equalable (SomeData repr) where
 146   equal = SomeData Equal
 147 instance Equalable (Data Equalable repr) where
 148   equal = Equal
 149
 150 -- IfThenElseable
 151 data instance Data IfThenElseable repr a where
 152   IfThenElse ::
 153     SomeData repr Bool ->
 154     SomeData repr a ->
 155     SomeData repr a ->
 156     Data IfThenElseable repr a
 157 instance IfThenElseable repr => Derivable (Data IfThenElseable repr) where
 158   derive = \case
 159     IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
 160 instance
 161   ( IfThenElseable repr
 162   ) => IfThenElseable (SomeData repr) where
 163   ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
 164 instance IfThenElseable repr => IfThenElseable (Data IfThenElseable repr) where
 165   ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
 166
 167 -- Listable
 168 data instance Data Listable repr a where
 169   Cons :: Data Listable repr (a -> [a] -> [a])
 170   Nil :: Data Listable repr [a]
 171 infixr 4 `Cons`
 172 instance Listable repr => Derivable (Data Listable repr) where
 173   derive = \case
 174     Cons -> cons
 175     Nil -> nil
 176 instance
 177   ( Listable repr
 178   ) => Listable (SomeData repr) where
 179   cons = SomeData Cons
 180   nil = SomeData Nil
 181 instance Listable (Data Listable repr) where
 182   cons = Cons
 183   nil = Nil
 184
 185 -- Maybeable
 186 data instance Data Maybeable repr a where
 187   Nothing :: Data Maybeable repr (Maybe a)
 188   Just :: Data Maybeable repr (a -> Maybe a)
 189 instance Maybeable repr => Derivable (Data Maybeable repr) where
 190   derive = \case
 191     Nothing -> nothing
 192     Just -> just
 193 instance
 194   ( Maybeable repr
 195   ) => Maybeable (SomeData repr) where
 196   nothing = SomeData Nothing
 197   just = SomeData Just
 198 instance Maybeable (Data Maybeable repr) where
 199   nothing = Nothing
 200   just = Just