src/Symantic/Data.hs

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