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