Remove constraints that use TagT. Add records back.

This commit is contained in:
Anupam Jain 2023-07-06 18:52:33 +05:30
parent ff06b1f240
commit 11e596fd26
3 changed files with 28 additions and 31 deletions

View File

@ -2,7 +2,7 @@ module Data.Data where
import Control.Alt ((<|>))
import Control.Alternative (empty)
import Control.Applicative (pure)
import Control.Applicative (class Applicative, pure)
import Control.Bind (bind, (>>=))
import Control.Category (identity, (<<<))
import Control.Monad (class Monad)
@ -19,7 +19,7 @@ import Data.Maybe (Maybe(..), fromMaybe, maybe)
import Data.Newtype (unwrap)
import Data.Ordering (Ordering)
import Data.Tuple (Tuple(..))
import Data.Typeable (class TagT, class Typeable, cast)
import Data.Typeable (class Typeable, cast)
import Data.Unit (Unit)
import Unsafe.Coerce (unsafeCoerce)
@ -29,7 +29,7 @@ mkT f = fromMaybe identity (cast f)
mkQ :: forall a b r. Typeable a => Typeable b => r -> (b -> r) -> a -> r
mkQ r q a = maybe r q (cast a)
mkM :: forall a b m. Typeable a => Typeable b => Monad m => TagT m => (b -> m b) -> a -> m a
mkM :: forall a b m. Typeable a => Typeable b => Typeable (m a) => Typeable (m b) => Applicative m => (b -> m b) -> a -> m a
mkM f = fromMaybe pure (cast f)
-- Purescript can't have cycles in typeclasses
@ -225,18 +225,17 @@ unMp (Mp f) = f
-- suitable for abstract datatypes with no substructures.
-- gfoldl
-- TODO: Why do we need `TagT` here? Instead of `Typeable`.
instance dataArray :: (TagT a, Data a) => Data (Array a) where
instance dataArray :: Data a => Data (Array a) where
dataDict = DataDict \k z arr -> case A.uncons arr of
Nothing -> z []
Just x -> (z A.cons `k` x.head) `k` x.tail
instance dataMaybe :: (TagT a, Data a) => Data (Maybe a) where
instance dataMaybe :: Data a => Data (Maybe a) where
dataDict = DataDict \k z e -> case e of
Nothing -> z Nothing
Just a -> z Just `k` a
instance dataEither :: (TagT a, TagT b, Data a, Data b) => Data (Either a b) where
instance dataEither :: (Data a, Data b) => Data (Either a b) where
dataDict = DataDict \k z e -> case e of
Left a -> z Left `k` a
Right b -> z Right `k` b

View File

@ -69,15 +69,12 @@ gcast a = m # map \f -> runLeibniz f a
where
m = eqT (typeRep :: _ a) (typeRep :: _ b)
-- TODO: The following gives an Error with overlapping instances
-- The instance (Typeable (f a)) partially overlaps (Typeable (Record a)),
-- which means the rest of its instance chain will not be considered.
gcast1 :: forall s t a c. Typeable a => TagT c => TagT s => TagT t => c (s a) -> Maybe (c (t a))
gcast1 :: forall s t a c. Typeable (s a) => Typeable (t a) => c (s a) -> Maybe (c (t a))
gcast1 a = m # map \f -> runLeibniz f a
where
m = eqT (typeRep :: _ (s a)) (typeRep :: _ (t a))
gcast2 :: forall s t a b c. Typeable a => Typeable b => TagT c => TagT s => TagT t => c (s a b) -> Maybe (c (t a b))
gcast2 :: forall s t a b c. Typeable (s a b) => Typeable (t a b) => c (s a b) -> Maybe (c (t a b))
gcast2 a = m # map \f -> runLeibniz f a
where
m = eqT (typeRep :: _ (s a b)) (typeRep :: _ (t a b))
@ -145,6 +142,8 @@ data ProxyT t
foreign import proxyT :: forall t. ProxyT t
-- | This class should only be used to specify instances for your own datatypes to automatically get Typeable instances
-- | It's never necessary to use TagT as a constraint in order to use Typeable
class TagT :: forall k. k -> Constraint
class TagT a where
tagT :: ProxyT a
@ -163,10 +162,9 @@ proxyTFromTagT = coerce proxyTFromTagTImpl
-- foreign import proxyTFromTagTImpl :: forall t a. TagT t => Typeable a => ProxyT (t a)
foreign import proxyTFromTagTImpl :: forall t a. TagTDict t -> TypeableDict a -> ProxyT (t a)
-- instance typeableRecord :: (RL.RowToList rs ls, TypeableRecordFields ls) => Typeable (Record rs) where
-- typeRep = typeRowToTypeRep (typeableRecordFields (Proxy :: _ ls))
instance typeableTag1 :: (TagT t, Typeable a) => Typeable (t a) where
-- else instance typeableTag1 :: (TagT t, Typeable a) => Typeable (t a) where
instance typeableRecord :: (RL.RowToList rs ls, TypeableRecordFields ls) => Typeable (Record rs) where
typeRep = typeRowToTypeRep (typeableRecordFields (Proxy :: _ ls))
else instance typeableTag1 :: (TagT t, Typeable a) => Typeable (t a) where
typeRep = typeRepFromTag1
else instance typeableTag0 :: TagT t => Typeable t where
typeRep = typeRepDefault0

View File

@ -4,7 +4,7 @@ import Prelude
import Control.Monad.Error.Class (class MonadThrow)
import Data.Either (Either)
import Data.Typeable (class TagT, eqTypeRep, proxyT, typeRep, typeRepFromVal)
import Data.Typeable (class TagT, TypeRep, eqTypeRep, proxyT, typeRep, typeRepFromVal)
import Effect (Effect)
import Effect.Aff (launchAff_)
import Effect.Exception (Error)
@ -43,26 +43,26 @@ main = do
assert $ eqTypeRep (typeRep :: _ (Either Int Person)) (typeRep :: _ (Either Int Person))
assert $ eqTypeRep (typeRep :: _ (Array Person)) typeArrPerson
deny $ eqTypeRep (typeRep :: _ (Array Person2)) typeArrPerson
-- it "can handle bare records" do
-- assert $ eqTypeRep typeRecord (typeRep :: _ { name :: String, age :: Int })
it "can handle bare records" do
assert $ eqTypeRep typeRecord (typeRep :: _ { name :: String, age :: Int })
it "can generate type reps from values" do
assert $ eqTypeRep (typeRep :: _ (Optional Int)) (typeRepFromVal (Some 1))
deny $ eqTypeRep (typeRep :: _ (Optional Person)) (typeRepFromVal (Some 1))
-- clog (eqTypeRep (typeRep :: _ Int) (typeRep :: _ Char))
-- clog (eqTypeRep (typeRep :: _ Int) (typeRep :: _ Int))
-- clog (typeRep :: _ Char)
-- clog (typeRep :: _ Int)
-- clog (eqTypeRep (typeRep :: _ Int) (typeRep :: _ Char))
-- clog (eqTypeRep (typeRep :: _ Int) (typeRep :: _ Int))
-- clog (typeRep :: _ Char)
-- clog (typeRep :: _ Int)
-- clog (typeRep :: _ Array)
-- clog (typeRep :: _ { name :: String, age :: Int })
-- clog (typeRep :: _ (Int -> Either (Either Int Int) (Optional (Array (Person)))))
-- clog (typeRep :: _ (Either (Either Int Int) (Optional (Array (Person)))))
-- clog (typeRep :: _ (Either Int Int))
-- clog (typeRep :: _ Array)
-- clog (typeRep :: _ { name :: String, age :: Int })
-- clog (typeRep :: _ (Int -> Either (Either Int Int) (Optional (Array (Person)))))
-- clog (typeRep :: _ (Either (Either Int Int) (Optional (Array (Person)))))
-- clog (typeRep :: _ (Either Int Int))
-- where
-- typeRecord :: TypeRep { age :: Int, name :: String }
-- typeRecord = typeRep
where
typeRecord :: TypeRep { age :: Int, name :: String }
typeRecord = typeRep
-- -- A data type without a typeable instance
-- data Break