Discussion: elaboration overhaul

[AndrasKovacs]

I'll give here a report on elaboration overhaul, also referenced in #1039.

Background

In April I made the nbe-elaboration branch, which demonstrates significant speedups. It also mostly implements the Dhall standard as of April, and most of the dhall commands and functionality as well. Concretely, features not recovered were (compared to the April state of master):

• dhall repl
• Custom HTTP headers
• Compatibility with other packages in dhall-haskell (I haven't tested or tried if they work).
• Local caches of frozen imports. However, I'm confident that this would have been net negative for performance, if implemented with the same semantics as in April master. The newer semi-semantic caching semantics seems more beneficial.
• The Dhall library module.

However, nbe-elaboration deviated a lot from master. The github PR diff says 3,980 additions and 6,423 deletions. Typechecking, imports and type errors were changed most, serialization, pretty printing and diffing were largely unchanged, and Expr also didn't change. Then, I got busy with academic things, and I didn't touch this project until last weekend.

In the summer, the activity in dhall-haskell ramped up, so I became more concerned about trampling the work of the current highly active contributors. Hence, my plan was to review nbe-elaboration and also the new features in master, and try to split the elaboration update into multiple less invasive pull requests.

However, when I started doing this, and tried to fix infelicities in nbe-elaboration, I actually started doing even more refactoring and compatibility-breaking, because there are some issues which should be rectified. I expand on this a bit more.

Phase separation

By "phase separation" I mean that we have a clear and enforced distinction between raw syntax and well-formed syntax. This is a completely standard technique, implemented in pretty much all functional language compilers with the exception of Dhall. I summarize the idea below, though I imagine many of you are familiar with this already, and in particular GHC is well-known for this.

1. Raw syntax supports elaboration into well-formed core syntax, but basically no other operation. Sometimes, as in GHC, raw syntax goes through scope checking as a separate step, yielding well-scoped syntax, which additionally supports renaming. For completely raw syntax, renaming, substitution, evaluation, serialization, etc. are all useless operations, because we have no idea whether we produce well-formed output. E.g. if we serialize an ill-typed term, the only thing we can do with that is to deserialize it and have it rejected by the type checker immediately afterwards.
2. The separation of core and raw syntax allows specializing each to its purpose. Raw syntax can be less verbose and support syntactic sugar, and can change frequently without disrupting much of the codebase. Core syntax can store all information necessary for convenient processing, evaluation and fast re-checking (for validation and linting purposes), and a well-chosen set of core primitives can support a wide variety of surface syntaxes, thereby facilitating a stable codebase. Deprecation is also better with this setup, because often we can purge a deprecated feature from core while still supporting it in raw syntax via desugaring.

In Dhall, we have a single Expr s a type, where s in practice is used for source locations and a is used for imports. Raw syntax, checked syntax, import-resolved syntax and normal syntax are all Expr. This provides a rather small amount of phase distinction, and there are many functions throughout the codebase which are polymorphic in s and/or a, although they only make sense on expressions known to be in a specific phase. For example, we can blithely serialize raw terms.

The reason why this setup functions in current Dhall is because of the heavily annotated raw syntax. We usually need explicitness in core syntax, but the raw syntax is already explicit, so why not reuse the same type for both? However, this doesn't work out well. I list the issues below.

1. Core syntax is actually not explicit enough

This is the biggest issue in relation to my elaboration overhaul. In short, there are no universe (Type, Kind, Sort) annotations in required places, which prevents us from elaborating in an optimally efficient way. Sometimes we need the universe of a type, but we obviously don't want to get it by inferring a type for an already elaborated type. That would be phase violation, i.e. recomputing something which should be already known. In nbe-elaboration, I didn't care about this issue, and just hacked around it by computing universes as needed via normalizing and rechecking types. I thought that it'd be possible to do this the proper way by threading universes through check and infer. However, this solution is blocked when we are checking lambdas, because we can't recover the universes of function domains and codomains from the universe of the function type itself. So at least function types should be universe-annotated in core syntax.

But we clearly don't want universe annotations on functions in the surface syntax! Hence, core and raw syntax should be just different. But you may ask, why not just put Maybe Const annotations on Pi, and have no annotations in raw syntax, and annotations in core syntax? Or add another type parameter to Expr for extra annotations, setting it to () for raw syntax? My answer would be a big nope. In fact, I already find the Maybe (Expr s a) type annotations on list literals, Merge and ToMap rather bad. Degrees of freedom with respect to type annotations should belong to surface syntax and not core syntax; the latter should be just simply annotated sufficiently all the time, without unwieldy invariants for e.g. annotating only empty list literals. Bidirectional checking plus regular : annotations can take care of this in the surface language.

2. Raw syntax is too explicit

This is not strictly related to performance improvements, but since I'm already writing about related topics in detail, I shall mention this as well. Basically, any straightforward and efficient implementation of elaboration is bidirectional; otherwise we are discarding known typing information, performing more conversion checking than necessary. But bidirectional typing allows us to omit many typing annotations in surface syntax. In particular, inferring many lambda argument types are almost trivial to implement with bidirectional setup. That we have a number of choices about implicit/explicit annotations in surface syntax, is also in favor of separating it from core syntax. And I'm pretty sure inferred lambda types would be a big UX win.

3. Lack of phasing allows bad implementations to go through

With enforced phasing, GHC's type checker rejects some bad implementations, or at least forces us to reconsider. An example for this is the current implementation of import resolution, which re-checks and re-normalizes the same expressions over and over again. If we clearly typed elaboration to yield core syntax from raw syntax, this would not be well-typed as it is, and would require some explicit back-conversions or coercions. Perhaps I am a bit uncharitable here, because a correctly phased implementation of import resolution (and similarly: elaboration of let-definitions) really requires the semantic/NbE checking algorithm, but in any case this doesn't subtract from the argument in favor of phasing.

Plans & Discussion

As I mentioned, my prior plan was to do multiple moderately invasive merges. But now I think that even more invasive changes are justified, and I don't feel much motivation for working around the mentioned issues.

I believe I can do this summer a fully or mostly standard-compliant branch which includes strict phasing together with the new elaboration, and since I'll be changing core syntax in any case, I can also throw into the mix additional optimizations for evaluation and conversion checking which require additional core syntax change. Inferred lambda types is a trivial extension, as I mentioned, so perhaps it can be an optional feature as well.

Expected changes would be:

• Major: typechecking, import resolution, error handling, module organization, REPL
• Moderate: testing (some restructuring needed, e.g. open terms changed to closed terms in normalization tests, because we'll only be able to support normalizing well-typed core syntax),
• Minor: AST for core syntax, parsing, serialization, diffing, printing.

Compatibility with external packages should not be hard, since changes to AST would be minor, and the same or more information would be available from elaboration as before.

The issue of not trampling code of current contributors is unfortunately not really addressed here. I've looked at the things @sjakobi and @EggBaconAndSpam are working on right now, and if my overhauled branch is eventually merged here, I'm relatively confident that code I will not be able to reuse or borrow will be:

• Core.hs splitting, refactoring and similar things, because my version is already heavily refactored
• Infrastructure for import resolution, because nbe-elaboration already has a heavily modified "recursive" import resolution which is also interleaved with elaboration.

I can likely still reuse some code for semi-semantic caching.

I don't want to convey the message that "stop working on typechecking and imports". For one thing, all I'm giving right now is vague promises, and from what we know, my branch could be vaporware, in which case we're better off with you working on typechecking and imports.

So, my general proposal is that I start implementing a standards-compliant branch, which is based on nbe-elaboration and includes major reorganization. I will also write documentation which explains the design choices and algorithms. And when this branch becomes robust and complete enough, you can evaluate it, and decide if merging is a good idea.

Comments and discussion are welcome.

[ocharles]

On point two, you can provide a less explicit syntax because your doing bidirectional type checking, but that is not a requirement. The requirements are set out by the standard, and the standard doesn't have as much inference as we'd like due to the complexity of standardizing it. That said, I think better inference is almost a requirement if Dhall is too succeed, I'm a very experienced Dhall user and I find it frustrating enough to have to provide types when the computer could figure it out. But it's somewhat orthogonal to just Haskell work

[ocharles]

a correctly phased implementation of import resolution (and similarly: elaboration of let-definitions) really requires the semantic checking algorithm

What is "the semantic checking algorithm"? The page you linked to has no mention of it, and only three mentions of "semantic"

[AndrasKovacs]

What is "the semantic checking algorithm"?

It is just the typechecking algorithm described in the post, a synonym for "NbE checking", perhaps the word choice is not ideal if the linked post itself doesn't use it. I have heard "semantic checking" from some other people, specifically @jonsterling, and I like it better than NbE because in principle the essence can be implemented without using NbE.

The requirements are set out by the standard, and the standard doesn't have as much inference as we'd like due to the complexity of standardizing it

True. I think the longer term solution is to standardize Dhall core instead of the surface language. Then the standardized part will be explicitly annotated, will support simple type checking, and could be probably simpler than what's in the standard now. I think the standard already has the intention/spirit for describing a core language.

[jonsterling]

(I believe I learned the term "semantic type checking" from either Andreas Abel or Thierry Coquand)

[Gabriella439]

@AndrasKovacs: My main feedback is that major and invasive changes are absolutely okay (in fact, they are welcome!), but I very strongly advise against long-lived unmerged branches. Instead, we should split your proposed changes into smaller changes, each of which we'll merge and review in sequence. The rough rule of thumb is that you should probably not go longer than a week without merging something into master.

One thing that I should clarify is that it's totally fine to merge invasive changes even if they haven't paid off, yet. For example, as you noted, we probably need two separate syntax trees (one for raw syntax and one for core syntax). We don't need to wait until the elaboration overhaul is done to begin making invasive changes like that. If you were to open up a pull request tomorrow that just added a new intermediate syntax tree with no immediate benefit I'd still merge it because I'm convinced that it is a necessary stepping stone along the way to fixing these issues.

So before you restart this effort, take some time to think about what are the self-contained, independently mergeable changes that are each only a few days to a week of work at most. It may slow things down in the short run to plan and break up the work into smaller functional units, but will ensure that in the worst case scenario you never lose more than a few days of work and greatly improves the likelihood of this project running successfully to completion.

[AndrasKovacs]

@Gabriel439 Okay. I'll think about what should be an appropriate chunk. I'll post some updates here, and will try to PR something in the next week.

By the way, what is an acceptable functionality regression on merges like this?

[Gabriella439]

@AndrasKovacs: I can't say for sure without knowing the specifics, but I can list off some regressions we've permitted in the past to give some reference point:

• Tolerating some minor deviations from the standard

  ... such as in whitespace handling or treating something as a type-checking vs. parsing failure

• Disabling certain tests if they are difficult to maintain

• Performance regressions

  For example, I'd easily tolerate a 5-10% regression (maybe even higher), knowing that it will go away once this work is done

• Breaking changes to the API if the API was poorly thought out

  I don't mind at all forcing users of the API to do things in a new way if the new way is better since we have types to guide them, but if it's not too difficult I'll still try to maintain backwards compatibility.

• Deleting API functionality if it's rarely used

The thing I want to emphasize is that no change is too small or trivial to merge. In fact, smaller changes are actually preferred. The mental model I have for these things is like software transactional memory in Haskell: the smaller the transactions the less contention they will have and the more likely they will make progress. If you think of pull requests as analogous to STM transactions and contributors as analogous to concurrent threads, then you're less likely to run into pull request "starvation" in the presence of multiple contributors if each pull request is small.

I also have been encouraging @EggBaconAndSpam to split up his pull requests into smaller ones for the exact same reason: to reduce the likelihood of his work conflicting with yours.

[AndrasKovacs]

I've done some exploration of different versions of core and raw syntax. I'd like to write first about the

Language Standard

I mentioned before that I'd like to have universe annotations on Pi, in the form of two Const -s, in order to avoid inefficiencies. It seems that the standard should be changed to support this. Let's see some solutions and non-solutions.

First, a non-solution: simply adding universe annotations to the standard. This doesn't work because I'm confident that no user wants to write these annotations (e.g. as forall (x : a : Type) -> b : Type).

Second: changing the standard so that it allows specified annotations to be omitted from the surface syntax in implementations. This would be also useful for inferred lambda types, empty list types, etc.

Third: dropping mandatory caching from the standard. Now, this is not so obvious, but once we drop caching, implementations have significant freedom to use whatever core syntax they like. Reasons are as follows. Currently, hashes and caches are specified using the same syntax. If I want to use more efficient internal syntax, e.g. one with more annotations, I can't use the specified syntax for efficient caching. For example, if I serialize an expression without universe annotations (as specified by standard), then I have to recheck it upon deserialization, in order to recover the missing annotations, and of course rechecking defeats the purpose of caching.

So, the solution to not specify/require caching, only hashing. For an example for how this works, assuming that I internally use universe-annotated syntax, I can hash my internal syntax according to the standard by simply ignoring the extra annotations. And for implementation-specific caching, I can use generics or TH for serialization, and that way I don't have to manually fiddle with tag integers in order to sync with the standard.

Fourth, a combination of the previous two: featuring allowance for inferred annotations, and caching left entirely to implementors. I think that this is the best option. This change can be also done in a PR which is completely backwards compatible, because it strictly increases the details left to implementation.

---

I'll do a PR on the language standard soon-ish, maybe tomorrow, so that I am not doomed to non-compliance, but first I'll wait for some comments here.

Workflow & Regressions

Secondly, I want to address comments on merging and workflow. In short, I don't think I am able to deliver a branch, which simultaneously

• stays unmerged for no longer than a week.
• has acceptable feature regressions, according to the previous post in this thread.
• has a meaningful diff pointing in the direction of the planned overhaul.

This was my sentiment originally in OP. I again considered more incrementalization, but I don't see really important or useful stuff which I can do in less than a week. Some less invasive optimizations, e.g. using full dB indices in variables, would be doable, but they would be equally doable after the elaboration overhaul. I also don't see much use for just committing a separate raw syntax type, because it's not compatible with the current type checker, and it would be dead code in any case without my elaboration implementation.

What I can try is to have a minimal package which includes the new elaborator without too much design compromises, but no inessential bells and whistles. But even this would feature large changes in types and APIs in checking and imports, and some code would be factored out of existence, or would be unusable under new APIs. So I generally stand by my proposal in the OP, that I can try to do a standards-compliant overhauled branch (with compliance requiring standards changes!), and try to reuse current and future master code whenever possible.

[f-f]

@AndrasKovacs all good points, some questions from the standard point of view:

• Re second point: I'm all for allowing some annotations to be omitted from the surface language in some places, but wouldn't this force other implementations to implement inference? (I mean in cases in which we'd allow currently required annotations to be optional instead)
• Re third point: I think we'll want to keep the caching standardized to prevent hitting the network if not necessary. However, would it help to change the binary representation (the one used for caching) to accommodate some more (optional, additional) annotations?

[Gabriella439]

I vote for option 3 (dropping mandatory caching), and I suggest two possible variations

• require some form of caching, even if it is not the form of caching described within the standard
• still require that the implementation write out the cache file even if the file is not used by the same implementation

The reason I suggest requiring some form of caching for imports protected with an integrity check is so that users can rely on the security guarantee that a frozen import is never retrieved more than once. This mitigates the exposure from attackers using the presence of import requests to track or monitor a user of the language.

The reason I suggest writing out the cache file is so that other implementations can benefit from the cached output, although I don't feel that strongly about this suggestion.

[Gabriella439]

Also, another thing I want to note: one of the things that limits us in the standard is the fact that it's using natural deduction as a language-independent semantics, but right now we're really hitting the limit of what we can express because it's not a real programming language that can be machine-checked and it allows a lot of room for imprecision.

The reason I mention this is in response to one of the proposed ideas:

changing the standard so that it allows specified annotations to be omitted from the surface syntax in implementations

This would be easier to do in the standard if the standard was a proper typed language where we could distinguish in the types between surface syntax and core syntax. So I think if we want to go down a route like that we should invest in porting the standard to a proper language like either Agda or a reference implementation in Haskell that is greatly simplified compared to this one.

[AndrasKovacs]

@f-f

wouldn't this force other implementations to implement inference?

Yes. But a) it would demand a relatively small implementation effort b) the standard could include bidirectional typing rules which would make implementation more obvious. I admit that b) would be a larger standards addition/change.

change the binary representation (the one used for caching) to accommodate some more (optional, additional) annotations?

The problem is, we need to handle optional annotations on deserialization, and that's not good if we need annotations to be always available. We'd need to distinguish between definitely annotated caches and optionally annotated caches, and I think this is a complication that should be avoided if possible.

@Gabriel439

The reason I suggest requiring some form of caching for imports protected with an integrity check is so that users can rely on the security guarantee that a frozen import is never retrieved more than once.

Interesting point!

one of the things that limits us in the standard is the fact that it's using natural deduction as a language-independent semantics,

I don't think that's much of a limitation, informal spec seems just fine to me, and we can be as precise as we want. In the absence of serious efforts directed towards proofs about Dhall (e.g. of type safety), and towards verified implementation, I don't think formal spec would provide enough benefits to offset the costs.

[Gabriella439]

There's another reason not to use optional annotations in the serialization format, which is that it would lead to inconsistent hashes between implementations depending on whether or not they used those optional annotations.

[Gabriella439]

Also, I forgot to comment on the second option: allowing annotations to be omitted and inferred. This basically comes down to whether or not it is easy to standardize and mirror to other existing implementations. I'd have to see whether or not the proposed change was invasive or not.

[Gabriella439]

@AndrasKovacs: So I'm taking a closer look at this again based on the discussion in #1306 to see if I can find ways to break up the work into smaller pieces. In order to do that I need to try to better understand what you are proposing by trying to phrase it in my own words.

One thing that would help me better understand this is specifying the phase distinctions you had in mind in terms of type signatures for the core program transformations.

Here is what I think you meant, and please correct me if I misunderstand.

First, you are proposing that the Haskell implementation have essentially two types, which for simplicity I will call RawSyntax and WellFormedSyntax:

• RawSyntax - Syntax that is not guaranteed to be well-typed
• WellFormedSyntax - Syntax that is well-typed

In the current Haskell implementation, I believe that you intend Expr to play the role of RawSyntax and possibly intend Val to play the role of WellFormedSyntax, but as a precaution I'll use RawSyntax/WellFormedSyntax for the rest of this comment to minimize confusion in case that assumption is wrong.

If we distinguish between those two types, then we need to change the types of the three core utilities: load, typeOf, and normalize. Specifically, their (rough) types would become:

load :: RawSyntax -> IO ???  -- This is the one I'm not sure about

-- I think this step is what you refer to as elaboration?
typeOf :: RawSyntax -> Either TypeError WellFormedSyntax

The type of typeOf leads to the nice emergent property that we never type-check code twice. Any attempt to check or infer the type of a well-formed expression is a type error.

I also believe that you are saying that if we make that phase distinction then it naturally forces us to do the right thing and add additional information (e.g. universe annotations to bound variables) to WellFormedSyntax because the types won't let us wastefully infer the same information twice.

So the next question is: what type does load return? My understanding is that you actually want to combine load and typeOf into a single function of type:

loadAndTypeOf :: RawSyntax -> IO (Either TypeError WellFormedSyntax)

... and that if we force our implementation to use that type then it will protect against duplicating work (such as when we have a long chain of transitive imports)

Does that sound correct so far? Also, have I missed anything not covered by that summary?

[AndrasKovacs]

@Gabriel439

First, I'm sorry to have disappeared over the summer. I lost some productive weeks to sickness, and the rest to some research projects which came up at my university. With the start of the semester, I have limited time right now and also in the coming weeks. Unfortunately I've found that doing what I proposed in the OP in this thread is substantial unpaid work that I don't really have time or resources for, except in very specific parts of the year; I hoped to sprint through it in the summer season but that didn't work out.

My understanding is that you actually want to combine load and typeOf into a single function of type.

That's correct. I just briefly summarize below the designs which I previously thought sensible, also partially included on my unfinished branch:

Types for syntax:

• Raw syntax which corresponds exactly to surface syntax. Only supports elaboration as operation, nothing else.
• Well-formed syntax which supports evaluation and perhaps renaming and substitution. Imports are already resolved here.
• Well-formed normal forms, which contain no import expressions. Supports serialization and de-serialization.

I thought that distinguishing normal forms and well-formed syntax was sensible, because we only serialized import-free normal forms. I don't know though if that's still the case. I used an Expr i for both, with i standing for imports.

Elaboration:

Elaboration goes from raw syntax to well-formed syntax. Imports are resolved during elaboration. There is no load function, whenever elaboration hits an import expression, if the import is not already elaborated, it elaborates the imported expression recursively and lazily computes its Val value, normal form and hash, and stores these into the output. This is important, because we never want to recompute or recheck anything in relation to imports. Hence, elaboration context already includes all information necessary for import resolution.

Function types are roughly:

 infer :: Context -> RawSyntax -> ElabMonad (WellFormedSyntax, Val)
 check :: Context -> RawSyntax -> Val -> ElabMonad WellFormedSyntax

Both Val-s are actually types, in infer it's an inferred type, in check it's the expected one. The ElabMonad in my implementation was ReaderT ImportState IO, following the ReaderT pattern, with all the stuff related to imports contained in ImportState, and errors thrown as exceptions.

Since there is no load, options for import resolution (e.g. freezing or disallowing imports) are included in ImportState.

Algorithm for elaboration is described here, or in checking-only form here, and here, for example. The main divergence from dhall-haskell is that the elaboration Context must contain Val-s for every let-defined thing and for every type in the context. My version was:

data Cxt = Cxt {
    _values :: !Env   -- ^ Values of bindings.
  , _types  :: !Types -- ^ Types of bindings.
  , _names  :: !Names -- ^ Names of binders.
  , _lvl    :: !Int   -- ^ Size of the context.
  }

[Gabriella439]

@AndrasKovacs: Yeah, no worries! I understand it's quite a bit of work, especially with the rate of changes coming in. This is why I'd like to try my hand at it because I have enough context about incoming changes to minimize code conflicts. The main thing is that I'll periodically ask you clarifying questions since I'm still pretty new to how elaboration works.

Speaking of which, I have few follow-up questions:

• (Ignoring import resolution) Are type-inference and elaboration the same thing or two different things?
• What is the difference between Val and WellFormedSyntax?
• Are there any books that explain these common patterns you describe?

[AndrasKovacs]

@Gabriel439

Are type-inference and elaboration the same thing or two different things?

The common terminology is that elaboration outputs well-formed syntax from raw syntax, and the two syntaxes are not the same. Type inference is inferring types which are not explicitly given. It may happen during elaboration, the amount depends on the sophistication of the elaborator.

What is the difference between Val and WellFormedSyntax?

Val are runtime objects, well-formed syntax is immutable machine code which yields runtime values when evaluated. E.g. a Lam in the syntax is the instruction for allocating a runtime VLam closure. The difference is not striking when both are plain data AST-s. In principle, we could compile syntax to machine code and keep Val almost the same, and then the difference would be more striking.

Are there any books that explain these common patterns you describe?

There aren't. The longest document I know is David Christiansen's. There's something of a growing consensus among the enthusiasts that the best basic implementation is what's described there and in my previous links. Opinions are more varied on best ways to do industry-strength implementation.

[Gabriella439]

@AndrasKovacs: Alright, the first thing I noticed is that we probably need to make a breaking change to drop support for normalizing expressions with custom imports, but I wanted to confirm with you just to be sure.

My understanding from studying the first commit on your nbe-elaboration branch (b65788b) is that we ultimately want the type of normalize to be:

normalize :: Expr s ResolvedImport -> Expr t Void

... which would not work if normalize was polymorphic in the Import type as it currently is:

-- current type on `master`
normalize :: Eq a => Expr s a -> Expr t a

Does that sound correct to you? If so, I can go ahead and make an initial breaking change to specialize the type of normalize to:

normalize :: Expr s Void -> Expr t Void

... which will then pave the way for the more correct type in a subsequent change.

[AndrasKovacs]

@Gabriel439 yes, if currently the intention is that only resolved expressions should be normalized, then Expr _ Void -> Expr _ Void makes sense. The ultimate type for normalize is right as well.

As a note, I would drop (did drop) the s/t params from core syntax, because it's only used for source position reporting in errors, and for that purpose it's sufficient and most sensible to put positions in raw syntax, where they're relevant during elaboration. In general, raw syntax is also the only syntax which corresponds exactly to source files, e.g. it's not possible to sensibly position-annotate core terms which don't originate from a source file, but instead originate from type inference.

[Profpatsch]

Small question, if I have something like

let
  unused = https://expensive-import.com
in 42

Would the expensive import be done after switching to elaboration?

[AndrasKovacs]

@Profpatsch: the expensive import will be elaborated, but will not be evaluated, normalized or hashed. Also, it will be elaborated at most once.

[Gabriella439]

@AndrasKovacs: Yeah, I can also set the s/t type parameter to Void for everything other than the input to elaboration since we only use source spans for type errors

[Gabriella439]

@AndrasKovacs: One small question: I noticed that for many of your monomorphic list-like types (such as Ctx, Env, Types, Names, etc.), you put the tail of the list first and the head of the list second, like this:

data Names
  = NEmpty
  | NBind !Names {-# UNPACK #-} !Text
       --  ↑ tail                ↑ head
  deriving Show

Is there a performance reason for doing things this way or is it only a stylistic preference?

[AndrasKovacs]

@Gabriel439: it's the standard ordering in formal syntax of type theories, where it's not really possible to define context extension the other way. In Agda I could have

Con   : Set                    -- contexts
Ty    : Con → Set              -- types in a context
empty : Con                    -- empty context
_,_   : (Γ : Con) → Ty Γ → Con -- extended context

Where, because types depend on contexts, we can't swap the order of parameters in context extension. Also, it's more visually correct to have snoc-lists when we have de Bruijn indices, because we want the rightmost entry in the context to be the outermost constructor.

Of course, cons lists are the same as snoc lists, and we can use cons lists with exactly the same performance characteristics as snoc lists, but I have found snoc lists to be more convenient, because I don't have to mentally reverse them.

[Gabriella439]

Alright, after studying @AndrasKovacs's branch I think I have a much better understanding of what is the smallest self-contained change to make that fixes the type-checking performance regression in #1306. The simplest way to explain the change is to revisit why we got the above performance regression.

Before the switch to dependent types, we had a type-checking "fast path" for let expressions that would only add the bound variable's type to the Context (cheap) instead of substituting the let-bound expression everywhere within the syntax tree (expensive).

For example, it leads to a pathological slowdown for the following use pattern from cpkgs:

let prelude = ../dhall/cpkg-prelude.dhall  -- The right-hand side is a giant record

in  {- code with 1000+ occurrences of accessing some field of this `prelude` record -}
    … prelude.showVersion … prelude.writeFile … prelude.unbounded …

... because the giant prelude record is substituted 1000+ times and each occurrence of this giant record needs have its type re-inferred again because we don't store the record's inferred type anywhere (not even in the Context).

This fast path was no longer correct once we switched to dependent types, so we ended up using the slow path everywhere, leading to the performance regression.

However, it turns out that you can actually fix the problem by implementing a variation on the original fast path: just extend the Context to store not only types, but also values, too. In other words, you begin by changing the type of typeWith from this:

typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s X) (Expr s X) 

... to this:

data Entry s a = Entry { entryType :: Expr s a, entryValue :: Maybe (Expr s a) }

typeWith :: Context (Entry s X) -> Expr s X -> Either (TypeError s X) (Expr s X) 

In other words, every time you descend past a Let you add the type and the value to the Context and if you descend past a Lam or Pi you add only the type to the Context (i.e. entryValue = Nothing). Storing the let bound value in the context means you no longer need to substitute the expression into every use site (which is great if there are 1000+ use sites 🙂) and by going back to storing the type in the Context you no longer need to reinfer the type at each use site.

However, keeping the let-bound value in the context instead of substituting it means that we need to change how we detect if expressions are judgmentally equal. We can no longer use Dhall.Core.judgmentallyEqual for this purpose since it is not equipped to use the bound values that we stored in the context.

Fortunately, there already exists a utility which can exploit the information we store in the Context when doing equivalence checking: Dhall.Eval.conv!

data Env a =
    Empty
  | Skip !(Env a) {-# unpack #-} !Text
  | Extend !(Env a) {-# unpack #-} !Text (Val a)

conv :: Eq a => Env a -> Val a -> Val a -> Bool

Notice how the type of Env is very similar to Context (Entry s a). In fact, if we change our typeWith function's type to:

data Entry a = Entry { entryType :: Val a, entryValue :: Maybe (Val a) }

typeWith :: Context (Entry X) -> Expr s X -> Either (TypeError s X) (Val X)

... then Context (Entry X) is exactly isomorphic to Env and we can now use our enriched Context for correct equivalence checking as long as we convert Context (Entry X) to Env.

In fact, this is already what @AndrasKovacs's branch does, except using an even more efficient representation. That branch actually refactors the Context type further, like this:

data Env a =
    Empty
  | Skip !(Env a) {-# unpack #-} !Text
  | Extend !(Env a) {-# unpack #-} !Text (Val a)

data Types = TEmpty | TBind !(Types a) {-# unpack #-} !Text (Val a)

data Cxt a = Cxt {
    _values :: !(Env a)
  , _types  :: !(Types a)
  }

This is has the exact same information as Context (Entry a), except stored in a more efficient representation because now the _values field already has the Env that conv needs, so no additional conversion step is necessary!

In fact, we can further minimize API disruption by wrapping the typeWith function so that the user-visible type is the exact same:

typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s X) (Expr s X) 
typeWith context expression = fmap (quote NEmpty) (infer (adapt context) expression)
  where
    adapt :: Context (Expr s X) -> Ctx X
    adapt = …

infer :: Ctx X -> Expr s X -> Either (TypeError s X) (Val X)

So if I do this right I think it should require no breaking changes at all to the API. Under the hood we use the more efficient infer function that uses Ctx/Val/conv and then wrap/unwrap things at the edges so that the user can't tell the difference.

Note that what I've discussed so far only pertains to fixing #1306. There are still many other elaboration improvements we can and should port from the nbe-elaboration branch not covered here.

[Gabriella439]

Turns out that it worked without a hitch. Type-checking performance is back to normal now without any breaking change to the API: #1335

[sjakobi]

What's the status of this issue? Is there something particular that still needs to be done?

[Gabriella439]

@sjakobi: I think at least one main remaining thing that @AndrasKovacs had in mind was to interleave import resolution with type inference, but I think we can still close this since this issue is stale and the scope needs to be more carefully defined.

[Gabriella439]

Closing as I don't think there is anything more that I plan to do along these lines