Poor performance during normalization

[vmchale]

Running dhall on pkg-set.dhall takes quite long, around 23 seconds.

Here is the .prof file:

	Sat Dec 29 22:56 2018 Time and Allocation Profiling Report  (Final)

	   dhall-profile +RTS -h -p -RTS

	total time  =       22.54 secs   (22541 ticks @ 1000 us, 1 processor)
	total alloc = 40,573,140,648 bytes  (excludes profiling overheads)

COST CENTRE               MODULE                                             SRC                                                                         %time %alloc

renderIO                  Data.Text.Prettyprint.Doc.Render.Terminal.Internal src/Data/Text/Prettyprint/Doc/Render/Terminal/Internal.hs:(171,1)-(210,58)   22.3   14.6
normalizeWithM            Dhall.Core                                         src/Dhall/Core.hs:(1571,1)-(1952,29)                                         21.6   25.6
normalizeWith             Dhall.Core                                         src/Dhall/Core.hs:1568:1-52                                                   8.3   24.9
toList                    Dhall.Map                                          src/Dhall/Map.hs:485:1-55                                                     5.4    2.7
shift                     Dhall.Core                                         src/Dhall/Core.hs:(801,1)-(973,29)                                            5.3    5.9
denote                    Dhall.Core                                         src/Dhall/Core.hs:(1484,1)-(1550,39)                                          5.0    3.5
styleToRawText            Data.Text.Prettyprint.Doc.Render.Terminal.Internal src/Data/Text/Prettyprint/Doc/Render/Terminal/Internal.hs:(278,1)-(304,29)    4.2    3.8
unorderedTraverseWithKey_ Dhall.Map                                          src/Dhall/Map.hs:476:1-80                                                     3.6    0.5
csi                       System.Console.ANSI.Codes                          src/System/Console/ANSI/Codes.hs:75:1-75                                      3.4    5.4
prettyCharacterSet        Dhall.Pretty.Internal                              src/Dhall/Pretty/Internal.hs:(321,1)-(886,61)                                 2.7    1.1
layoutWadlerLeijen        Data.Text.Prettyprint.Doc.Internal                 src/Data/Text/Prettyprint/Doc/Internal.hs:(1693,1)-(1752,60)                  2.7    2.8
sort                      Dhall.Map                                          src/Dhall/Map.hs:(178,1)-(180,24)                                             1.9    1.2
uncons                    Dhall.Map                                          src/Dhall/Map.hs:(308,1)-(309,78)                                             1.6    0.3
changesUponFlattening     Data.Text.Prettyprint.Doc.Internal                 src/Data/Text/Prettyprint/Doc/Internal.hs:(535,1)-(573,21)                    1.3    1.1
setSGRCode                System.Console.ANSI.Codes                          src/System/Console/ANSI/Codes.hs:197:1-52                                     1.3    1.2
subst                     Dhall.Core                                         src/Dhall/Core.hs:(980,1)-(1143,29)                                           1.2    1.1

As you can see, normalizeWithM takes quite a lot of time. I am not quite sure why - I haven't inserted profiling pragmas - but the performance is not where it should be.

I suspect this is because lookups/etc. during normalization are performed using values of type Text; if identifiers were interned then the dhall library would likely have more sensible performance.

Thanks again.

[Gabriella439]

Here is a complete profile that I collected locally: dhall.prof.gz

I'm using profiteur to browse that profile and the main thing I notice so far is that most of the time is spent type-checking either unions or records (I need to add more annotations to be sure which one it is). Interestingly, producing the final normalized expression is only a small fraction of the total running time and the huge cost attribution that you see to normalizeWithM is slightly misleading because that is due to normalization cost incurred in the process of type-checking the expression (such as here)

I also confirmed this by turning off type-checking which sped up the (profiled) program 4x and when I profiled that the majority of the remaining cost was rendering the expression. Here is the diff:

diff --git a/dhall/src/Dhall/Import.hs b/dhall/src/Dhall/Import.hs
index c474de9..2d3a2f1 100644
--- a/dhall/src/Dhall/Import.hs
+++ b/dhall/src/Dhall/Import.hs
@@ -518,8 +518,6 @@ exprToImport here expression = do
         Just expectedHash  <- return hash
         cacheFile          <- getCacheFile expectedHash
 
-        _ <- throws (Dhall.TypeCheck.typeWith _startingContext expression)
-
         let normalizedExpression =
                 Dhall.Core.alphaNormalize
                     (Dhall.Core.normalizeWith
@@ -660,10 +658,6 @@ exprFromUncachedImport (Import {..}) = do
                             _ ->
                                 Annot expr expected
 
-                    case Dhall.TypeCheck.typeOf annot of
-                        Left err -> liftIO (throwIO err)
-                        Right _  -> return ()
-
                     let expr' = Dhall.Core.normalize expr
 
                     case toHeaders expr' of
@@ -818,9 +812,7 @@ loadWith expr₀ = case expr₀ of
                     --
                     -- There is no need to check expressions that have been
                     -- cached, since they have already been checked
-                    expr''' <- case Dhall.TypeCheck.typeWith _startingContext expr'' of
-                        Left  err -> throwM (Imported imports' err)
-                        Right _   -> return (Dhall.Core.normalizeWith (getReifiedNormalizer _normalizer) expr'')
+                    expr''' <- return (Dhall.Core.normalizeWith (getReifiedNormalizer _normalizer) expr'')
                     zoom cache (State.modify' (Map.insert here (hereNodeId, expr''')))
                     return expr'''
 
diff --git a/dhall/src/Dhall/Main.hs b/dhall/src/Dhall/Main.hs
index d791145..993cf5d 100644
--- a/dhall/src/Dhall/Main.hs
+++ b/dhall/src/Dhall/Main.hs
@@ -294,14 +294,10 @@ command (Options {..}) = do
 
             resolvedExpression <- State.evalStateT (Dhall.Import.loadWith expression) status
 
-            inferredType <- throws (Dhall.TypeCheck.typeOf resolvedExpression)
-
             let normalizedExpression = Dhall.Core.normalize resolvedExpression
 
             let annotatedExpression =
-                    if annotate
-                        then Annot normalizedExpression inferredType
-                        else normalizedExpression
+                        normalizedExpression
 
             render System.IO.stdout annotatedExpression

... and here is the corresponding profile: dhall.prof.gz

So now I'm trying to figure out why type-checking the expression is significantly more expensive.

[Gabriella439]

So once #1048 is merged the interpretation time is about 16.5 seconds on my machine. After profiling that the next bottleneck appears to be type-checking a record of record types, but I might be misinterpreting the profile.

If that interpretation were correct, then I thought it would most likely be due to type-checking this expression:

https://github.com/vmchale/cpkg/blob/master/dhall/cpkg-types.dhall

... which is a record literal containing record types. That in turn would suggest that the record is type-checked repeatedly because it triggers the slow path of this substitution logic:

dhall-haskell/dhall/src/Dhall/TypeCheck.hs

Lines 176 to 196 in 92bdd56

	-- The catch-all branch directly implements the Dhall
	-- specification as written; it is necessary to substitute in
	-- types in order to get 'dependent let' behaviour and to
	-- allow type synonyms (see #69). However, doing a full
	-- substitution is slow if the value is large and used many
	-- times. If the value being substitued in is a term (i.e.,
	-- its type is a Type), then we can get a very significant
	-- speed-up by doing the type-checking once at binding-time,
	-- as opposed to doing it at every use site (see #412).
	case Dhall.Core.normalize t of
	Const Type -> do
	let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x (Dhall.Core.normalize _A1) ctx)
	_B0 <- loop ctx' rest
	let _B1 = Dhall.Core.subst (V x 0) a2 _B0
	let _B2 = Dhall.Core.shift (-1) (V x 0) _B1
	return _B2
	_ -> do
	let b1 = Dhall.Core.subst (V x 0) a2 rest
	let b2 = Dhall.Core.shift (-1) (V x 0) b1
	loop ctx b2

Specifically, if you let-bind anything that is not a term (such as a record of types), it has to be substituted into all use sites and type-checked at each site (instead of being checked just once where it is let-bound) in order for type synonyms to work. For example, the cpkg project let-binds the cpkg-types.dhall record as a bound variable named types and then accesses types from that record repeatedly.

However, I tested that hypothesis by creating a modified cpkg branch where every type was imported directly instead of accessed via a record and that change had absolutely no effect on performance:

vmchale/cpkg@master...Gabriel439:gabriel/speedup

... so I think I must be misinterpreting the performance profile. However, I thought I would share that branch anyway since it narrows down the possible performance issues.