google-research / dex-lang

Research language for array processing in the Haskell/ML family
BSD 3-Clause "New" or "Revised" License
1.58k stars 107 forks source link

Allow SubstE to access Env #1197

Closed dougalm closed 1 year ago

dougalm commented 1 year ago

This allows us to normalize properly as we substitute. Previously, when we encountered redexes like ProjectElt 0 (ProdVal [...]) we were limited to purely syntactic normalization (e.g. no type querying). That lead to hacks like "deferred repval" which bundled a repval with a bunch of deferred projections. And it was a blocker for my newtype-stripping patch (#1188), because I needed to embed two lists of projections in SimpInCore.

To check that it works I removed DRepVal and changed ProjectElt to be unary and take an atom (rather than a var) as its RHS. Note that this means we're no longer syntactically enforcing normalization. But we were always going to have to give that up once we started allowing more reducible-upon-substitution terms in our types, like table indexing and function application. The plan is to maintain normalization by (1) normalizing within substitution and (2) being careful about using ProjectElt and similar, preferring the normalizing builders versions instead. At some point I'd like to distinguish terms in type position using the IR variant system. Then we might be able to enforce normalization (and drop ANF!) on those terms specifically.

dougalm commented 1 year ago

@axch , thanks for review. Made follow-up PR here: #1200