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 {-
  58 class TransUnit able where
  59   -- | The 'Bottomable' constraint is needed when a @(repr)@ value
  60   -- has to be constructed.
  61   reprFromUnit :: Bottomable repr => Data able Unit a -> SomeData repr a
  62   -- | The 'Bottomable' constraint is also needed here
  63   -- to call 'reprFromUnit' in the 'Lam' case.
  64   unitFromRepr :: Bottomable repr => Data able repr a -> SomeData Unit a
  65
  66 coerceRepr ::
  67   Bottomable repr => Bottomable repr' =>
  68   SomeData repr a -> SomeData repr' a
  69 coerceRepr (SomeData r) =
  70   case unitFromRepr r of
  71     SomeData d -> reprFromUnit d
  72 -}
  73
  74 -- | @(unSomeData c :: 'Maybe' ('Data' able repr a))@
  75 -- extract the data-constructor from the given 'SomeData'
  76 -- iif. it belongs to the @('Data' able repr a)@ data-instance.
  77 unSomeData ::
  78   forall able repr a.
  79   Typeable able =>
  80   SomeData repr a -> Maybe (Data able repr a)
  81 unSomeData (SomeData (c::Data c repr a)) =
  82   case typeRep @able `eqTypeRep` typeRep @c of
  83     Maybe.Just HRefl -> Maybe.Just c
  84     Maybe.Nothing -> Maybe.Nothing
  85
  86 -- Abstractable
  87 data instance Data Abstractable repr a where
  88   (:@) :: SomeData repr (a->b) -> SomeData repr a -> Data Abstractable repr b
  89   Lam :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
  90   Lam1 :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
  91   Var :: repr a -> Data Abstractable repr a
  92   -- FIXME: add constructors
  93 instance
  94   ( Abstractable repr
  95   --, Trans (SomeData repr) repr
  96   --, Trans repr (SomeData repr)
  97   ) => Trans (Data Abstractable repr) repr where
  98   trans = \case
  99     f :@ x -> trans f .@ trans x
 100     Lam f -> lam (\x -> trans (f (SomeData (Var x))))
 101     Lam1 f -> lam1 (\x -> trans (f (SomeData (Var x))))
 102     Var x -> var x
 103 instance
 104   ( Abstractable repr
 105   --, Trans (SomeData repr) repr
 106   --, Trans repr (SomeData repr)
 107   ) => Abstractable (SomeData repr) where
 108   f .@ x = SomeData (f :@ x)
 109   lam f = SomeData (Lam f)
 110   lam1 f = SomeData (Lam1 f)
 111   var = Fun.id
 112   ($) = lam1 (\f -> lam1 (\x -> f .@ x))
 113   (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
 114   const = lam1 (\x -> lam1 (\_y -> x))
 115   flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
 116   id = lam1 (\x -> x)
 117
 118 {-
 119 instance
 120   ( Abstractable repr
 121   ) =>
 122   Abstractable (Data Abstractable repr) where
 123   var = Var Fun.. SomeData
 124   f .@ x = SomeData f :@ SomeData x
 125   lam f = Lam (SomeData Fun.. f Fun.. Var)
 126   lam1 f = Lam1 (SomeData Fun.. f Fun.. Var)
 127   ($) = lam1 (\f -> lam1 (\x -> f .@ x))
 128   (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
 129   const = lam1 (\x -> lam1 (\_y -> x))
 130   flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
 131   id = lam1 (\x -> x)
 132 -}
 133 {-
 134 instance Bottomable repr => Morph (SomeData repr) (SomeData Unit) where
 135   morph (SomeData x) = morph x
 136 instance Bottomable repr => Morph (SomeData Unit) (SomeData repr) where
 137   morph (SomeData x) = morph x
 138 instance Abstractable Unit where
 139   (.@) _f _x = Unit
 140   lam _f = Unit
 141   lam1 _f = Unit
 142   ($) = Unit
 143   (.) = Unit
 144   const = Unit
 145   flip = Unit
 146   id = Unit
 147 instance Abstractable (Data Abstractable Unit) where
 148   f .@ x = SomeData f :@ SomeData x
 149   lam f = Lam (\(SomeData x) -> SomeData (f (trans x)))
 150   lam1 f = Lam1 (\(SomeData x) -> SomeData (f (trans x)))
 151   ($) = ($)
 152   (.) = (.)
 153   const = const
 154   flip = flip
 155   id = id
 156 -}
 157
 158 -- Anythingable
 159 data instance Data Anythingable repr a where
 160   Anything :: repr a -> Data Anythingable repr a
 161 instance
 162   ( Anythingable repr
 163   ) =>
 164   Trans (Data Anythingable repr) repr where
 165   trans = \case
 166     Anything x -> anything x
 167 instance Anythingable (SomeData repr)
 168 instance Anythingable (Data Anythingable repr)
 169
 170 -- Bottomable
 171 class Bottomable repr where
 172   bottom :: repr a
 173 data instance Data Bottomable repr a where
 174   Bottom :: Data Bottomable repr a
 175 instance Bottomable repr => Trans (Data Bottomable repr) repr where
 176   trans Bottom{} = bottom
 177
 178 -- Constantable
 179 data instance Data (Constantable c) repr a where
 180   Constant :: c -> Data (Constantable c) repr c
 181 instance Constantable c repr => Trans (Data (Constantable c) repr) repr where
 182   trans = \case
 183     Constant x -> constant x
 184 instance
 185   ( Constantable c repr
 186   , Typeable c
 187   ) => Constantable c (SomeData repr) where
 188   constant c = SomeData (Constant c)
 189 instance Constantable c (Data (Constantable c) repr) where
 190   constant = Constant
 191
 192 -- Eitherable
 193 data instance Data Eitherable repr a where
 194   Left :: Data Eitherable repr (l -> Either l r)
 195   Right :: Data Eitherable repr (r -> Either l r)
 196 instance Eitherable repr => Trans (Data Eitherable repr) repr where
 197   trans = \case
 198     Left -> left
 199     Right -> right
 200 instance
 201   ( Eitherable repr
 202   ) => Eitherable (SomeData repr) where
 203   left = SomeData Left
 204   right = SomeData Right
 205 instance Eitherable (Data Eitherable repr) where
 206   left = Left
 207   right = Right
 208
 209 -- Equalable
 210 data instance Data Equalable repr a where
 211   Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
 212 instance Equalable repr => Trans (Data Equalable repr) repr where
 213   trans = \case
 214     Equal -> equal
 215 instance
 216   ( Equalable repr
 217   ) => Equalable (SomeData repr) where
 218   equal = SomeData Equal
 219 instance Equalable (Data Equalable repr) where
 220   equal = Equal
 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