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
  82 -- Functionable
  83 instance
  84   ( Abstractable repr
  85   ) => Functionable (SomeData repr) where
  86   ($) = lam1 (\f -> lam1 (\x -> f .@ x))
  87   (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
  88   const = lam1 (\x -> lam1 (\_y -> x))
  89   flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
  90   id = lam1 (\x -> x)
  91
  92 -- Anythingable
  93 data instance Data Anythingable repr a where
  94   Anything :: repr a -> Data Anythingable repr a
  95 instance
  96   ( Anythingable repr
  97   ) => Derivable (Data Anythingable repr) where
  98   derive = \case
  99     Anything x -> anything x
 100 instance Anythingable (SomeData repr)
 101 instance Anythingable (Data Anythingable repr)
 102
 103 -- Bottomable
 104 data instance Data Bottomable repr a where
 105   Bottom :: Data Bottomable repr a
 106 instance Bottomable repr => Derivable (Data Bottomable repr) where
 107   derive Bottom{} = bottom
 108
 109 -- Constantable
 110 data instance Data (Constantable c) repr a where
 111   Constant :: {-Typeable c =>-} c -> Data (Constantable c) repr c
 112 instance Constantable c repr => Derivable (Data (Constantable c) repr) where
 113   derive = \case
 114     Constant x -> constant x
 115 instance
 116   ( Constantable c repr
 117   , Typeable c
 118   ) => Constantable c (SomeData repr) where
 119   constant c = SomeData (Constant c)
 120 instance {-Typeable c =>-} Constantable c (Data (Constantable c) repr) where
 121   constant = Constant
 122
 123 -- Eitherable
 124 data instance Data Eitherable repr a where
 125   Left :: Data Eitherable repr (l -> Either l r)
 126   Right :: Data Eitherable repr (r -> Either l r)
 127 instance Eitherable repr => Derivable (Data Eitherable repr) where
 128   derive = \case
 129     Left -> left
 130     Right -> right
 131 instance
 132   ( Eitherable repr
 133   ) => Eitherable (SomeData repr) where
 134   left = SomeData Left
 135   right = SomeData Right
 136 instance Eitherable (Data Eitherable repr) where
 137   left = Left
 138   right = Right
 139
 140 -- Equalable
 141 data instance Data Equalable repr a where
 142   Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
 143 instance Equalable repr => Derivable (Data Equalable repr) where
 144   derive = \case
 145     Equal -> equal
 146 instance
 147   ( Equalable repr
 148   ) => Equalable (SomeData repr) where
 149   equal = SomeData Equal
 150 instance Equalable (Data Equalable repr) where
 151   equal = Equal
 152
 153 -- IfThenElseable
 154 data instance Data IfThenElseable repr a where
 155   IfThenElse ::
 156     SomeData repr Bool ->
 157     SomeData repr a ->
 158     SomeData repr a ->
 159     Data IfThenElseable repr a
 160 instance IfThenElseable repr => Derivable (Data IfThenElseable repr) where
 161   derive = \case
 162     IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
 163 instance
 164   ( IfThenElseable repr
 165   ) => IfThenElseable (SomeData repr) where
 166   ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
 167 instance IfThenElseable repr => IfThenElseable (Data IfThenElseable repr) where
 168   ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
 169
 170 -- Listable
 171 data instance Data Listable repr a where
 172   Cons :: Data Listable repr (a -> [a] -> [a])
 173   Nil :: Data Listable repr [a]
 174 infixr 4 `Cons`
 175 instance Listable repr => Derivable (Data Listable repr) where
 176   derive = \case
 177     Cons -> cons
 178     Nil -> nil
 179 instance
 180   ( Listable repr
 181   ) => Listable (SomeData repr) where
 182   cons = SomeData Cons
 183   nil = SomeData Nil
 184 instance Listable (Data Listable repr) where
 185   cons = Cons
 186   nil = Nil
 187
 188 -- Maybeable
 189 data instance Data Maybeable repr a where
 190   Nothing :: Data Maybeable repr (Maybe a)
 191   Just :: Data Maybeable repr (a -> Maybe a)
 192 instance Maybeable repr => Derivable (Data Maybeable repr) where
 193   derive = \case
 194     Nothing -> nothing
 195     Just -> just
 196 instance
 197   ( Maybeable repr
 198   ) => Maybeable (SomeData repr) where
 199   nothing = SomeData Nothing
 200   just = SomeData Just
 201 instance Maybeable (Data Maybeable repr) where
 202   nothing = Nothing
 203   just = Just