From ddbc49750609f55cff36a654b0a4a3e0e287901c Mon Sep 17 00:00:00 2001 From: Vladimir Ciobanu Date: Mon, 1 Mar 2021 23:37:49 +0200 Subject: [PATCH] docs: add note on existentials and references to it Added a note on existentials. I plan to create a subsequent PR with a note on how we use the singletons trick to recover the type inside an existential. GitOrigin-RevId: 1f227d859dcc384b4ac7e103053f643f879827d1 --- .../Hasura/Backends/Postgres/Execute/Types.hs | 1 + server/src-lib/Hasura/GraphQL/Execute.hs | 1 + server/src-lib/Hasura/Logging.hs | 30 ++++----- server/src-lib/Hasura/RQL/Types/Metadata.hs | 1 + .../Hasura/RQL/Types/Metadata/Object.hs | 1 + .../Hasura/RQL/Types/SchemaCacheTypes.hs | 1 + server/src-lib/Hasura/RQL/Types/Source.hs | 63 +++++++++++++++++++ 7 files changed, 83 insertions(+), 15 deletions(-) diff --git a/server/src-lib/Hasura/Backends/Postgres/Execute/Types.hs b/server/src-lib/Hasura/Backends/Postgres/Execute/Types.hs index f1fd66a8e54..0077587d409 100644 --- a/server/src-lib/Hasura/Backends/Postgres/Execute/Types.hs +++ b/server/src-lib/Hasura/Backends/Postgres/Execute/Types.hs @@ -27,6 +27,7 @@ import Hasura.Backends.Postgres.SQL.Error import Hasura.Incremental (Cacheable (..)) import Hasura.RQL.Types.Error +-- See Note [Existentially Quantified Types] type RunTx = forall m a. (MonadIO m, MonadBaseControl IO m) => Q.TxET QErr m a -> ExceptT QErr m a diff --git a/server/src-lib/Hasura/GraphQL/Execute.hs b/server/src-lib/Hasura/GraphQL/Execute.hs index 2387413e954..7a4ed170d12 100644 --- a/server/src-lib/Hasura/GraphQL/Execute.hs +++ b/server/src-lib/Hasura/GraphQL/Execute.hs @@ -163,6 +163,7 @@ data ResolvedExecutionPlan | SubscriptionExecutionPlan SourceName LiveQueryPlan -- ^ live query execution; remote schemas and introspection not supported +-- See Note [Existentially Quantified Types] data LiveQueryPlan where LQP :: forall b. EB.BackendExecute b => EL.LiveQueryPlan b (EB.MultiplexedQuery b) -> LiveQueryPlan diff --git a/server/src-lib/Hasura/Logging.hs b/server/src-lib/Hasura/Logging.hs index 256d5832cea..4ac73b40ad8 100644 --- a/server/src-lib/Hasura/Logging.hs +++ b/server/src-lib/Hasura/Logging.hs @@ -29,22 +29,22 @@ module Hasura.Logging import Hasura.Prelude -import Control.Monad.Trans.Managed (ManagedT(..), allocate) import Control.Monad.Trans.Control +import Control.Monad.Trans.Managed (ManagedT (..), allocate) -import qualified Control.AutoUpdate as Auto -import qualified Data.Aeson as J -import qualified Data.Aeson.TH as J -import qualified Data.ByteString as B -import qualified Data.ByteString.Lazy as BL -import qualified Data.ByteString.Lazy.Char8 as BLC -import qualified Data.HashSet as Set -import qualified Data.TByteString as TBS -import qualified Data.Text as T -import qualified Data.Time.Clock as Time -import qualified Data.Time.Format as Format -import qualified Data.Time.LocalTime as Time -import qualified System.Log.FastLogger as FL +import qualified Control.AutoUpdate as Auto +import qualified Data.Aeson as J +import qualified Data.Aeson.TH as J +import qualified Data.ByteString as B +import qualified Data.ByteString.Lazy as BL +import qualified Data.ByteString.Lazy.Char8 as BLC +import qualified Data.HashSet as Set +import qualified Data.TByteString as TBS +import qualified Data.Text as T +import qualified Data.Time.Clock as Time +import qualified Data.Time.Format as Format +import qualified Data.Time.LocalTime as Time +import qualified System.Log.FastLogger as FL newtype FormattedTime @@ -269,7 +269,7 @@ cleanLoggerCtx :: LoggerCtx a -> IO () cleanLoggerCtx = FL.rmLoggerSet . _lcLoggerSet - +-- See Note [Existentially Quantified Types] newtype Logger impl = Logger { unLogger :: forall a m. (ToEngineLog a impl, MonadIO m) => a -> m () } diff --git a/server/src-lib/Hasura/RQL/Types/Metadata.hs b/server/src-lib/Hasura/RQL/Types/Metadata.hs index ec08bd8b82d..525745b2aea 100644 --- a/server/src-lib/Hasura/RQL/Types/Metadata.hs +++ b/server/src-lib/Hasura/RQL/Types/Metadata.hs @@ -258,6 +258,7 @@ mkSourceMetadata mkSourceMetadata name config = BackendSourceMetadata $ SourceMetadata name mempty mempty config +-- See Note [Existentially Quantified Types] data BackendSourceMetadata = forall b. (BackendMetadata b) => BackendSourceMetadata (SourceMetadata b) diff --git a/server/src-lib/Hasura/RQL/Types/Metadata/Object.hs b/server/src-lib/Hasura/RQL/Types/Metadata/Object.hs index 37f7e3653c0..55a9dc768d8 100644 --- a/server/src-lib/Hasura/RQL/Types/Metadata/Object.hs +++ b/server/src-lib/Hasura/RQL/Types/Metadata/Object.hs @@ -41,6 +41,7 @@ deriving instance (Backend b) => Show (SourceMetadataObjId b) deriving instance (Backend b) => Eq (SourceMetadataObjId b) instance (Backend b) => Hashable (SourceMetadataObjId b) +-- See Note [Existentially Quantified Types] data MetadataObjId = MOSource !SourceName | forall b. (Backend b) => MOSourceObjId !SourceName !(SourceMetadataObjId b) diff --git a/server/src-lib/Hasura/RQL/Types/SchemaCacheTypes.hs b/server/src-lib/Hasura/RQL/Types/SchemaCacheTypes.hs index c5b3fc1f374..2fe65169f16 100644 --- a/server/src-lib/Hasura/RQL/Types/SchemaCacheTypes.hs +++ b/server/src-lib/Hasura/RQL/Types/SchemaCacheTypes.hs @@ -43,6 +43,7 @@ data SourceObjId (b :: BackendType) deriving (Show, Eq, Generic) instance (Backend b) => Hashable (SourceObjId b) +-- See Note [Existentially Quantified Types] data SchemaObjId = SOSource !SourceName | forall b . (Backend b) => SOSourceObj !SourceName !(SourceObjId b) diff --git a/server/src-lib/Hasura/RQL/Types/Source.hs b/server/src-lib/Hasura/RQL/Types/Source.hs index aea59a38f6c..7e19e60043e 100644 --- a/server/src-lib/Hasura/RQL/Types/Source.hs +++ b/server/src-lib/Hasura/RQL/Types/Source.hs @@ -22,6 +22,68 @@ import Hasura.RQL.Types.Table import Hasura.SQL.Backend import Hasura.Session + +{- Note [Existentially Quantified Types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +This note contains a brief introduction to existential types, along with some +examples from this codebase on how to deal with such types. + +If we consider the identity function: + + id :: forall a. a -> a + +Then for all /callers/ of this function, the type variable 'a' is universally +quantified: the caller can pick any type for 'a' when calling the function. + +On the other hand, the /implementer/ of this function cannot pick an 'a'. From +this perspective, the type variable 'a' is existentially quantified. + +Let's consider a rank-2 function: + + rank2 :: forall a. (forall b. b -> String) -> a -> String + +In this example, the /caller/ gets to pick 'a' since it's universally quantified, +but 'b' is existentially quantified from this perspective. We have to provide +a function that works for any 'b' the implementer may pick! + +From the perspective of the /implementer/, 'a' is existentially quantified, +whereas 'b' is universally quantified: we (the implementers) get to pick +'b' (and we may call it multiple times with different types!). + + +One thing that we cannot do is we cannot return an existentially quantified +value. In order to do that, we need to wrap it in a constructor, e.g.: + + data Exists = forall a. Exists a + +Normally, type variables that appear on the right hand side of a type declaration +also appear on the left hand side. This is precisely what existential quantification +relaxes. + +IMPORTANT: please keep in mind that existential types /erase/ all type information. + +Similarly to implementing the 'id' function), there are few functions we can write +without more context: + + idExists :: Exists -> Exists + idExists (Exists a) = Exists a + + existsList :: Exists + existsList = [ Exists "hello", Exists (Just '1'), Exists (42 :: Int) ] + + +However, we can't do anything else: we cannot recover the original values or do +any operations. The way to deal with this problem is to pack a dictionary along +with the value. The most common example is 'Showable': + + data Showable = forall a. Show a => Showable a + + showShowable :: Showable -> String + showShowable (Showable a) = show a + +We are able to call 'show' on 'a' because we are /packing/ the 'Show' constraint +along with the value. This is key to using existential types. -} + data SourceInfo b = SourceInfo { _siName :: !SourceName @@ -33,6 +95,7 @@ $(makeLenses ''SourceInfo) instance Backend b => ToJSON (SourceInfo b) where toJSON = genericToJSON hasuraJSON +-- See Note [Existentially Quantified Types] data BackendSourceInfo = forall b. Backend b => BackendSourceInfo (SourceInfo b)