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.Transformable
  29
  30 -- * Type 'SomeData'
  31 data SomeData repr a =
  32   forall able.
  33   ( Derive (Data able repr)
  34   , Typeable able
  35   ) => SomeData (Data able repr a)
  36
  37 type instance Derived (SomeData repr) = repr
  38 instance Derive (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   ) => Derive (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   Derive (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 class Bottomable repr where
 113   bottom :: repr a
 114 data instance Data Bottomable repr a where
 115   Bottom :: Data Bottomable repr a
 116 instance Bottomable repr => Derive (Data Bottomable repr) where
 117   derive Bottom{} = bottom
 118
 119 -- Constantable
 120 data instance Data (Constantable c) repr a where
 121   Constant :: {-Typeable c =>-} c -> Data (Constantable c) repr c
 122 instance Constantable c repr => Derive (Data (Constantable c) repr) where
 123   derive = \case
 124     Constant x -> constant x
 125 instance
 126   ( Constantable c repr
 127   , Typeable c
 128   ) => Constantable c (SomeData repr) where
 129   constant c = SomeData (Constant c)
 130 instance {-Typeable c =>-} Constantable c (Data (Constantable c) repr) where
 131   constant = Constant
 132
 133 -- Eitherable
 134 data instance Data Eitherable repr a where
 135   Left :: Data Eitherable repr (l -> Either l r)
 136   Right :: Data Eitherable repr (r -> Either l r)
 137 instance Eitherable repr => Derive (Data Eitherable repr) where
 138   derive = \case
 139     Left -> left
 140     Right -> right
 141 instance
 142   ( Eitherable repr
 143   ) => Eitherable (SomeData repr) where
 144   left = SomeData Left
 145   right = SomeData Right
 146 instance Eitherable (Data Eitherable repr) where
 147   left = Left
 148   right = Right
 149
 150 -- Equalable
 151 data instance Data Equalable repr a where
 152   Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
 153 instance Equalable repr => Derive (Data Equalable repr) where
 154   derive = \case
 155     Equal -> equal
 156 instance
 157   ( Equalable repr
 158   ) => Equalable (SomeData repr) where
 159   equal = SomeData Equal
 160 instance Equalable (Data Equalable repr) where
 161   equal = Equal
 162
 163 -- IfThenElseable
 164 data instance Data IfThenElseable repr a where
 165   IfThenElse ::
 166     SomeData repr Bool ->
 167     SomeData repr a ->
 168     SomeData repr a ->
 169     Data IfThenElseable repr a
 170 instance IfThenElseable repr => Derive (Data IfThenElseable repr) where
 171   derive = \case
 172     IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
 173 instance
 174   ( IfThenElseable repr
 175   ) => IfThenElseable (SomeData repr) where
 176   ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
 177 instance IfThenElseable repr => IfThenElseable (Data IfThenElseable repr) where
 178   ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
 179
 180 -- Listable
 181 data instance Data Listable repr a where
 182   Cons :: Data Listable repr (a -> [a] -> [a])
 183   Nil :: Data Listable repr [a]
 184 infixr 4 `Cons`
 185 instance Listable repr => Derive (Data Listable repr) where
 186   derive = \case
 187     Cons -> cons
 188     Nil -> nil
 189 instance
 190   ( Listable repr
 191   ) => Listable (SomeData repr) where
 192   cons = SomeData Cons
 193   nil = SomeData Nil
 194 instance Listable (Data Listable repr) where
 195   cons = Cons
 196   nil = Nil
 197
 198 -- Maybeable
 199 data instance Data Maybeable repr a where
 200   Nothing :: Data Maybeable repr (Maybe a)
 201   Just :: Data Maybeable repr (a -> Maybe a)
 202 instance Maybeable repr => Derive (Data Maybeable repr) where
 203   derive = \case
 204     Nothing -> nothing
 205     Just -> just
 206 instance
 207   ( Maybeable repr
 208   ) => Maybeable (SomeData repr) where
 209   nothing = SomeData Nothing
 210   just = SomeData Just
 211 instance Maybeable (Data Maybeable repr) where
 212   nothing = Nothing
 213   just = Just