src/Symantic/Univariant/Data.hs

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