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.Kind (Constraint, Type)
  19 import Type.Reflection (Typeable, (:~~:)(..), eqTypeRep, typeRep)
  20 import Data.Bool (Bool)
  21 import Data.Either (Either)
  22 import Data.Maybe (Maybe)
  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.Trans
  29
  30 data SomeData repr a =
  31   forall able.
  32   ( Trans (Data able repr) repr
  33   , Typeable able
  34   ) => SomeData (Data able repr a)
  35
  36 instance Trans (SomeData repr) repr where
  37   trans (SomeData x) = trans x
  38
  39 type TypedRepr = Type -> Type
  40
  41 -- TODO: neither data families nor data instances
  42 -- can have phantom roles with GHC-9's RoleAnnotations,
  43 -- hence 'Data.Coerce.coerce' cannot be used on them for now.
  44 -- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
  45 -- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
  46 -- Would be useful for @Trans (Data able repr) (Data able repr')@ instances.
  47 data family Data
  48   (able :: TypedRepr -> Constraint)
  49   :: TypedRepr -> TypedRepr
  50 --instance Trans (Data able repr) (Data able repr) where
  51 --  trans = Fun.id
  52
  53 -- | Convenient utility to pattern-match a 'SomeData'.
  54 pattern Data :: Typeable able => Data able repr a -> SomeData repr a
  55 pattern Data x <- (unSomeData -> Maybe.Just x)
  56
  57 -- | @(unSomeData c :: 'Maybe' ('Data' able repr a))@
  58 -- extract the data-constructor from the given 'SomeData'
  59 -- iif. it belongs to the @('Data' able repr a)@ data-instance.
  60 unSomeData ::
  61   forall able repr a.
  62   Typeable able =>
  63   SomeData repr a -> Maybe (Data able repr a)
  64 unSomeData (SomeData (c::Data c repr a)) =
  65   case typeRep @able `eqTypeRep` typeRep @c of
  66     Maybe.Just HRefl -> Maybe.Just c
  67     Maybe.Nothing -> Maybe.Nothing
  68
  69 -- Abstractable
  70 data instance Data Abstractable repr a where
  71   (:@) :: SomeData repr (a->b) -> SomeData repr a -> Data Abstractable repr b
  72   Lam :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
  73   Lam1 :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
  74   Var :: repr a -> Data Abstractable repr a
  75   -- FIXME: add constructors
  76 instance
  77   ( Abstractable repr
  78   --, Trans (SomeData repr) repr
  79   --, Trans repr (SomeData repr)
  80   ) => Trans (Data Abstractable repr) repr where
  81   trans = \case
  82     f :@ x -> trans f .@ trans x
  83     Lam f -> lam (\x -> trans (f (SomeData (Var x))))
  84     Lam1 f -> lam1 (\x -> trans (f (SomeData (Var x))))
  85     Var x -> var x
  86 instance
  87   ( Abstractable repr
  88   --, Trans (SomeData repr) repr
  89   --, Trans repr (SomeData repr)
  90   ) => Abstractable (SomeData repr) where
  91   f .@ x = SomeData (f :@ x)
  92   lam f = SomeData (Lam f)
  93   lam1 f = SomeData (Lam1 f)
  94   var = Fun.id
  95   ($) = lam1 (\f -> lam1 (\x -> f .@ x))
  96   (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
  97   const = lam1 (\x -> lam1 (\_y -> x))
  98   flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
  99   id = lam1 (\x -> x)
 100
 101 {-
 102 instance
 103   ( Abstractable repr
 104   ) =>
 105   Abstractable (Data Abstractable repr) where
 106   var = Var Fun.. SomeData
 107   f .@ x = SomeData f :@ SomeData x
 108   lam f = Lam (SomeData Fun.. f Fun.. Var)
 109   lam1 f = Lam1 (SomeData Fun.. f Fun.. Var)
 110   ($) = lam1 (\f -> lam1 (\x -> f .@ x))
 111   (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
 112   const = lam1 (\x -> lam1 (\_y -> x))
 113   flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
 114   id = lam1 (\x -> x)
 115 -}
 116 {-
 117 instance Bottomable repr => Morph (SomeData repr) (SomeData Unit) where
 118   morph (SomeData x) = morph x
 119 instance Bottomable repr => Morph (SomeData Unit) (SomeData repr) where
 120   morph (SomeData x) = morph x
 121 instance Abstractable Unit where
 122   (.@) _f _x = Unit
 123   lam _f = Unit
 124   lam1 _f = Unit
 125   ($) = Unit
 126   (.) = Unit
 127   const = Unit
 128   flip = Unit
 129   id = Unit
 130 instance Abstractable (Data Abstractable Unit) where
 131   f .@ x = SomeData f :@ SomeData x
 132   lam f = Lam (\(SomeData x) -> SomeData (f (trans x)))
 133   lam1 f = Lam1 (\(SomeData x) -> SomeData (f (trans x)))
 134   ($) = ($)
 135   (.) = (.)
 136   const = const
 137   flip = flip
 138   id = id
 139 -}
 140
 141 -- Anythingable
 142 data instance Data Anythingable repr a where
 143   Anything :: repr a -> Data Anythingable repr a
 144 instance
 145   ( Anythingable repr
 146   ) =>
 147   Trans (Data Anythingable repr) repr where
 148   trans = \case
 149     Anything x -> anything x
 150 instance Anythingable (SomeData repr)
 151 instance Anythingable (Data Anythingable repr)
 152
 153 -- Bottomable
 154 class Bottomable repr where
 155   bottom :: repr a
 156 data instance Data Bottomable repr a where
 157   Bottom :: Data Bottomable repr a
 158 instance Bottomable repr => Trans (Data Bottomable repr) repr where
 159   trans Bottom{} = bottom
 160
 161 -- Constantable
 162 data instance Data (Constantable c) repr a where
 163   Constant :: {-Typeable c =>-} c -> Data (Constantable c) repr c
 164 instance Constantable c repr => Trans (Data (Constantable c) repr) repr where
 165   trans = \case
 166     Constant x -> constant x
 167 instance
 168   ( Constantable c repr
 169   , Typeable c
 170   ) => Constantable c (SomeData repr) where
 171   constant c = SomeData (Constant c)
 172 instance {-Typeable c =>-} Constantable c (Data (Constantable c) repr) where
 173   constant = Constant
 174
 175 -- Eitherable
 176 data instance Data Eitherable repr a where
 177   Left :: Data Eitherable repr (l -> Either l r)
 178   Right :: Data Eitherable repr (r -> Either l r)
 179 instance Eitherable repr => Trans (Data Eitherable repr) repr where
 180   trans = \case
 181     Left -> left
 182     Right -> right
 183 instance
 184   ( Eitherable repr
 185   ) => Eitherable (SomeData repr) where
 186   left = SomeData Left
 187   right = SomeData Right
 188 instance Eitherable (Data Eitherable repr) where
 189   left = Left
 190   right = Right
 191
 192 -- Equalable
 193 data instance Data Equalable repr a where
 194   Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
 195 instance Equalable repr => Trans (Data Equalable repr) repr where
 196   trans = \case
 197     Equal -> equal
 198 instance
 199   ( Equalable repr
 200   ) => Equalable (SomeData repr) where
 201   equal = SomeData Equal
 202 instance Equalable (Data Equalable repr) where
 203   equal = Equal
 204
 205 -- IfThenElseable
 206 data instance Data IfThenElseable repr a where
 207   IfThenElse ::
 208     SomeData repr Bool ->
 209     SomeData repr a ->
 210     SomeData repr a ->
 211     Data IfThenElseable repr a
 212 instance IfThenElseable repr => Trans (Data IfThenElseable repr) repr where
 213   trans = \case
 214     IfThenElse test ok ko -> ifThenElse (trans test) (trans ok) (trans ko)
 215 instance
 216   ( IfThenElseable repr
 217   ) => IfThenElseable (SomeData repr) where
 218   ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
 219 instance IfThenElseable repr => IfThenElseable (Data IfThenElseable repr) where
 220   ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
 221
 222 -- Listable
 223 data instance Data Listable repr a where
 224   Cons :: Data Listable repr (a -> [a] -> [a])
 225   Nil :: Data Listable repr [a]
 226 infixr 4 `Cons`
 227 instance Listable repr => Trans (Data Listable repr) repr where
 228   trans = \case
 229     Cons -> cons
 230     Nil -> nil
 231 instance
 232   ( Listable repr
 233   ) => Listable (SomeData repr) where
 234   cons = SomeData Cons
 235   nil = SomeData Nil
 236 instance Listable (Data Listable repr) where
 237   cons = Cons
 238   nil = Nil
 239
 240 -- Maybeable
 241 data instance Data Maybeable repr a where
 242   Nothing :: Data Maybeable repr (Maybe a)
 243   Just :: Data Maybeable repr (a -> Maybe a)
 244 instance Maybeable repr => Trans (Data Maybeable repr) repr where
 245   trans = \case
 246     Nothing -> nothing
 247     Just -> just
 248 instance
 249   ( Maybeable repr
 250   ) => Maybeable (SomeData repr) where
 251   nothing = SomeData Nothing
 252   just = SomeData Just
 253 instance Maybeable (Data Maybeable repr) where
 254   nothing = Nothing
 255   just = Just