src/Symantic/Typed/Data.hs

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