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
This commit is contained in:
Vladimir Ciobanu 2021-03-01 23:37:49 +02:00 committed by hasura-bot
parent 01cb59919f
commit ddbc497506
7 changed files with 83 additions and 15 deletions

View File

@ -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

View File

@ -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

View File

@ -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 () }

View File

@ -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)

View File

@ -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)

View File

@ -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)

View File

@ -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)