Repository: tweag/nickel
Pull request #1066 (2023-01-23 14:20:43)

Feature/incremental cache
This branch introduces `IncCache` a first draft of a real implementation of the `Cache` interface.
`IncCache` will be the basis of a new incremental re-computation back-end. While this is still not a real incremental cache, and it won't be used in the main branch it's probably better to merge it in ASAP. I'll be opening other PRs once I'll finish experimenting.

TO-DO (possibly in following PRs):
- Bump allocation for the `IncCache` `store`: This would make caching faster at the cost of pre-allocating some memory at the start of evaluation.
- **(IMPORTANT)** Incremental node updating and backlinks: The content of an `IncNode` is modified it should be marked as "to be re-evaluated" along with all the other nodes that depend on it. To this end, each node should have a backlinks field, storing all the indices of the nodes that depend on it (suggestions are welcome if you have a better way of reversing the dependency graph/propagating the "to be re-evaluated" status).


Patch:
diff --git a/pyckel/src/lib.rs b/pyckel/src/lib.rs
index b2d44eee..de093036 100644
--- a/pyckel/src/lib.rs
+++ b/pyckel/src/lib.rs
@@ -2,7 +2,7 @@ use std::io::Cursor;
 
 use nickel_lang::{
     error::Error,
-    eval::cache::{CBNCache, Cache},
+    eval::cache::{Cache, CacheImpl},
     program::Program,
     serialize,
 };
@@ -19,7 +19,7 @@ fn error_to_exception<E: Into<Error>, EC: Cache>(error: E, program: &mut Program
 /// Evaluate from a Python str of a Nickel expression to a Python str of the resulting JSON.
 #[pyfunction]
 pub fn run(s: String) -> PyResult<String> {
-    let mut program: Program<CBNCache> =
+    let mut program: Program<CacheImpl> =
         Program::new_from_source(Cursor::new(s.to_string()), "python")?;
 
     let term = program
diff --git a/src/bin/nickel.rs b/src/bin/nickel.rs
index 80cd34ff..07151d37 100644
--- a/src/bin/nickel.rs
+++ b/src/bin/nickel.rs
@@ -1,6 +1,6 @@
 //! Entry point of the program.
 use nickel_lang::error::{Error, IOError};
-use nickel_lang::eval::cache::CBNCache;
+use nickel_lang::eval::cache::CacheImpl;
 use nickel_lang::program::{ColorOpt, Program};
 use nickel_lang::repl::query_print;
 #[cfg(feature = "repl")]
@@ -16,8 +16,6 @@ use std::{
 use directories::BaseDirs;
 use structopt::StructOpt;
 
-type EC = CBNCache;
-
 /// Command-line options and subcommands.
 #[derive(StructOpt, Debug)]
 /// The interpreter of the Nickel language.
@@ -220,7 +218,7 @@ fn main() {
 }
 
 fn export(
-    program: &mut Program<EC>,
+    program: &mut Program<CacheImpl>,
     format: Option<ExportFormat>,
     output: Option<PathBuf>,
 ) -> Result<(), Error> {
diff --git a/src/deserialize.rs b/src/deserialize.rs
index c26c84d1..d4619b6e 100644
--- a/src/deserialize.rs
+++ b/src/deserialize.rs
@@ -604,7 +604,7 @@ mod tests {
     use nickel_lang_utilities::TestProgram;
     use serde::Deserialize;
 
-    use crate::{eval::cache::CBNCache, program::Program};
+    use crate::{eval::cache::CacheImpl, program::Program};
 
     use super::RustDeserializationError;
 
@@ -681,7 +681,7 @@ mod tests {
         #[derive(Debug, PartialEq, Deserialize)]
         struct A;
 
-        let mut p = Program::<CBNCache>::new_from_source(
+        let mut p = Program::<CacheImpl>::new_from_source(
             Cursor::new(br#"fun a b => a + b"#.to_vec()),
             "source",
         )
diff --git a/src/destruct.rs b/src/destructuring.rs
similarity index 78%
rename from src/destruct.rs
rename to src/destructuring.rs
index cbb0227b..1f46a773 100644
--- a/src/destruct.rs
+++ b/src/destructuring.rs
@@ -19,7 +19,7 @@ pub enum Match {
     /// `{..., a=b, ...}` will bind the field `a` of the record to variable `b`. Here, `a` is the
     /// first field of this variant and `b` the optional one. The last field can actualy be a
     /// nested destruct pattern.
-    Assign(Ident, Field, (Option<Ident>, Destruct)),
+    Assign(Ident, Field, (Option<Ident>, Option<RecordPattern>)),
     /// Simple binding. the `Ident` is bind to a variable with the same name.
     Simple(Ident, Field),
 }
@@ -35,22 +35,16 @@ pub enum LastMatch {
     Ellipsis(Option<Ident>),
 }
 
-/// A destructuring pattern without the `x @` part.
+/// A destructured record pattern
 #[derive(Debug, PartialEq, Clone)]
-pub enum Destruct {
-    /// A record pattern, the only one implemented for now.
-    Record {
-        matches: Vec<Match>,
-        open: bool,
-        rest: Option<Ident>,
-        span: RawSpan,
-    },
-    /// An empty destructuring. In this case, the pattern is a classical `let var = something in
-    /// body` form.
-    Empty,
+pub struct RecordPattern {
+    pub matches: Vec<Match>,
+    pub open: bool,
+    pub rest: Option<Ident>,
+    pub span: RawSpan,
 }
 
-impl Destruct {
+impl RecordPattern {
     /// Generate the contract elaborated from this pattern.
     pub fn into_contract(self) -> LabeledType {
         let label = self.label();
@@ -75,31 +69,20 @@ impl Destruct {
 
     /// Get the inner vector of `Matches` of the pattern. If `Empty` return a empty vector.
     pub fn inner(self) -> Vec<Match> {
-        match self {
-            Destruct::Record { matches, .. } => matches,
-            Destruct::Empty => vec![],
-        }
+        self.matches
     }
 
     // Generate a label for this `Destruct`. if `Empty`, return default label.
     fn label(&self) -> Label {
-        match *self {
-            Destruct::Record { span, .. } => Label {
-                span,
-                ..Default::default()
-            },
-            Destruct::Empty => Label::default(),
+        Label {
+            span: self.span,
+            ..Default::default()
         }
     }
 
     /// Is this pattern open? Does it finish with `, ..}` form?
     pub fn is_open(&self) -> bool {
-        matches!(self, Destruct::Record { open: true, .. })
-    }
-
-    /// check if the pattern is empty.
-    pub fn is_empty(&self) -> bool {
-        matches!(self, Destruct::Empty)
+        self.open
     }
 }
 
@@ -108,16 +91,14 @@ impl Match {
     /// contract representing a record pattern destructuring.
     pub fn as_binding(self) -> (Ident, Field) {
         match self {
-            Match::Assign(id, field, (_, Destruct::Empty)) | Match::Simple(id, field) => {
-                (id, field)
-            }
+            Match::Assign(id, field, (_, None)) | Match::Simple(id, field) => (id, field),
 
             // In this case we fuse spans of the `Ident` (LHS) with the destruct (RHS)
             // because we can have two cases:
             //
             // - extra field on the destructuring `d`
             // - missing field on the `id`
-            Match::Assign(id, mut field, (_, destruct @ Destruct::Record { .. })) => {
+            Match::Assign(id, mut field, (_, Some(destruct))) => {
                 let mut label = destruct.label();
                 label.span = RawSpan::fuse(id.pos.unwrap(), label.span).unwrap();
                 field
@@ -137,13 +118,13 @@ impl Match {
     pub fn as_flattened_bindings(self) -> Vec<(Vec<Ident>, Option<Ident>, Field)> {
         match self {
             Match::Simple(id, field) => vec![(vec![id], None, field)],
-            Match::Assign(id, field, (bind_id, Destruct::Empty)) => {
+            Match::Assign(id, field, (bind_id, None)) => {
                 vec![(vec![id], bind_id, field)]
             }
             Match::Assign(
                 id,
                 mut field,
-                (bind_id, ref destruct @ Destruct::Record { ref matches, .. }),
+                (bind_id, Some(ref destruct @ RecordPattern { ref matches, .. })),
             ) => {
                 let destruct = destruct.clone();
                 let mut label = destruct.label();
diff --git a/src/error.rs b/src/error.rs
index 2d67536a..4a379ae3 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -99,7 +99,7 @@ pub enum EvalError {
     ),
     /// An unbound identifier was referenced.
     UnboundIdentifier(Ident, TermPos),
-    /// A thunk was entered during its own update.
+    /// An element in the evaluation Cache was entered during its own update.
     InfiniteRecursion(CallStack, TermPos),
     /// A serialization error occurred during a call to the builtin `serialize`.
     SerializationError(SerializationError),
@@ -1109,7 +1109,7 @@ mod blame_error {
             // of an higher order functions for example, the original argument position can
             // point to the builtin implementation contract like `func` or `record`, so
             // there's no good reason to show it. Note than even in that case, the
-            // information contained in the argument thunk can still be useful.
+            // information contained at the argument index can still be useful.
             if contract_id
                 .map(|ctrs_id| arg_pos.src_id != ctrs_id)
                 .unwrap_or(true)
@@ -1118,9 +1118,9 @@ mod blame_error {
             }
         }
 
-        // If we have a reference to the thunk that was being tested, we can try to show
-        // more information about the final, evaluated value that is responsible for the
-        // blame.
+        // If we have a reference to the element in the cache that was being tested,
+        // we can try to show more information about the final, evaluated value that is
+        // responsible for the blame.
         if let Some(mut evaluated_arg) = evaluated_arg {
             match (
                 evaluated_arg.pos,
@@ -1142,7 +1142,7 @@ mod blame_error {
                 (TermPos::Original(ref val_pos), ..) => {
                     labels.push(secondary(val_pos).with_message("evaluated to this expression"))
                 }
-                // If the final thunk is a direct reduct of the original value, rather
+                // If the final element is a direct reduct of the original value, rather
                 // print the actual value than referring to the same position as
                 // before.
                 (TermPos::Inherited(ref val_pos), Some(arg_pos), _) if val_pos == arg_pos => {
diff --git a/src/eval/cache/incremental.rs b/src/eval/cache/incremental.rs
new file mode 100644
index 00000000..9db27526
--- /dev/null
+++ b/src/eval/cache/incremental.rs
@@ -0,0 +1,267 @@
+/// A [Cache] implementation with incremental computation features.
+
+use super::{BlackholedError, Cache, CacheIndex, Closure, Environment, IdentKind};
+use crate::{
+    identifier::Ident,
+    term::{record::FieldDeps, BindingType, RichTerm, Term},
+};
+
+/// The evaluation state of an [IncNode].
+#[derive(Debug, Copy, Clone, Default, PartialEq, Eq)]
+pub enum IncNodeState {
+    #[default]
+    Suspended,
+    Blackholed,
+    Evaluated,
+}
+
+/// A node in the dependent computation graph stored in [IncCache].
+#[derive(Debug, Clone)]
+pub struct IncNode {
+    // The original closure.
+    orig: Closure,
+    // The cached value of the closure.
+    cached: Option<Closure>,
+    kind: IdentKind,
+    bty: BindingType,
+    // The state of the node.
+    state: IncNodeState,
+    // Backlinks to nodes depending on this node.
+    backlinks: Vec<CacheIndex>,
+}
+
+impl IncNode {
+    fn new(clos: Closure, kind: IdentKind, bty: BindingType) -> Self {
+        IncNode {
+            orig: clos,
+            cached: None,
+            kind,
+            bty,
+            state: IncNodeState::default(),
+            backlinks: Vec::new(),
+        }
+    }
+}
+
+/// A [Cache] implementation supporting incremental computation features.
+/// Stores a dependent computation graph to keep track of what needs to be recomputed.
+#[derive(Debug, Clone)]
+pub struct IncCache {
+    store: Vec<IncNode>,
+    next: CacheIndex,
+}
+
+impl IncCache {
+    fn add_node(&mut self, node: IncNode) -> CacheIndex {
+        let idx = self.next;
+        self.store.insert(idx, node);
+        self.next += 1;
+
+        idx
+    }
+
+    fn revnode_as_explicit_fun<'a, I>(node: &IncNode, args: I) -> IncNode
+    where
+        I: DoubleEndedIterator<Item = &'a Ident>,
+    {
+        match &node.bty {
+            BindingType::Revertible(deps) if !deps.is_empty() => {
+                let Closure { body, env } = node.orig.clone();
+
+                // Build a list of the arguments that the function will need in the same order as
+                // the original iterator. If the identifiers inside `args` are `a`, `b` and `c`, in
+                // that order, we want to build `fun a => (fun b => (fun c => body))`. We thus need a
+                // reverse fold.
+                let as_function =
+                    args.rfold(body, |built, id| RichTerm::from(Term::Fun(*id, built)));
+
+                IncNode::new(
+                    Closure {
+                        body: as_function,
+                        env,
+                    },
+                    node.kind,
+                    node.bty.clone(),
+                )
+            }
+            _ => node.clone(),
+        }
+    }
+}
+
+impl Cache for IncCache {
+    type UpdateIndex = CacheIndex;
+
+    fn new() -> Self {
+        IncCache {
+            store: Vec::new(),
+            next: 0,
+        }
+    }
+
+    fn get(&self, idx: CacheIndex) -> Closure {
+        let node = self.store.get(idx).unwrap();
+
+        node.cached.clone().unwrap_or(node.orig.clone())
+    }
+
+    fn get_update_index(
+        &mut self,
+        idx: &mut CacheIndex,
+    ) -> Result<Option<Self::UpdateIndex>, BlackholedError> {
+        let node = self.store.get_mut(*idx).unwrap();
+
+        if node.state == IncNodeState::Blackholed {
+            Err(BlackholedError)
+        } else if node.state == IncNodeState::Evaluated {
+            Ok(None)
+        } else {
+            node.state = IncNodeState::Blackholed;
+            Ok(Some(*idx))
+        }
+    }
+
+    fn add(&mut self, clos: Closure, kind: IdentKind, bty: BindingType) -> CacheIndex {
+        let node = IncNode::new(clos, kind, bty);
+
+        self.add_node(node)
+    }
+
+    fn update(&mut self, clos: Closure, idx: Self::UpdateIndex) {
+        let node = self.store.get_mut(idx).unwrap();
+
+        node.cached = Some(clos);
+        node.state = IncNodeState::Evaluated;
+    }
+
+    fn revert(&mut self, idx: &CacheIndex) -> CacheIndex {
+        let node = self.store.get(*idx).unwrap();
+
+        let new_node = match node.bty.clone() {
+            BindingType::Normal => node.clone(),
+            BindingType::Revertible(_) => {
+                IncNode::new(node.orig.clone(), node.kind, node.bty.clone())
+            }
+        };
+
+        self.add_node(new_node)
+    }
+
+    fn ident_kind(&self, idx: &CacheIndex) -> IdentKind {
+        self.store.get(*idx).unwrap().kind
+    }
+
+    fn deps(&self, idx: &CacheIndex) -> Option<FieldDeps> {
+        let node = self.store.get(*idx).unwrap();
+        match node.bty.clone() {
+            BindingType::Normal => None,
+            BindingType::Revertible(deps) => Some(deps),
+        }
+    }
+
+    fn get_then<T, F: FnOnce(&Closure) -> T>(&self, idx: CacheIndex, f: F) -> T {
+        f(&self.get(idx))
+    }
+
+    fn patch<F: Fn(&mut Closure)>(&mut self, idx: CacheIndex, f: F) {
+        let node = self.store.get_mut(idx).unwrap();
+
+        f(&mut node.orig);
+        node.cached.as_mut().map(|mut clos| f(&mut clos));
+    }
+
+    fn make_update_index(
+        &mut self,
+        idx: &mut CacheIndex,
+    ) -> Result<Self::UpdateIndex, BlackholedError> {
+        let node = self.store.get_mut(*idx).unwrap();
+
+        if node.state == IncNodeState::Blackholed {
+            return Err(BlackholedError);
+        } else {
+            node.state = IncNodeState::Blackholed;
+
+            Ok(*idx)
+        }
+    }
+
+    fn reset_index_state(&mut self, idx: &mut Self::UpdateIndex) {
+        let node = self.store.get_mut(*idx).unwrap();
+
+        node.state = IncNodeState::default();
+    }
+
+    fn map_at_index<F: FnMut(&mut Self, &Closure) -> Closure>(
+        &mut self,
+        idx: &CacheIndex,
+        mut f: F,
+    ) -> CacheIndex {
+        let node = self.store.get(*idx).unwrap().clone();
+
+        let new_node = IncNode {
+            orig: f(self, &node.orig),
+            cached: node.cached.clone().map(|clos| f(self, &clos)),
+            kind: node.kind,
+            bty: node.bty.clone(),
+            state: node.state,
+            backlinks: node.backlinks.clone(),
+        };
+
+        self.add_node(new_node)
+    }
+
+    fn build_cached(&mut self, idx: &mut CacheIndex, rec_env: &[(Ident, CacheIndex)]) {
+        let node = self.store.get_mut(*idx).unwrap();
+
+        if node.cached.is_some() {
+            return ();
+        }
+
+        let mut new_cached = Closure::clone(&node.orig);
+
+        match node.bty {
+            BindingType::Normal => (),
+            BindingType::Revertible(ref deps) => match deps {
+                FieldDeps::Unknown => new_cached.env.extend(rec_env.iter().cloned()),
+                FieldDeps::Known(deps) if deps.is_empty() => (),
+                FieldDeps::Known(deps) => new_cached
+                    .env
+                    .extend(rec_env.iter().filter(|(id, _)| deps.contains(id)).cloned()),
+            },
+        }
+
+        node.cached = Some(new_cached);
+    }
+
+    fn saturate<'a, I: DoubleEndedIterator<Item = &'a Ident> + Clone>(
+        &mut self,
+        idx: CacheIndex,
+        env: &mut Environment,
+        fields: I,
+    ) -> RichTerm {
+        let node = self.store.get(idx).unwrap();
+
+        let mut deps_filter: Box<dyn FnMut(&&Ident) -> bool> = match node.bty.clone() {
+            BindingType::Revertible(FieldDeps::Known(deps)) => {
+                Box::new(move |id: &&Ident| deps.contains(id))
+            }
+            BindingType::Revertible(FieldDeps::Unknown) => Box::new(|_: &&Ident| true),
+            BindingType::Normal => Box::new(|_: &&Ident| false),
+        };
+
+        let node_as_function = self.add_node(IncCache::revnode_as_explicit_fun(
+            node,
+            fields.clone().filter(&mut deps_filter),
+        ));
+
+        let fresh_var = Ident::fresh();
+        env.insert(fresh_var, node_as_function);
+
+        let as_function_closurized = RichTerm::from(Term::Var(fresh_var));
+        let args = fields.filter_map(|id| deps_filter(&id).then(|| RichTerm::from(Term::Var(*id))));
+
+        args.fold(as_function_closurized, |partial_app, arg| {
+            RichTerm::from(Term::App(partial_app, arg))
+        })
+    }
+}
diff --git a/src/eval/lazy.rs b/src/eval/cache/lazy.rs
similarity index 88%
rename from src/eval/lazy.rs
rename to src/eval/cache/lazy.rs
index c37d575d..552eabcb 100644
--- a/src/eval/lazy.rs
+++ b/src/eval/cache/lazy.rs
@@ -1,8 +1,8 @@
 //! Thunks and associated devices used to implement lazy evaluation.
-use super::{cache::CacheIndex, Closure, Environment, IdentKind};
+use super::{BlackholedError, Cache, CacheIndex, Closure, Environment, IdentKind};
 use crate::{
     identifier::Ident,
-    term::{record::FieldDeps, RichTerm, Term},
+    term::{record::FieldDeps, BindingType, RichTerm, Term},
 };
 use std::cell::{Ref, RefCell, RefMut};
 use std::rc::{Rc, Weak};
@@ -32,8 +32,6 @@ pub struct ThunkData {
     state: ThunkState,
 }
 
-type CBNClosure = Closure;
-
 /// The part of [ThunkData] responsible for storing the closure itself. It can either be:
 /// - A standard thunk, that is destructively updated once and for all
 /// - A revertible thunk, that can be restored to its original expression. Used to implement
@@ -106,7 +104,7 @@ type CBNClosure = Closure;
 /// variables of `orig`.
 #[derive(Clone, Debug, PartialEq)]
 pub enum InnerThunkData {
-    Standard(CBNClosure),
+    Standard(Closure),
     Revertible {
         orig: Rc<Closure>,
         cached: Option<Closure>,
@@ -119,7 +117,7 @@ const REVTHUNK_NO_CACHED_VALUE_MSG: &str =
 
 impl ThunkData {
     /// Create new standard thunk data.
-    pub fn new(closure: CBNClosure) -> Self {
+    pub fn new(closure: Closure) -> Self {
         ThunkData {
             inner: InnerThunkData::Standard(closure),
             state: ThunkState::Suspended,
@@ -226,7 +224,7 @@ impl ThunkData {
     }
 
     /// Return a reference to the closure currently cached.
-    pub fn closure(&self) -> &CBNClosure {
+    pub fn closure(&self) -> &Closure {
         match self.inner {
             InnerThunkData::Standard(ref closure) => closure,
             // Nothing should peek into a revertible thunk before the cached value has been
@@ -245,7 +243,7 @@ impl ThunkData {
     }
 
     /// Return a mutable reference to the closure currently cached.
-    pub fn closure_mut(&mut self) -> &mut CBNClosure {
+    pub fn closure_mut(&mut self) -> &mut Closure {
         match self.inner {
             InnerThunkData::Standard(ref mut closure) => closure,
             InnerThunkData::Revertible {
@@ -257,7 +255,7 @@ impl ThunkData {
     }
 
     /// Consume the data and return the cached closure.
-    pub fn into_closure(self) -> CBNClosure {
+    pub fn into_closure(self) -> Closure {
         match self.inner {
             InnerThunkData::Standard(closure) => closure,
             // Nothing should access the cached value of a revertible thunk before the cached
@@ -276,7 +274,7 @@ impl ThunkData {
     }
 
     /// Update the cached closure.
-    pub fn update(&mut self, new: CBNClosure) {
+    pub fn update(&mut self, new: Closure) {
         match self.inner {
             InnerThunkData::Standard(ref mut closure) => *closure = new,
             InnerThunkData::Revertible { ref mut cached, .. } => *cached = Some(new),
@@ -314,7 +312,7 @@ impl ThunkData {
     /// the cached expression.
     pub fn map<F>(&self, mut f: F) -> Self
     where
-        F: FnMut(&CBNClosure) -> CBNClosure,
+        F: FnMut(&Closure) -> Closure,
     {
         match self.inner {
             InnerThunkData::Standard(ref c) => ThunkData {
@@ -363,13 +361,9 @@ pub struct Thunk {
     ident_kind: IdentKind,
 }
 
-/// A black-holed thunk was accessed, which would lead to infinite recursion.
-#[derive(Clone, Copy, Debug, Eq, PartialEq)]
-pub struct BlackholedError;
-
 impl Thunk {
     /// Create a new standard thunk.
-    pub fn new(closure: CBNClosure, ident_kind: IdentKind) -> Self {
+    pub fn new(closure: Closure, ident_kind: IdentKind) -> Self {
         Thunk {
             data: Rc::new(RefCell::new(ThunkData::new(closure))),
             ident_kind,
@@ -413,17 +407,17 @@ impl Thunk {
     }
 
     /// Immutably borrow the inner closure. Panic if there is another active mutable borrow.
-    pub fn borrow(&self) -> Ref<'_, CBNClosure> {
+    pub fn borrow(&self) -> Ref<'_, Closure> {
         Ref::map(self.data.borrow(), |data| data.closure())
     }
 
     /// Mutably borrow the inner closure. Panic if there is any other active borrow.
-    pub fn borrow_mut(&mut self) -> RefMut<'_, CBNClosure> {
+    pub fn borrow_mut(&mut self) -> RefMut<'_, Closure> {
         RefMut::map(self.data.borrow_mut(), |data| data.closure_mut())
     }
 
     /// Get an owned clone of the inner closure.
-    pub fn get_owned(&self) -> CBNClosure {
+    pub fn get_owned(&self) -> Closure {
         self.data.borrow().closure().clone()
     }
 
@@ -433,7 +427,7 @@ impl Thunk {
 
     /// Consume the thunk and return an owned closure. Avoid cloning if this thunk is the only
     /// reference to the inner closure.
-    pub fn into_closure(self) -> CBNClosure {
+    pub fn into_closure(self) -> Closure {
         match Rc::try_unwrap(self.data) {
             Ok(inner) => inner.into_inner().into_closure(),
             Err(rc) => rc.borrow().closure().clone(),
@@ -450,7 +444,7 @@ impl Thunk {
         }
     }
 
-    pub fn build_cached(&mut self, rec_env: &[(Ident, CacheIndex)]) {
+    pub fn build_cached(&mut self, rec_env: &[(Ident, Thunk)]) {
         self.data.borrow_mut().init_cached(rec_env)
     }
 
@@ -543,7 +537,7 @@ impl Thunk {
     /// cached expression.
     pub fn map<F>(&self, f: F) -> Self
     where
-        F: FnMut(&CBNClosure) -> CBNClosure,
+        F: FnMut(&Closure) -> Closure,
     {
         Thunk {
             data: Rc::new(RefCell::new(self.data.borrow().map(f))),
@@ -585,7 +579,7 @@ impl ThunkUpdateFrame {
     ///
     /// - `true` if the thunk was successfully updated
     /// - `false` if the corresponding closure has been dropped since
-    pub fn update(self, closure: CBNClosure) -> bool {
+    pub fn update(self, closure: Closure) -> bool {
         if let Some(data) = Weak::upgrade(&self.data) {
             data.borrow_mut().update(closure);
             true
@@ -602,3 +596,100 @@ impl ThunkUpdateFrame {
         }
     }
 }
+
+/// Placeholder [Cache] for the call-by-need evaluation strategy.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct CBNCache {}
+
+impl Cache for CBNCache {
+    type UpdateIndex = ThunkUpdateFrame;
+
+    fn get(&self, idx: CacheIndex) -> Closure {
+        idx.get_owned()
+    }
+
+    fn get_update_index(
+        &mut self,
+        idx: &mut CacheIndex,
+    ) -> Result<Option<Self::UpdateIndex>, BlackholedError> {
+        if idx.state() != ThunkState::Evaluated {
+            if idx.should_update() {
+                idx.mk_update_frame().map(Some)
+            }
+            // If the thunk isn't to be updated, directly set the evaluated flag.
+            else {
+                idx.set_evaluated();
+                Ok(None)
+            }
+        } else {
+            Ok(None)
+        }
+    }
+
+    fn add(&mut self, clos: Closure, kind: IdentKind, bty: BindingType) -> CacheIndex {
+        match bty {
+            BindingType::Normal => Thunk::new(clos, kind),
+            BindingType::Revertible(deps) => Thunk::new_rev(clos, kind, deps),
+        }
+    }
+
+    fn patch<F: FnOnce(&mut Closure)>(&mut self, mut idx: CacheIndex, f: F) {
+        f(&mut idx.borrow_mut());
+    }
+
+    fn get_then<T, F: FnOnce(&Closure) -> T>(&self, idx: CacheIndex, f: F) -> T {
+        f(&idx.borrow())
+    }
+
+    fn update(&mut self, clos: Closure, uidx: Self::UpdateIndex) {
+        uidx.update(clos);
+    }
+
+    fn new() -> Self {
+        CBNCache {}
+    }
+
+    fn reset_index_state(&mut self, idx: &mut Self::UpdateIndex) {
+        idx.reset_state();
+    }
+
+    fn map_at_index<F: FnMut(&mut Self, &Closure) -> Closure>(
+        &mut self,
+        idx: &CacheIndex,
+        mut f: F,
+    ) -> CacheIndex {
+        idx.map(|v| f(self, v))
+    }
+
+    fn build_cached(&mut self, idx: &mut CacheIndex, rec_env: &[(Ident, CacheIndex)]) {
+        idx.build_cached(rec_env)
+    }
+
+    fn ident_kind(&self, idx: &CacheIndex) -> IdentKind {
+        idx.ident_kind()
+    }
+
+    fn saturate<'a, I: DoubleEndedIterator<Item = &'a Ident> + Clone>(
+        &mut self,
+        idx: CacheIndex,
+        env: &mut Environment,
+        fields: I,
+    ) -> RichTerm {
+        idx.saturate(env, fields)
+    }
+
+    fn deps(&self, idx: &CacheIndex) -> Option<FieldDeps> {
+        Some(idx.deps())
+    }
+
+    fn revert(&mut self, idx: &CacheIndex) -> CacheIndex {
+        idx.revert()
+    }
+
+    fn make_update_index(
+        &mut self,
+        idx: &mut CacheIndex,
+    ) -> Result<Self::UpdateIndex, BlackholedError> {
+        idx.mk_update_frame()
+    }
+}
diff --git a/src/eval/cache/mod.rs b/src/eval/cache/mod.rs
new file mode 100644
index 00000000..978b21e2
--- /dev/null
+++ b/src/eval/cache/mod.rs
@@ -0,0 +1,97 @@
+/// The Nickel generic evaluation cache. This module abstracts away the details for managing
+/// suspended computations and their memoization strategies.
+///
+/// Terminology:
+/// An *element* of the cache is what is stored inside of it.
+/// An *index* into the cache points to a given element.
+use super::{Closure, Environment, IdentKind};
+use crate::{
+    identifier::Ident,
+    term::{record::FieldDeps, BindingType, RichTerm},
+};
+
+pub mod lazy;
+//pub mod incremental;
+
+/// An index to a specific item stored in the cache
+pub type CacheIndex = lazy::Thunk;
+//pub type CacheIndex = usize;
+
+/// The current Cache implementation
+pub type CacheImpl = lazy::CBNCache;
+//pub type CacheImpl = incremental::IncCache;
+
+/// A black-holed node was accessed, which would lead to infinite recursion.
+#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+pub struct BlackholedError;
+
+pub trait Cache: Clone {
+    /// Temporary: as of now we only need this for [lazy::CBNCache].
+    type UpdateIndex;
+
+    /// Gets the [Closure] from the element at index `idx`.
+    fn get(&self, idx: CacheIndex) -> Closure;
+
+    /// Checks whether the element at index `idx` is blackholed and returns a
+    /// [BlackholedError] if it is. Otherwise, returns `Some(idx)` if the element
+    /// needs to be updated, returns `None` if not.
+    /// Should use [Cache::make_update_index].
+    fn get_update_index(
+        &mut self,
+        idx: &mut CacheIndex,
+    ) -> Result<Option<Self::UpdateIndex>, BlackholedError>;
+
+    /// Adds an element into the [Cache] and returns its index.
+    fn add(&mut self, clos: Closure, kind: IdentKind, bty: BindingType) -> CacheIndex;
+
+    /// Applies `f` to the [Closure] stored inside the element at index `idx`.
+    fn patch<F: Fn(&mut Closure)>(&mut self, idx: CacheIndex, f: F);
+
+    /// Clones the [Closure] from the element at index `idx` and applies `f` to it.
+    fn get_then<T, F: FnOnce(&Closure) -> T>(&self, idx: CacheIndex, f: F) -> T;
+
+    /// Updates the [Closure] from the element at index `idx` with `clos`.
+    fn update(&mut self, clos: Closure, idx: Self::UpdateIndex);
+
+    /// Initializes a new [Cache].
+    fn new() -> Self;
+
+    /// Resets the state of the element at index `idx` to `Suspended`
+    fn reset_index_state(&mut self, idx: &mut Self::UpdateIndex);
+
+    fn map_at_index<F: FnMut(&mut Self, &Closure) -> Closure>(
+        &mut self,
+        idx: &CacheIndex,
+        f: F,
+    ) -> CacheIndex;
+
+    /// Initializes the cached value of the element at index `idx` with the given `rec_env`.
+    fn build_cached(&mut self, idx: &mut CacheIndex, rec_env: &[(Ident, CacheIndex)]);
+
+    /// Returns the [IdentKind] of the element stored at index `idx`
+    fn ident_kind(&self, idx: &CacheIndex) -> IdentKind;
+
+    /// Revert the element at index `idx`, abstract over its dependencies to get back a function,
+    /// and apply the function to the given variables. The function part is allocated in a new
+    /// cache entry, stored as a generated variable, with the same environment as the original
+    /// expression.
+    fn saturate<'a, I: DoubleEndedIterator<Item = &'a Ident> + Clone>(
+        &mut self,
+        idx: CacheIndex,
+        env: &mut Environment,
+        fields: I,
+    ) -> RichTerm;
+
+    /// Reverts the element stored at index `idx` to its original value.
+    fn revert(&mut self, idx: &CacheIndex) -> CacheIndex;
+
+    /// Returns the dependencies of the element stored at index `idx`, if it has any.
+    fn deps(&self, idx: &CacheIndex) -> Option<FieldDeps>;
+
+    /// Checks whether the element at index `idx` is blackholed and returns a
+    /// [BlackholedError] if it is. Otherwise, returns `idx`.
+    fn make_update_index(
+        &mut self,
+        idx: &mut CacheIndex,
+    ) -> Result<Self::UpdateIndex, BlackholedError>;
+}
diff --git a/src/eval/cache.rs b/src/eval/cache_old.rs
similarity index 100%
rename from src/eval/cache.rs
rename to src/eval/cache_old.rs
diff --git a/src/eval/fixpoint.rs b/src/eval/fixpoint.rs
index 4f150bb7..1ed402c0 100644
--- a/src/eval/fixpoint.rs
+++ b/src/eval/fixpoint.rs
@@ -3,7 +3,7 @@ use super::*;
 use crate::position::TermPos;
 
 // Update the environment of a term by extending it with a recursive environment. In the general
-// case, the term is expected to be a variable pointing to the thunk to be patched. Otherwise, it's
+// case, the term is expected to be a variable pointing to the element to be patched. Otherwise, it's
 // considered to have no dependencies and is left untouched.
 //
 // This function achieve the same as `patch_field`, but is somehow lower-level, as it operates on a
@@ -29,8 +29,8 @@ fn patch_term<C: Cache>(
 }
 
 /// Build a recursive environment from record bindings. For each field, `rec_env` either extracts
-/// the corresponding thunk from the environment in the general case, or create a closure on the
-/// fly if the field is a constant. The resulting environment is to be passed to the
+/// the corresponding cache element from the environment in the general case, or create a closure
+/// on the fly if the field is a constant. The resulting environment is to be passed to the
 /// [`patch_field`] function.
 ///
 /// # Pending contracts
@@ -131,10 +131,10 @@ pub fn rec_env<'a, I: Iterator<Item = (&'a Ident, &'a Field)>, C: Cache>(
 }
 
 /// Update the environment of the content of a recursive record field by extending it with a
-/// recursive environment. When seeing revertible thunks as a memoizing device for functions, this
+/// recursive environment. When seeing revertible elements as a memoizing device for functions, this
 /// step correspond to function application (see documentation of [crate::eval::lazy::ThunkData]).
 ///
-/// For each field, retrieve the set set of dependencies from the corresponding thunk in the
+/// For each field, retrieve the set set of dependencies from the corresponding element in the
 /// environment, and only add those dependencies to the environment. This avoids retaining
 /// reference-counted pointers to unused data. If no dependencies are available, conservatively add
 /// all the recursive environment. See [`crate::transform::free_vars`].
diff --git a/src/eval/merge.rs b/src/eval/merge.rs
index db5a13df..e6b8d3c2 100644
--- a/src/eval/merge.rs
+++ b/src/eval/merge.rs
@@ -267,13 +267,13 @@ pub fn merge<C: Cache>(
 
             // Merging recursive records is the one operation that may override recursive fields. To
             // have the recursive fields depend on the updated values, we need to revert the
-            // corresponding thunks to their original expression.
+            // corresponding elements in the cache to their original expression.
             //
             // We do that for the left and the right part.
             //
             // The fields in the intersection (center) need a slightly more general treatment to
             // correctly propagate the recursive values down each field: saturation. See
-            // [crate::eval::lazy::Thunk::saturate].
+            // [crate::eval::cache::Cache::saturate()].
             m.extend(
                 left.into_iter()
                     .map(|(id, field)| (id, field.revert_closurize(cache, &mut env, env1.clone()))),
@@ -311,7 +311,7 @@ pub fn merge<C: Cache>(
                     // We don't have to provide RecordDeps, which are required in a previous stage
                     // of program transformations. At this point, the interpreter doesn't care
                     // about them anymore, and dependencies are stored at the level of revertible
-                    // thunks directly.
+                    // cache elements directly.
                     Term::RecRecord(
                         RecordData::new(m, RecordAttrs::merge(r1.attrs, r2.attrs), None),
                         Vec::new(),
@@ -450,7 +450,7 @@ fn merge_doc(doc1: Option<String>, doc2: Option<String>) -> Option<String> {
     doc1.or(doc2)
 }
 
-/// See [crate::eval::lazy::Thunk::saturate]. Saturation is a transformation on recursive thunks
+/// See [crate::eval::cache::Cache::saturate]. Saturation is a transformation on recursive cache elements
 /// that is used when we must combine different values with different recursive dependencies (say,
 /// the two values of fields being merged) into one expression.
 ///
@@ -458,12 +458,12 @@ fn merge_doc(doc1: Option<String>, doc2: Option<String>) -> Option<String> {
 /// [crate::transform::Closurizable], it can be applied to other types that contain terms, hence
 /// the trait.
 trait Saturate: Sized {
-    /// Take the content of a record field, and saturate the potential revertible thunk with the given
-    /// fields. See [crate::eval::lazy::Thunk::saturate].
+    /// Take the content of a record field, and saturate the potential revertible element with the given
+    /// fields. See [crate::eval::cache::Cache::saturate].
     ///
-    /// If the expression is not a variable referring to a thunk (this can happen e.g. for numeric
-    /// constants), we just return the term as it is, which falls into the zero dependencies special
-    /// case.
+    /// If the expression is not a variable referring to an element in the cache
+    ///  (this can happen e.g. for numeric constants), we just return the term as it is, which
+    /// falls into the zero dependencies special case.
     fn saturate<'a, I: DoubleEndedIterator<Item = &'a Ident> + Clone, C: Cache>(
         self,
         cache: &mut C,
@@ -513,9 +513,9 @@ fn field_deps<C: Cache>(
 /// Take the current environment, two fields with their local environment, and return a term which
 /// is the merge of the two fields, closurized in the provided final environment.
 ///
-/// The thunk allocated for the result is revertible if and only if at least one of the original
-/// thunks is (if one of the original values is overridable, then so is the merge of the two). In
-/// this case, the field dependencies are the union of the dependencies of each field.
+/// The element in the cache allocated for the result is revertible if and only if at least one of
+/// the original elements is (if one of the original values is overridable, then so is the merge of
+/// the two). In this case, the field dependencies are the union of the dependencies of each field.
 ///
 /// The fields are saturated (see [saturate]) to properly propagate recursive dependencies down to
 /// `t1` and `t2` in the final, merged record.
@@ -537,14 +537,14 @@ fn fields_merge_closurize<'a, I: DoubleEndedIterator<Item = &'a Ident> + Clone,
         t2.saturate(cache, &mut local_env, env2, fields)?,
     ));
 
-    // We closurize the final result in a thunk with appropriate dependencies
+    // We closurize the final result in an element with appropriate dependencies
     let closure = Closure {
         body,
         env: local_env,
     };
     let fresh_var = Ident::fresh();
 
-    // new_rev takes care of not creating a revertible thunk if the dependencies are empty.
+    // new_rev takes care of not creating a revertible element in the cache if the dependencies are empty.
     env.insert(
         fresh_var,
         cache.add(
@@ -557,9 +557,9 @@ fn fields_merge_closurize<'a, I: DoubleEndedIterator<Item = &'a Ident> + Clone,
     Ok(RichTerm::from(Term::Var(fresh_var)))
 }
 
-/// Same as [Closurizable], but also revert the thunk if the term is a variable.
+/// Same as [Closurizable], but also revert the element if the term is a variable.
 trait RevertClosurize {
-    /// Revert the thunk inside the term (if any), and closurize the result inside `env`.
+    /// Revert the element at the index inside the term (if any), and closurize the result inside `env`.
     fn revert_closurize<C: Cache>(
         self,
         cache: &mut C,
@@ -576,7 +576,7 @@ impl RevertClosurize for RichTerm {
         with_env: Environment,
     ) -> RichTerm {
         if let Term::Var(id) = self.as_ref() {
-            // This create a fresh variable which is bound to a reverted copy of the original thunk
+            // This create a fresh variable which is bound to a reverted copy of the original element
             let reverted = cache.revert(with_env.get(id).unwrap());
             let fresh_id = Ident::fresh();
             env.insert(fresh_id, reverted);
diff --git a/src/eval/mod.rs b/src/eval/mod.rs
index 1cf9b0ba..5f59a8d4 100644
--- a/src/eval/mod.rs
+++ b/src/eval/mod.rs
@@ -7,7 +7,7 @@
 //! # The Nickel Abstract Machine
 //! The abstract machine is a stack machine composed of the following elements:
 //! - The term being currently evaluated
-//! - The main stack, storing arguments, thunks and pending computations
+//! - The main stack, storing arguments, cache indices and pending computations
 //! - A pair of [environment][Environment], mapping identifiers to [closures][Closure]:
 //!     * The initial environment contains builtin functions accessible from anywhere, and alive
 //!     during the whole evaluation
@@ -18,7 +18,7 @@
 //! Depending on the shape of the current term, the following actions are performed:
 //!
 //! ## Core calculus
-//! - **Var(id)**: the term bound to `id` in the environment is fetched, and an update thunk is
+//! - **Var(id)**: the term bound to `id` in the environment is fetched, and an update index is
 //!   pushed on the stack to indicate that once this term has been evaluated, the content of the
 //!   variable must be updated
 //! - **App(func, arg)**: a closure containing the argument and the current environment is pushed
@@ -27,8 +27,8 @@
 //! - **Fun(id, body)**: Try to pop an argument from the stack. If there is some, we bound it to
 //!   `id` in the environment, and proceed with the body of the function. Otherwise, we are done: the
 //!   end result is an unapplied function
-//! - **Thunk on stack**: If the evaluation of the current term is done, and there is one (or
-//!   several) thunk on the stack, this means we have to perform an update. Consecutive thunks are
+//! - **Index on stack**: If the evaluation of the current term is done, and there is one (or
+//!   several) index on the stack, this means we have to perform an update. Consecutive indices are
 //!   popped from the stack and are updated to point to the current evaluated term.
 //! - **Import**: Import must have been resolved before the evaluation starts. An unresolved import
 //!   causes an [`crate::error::EvalError::InternalError`]. A resolved import, identified by a
@@ -94,7 +94,6 @@ use crate::{
 pub mod cache;
 pub mod callstack;
 pub mod fixpoint;
-pub mod lazy;
 pub mod merge;
 pub mod operation;
 pub mod stack;
@@ -114,7 +113,7 @@ impl AsRef<Vec<StackElem>> for CallStack {
 
 // The current state of the Nickel virtual machine.
 pub struct VirtualMachine<R: ImportResolver, C: Cache> {
-    // The main stack, storing arguments, thunks and pending computations.
+    // The main stack, storing arguments, cache indices and pending computations.
     stack: Stack<C>,
     // The call stack, for error reporting.
     call_stack: CallStack,
@@ -143,11 +142,11 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
         }
     }
 
-    /// Reset the state of the machine (stacks, eval mode and thunk state) to prepare for another evaluation round.
+    /// Reset the state of the machine (stacks, eval mode and state of cached elements) to prepare
+    /// for another evaluation round.
     pub fn reset(&mut self) {
         self.call_stack.0.clear();
         self.stack.reset(&mut self.cache);
-        self.cache = Cache::new();
     }
 
     pub fn import_resolver(&self) -> &R {
@@ -286,8 +285,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
 
     /// The main loop of evaluation.
     ///
-    /// Implement the evaluation of the core language, which includes application, thunk update,
-    /// evaluation of the arguments of operations, and a few others. The specific implementations of
+    /// Implement the evaluation loop of the core language. The specific implementations of
     /// primitive operations is delegated to the modules [operation] and [merge].
     ///
     /// # Arguments
@@ -326,7 +324,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                         },
                         env: env.clone(),
                     };
-                    // Update the original thunk (the thunk which holds the result of the op) in both cases,
+                    // Update at the original index (the index which holds the result of the op) in both cases,
                     // even if we continue with a seq.
                     // We do this because  we are on a `Sealed` term, and this is in WHNF, and if we don't,
                     // we will be unwrapping a `Sealed` term and assigning the "unsealed" value to the result
@@ -426,7 +424,8 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     // Patch the environment with the (x <- closure) binding
                     if *rec {
                         let idx_ = idx.clone();
-                        self.cache.patch(idx_.clone(), |cl| cl.env.insert(*x, idx_));
+                        self.cache
+                            .patch(idx_.clone(), |cl| cl.env.insert(*x, idx_.clone()));
                     }
 
                     env.insert(*x, idx);
@@ -691,7 +690,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                         env,
                     }
                 }
-                // Continuation of operations and thunk update
+                // Continuation of operations and element update
                 _ if self.stack.is_top_idx() || self.stack.is_top_cont() => {
                     clos = Closure {
                         body: RichTerm {
@@ -892,7 +891,7 @@ pub fn env_add<C: Cache>(
     env.insert(id, cache.add(closure, IdentKind::Let, BindingType::Normal));
 }
 
-/// Pop and update all the thunks on the top of the stack with the given closure.
+/// Pop and update all the indices on the top of the stack with the given closure.
 fn update_at_indices<C: Cache>(cache: &mut C, stack: &mut Stack<C>, closure: &Closure) {
     while let Some(idx) = stack.pop_update_index() {
         cache.update(closure.clone(), idx);
diff --git a/src/eval/operation.rs b/src/eval/operation.rs
index 406eaff7..2d8a9a04 100644
--- a/src/eval/operation.rs
+++ b/src/eval/operation.rs
@@ -549,7 +549,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                             let f_as_var = f.body.closurize(&mut self.cache, &mut env, f.env);
 
                             // Array elements are closurized to preserve laziness of data structures. It
-                            // maintains the invariant that any data structure only contain thunks (that is,
+                            // maintains the invariant that any data structure only contain indices (that is,
                             // currently, variables).
                             let ts = ts
                                 .into_iter()
@@ -600,7 +600,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                         let f_as_var = f.body.closurize(&mut self.cache, &mut env, f.env);
 
                         // Array elements are closurized to preserve laziness of data structures. It
-                        // maintains the invariant that any data structure only contain thunks (that is,
+                        // maintains the invariant that any data structure only contain indices (that is,
                         // currently, variables).
                         let ts = (0..n_int)
                             .map(|n| {
@@ -2935,7 +2935,7 @@ impl RecPriority {
                 // ```
                 //
                 // In the example above, if we just map `$rec_default` on the value of `foo` and
-                // closurize it into a new, normal thunk (non revertible), we lose the ability to
+                // closurize it into a new, normal cache element (non revertible), we lose the ability to
                 // override `foo` and we end up with the unexpected result `{foo = 2, bar = 2}`.
                 //
                 // What we want is that:
@@ -2950,12 +2950,12 @@ impl RecPriority {
                 // {foo | default = bar + 1, bar | default = 1}
                 // ```
                 //
-                // For revertible thunks, we don't want to only map the push operator on the
+                // For revertible elements, we don't want to only map the push operator on the
                 // current cached value, but also on the original expression.
                 //
-                // To do so, we create a new independent copy of the original thunk by mapping the
+                // To do so, we create a new independent copy of the original element by mapping the
                 // function over both expressions (in the sense of both the original expression and
-                // the cached expression). This logic is encapsulated by `Thunk::map`.
+                // the cached expression). This logic is encapsulated by [crate::eval::cache::Cache::map_at_index].
 
                 field.value = field.value.take().map(|value| {
                     if let Term::Var(id_inner) = value.as_ref() {
@@ -3319,15 +3319,14 @@ impl RecordDataExt for RecordData {
 mod tests {
     use super::*;
     use crate::cache::resolvers::DummyResolver;
-    use crate::eval::cache::CBNCache;
+    use crate::eval::cache::CacheImpl;
     use crate::eval::Environment;
 
-    type EC = CBNCache;
-
     #[test]
     fn ite_operation() {
         let cont: OperationCont = OperationCont::Op1(UnaryOp::Ite(), TermPos::None);
-        let mut vm: VirtualMachine<DummyResolver, EC> = VirtualMachine::new(DummyResolver {});
+        let mut vm: VirtualMachine<DummyResolver, CacheImpl> =
+            VirtualMachine::new(DummyResolver {});
 
         vm.stack.push_arg(
             Closure::atomic_closure(Term::Num(5.0).into()),
@@ -3416,7 +3415,8 @@ mod tests {
             TermPos::None,
         );
 
-        let mut vm: VirtualMachine<DummyResolver, EC> = VirtualMachine::new(DummyResolver {});
+        let mut vm: VirtualMachine<DummyResolver, CacheImpl> =
+            VirtualMachine::new(DummyResolver {});
         let mut clos = Closure {
             body: Term::Num(6.0).into(),
             env: Environment::new(),
diff --git a/src/eval/stack.rs b/src/eval/stack.rs
index cfad05b0..feacb90c 100644
--- a/src/eval/stack.rs
+++ b/src/eval/stack.rs
@@ -31,7 +31,7 @@ pub enum Marker<C: Cache> {
     Eq(Closure, Closure),
     /// An argument of an application.
     Arg(Closure, TermPos),
-    /// A tracked argument. Behave the same as a standard argument, but is given directly as a thunk, such that
+    /// A tracked argument. Behave the same as a standard argument, but is given directly as a cache index, such that
     /// it can be shared with other part of the program.
     ///
     /// In particular, contract arguments are tracked, in order to report the actual, evaluated offending term in case of blame.
@@ -130,7 +130,7 @@ impl<C: Cache> Stack<C> {
         count
     }
 
-    /// Pops all items in the stack and resets the state of the thunks it encounters.
+    /// Pops all items in the stack and resets the state of the [Cache] elements it encounters.
     pub fn reset(&mut self, cache: &mut C) {
         while let Some(marker) = self.0.pop() {
             if let Marker::UpdateIndex(mut uidx) = marker {
@@ -293,7 +293,7 @@ impl<C: Cache> Stack<C> {
         }
     }
 
-    /// Check if the top element is a thunk.
+    /// Check if the top element is a [CacheIndex].
     pub fn is_top_idx(&self) -> bool {
         self.0.last().map(Marker::is_idx).unwrap_or(false)
     }
@@ -310,7 +310,7 @@ impl<C: Cache> Stack<C> {
     }
 
     /// Turning the top element of the stack into a tracked arg if it was not already. Returns the
-    /// corresponding thunk, or `None` if the top element wasn't an argument.
+    /// corresponding index, or `None` if the top element wasn't an argument.
     pub fn track_arg(&mut self, cache: &mut C) -> Option<CacheIndex> {
         match self.0.last_mut() {
             Some(Marker::TrackedArg(idx, _)) => Some(idx.clone()),
@@ -338,14 +338,12 @@ impl<C: Cache> std::fmt::Debug for Stack<C> {
 #[cfg(test)]
 mod tests {
     use super::*;
-    use crate::eval::{cache::CBNCache, IdentKind};
+    use crate::eval::{cache::CacheImpl, IdentKind};
     use crate::term::{Term, UnaryOp};
     use assert_matches::assert_matches;
 
-    type EC = CBNCache;
-
-    impl Stack<EC> {
-        /// Count the number of thunks at the top of the stack.
+    impl Stack<CacheImpl> {
+        /// Count the number of indices at the top of the stack.
         pub fn count_thunks(&self) -> usize {
             Stack::count(self, Marker::is_idx)
         }
@@ -364,23 +362,23 @@ mod tests {
         OperationCont::Op1(UnaryOp::Typeof(), TermPos::None)
     }
 
-    fn some_arg_marker() -> Marker<EC> {
+    fn some_arg_marker() -> Marker<CacheImpl> {
         Marker::Arg(some_closure(), TermPos::None)
     }
 
-    fn some_thunk_marker(eval_cache: &mut EC) -> Marker<EC> {
+    fn some_thunk_marker(eval_cache: &mut CacheImpl) -> Marker<CacheImpl> {
         let mut idx = eval_cache.add(some_closure(), IdentKind::Let, BindingType::Normal);
         let uidx = eval_cache.make_update_index(&mut idx).unwrap();
         Marker::UpdateIndex(uidx)
     }
 
-    fn some_cont_marker() -> Marker<EC> {
+    fn some_cont_marker() -> Marker<CacheImpl> {
         Marker::Cont(some_cont(), 42, TermPos::None)
     }
 
     #[test]
     fn marker_differentiates() {
-        let mut eval_cache = EC::new();
+        let mut eval_cache = CacheImpl::new();
         assert!(some_arg_marker().is_arg());
         assert!(some_thunk_marker(&mut eval_cache).is_idx());
         assert!(some_cont_marker().is_cont());
@@ -396,7 +394,7 @@ mod tests {
         assert_eq!(2, s.count_args());
         assert_eq!(
             some_closure(),
-            s.pop_arg(&EC::new()).expect("Already checked").0
+            s.pop_arg(&CacheImpl::new()).expect("Already checked").0
         );
         assert_eq!(1, s.count_args());
     }
@@ -406,7 +404,7 @@ mod tests {
         let mut s = Stack::new();
         assert_eq!(0, s.count_thunks());
 
-        let mut eval_cache = EC::new();
+        let mut eval_cache = CacheImpl::new();
 
         let mut idx = eval_cache.add(some_closure(), IdentKind::Let, BindingType::Normal);
         s.push_update_index(eval_cache.make_update_index(&mut idx).unwrap());
@@ -420,7 +418,7 @@ mod tests {
 
     #[test]
     fn thunk_blackhole() {
-        let mut eval_cache = CBNCache::new();
+        let mut eval_cache = CacheImpl::new();
         let mut idx = eval_cache.add(some_closure(), IdentKind::Let, BindingType::Normal);
         let idx_upd = eval_cache.make_update_index(&mut idx);
         assert_matches!(idx_upd, Ok(..));
diff --git a/src/lib.rs b/src/lib.rs
index c7769aca..eda28e2c 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1,6 +1,6 @@
 pub mod cache;
 pub mod deserialize;
-pub mod destruct;
+pub mod destructuring;
 pub mod environment;
 pub mod error;
 pub mod eval;
diff --git a/src/parser/grammar.lalrpop b/src/parser/grammar.lalrpop
index 58238747..00e7d0d0 100644
--- a/src/parser/grammar.lalrpop
+++ b/src/parser/grammar.lalrpop
@@ -56,7 +56,7 @@ use crate::{
     mk_opn,
     mk_fun,
     identifier::Ident,
-    destruct::{Match, LastMatch, Destruct},
+    destructuring::{Match, LastMatch, RecordPattern},
     term::{
         *,
         record::{RecordAttrs, Field, FieldMetadata},
@@ -233,7 +233,7 @@ UniTerm: UniTerm = {
     <l: @L> "fun" <pats: Pattern+> "=>" <t: Term> <r: @R> => {
         let pos = mk_pos(src_id, l, r);
         let rt = pats.into_iter().rev().fold(t, |t, (id, destruct)| RichTerm {
-            term: SharedTerm::new(Term::FunPattern(id, destruct, t)),
+            term: SharedTerm::new(mk_fun(id, destruct, t)),
             pos,
         });
 
@@ -450,13 +450,13 @@ LastMatch: LastMatch = {
 
 // The right hand side of an `=` inside a destructuring pattern.
 #[inline]
-Pattern: (Option<Ident>,Destruct) = {
-    <id:(<Ident> "@")?> <pat:Destruct> => (id,pat),
-    Ident => (Some(<>),Destruct::Empty),
+Pattern: (Option<Ident>, Option<RecordPattern>) = {
+    <id:(<Ident> "@")?> <pat: RecordPattern> => (id, Some(pat)),
+    Ident => (Some(<>), None),
 };
 
 // A full pattern at the left-hand side of a destructuring let.
-Destruct: Destruct = {
+RecordPattern: RecordPattern = {
     <start: @L> "{" <mut matches: (<Match> ",")*> <last:LastMatch?> "}" <end: @R> => {
         let (open, rest) = match last {
             Some(LastMatch::Match(m)) => {
@@ -468,7 +468,7 @@ Destruct: Destruct = {
         };
 
         let span = mk_span(src_id, start, end);
-        Destruct::Record{matches, open, rest, span}
+        RecordPattern{ matches, open, rest, span }
     },
 };
 
diff --git a/src/parser/utils.rs b/src/parser/utils.rs
index a4415599..d34a2005 100644
--- a/src/parser/utils.rs
+++ b/src/parser/utils.rs
@@ -10,7 +10,7 @@ use codespan::FileId;
 use super::error::ParseError;
 
 use crate::{
-    destruct::Destruct,
+    destructuring::RecordPattern,
     eval::operation::RecPriority,
     identifier::Ident,
     label::Label,
@@ -565,19 +565,19 @@ pub fn mk_label(types: Types, src_id: FileId, l: usize, r: usize) -> Label {
 pub fn mk_let(
     rec: bool,
     id: Option<Ident>,
-    pat: Destruct,
+    pat: Option<RecordPattern>,
     t1: RichTerm,
     t2: RichTerm,
     span: RawSpan,
 ) -> Result<RichTerm, ParseError> {
     let result = match pat {
-        d @ Destruct::Record { .. } => {
+        Some(d) => {
             if rec {
                 return Err(ParseError::RecursiveLetPattern(span));
             }
             mk_term::let_pat(id, d, t1, t2)
         }
-        Destruct::Empty => {
+        None => {
             if let Some(id) = id {
                 if rec {
                     mk_term::let_rec_in(id, t1, t2)
@@ -593,6 +593,21 @@ pub fn mk_let(
     Ok(result)
 }
 
+/// Generate a `Fun` or a `FunPattern` (depending on `pat` being empty or not) from the
+/// parsing of a function definition. This function panics if the definition somehow
+/// has neither an `Ident` nor a non-`Empty` `Destruct` pattern.
+pub fn mk_fun(id: Option<Ident>, pat: Option<RecordPattern>, body: RichTerm) -> Term {
+    match pat {
+        Some(d) => Term::FunPattern(id, d, body),
+        None => {
+            let Some(id) = id else {
+                unreachable!("functions always have either a non-Empty pattern or an ident")
+            };
+            Term::Fun(id, body)
+        }
+    }
+}
+
 /// Determine the minimal level of indentation of a multi-line string.
 ///
 /// The result is determined by computing the minimum indentation level among all lines, where the
diff --git a/src/pretty.rs b/src/pretty.rs
index 50421599..81b9f80f 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -1,4 +1,4 @@
-use crate::destruct::{self, Destruct};
+use crate::destructuring::{self, RecordPattern};
 use crate::identifier::Ident;
 use crate::parser::lexer::KEYWORDS;
 
@@ -358,68 +358,66 @@ where
     }
 }
 
-impl<'a, D, A> Pretty<'a, D, A> for &Destruct
+impl<'a, D, A> Pretty<'a, D, A> for &RecordPattern
 where
     D: NickelAllocatorExt<'a, A>,
     D::Doc: Clone,
     A: Clone + 'a,
 {
     fn pretty(self, allocator: &'a D) -> DocBuilder<'a, D, A> {
-        match self {
-            Destruct::Record {
-                matches,
-                open,
-                rest,
-                ..
-            } => allocator
-                .intersperse(
-                    matches.iter().map(|m| match m {
-                        destruct::Match::Simple(id, field) => allocator
-                            .as_string(id)
-                            .append(allocator.space())
-                            .append(match field {
-                                Field {
-                                    value: Some(value),
-                                    metadata:
-                                        FieldMetadata {
-                                            annotation,
-                                            priority: MergePriority::Bottom,
-                                            ..
-                                        },
-                                    ..
-                                } => allocator
-                                    .text("?")
-                                    .append(allocator.space())
-                                    .append(allocator.atom(value))
-                                    .append(allocator.field_metadata(
-                                        &FieldMetadata {
-                                            annotation: annotation.clone(),
-                                            ..Default::default()
-                                        },
-                                        false,
-                                    )),
-                                field => allocator.field_metadata(&field.metadata, false),
-                            }),
-                        _ => unimplemented!(),
-                    }),
-                    allocator.text(",").append(allocator.space()),
-                )
-                .append(if *open {
-                    allocator
-                        .text(",")
+        let RecordPattern {
+            matches,
+            open,
+            rest,
+            ..
+        } = self;
+        allocator
+            .intersperse(
+                matches.iter().map(|m| match m {
+                    destructuring::Match::Simple(id, field) => allocator
+                        .as_string(id)
                         .append(allocator.space())
-                        .append(allocator.text(".."))
-                        .append(if let Some(rest) = rest {
-                            allocator.as_string(rest)
-                        } else {
-                            allocator.nil()
-                        })
-                } else {
-                    allocator.nil()
-                })
-                .braces(),
-            Destruct::Empty => allocator.nil(),
-        }
+                        .append(match field {
+                            Field {
+                                value: Some(value),
+                                metadata:
+                                    FieldMetadata {
+                                        annotation,
+                                        priority: MergePriority::Bottom,
+                                        ..
+                                    },
+                                ..
+                            } => allocator
+                                .text("?")
+                                .append(allocator.space())
+                                .append(allocator.atom(value))
+                                .append(allocator.field_metadata(
+                                    &FieldMetadata {
+                                        annotation: annotation.clone(),
+                                        ..Default::default()
+                                    },
+                                    false,
+                                )),
+                            field => allocator.field_metadata(&field.metadata, false),
+                        }),
+                    _ => unimplemented!(),
+                }),
+                allocator.text(",").append(allocator.space()),
+            )
+            .append(if *open {
+                allocator
+                    .text(",")
+                    .append(allocator.space())
+                    .append(allocator.text(".."))
+                    .append(if let Some(rest) = rest {
+                        allocator.as_string(rest)
+                    } else {
+                        allocator.nil()
+                    })
+            } else {
+                allocator.nil()
+            })
+            .braces()
     }
 }
 
@@ -470,11 +468,9 @@ where
                 let mut rt = &self;
                 while let FunPattern(id, dst, t) = rt.as_ref() {
                     params.push(if let Some(id) = id {
-                        allocator.as_string(id).append(if !dst.is_empty() {
-                            allocator.text("@").append(dst.pretty(allocator))
-                        } else {
-                            allocator.nil()
-                        })
+                        allocator
+                            .as_string(id)
+                            .append(allocator.text("@").append(dst.pretty(allocator)))
                     } else {
                         dst.pretty(allocator)
                     });
@@ -525,14 +521,12 @@ where
                 .append(
                     (*opt_id)
                         .map(|id| {
-                            allocator.as_string(id).append(if dst.is_empty() {
-                                allocator.nil()
-                            } else {
+                            allocator.as_string(id).append(
                                 allocator
                                     .space()
                                     .append(allocator.text("@"))
-                                    .append(allocator.space())
-                            })
+                                    .append(allocator.space()),
+                            )
                         })
                         .unwrap_or_else(|| allocator.nil()),
                 )
diff --git a/src/program.rs b/src/program.rs
index d09d2c16..8ad54730 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -519,35 +519,35 @@ mod doc {
 mod tests {
     use super::*;
     use crate::error::EvalError;
-    use crate::eval::cache::CBNCache;
+    use crate::eval::cache::CacheImpl;
     use crate::position::TermPos;
     use crate::term::array::ArrayAttrs;
     use assert_matches::assert_matches;
     use std::io::Cursor;
 
-    type EC = CBNCache;
-
     fn eval_full(s: &str) -> Result<RichTerm, Error> {
         let src = Cursor::new(s);
 
-        let mut p: Program<EC> = Program::new_from_source(src, "<test>").map_err(|io_err| {
-            Error::EvalError(EvalError::Other(
-                format!("IO error: {io_err}"),
-                TermPos::None,
-            ))
-        })?;
+        let mut p: Program<CacheImpl> =
+            Program::new_from_source(src, "<test>").map_err(|io_err| {
+                Error::EvalError(EvalError::Other(
+                    format!("IO error: {io_err}"),
+                    TermPos::None,
+                ))
+            })?;
         p.eval_full()
     }
 
     fn typecheck(s: &str) -> Result<(), Error> {
         let src = Cursor::new(s);
 
-        let mut p: Program<EC> = Program::new_from_source(src, "<test>").map_err(|io_err| {
-            Error::EvalError(EvalError::Other(
-                format!("IO error: {io_err}"),
-                TermPos::None,
-            ))
-        })?;
+        let mut p: Program<CacheImpl> =
+            Program::new_from_source(src, "<test>").map_err(|io_err| {
+                Error::EvalError(EvalError::Other(
+                    format!("IO error: {io_err}"),
+                    TermPos::None,
+                ))
+            })?;
         p.typecheck()
     }
 
diff --git a/src/repl/rustyline_frontend.rs b/src/repl/rustyline_frontend.rs
index 1a147c5e..8914805c 100644
--- a/src/repl/rustyline_frontend.rs
+++ b/src/repl/rustyline_frontend.rs
@@ -4,6 +4,7 @@ use std::path::PathBuf;
 use super::command::Command;
 use super::*;
 
+use crate::eval::cache::CacheImpl;
 use crate::program::{self, ColorOpt};
 use ansi_term::{Colour, Style};
 use rustyline::config::OutputStreamType;
@@ -33,7 +34,7 @@ impl From<ColorOpt> for rustyline::config::ColorMode {
 
 /// Main loop of the REPL.
 pub fn repl(histfile: PathBuf, color_opt: ColorOpt) -> Result<(), InitError> {
-    let mut repl = ReplImpl::<crate::eval::cache::CBNCache>::new();
+    let mut repl = ReplImpl::<CacheImpl>::new();
 
     match repl.load_stdlib() {
         Ok(()) => (),
diff --git a/src/repl/wasm_frontend.rs b/src/repl/wasm_frontend.rs
index c83c97b6..78c991a7 100644
--- a/src/repl/wasm_frontend.rs
+++ b/src/repl/wasm_frontend.rs
@@ -3,7 +3,7 @@ use super::simple_frontend::{input, serialize, InputError, InputResult};
 use super::{Repl, ReplImpl};
 use crate::cache::Cache;
 use crate::error::ToDiagnostic;
-use crate::eval::cache::CBNCache;
+use crate::eval::cache::CacheImpl;
 use crate::serialize::ExportFormat;
 use codespan::{FileId, Files};
 use codespan_reporting::{
@@ -244,7 +244,7 @@ impl From<InputResult> for WasmInputResult {
 
 /// WASM-compatible wrapper around `ReplImpl`.
 #[wasm_bindgen]
-pub struct ReplState(ReplImpl<CBNCache>);
+pub struct ReplState(ReplImpl<CacheImpl>);
 
 /// WASM-compatible wrapper around `serialize::ExportFormat`.
 #[wasm_bindgen]
diff --git a/src/serialize.rs b/src/serialize.rs
index 08261df8..927d95d7 100644
--- a/src/serialize.rs
+++ b/src/serialize.rs
@@ -271,16 +271,15 @@ mod tests {
     use super::*;
     use crate::cache::resolvers::DummyResolver;
     use crate::error::{Error, EvalError};
-    use crate::eval::{cache::CBNCache, Environment, VirtualMachine};
+    use crate::eval::cache::CacheImpl;
+    use crate::eval::{Environment, VirtualMachine};
     use crate::position::TermPos;
     use crate::program::Program;
     use crate::term::{make as mk_term, BinaryOp};
     use serde_json::json;
     use std::io::Cursor;
 
-    type EC = CBNCache;
-
-    fn mk_program(s: &str) -> Result<Program<EC>, Error> {
+    fn mk_program(s: &str) -> Result<Program<CacheImpl>, Error> {
         let src = Cursor::new(s);
 
         Program::new_from_source(src, "<test>").map_err(|io_err| {
@@ -336,7 +335,7 @@ mod tests {
                     .unwrap();
 
             assert_eq!(
-                VirtualMachine::<_, EC>::new(DummyResolver {})
+                VirtualMachine::<_, CacheImpl>::new(DummyResolver {})
                     .eval(
                         mk_term::op2(BinaryOp::Eq(), from_json, evaluated.clone()),
                         &Environment::new(),
@@ -345,7 +344,7 @@ mod tests {
                 Ok(Term::Bool(true))
             );
             assert_eq!(
-                VirtualMachine::<_, EC>::new(DummyResolver {})
+                VirtualMachine::<_, CacheImpl>::new(DummyResolver {})
                     .eval(
                         mk_term::op2(BinaryOp::Eq(), from_yaml, evaluated.clone()),
                         &Environment::new(),
@@ -354,7 +353,7 @@ mod tests {
                 Ok(Term::Bool(true))
             );
             assert_eq!(
-                VirtualMachine::<_, EC>::new(DummyResolver {})
+                VirtualMachine::<_, CacheImpl>::new(DummyResolver {})
                     .eval(
                         mk_term::op2(BinaryOp::Eq(), from_toml, evaluated),
                         &Environment::new(),
diff --git a/src/term/array.rs b/src/term/array.rs
index 62ed77e9..13f24fb6 100644
--- a/src/term/array.rs
+++ b/src/term/array.rs
@@ -7,7 +7,7 @@ use super::*;
 pub struct ArrayAttrs {
     /// A `closurized` array verifies the following conditions:
     ///   - Each element is a generated variable with a unique name (although the same
-    ///     variable can occur in several places, it should always refer to the same thunk anyway).
+    ///     variable can occur in several places, it should always refer to the same index anyway).
     ///   - The environment of the array's closure only contains those generated variables.
     pub closurized: bool,
     /// List of lazily-applied contracts.
diff --git a/src/term/mod.rs b/src/term/mod.rs
index 76cc112a..d17db9d7 100644
--- a/src/term/mod.rs
+++ b/src/term/mod.rs
@@ -24,7 +24,7 @@ use array::{Array, ArrayAttrs};
 use record::{Field, FieldDeps, FieldMetadata, RecordData, RecordDeps};
 
 use crate::{
-    destruct::Destruct,
+    destructuring::RecordPattern,
     error::{EvalError, ParseError},
     identifier::Ident,
     label::Label,
@@ -78,7 +78,7 @@ pub enum Term {
     Fun(Ident, RichTerm),
     /// A function able to destruct its arguments.
     #[serde(skip)]
-    FunPattern(Option<Ident>, Destruct, RichTerm),
+    FunPattern(Option<Ident>, RecordPattern, RichTerm),
     /// A blame label.
     #[serde(skip)]
     Lbl(Label),
@@ -88,7 +88,7 @@ pub enum Term {
     Let(Ident, RichTerm, RichTerm, LetAttrs),
     /// A destructuring let-binding.
     #[serde(skip)]
-    LetPattern(Option<Ident>, Destruct, RichTerm, RichTerm),
+    LetPattern(Option<Ident>, RecordPattern, RichTerm, RichTerm),
     /// An application.
     #[serde(skip)]
     App(RichTerm, RichTerm),
@@ -208,7 +208,7 @@ pub enum Term {
 pub type SealingKey = i32;
 
 /// Type of let-binding. This only affects run-time behavior. Revertible bindings introduce
-/// revertible thunks at evaluation, which are devices used for the implementation of recursive
+/// revertible cache elements at evaluation, which are devices used for the implementation of recursive
 /// records merging. See the [`crate::eval::merge`] and [`crate::eval`] modules for more details.
 #[derive(Debug, Eq, PartialEq, Clone)]
 pub enum BindingType {
@@ -1100,8 +1100,8 @@ pub enum UnaryOp {
     ///
     /// # `Force` vs. `DeepSeq`
     ///
-    /// [`UnaryOp::Force`] updates the thunks containing arrays with a new version where the lazy contracts have all been applied,
-    /// whereas [`UnaryOp::DeepSeq`] evaluates the same expressions, but it never updates the thunk of an array with lazy contracts
+    /// [`UnaryOp::Force`] updates at the indices containing arrays with a new version where the lazy contracts have all been applied,
+    /// whereas [`UnaryOp::DeepSeq`] evaluates the same expressions, but it never updates at the index of an array with lazy contracts
     /// with an array where those contracts have been applied. In a way, the result of lazy contract application in arrays is "lost"
     /// in [`UnaryOp::DeepSeq`], while it's returned in [`UnaryOp::Force`].
     ///
@@ -1868,7 +1868,7 @@ pub mod make {
     where
         T1: Into<RichTerm>,
         T2: Into<RichTerm>,
-        D: Into<Destruct>,
+        D: Into<RecordPattern>,
         I: Into<Ident>,
     {
         Term::LetPattern(id.map(|i| i.into()), pat.into(), t1.into(), t2.into()).into()
diff --git a/src/term/record.rs b/src/term/record.rs
index 576d4eda..8be0087f 100644
--- a/src/term/record.rs
+++ b/src/term/record.rs
@@ -21,20 +21,20 @@ impl RecordAttrs {
     }
 }
 
-/// Dependencies of a field or a thunk over the other recursive fields of a recursive record.
+/// Dependencies of a field or a cache element over the other recursive fields of a recursive record.
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub enum FieldDeps {
-    /// The set of dependencies is fixed and has been computed. When attached to a thunk, an empty
-    /// set of dependency means that the thunk isn't revertible, but standard.
+    /// The set of dependencies is fixed and has been computed. When attached to an element, an empty
+    /// set of dependency means that the element isn't revertible, but standard.
     Known(Rc<HashSet<Ident>>),
-    /// The thunk is revertible, but the set of dependencies hasn't been computed. In that case,
+    /// The element is revertible, but the set of dependencies hasn't been computed. In that case,
     /// the interpreter should be conservative and assume that any recursive references can appear
-    /// in the content of the corresponding thunk.
+    /// in the content of the corresponding element.
     Unknown,
 }
 
 impl FieldDeps {
-    /// Compute the union of two thunk dependencies. [`FieldDeps::Unknown`] can be see as the top
+    /// Compute the union of two cache elements dependencies. [`FieldDeps::Unknown`] can be see as the top
     /// element, meaning that if one of the two set of dependencies is [`FieldDeps::Unknown`], so
     /// is the result.
     pub fn union(self, other: Self) -> Self {
diff --git a/src/transform/desugar_destructuring.rs b/src/transform/desugar_destructuring.rs
index 366fa528..c129df15 100644
--- a/src/transform/desugar_destructuring.rs
+++ b/src/transform/desugar_destructuring.rs
@@ -30,11 +30,12 @@
 //!     <do_something>
 //! ) in ...
 //! ```
-use crate::destruct::{Destruct, Match};
+use crate::destructuring::{Match, RecordPattern};
 use crate::identifier::Ident;
 use crate::match_sharedterm;
 use crate::term::make::{op1, op2};
 use crate::term::{BinaryOp::DynRemove, RichTerm, Term, TypeAnnotation, UnaryOp::StaticAccess};
+use crate::term::{BindingType, LetAttrs};
 
 /// Entry point of the patterns desugaring.
 /// It desugar a `RichTerm` if possible (the term is a let pattern or a function with patterns in
@@ -54,23 +55,23 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
 /// down traversal. This means that the return value is a normal `Term::Fun` but it can contain
 /// `Term::FunPattern` and `Term::LetPattern` inside.
 pub fn desugar_fun(rt: RichTerm) -> RichTerm {
-    match_sharedterm! {rt.term, with {
-        Term::FunPattern(x, pat, t_) if !pat.is_empty() => {
-            let x = x.unwrap_or_else(Ident::fresh);
-            let t_pos = t_.pos;
-            RichTerm::new(
-                Term::Fun(
-                    x,
-                    RichTerm::new(Term::LetPattern(None, pat, Term::Var(x).into(), t_), t_pos /* TODO: should we use rt.pos? */),
-                ),
-                rt.pos,
-            )
-        },
-        Term::FunPattern(Some(x), Destruct::Empty, t_) => RichTerm::new(Term::Fun(x, t_), rt.pos),
-        t@Term::FunPattern(..) => panic!(
-            "A function can not have empty pattern without name in {t:?}"
-        ),
-    } else rt
+    match_sharedterm! { rt.term,
+        with {
+            Term::FunPattern(x, pat, t_) => {
+                let x = x.unwrap_or_else(Ident::fresh);
+                let t_pos = t_.pos;
+                RichTerm::new(
+                    Term::Fun(
+                        x,
+                        RichTerm::new(Term::LetPattern(None, pat, Term::Var(x).into(), t_), t_pos /* TODO: should we use rt.pos? */),
+                    ),
+                    rt.pos,
+                )
+            }
+        }
+        else {
+            rt
+        }
     }
 }
 
@@ -128,26 +129,25 @@ pub fn desugar(rt: RichTerm) -> RichTerm {
 /// `x` is the identifier pointing to the full record. If having `val @ {...} = ... in ...` the
 /// variable x should be `Ident("val")` but if we have a `@` binding less form, you will probably
 /// generate a fresh variable.
-fn bind_open_field(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
+fn bind_open_field(x: Ident, pat: &RecordPattern, body: RichTerm) -> RichTerm {
     let (matches, var) = match pat {
-        Destruct::Record {
+        RecordPattern {
             matches,
             open: true,
             rest: Some(x),
             ..
         } => (matches, *x),
-        Destruct::Record {
+        RecordPattern {
             matches,
             open: true,
             rest: None,
             ..
         } => (matches, Ident::fresh()),
-        Destruct::Record {
+        RecordPattern {
             open: false,
             rest: None,
             ..
-        }
-        | Destruct::Empty => return body,
+        } => return body,
         _ => panic!("A closed pattern can not have a rest binding"),
     };
     Term::Let(
@@ -165,24 +165,35 @@ fn bind_open_field(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
 
 /// Core of the destructuring. Bind all the variables of the pattern except the "open" (`..y`)
 /// part. For that, see `bind_open_field`.
-fn destruct_term(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
+fn destruct_term(x: Ident, pat: &RecordPattern, body: RichTerm) -> RichTerm {
     let pos = body.pos;
-    match pat {
-        Destruct::Record { matches, .. } => matches.iter().fold(body, move |t, m| match m {
-            Match::Simple(id, _) => RichTerm::new(
-                Term::Let(
-                    *id,
-                    op1(StaticAccess(*id), Term::Var(x)),
-                    t,
-                    Default::default(),
-                ),
-                pos,
+    let RecordPattern { matches, .. } = pat;
+    matches.iter().fold(body, move |t, m| match m {
+        Match::Simple(id, _) => RichTerm::new(
+            Term::Let(
+                *id,
+                op1(StaticAccess(*id), Term::Var(x)),
+                t,
+                Default::default(),
             ),
-            Match::Assign(f, _, (id, pat)) => desugar(RichTerm::new(
-                Term::LetPattern(*id, pat.clone(), op1(StaticAccess(*f), Term::Var(x)), t),
-                pos,
-            )),
-        }),
-        _ => body,
-    }
+            pos,
+        ),
+        Match::Assign(f, _, (id, Some(pat))) => desugar(RichTerm::new(
+            Term::LetPattern(*id, pat.clone(), op1(StaticAccess(*f), Term::Var(x)), t),
+            pos,
+        )),
+        Match::Assign(f, _, (Some(id), None)) => desugar(RichTerm::new(
+            Term::Let(
+                *id,
+                op1(StaticAccess(*f), Term::Var(x)),
+                t,
+                LetAttrs {
+                    binding_type: BindingType::Normal,
+                    rec: false,
+                },
+            ),
+            pos,
+        )),
+        _ => unreachable!("Match::Assign always has either an ident or a pattern"),
+    })
 }
diff --git a/src/transform/free_vars.rs b/src/transform/free_vars.rs
index b8536c95..dc861f1c 100644
--- a/src/transform/free_vars.rs
+++ b/src/transform/free_vars.rs
@@ -4,7 +4,7 @@
 //! the recursive fields that actually appear in the definition of each field when computing the
 //! fixpoint.
 use crate::{
-    destruct::{Destruct, Match},
+    destructuring::{Match, RecordPattern},
     identifier::Ident,
     term::{
         record::{Field, FieldDeps, RecordDeps},
@@ -229,18 +229,14 @@ impl CollectFreeVars for Field {
 }
 
 /// Remove the variables bound by a destructuring pattern from a set of free variables.
-fn bind_pattern(dest_pat: &Destruct, free_vars: &mut HashSet<Ident>) {
-    match dest_pat {
-        Destruct::Record { matches, rest, .. } => {
-            for m in matches {
-                bind_match(m, free_vars);
-            }
+fn bind_pattern(dest_pat: &RecordPattern, free_vars: &mut HashSet<Ident>) {
+    let RecordPattern { matches, rest, .. } = dest_pat;
+    for m in matches {
+        bind_match(m, free_vars);
+    }
 
-            if let Some(rest) = rest {
-                free_vars.remove(rest);
-            }
-        }
-        Destruct::Empty => {}
+    if let Some(rest) = rest {
+        free_vars.remove(rest);
     }
 }
 
@@ -252,7 +248,9 @@ fn bind_match(m: &Match, free_vars: &mut HashSet<Ident>) {
             if let Some(id) = id {
                 free_vars.remove(id);
             }
-            bind_pattern(sub_pat, free_vars);
+            if let Some(sub_pat) = sub_pat {
+                bind_pattern(sub_pat, free_vars);
+            }
         }
         Match::Simple(id, _) => {
             free_vars.remove(id);
diff --git a/src/transform/mod.rs b/src/transform/mod.rs
index 1f05b326..7f3b2ed9 100644
--- a/src/transform/mod.rs
+++ b/src/transform/mod.rs
@@ -100,15 +100,15 @@ impl Closurizable for RichTerm {
         with_env: Environment,
     ) -> RichTerm {
         // If the term is already a variable, we don't have to create a useless intermediate
-        // closure. We just transfer the original thunk to the new environment. This is not only an
+        // closure. We just transfer the original index to the new environment. This is not only an
         // optimization: this is relied upon by recursive record merging when computing the
         // fixpoint.
         //
         // More specifically, the evaluation of a recursive record patches the environment of each
-        // field with the thunks recursively referring to the other fields of the record. `eval`
+        // field with the indices recursively referring to the other fields of the record. `eval`
         // assumes that a recursive record field is either a constant or a generated variable whose
-        // thunks *immediately* contain the original unevaluated expression (both properties are
-        // true after the share normal form transformation and maintained when reverting thunks
+        // cache elements *immediately* contain the original unevaluated expression (both properties are
+        // true after the share normal form transformation and maintained when reverting elements
         // before merging recursive records).
         //
         // To maintain this invariant, `closurize` must NOT introduce an indirection through a
diff --git a/src/transform/share_normal_form.rs b/src/transform/share_normal_form.rs
index d9ea5fea..e26b69f4 100644
--- a/src/transform/share_normal_form.rs
+++ b/src/transform/share_normal_form.rs
@@ -1,6 +1,6 @@
 //! Share normal form.
 //!
-//! Replace the subexpressions of WHNFs that are not functions by thunks, such that they can be
+//! Replace the subexpressions of WHNFs that are not functions by indices, such that they can be
 //! shared. It is similar to the behavior of other lazy languages with respect to data
 //! constructors.  To do so, subexpressions are replaced by fresh variables, introduced by new let
 //! bindings put at the beginning of the WHNF.
@@ -10,7 +10,7 @@
 //! let x = {a = 1 + 1} in x.a + x.a
 //! ```
 //!
-//! The term `{a = 1 + 1}` is a record, and hence a WHNF. In consequence, the thunk allocated to x
+//! The term `{a = 1 + 1}` is a record, and hence a WHNF. In consequence, the index pointing to x
 //! is never updated. Without additional machinery, `a` will be recomputed each time is it used,
 //! two times here.
 //!
@@ -22,8 +22,8 @@
 //! let x = (let var = 1 + 1 in {a = var}) in x.a + x.a
 //! ```
 //!
-//! Now, the field `a` points to the thunk introduced by `var`: at the evaluation of the first
-//! occurrence of `x.a`, this thunk is updated with `2`, and is not recomputed the second time.
+//! Now, the field `a` points to the element introduced by `var`: at the evaluation of the first
+//! occurrence of `x.a`, this element is updated with `2`, and is not recomputed the second time.
 //!
 //! Newly introduced variables begin with a special character to avoid clashing with user-defined
 //! variables.
@@ -177,7 +177,7 @@ fn transform_rec_field(
 
 fn mk_binding_type(field_deps: Option<FieldDeps>) -> BindingType {
     // If the fields has an empty set of dependencies, we can eschew the
-    // useless introduction of a revertible thunk. Note that
+    // useless introduction of a revertible element. Note that
     // `field_deps` being `None` doesn't mean "empty dependencies" but
     // rather that the dependencies haven't been computed. In the latter
     // case, we must be conservative and assume the field is potentially
@@ -193,7 +193,7 @@ fn mk_binding_type(field_deps: Option<FieldDeps>) -> BindingType {
     }
 }
 
-/// Determine if a subterm of a WHNF should be wrapped in a thunk in order to be shared.
+/// Determine if a subterm of a WHNF should be cached in order to be shared.
 ///
 /// Sharing is typically useless if the subterm is already a WHNF which can be copied without
 /// duplicating any work. On the other hand, a WHNF which can contain other shareable
diff --git a/src/typecheck/destructuring.rs b/src/typecheck/destructuring.rs
index 4e6ad075..82a0b2c6 100644
--- a/src/typecheck/destructuring.rs
+++ b/src/typecheck/destructuring.rs
@@ -1,56 +1,83 @@
 use std::collections::HashMap;
 
 use crate::{
-    destruct::{Destruct, Match},
+    destructuring::{Match, RecordPattern},
     identifier::Ident,
+    mk_uty_row,
     types::{RecordRowF, RecordRowsF, TypeF},
 };
 
 use super::{
-    mk_uniftype, Environment, GenericUnifRecordRowsIteratorItem, GenericUnifType, State,
-    UnifRecordRows, UnifType,
+    mk_uniftype, Environment, GenericUnifRecordRowsIteratorItem, State, UnifRecordRows, UnifType,
 };
 
-/// Build a `UnifType` from a `Destruct` pattern, creating fresh unification
-/// variables wherever specific types are unknown.
-pub fn build_pattern_type(state: &mut State, pat: &Destruct) -> UnifType {
-    match pat {
-        Destruct::Record { matches, open, .. } => {
-            let tail = if *open {
-                state.table.fresh_rrows_uvar()
-            } else {
-                UnifRecordRows::Concrete(RecordRowsF::Empty)
-            };
-
-            let rows = matches.iter().map(|m| match m {
-                Match::Simple(id, _) => RecordRowF {
-                    id: *id,
-                    types: Box::new(state.table.fresh_type_uvar()),
-                },
-                Match::Assign(id, _, (_, Destruct::Empty)) => RecordRowF {
-                    id: *id,
-                    types: Box::new(state.table.fresh_type_uvar()),
-                },
-                Match::Assign(id, _, (_, r_pat @ Destruct::Record { .. })) => {
-                    let ty = build_pattern_type(state, r_pat);
-                    RecordRowF {
-                        id: *id,
-                        types: Box::new(ty),
-                    }
-                }
-            });
+pub fn build_pattern_type_walk_mode(state: &mut State, pat: &RecordPattern) -> UnifRecordRows {
+    build_pattern_type(state, pat, TypecheckMode::Walk)
+}
 
-            let rrows = rows.fold(tail, |tail, row| {
-                UnifRecordRows::Concrete(RecordRowsF::Extend {
-                    row,
-                    tail: Box::new(tail),
-                })
-            });
+pub fn build_pattern_type_check_mode(state: &mut State, pat: &RecordPattern) -> UnifRecordRows {
+    build_pattern_type(state, pat, TypecheckMode::Check)
+}
 
-            UnifType::Concrete(TypeF::Record(rrows))
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+enum TypecheckMode {
+    Walk,
+    Check,
+}
+
+/// Build a `UnifType` from a `Destruct` pattern. The type of each "leaf"
+/// identifier will be assigned based on the `leaf_type` argument. The
+/// current possibilities are for each leaf to have type `Dyn` or to be
+/// assigned a fresh unification variable.
+fn build_pattern_type(
+    state: &mut State,
+    pat: &RecordPattern,
+    leaf_type: TypecheckMode,
+) -> UnifRecordRows {
+    fn new_leaf_type(state: &mut State, leaf_type: TypecheckMode) -> UnifType {
+        match leaf_type {
+            TypecheckMode::Walk => mk_uniftype::dynamic(),
+            TypecheckMode::Check => state.table.fresh_type_uvar(),
         }
-        Destruct::Empty => state.table.fresh_type_uvar(),
     }
+
+    let tail = if pat.open {
+        match leaf_type {
+            // We use a dynamic tail here since we're in walk mode,
+            // but if/when we remove dynamic record tails this could
+            // likely be made an empty tail with no impact.
+            TypecheckMode::Walk => mk_uty_row!(; RecordRowsF::TailDyn),
+            TypecheckMode::Check => state.table.fresh_rrows_uvar(),
+        }
+    } else {
+        UnifRecordRows::Concrete(RecordRowsF::Empty)
+    };
+
+    let rows = pat.matches.iter().map(|m| match m {
+        Match::Simple(id, _) => RecordRowF {
+            id: *id,
+            types: Box::new(new_leaf_type(state, leaf_type)),
+        },
+        Match::Assign(id, _, (_, None)) => RecordRowF {
+            id: *id,
+            types: Box::new(new_leaf_type(state, leaf_type)),
+        },
+        Match::Assign(id, _, (_, Some(r_pat))) => {
+            let row_tys = build_pattern_type(state, r_pat, leaf_type);
+            let ty = UnifType::Concrete(TypeF::Record(row_tys));
+            RecordRowF {
+                id: *id,
+                types: Box::new(ty),
+            }
+        }
+    });
+
+    rows.fold(tail, |tail, row| {
+        UnifRecordRows::Concrete(RecordRowsF::Extend {
+            row,
+            tail: Box::new(tail),
+        })
+    })
 }
 
 /// Extend `env` with any new bindings brought into scope in `pat`. The
@@ -62,50 +89,49 @@ pub fn build_pattern_type(state: &mut State, pat: &Destruct) -> UnifType {
 pub fn inject_pattern_variables(
     state: &State,
     env: &mut Environment,
-    pat: &Destruct,
-    pat_ty: UnifType,
+    pat: &RecordPattern,
+    pat_ty: UnifRecordRows,
 ) {
     let pat_ty = pat_ty.into_root(state.table);
+    let mut type_map = RecordTypes::from(&pat_ty);
 
-    match pat {
-        Destruct::Record { matches, rest, .. } => {
-            let mut type_map = RecordTypes::from(&pat_ty);
-
-            matches.iter().for_each(|m| match m {
-                Match::Simple(id, ..) => {
-                    let ty = type_map.get_type(id);
-                    env.insert(*id, ty);
-                }
-                Match::Assign(id, _, (bind_id, pat)) => {
-                    let ty = type_map.get_type(id);
-
-                    // If we don't have a `bind_id`, we can infer that `id` is
-                    // an intermediate value that isn't accessible from the code.
-                    // e.g. the `foo` in a binding like:
-                    //
-                    // ```
-                    //   let { foo = { bar = baz } } = { foo.bar = 1 } in ...
-                    // ```
-                    //
-                    // As such, we don't need to add it to the environment.
-                    if let Some(id) = bind_id {
-                        env.insert(*id, ty.clone());
-                    }
-
-                    // A non-empty `pat` here means we have a nested destructuring,
-                    // so we recursively call this function.
-                    if !pat.is_empty() {
-                        inject_pattern_variables(state, env, pat, ty)
-                    }
-                }
-            });
+    pat.matches.iter().for_each(|m| match m {
+        Match::Simple(id, ..) => {
+            let ty = type_map.get_type(id);
+            env.insert(*id, ty);
+        }
+        Match::Assign(id, _, (bind_id, pat)) => {
+            let ty = type_map.get_type(id);
+
+            // If we don't have a `bind_id`, we can infer that `id` is
+            // an intermediate value that isn't accessible from the code.
+            // e.g. the `foo` in a binding like:
+            //
+            // ```
+            //   let { foo = { bar = baz } } = { foo.bar = 1 } in ...
+            // ```
+            //
+            // As such, we don't need to add it to the environment.
+            if let Some(id) = bind_id {
+                env.insert(*id, ty.clone());
+            }
 
-            if let Some(id) = rest {
-                let rest_ty = type_map.rest();
-                env.insert(*id, rest_ty);
+            // A non-None `pat` here means we have a nested destructuring,
+            // so we recursively call this function.
+            if let Some(pat) = pat {
+                let UnifType::Concrete(TypeF::Record(rs)) = ty else {
+                            unreachable!("since this is a destructured record, \
+                                its type was constructed by build_pattern_ty, \
+                                so it must be a concrete record type")
+                        };
+                inject_pattern_variables(state, env, pat, rs)
             }
         }
-        Destruct::Empty => (),
+    });
+
+    if let Some(id) = pat.rest {
+        let rest_ty = type_map.rest();
+        env.insert(id, rest_ty);
     }
 }
 
@@ -115,44 +141,36 @@ pub fn inject_pattern_variables(
 /// pattern and its type. As well as keeping track of which identifiers
 /// have already been "used" in the pattern, to ensure that we can
 /// correctly construct the type of a `..rest` match, if it exists.
-enum RecordTypes {
-    Rows {
-        known_types: HashMap<Ident, UnifType>,
-        tail: UnifRecordRows,
-    },
-    Dyn,
+struct RecordTypes {
+    known_types: HashMap<Ident, UnifType>,
+    tail: UnifRecordRows,
 }
 
-impl From<&UnifType> for RecordTypes {
-    fn from(u: &UnifType) -> Self {
-        match u {
-            GenericUnifType::Concrete(TypeF::Record(t)) => {
-                let (tys, tail) =
-                    t.iter()
-                        .fold((HashMap::new(), None), |(mut m, _), ty| match ty {
-                            GenericUnifRecordRowsIteratorItem::Row(rt) => {
-                                m.insert(rt.id, rt.types.clone());
-                                (m, None)
-                            }
-                            GenericUnifRecordRowsIteratorItem::TailDyn => {
-                                (m, Some(UnifRecordRows::Concrete(RecordRowsF::TailDyn)))
-                            }
-                            GenericUnifRecordRowsIteratorItem::TailVar(v) => {
-                                (m, Some(UnifRecordRows::Concrete(RecordRowsF::TailVar(*v))))
-                            }
-                            GenericUnifRecordRowsIteratorItem::TailUnifVar(n) => {
-                                (m, Some(UnifRecordRows::UnifVar(n)))
-                            }
-                            GenericUnifRecordRowsIteratorItem::TailConstant(n) => {
-                                (m, Some(UnifRecordRows::Constant(n)))
-                            }
-                        });
-                RecordTypes::Rows {
-                    known_types: tys,
-                    tail: tail.unwrap_or(UnifRecordRows::Concrete(RecordRowsF::Empty)),
-                }
-            }
-            _ => RecordTypes::Dyn,
+impl From<&UnifRecordRows> for RecordTypes {
+    fn from(u: &UnifRecordRows) -> Self {
+        let (known_types, tail) =
+            u.iter()
+                .fold((HashMap::new(), None), |(mut m, _), ty| match ty {
+                    GenericUnifRecordRowsIteratorItem::Row(rt) => {
+                        m.insert(rt.id, rt.types.clone());
+                        (m, None)
+                    }
+                    GenericUnifRecordRowsIteratorItem::TailDyn => {
+                        (m, Some(UnifRecordRows::Concrete(RecordRowsF::TailDyn)))
+                    }
+                    GenericUnifRecordRowsIteratorItem::TailVar(v) => {
+                        (m, Some(UnifRecordRows::Concrete(RecordRowsF::TailVar(*v))))
+                    }
+                    GenericUnifRecordRowsIteratorItem::TailUnifVar(n) => {
+                        (m, Some(UnifRecordRows::UnifVar(n)))
+                    }
+                    GenericUnifRecordRowsIteratorItem::TailConstant(n) => {
+                        (m, Some(UnifRecordRows::Constant(n)))
+                    }
+                });
+        RecordTypes {
+            known_types,
+            tail: tail.unwrap_or(UnifRecordRows::Concrete(RecordRowsF::Empty)),
         }
     }
 }
@@ -164,35 +182,25 @@ impl RecordTypes {
     /// map, so that it won't be considered as part of the "tail type"
     /// when `rest` is called.
     fn get_type(&mut self, id: &Ident) -> UnifType {
-        match self {
-            Self::Rows {
-                known_types: h,
-                tail: _,
-            } => h
-                .remove(id)
-                .expect("Scopes of identifiers in destruct patterns should be checked already"),
-            Self::Dyn => mk_uniftype::dynamic(),
-        }
+        self.known_types
+            .remove(id)
+            .expect("Scopes of identifiers in destruct patterns should be checked already")
     }
 
     /// Returns the "tail type" of the record. I.e., the record's tail
     /// plus any "unused" matches from `known_types`.
     fn rest(self) -> UnifType {
-        match self {
-            Self::Rows { known_types, tail } => {
-                let rows = known_types.iter().map(|(id, ty)| RecordRowF {
-                    id: *id,
-                    types: Box::new(ty.clone()),
-                });
-                let rrows = rows.fold(tail, |tail, row| {
-                    UnifRecordRows::Concrete(RecordRowsF::Extend {
-                        row,
-                        tail: Box::new(tail),
-                    })
-                });
-                UnifType::Concrete(TypeF::Record(rrows))
-            }
-            Self::Dyn => mk_uniftype::dyn_record(mk_uniftype::dynamic()),
-        }
+        let Self { known_types, tail } = self;
+        let rows = known_types.iter().map(|(id, ty)| RecordRowF {
+            id: *id,
+            types: Box::new(ty.clone()),
+        });
+        let rrows = rows.fold(tail, |tail, row| {
+            UnifRecordRows::Concrete(RecordRowsF::Extend {
+                row,
+                tail: Box::new(tail),
+            })
+        });
+        UnifType::Concrete(TypeF::Record(rrows))
     }
 }
diff --git a/src/typecheck/eq.rs b/src/typecheck/eq.rs
index 5112e28a..bca53e2a 100644
--- a/src/typecheck/eq.rs
+++ b/src/typecheck/eq.rs
@@ -56,8 +56,8 @@ pub const MAX_GAS: u8 = 8;
 /// Abstract over the term environment, which is represented differently in the typechecker and
 /// during evaluation.
 ///
-/// The evaluation environment holds [crate::eval::lazy::Thunk]s, which are `Rc<RefCell<_>>`
-/// under the hood, while the term environment used during typechecking is just maps identifiers to
+/// The evaluation environment holds [crate::eval::cache::CacheIndex]es,
+/// while the term environment used during typechecking is just maps identifiers to
 /// a pair `(RichTerm, Environment)`. To have an interface that works with both,
 /// `TermEnvironment::get_then` has to take a closure representing the continuation of the task to
 /// do with the result instead of merely returning it.
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index 2b03beb8..9f644b5f 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -826,16 +826,17 @@ fn walk<L: Linearizer>(
                 })
         }
         Term::Fun(id, t) => {
-            // The parameter of an un-annotated function is assigned the type `Dyn`.
+            // The parameter of an unannotated function is always assigned type `Dyn`.
             ctxt.type_env.insert(*id, mk_uniftype::dynamic());
             walk(state, ctxt, lin, linearizer, t)
         }
         Term::FunPattern(id, pat, t) => {
             if let Some(id) = id {
-                ctxt.type_env.insert(*id, binding_type(state, t.as_ref(), &ctxt, false));
+                // The parameter of an unannotated function is always assigned type `Dyn`.
+                ctxt.type_env.insert(*id, mk_uniftype::dynamic());
             }
 
-            let pattern_ty = destructuring::build_pattern_type(state, pat);
+            let pattern_ty = destructuring::build_pattern_type_walk_mode(state, pat);
             destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, pattern_ty);
             walk(state, ctxt, lin, linearizer, t)
         }
@@ -878,7 +879,7 @@ fn walk<L: Linearizer>(
                 ctxt.type_env.insert(*x, ty_let);
             }
 
-            let pattern_ty = destructuring::build_pattern_type(state, pat);
+            let pattern_ty = destructuring::build_pattern_type_walk_mode(state, pat);
             destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, pattern_ty);
 
             walk(state, ctxt, lin, linearizer, rt)
@@ -1140,17 +1141,19 @@ fn type_check_<L: Linearizer>(
             type_check_(state, ctxt, lin, linearizer, t, trg)
         }
         Term::FunPattern(x, pat, t) => {
-            let src = destructuring::build_pattern_type(state, pat);
+            let src_rows_ty = destructuring::build_pattern_type_check_mode(state, pat);
+            let src = UnifType::Concrete(TypeF::Record(src_rows_ty.clone()));
+
             // TODO what to do here, this makes more sense to me, but it means let x = foo in bar
             // behaves quite different to (\x.bar) foo, worth considering if it's ok to type these two differently
             let trg = state.table.fresh_type_uvar();
             let arr = mk_uty_arrow!(src.clone(), trg.clone());
             if let Some(x) = x {
                 linearizer.retype_ident(lin, x, src.clone());
-                ctxt.type_env.insert(*x, src.clone());
+                ctxt.type_env.insert(*x, src);
             }
 
-            destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, src);
+            destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, src_rows_ty);
             unify(state, &ctxt, ty, arr).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
             type_check_(state, ctxt, lin, linearizer, t, trg)
         }
@@ -1208,7 +1211,8 @@ fn type_check_<L: Linearizer>(
         }
         Term::LetPattern(x, pat, re, rt) => {
             // The inferred type of the pattern w/ unification vars
-            let pattern_type = destructuring::build_pattern_type(state, pat);
+            let pattern_rows_type = destructuring::build_pattern_type_check_mode(state, pat);
+            let pattern_type = UnifType::Concrete(TypeF::Record(pattern_rows_type.clone()));
             // The inferred type of the expr being bound
             let ty_let = binding_type(state, re.as_ref(), &ctxt, true);
 
@@ -1226,10 +1230,15 @@ fn type_check_<L: Linearizer>(
 
             if let Some(x) = x {
                 linearizer.retype_ident(lin, x, ty_let.clone());
-                ctxt.type_env.insert(*x, ty_let.clone());
+                ctxt.type_env.insert(*x, ty_let);
             }
 
-            destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, ty_let);
+            destructuring::inject_pattern_variables(
+                state,
+                &mut ctxt.type_env,
+                pat,
+                pattern_rows_type,
+            );
 
             type_check_(state, ctxt, lin, linearizer, rt, ty)
         }
diff --git a/utilities/src/lib.rs b/utilities/src/lib.rs
index 85dfeb1a..2a6ffac6 100644
--- a/utilities/src/lib.rs
+++ b/utilities/src/lib.rs
@@ -5,7 +5,7 @@ use nickel_lang::{
     cache::{Cache, Envs, ErrorTolerance},
     error::{Error, ParseError},
     eval::{
-        cache::{CBNCache, Cache as EvalCache},
+        cache::{Cache as EvalCache, CacheImpl},
         VirtualMachine,
     },
     parser::{grammar, lexer},
@@ -16,12 +16,11 @@ use nickel_lang::{
 
 use std::{io::Cursor, path::PathBuf};
 
-pub type EC = CBNCache;
-pub type TestProgram = Program<EC>;
+pub type TestProgram = Program<CacheImpl>;
 
 /// Create a program from a Nickel expression provided as a string.
-pub fn program_from_expr(s: impl std::string::ToString) -> Program<EC> {
-    Program::<EC>::new_from_source(Cursor::new(s.to_string()), "test").unwrap()
+pub fn program_from_expr(s: impl std::string::ToString) -> Program<CacheImpl> {
+    Program::<CacheImpl>::new_from_source(Cursor::new(s.to_string()), "test").unwrap()
 }
 
 pub fn eval(s: impl std::string::ToString) -> Result<Term, Error> {
@@ -29,7 +28,7 @@ pub fn eval(s: impl std::string::ToString) -> Result<Term, Error> {
 }
 
 pub fn eval_file(f: &str) -> Result<Term, Error> {
-    let mut p: Program<EC> = program_from_test_fixture(f);
+    let mut p: Program<CacheImpl> = program_from_test_fixture(f);
     p.eval().map(Term::from)
 }
 
@@ -42,11 +41,11 @@ pub fn parse(s: &str) -> Result<RichTerm, ParseError> {
 }
 
 pub fn typecheck_fixture(f: &str) -> Result<(), Error> {
-    let mut p: Program<EC> = program_from_test_fixture(f);
+    let mut p: Program<CacheImpl> = program_from_test_fixture(f);
     p.typecheck()
 }
 
-fn program_from_test_fixture(f: &str) -> Program<EC> {
+fn program_from_test_fixture(f: &str) -> Program<CacheImpl> {
     let path = format!("{}/../tests/integration/{}", env!("CARGO_MANIFEST_DIR"), f);
     Program::new_from_file(&path)
         .unwrap_or_else(|e| panic!("Could not create program from `{}`\n {}", path, e))
@@ -137,7 +136,7 @@ impl<'b> Bench<'b> {
 
 pub fn bench_terms<'r>(rts: Vec<Bench<'r>>) -> Box<dyn Fn(&mut Criterion) + 'r> {
     let mut cache = Cache::new(ErrorTolerance::Strict);
-    let mut eval_cache = EC::new();
+    let mut eval_cache = CacheImpl::new();
     let Envs {
         eval_env,
         type_ctxt,
@@ -205,14 +204,14 @@ macro_rules! ncl_bench_group {
         pub fn $group_name() {
             use nickel_lang::{
                 cache::{Envs, Cache, ErrorTolerance, ImportResolver},
-                eval::{VirtualMachine, cache::Cache as EvalCache},
+                eval::{VirtualMachine, cache::{CacheImpl, Cache as EvalCache}},
                 transform::import_resolution::strict::resolve_imports,
             };
 
             let mut c: criterion::Criterion<_> = $config
                 .configure_from_args();
             let mut cache = Cache::new(ErrorTolerance::Strict);
-            let mut eval_cache = nickel_lang_utilities::EC::new();
+            let mut eval_cache = CacheImpl::new();
             let Envs {eval_env, type_ctxt} = cache.prepare_stdlib(&mut eval_cache).unwrap();
             $(
                 let bench = $crate::ncl_bench!$b;


Test patch:
diff --git a/src/eval/tests.rs b/src/eval/tests.rs
index 82e1ea36..0fe79a6e 100644
--- a/src/eval/tests.rs
+++ b/src/eval/tests.rs
@@ -1,4 +1,4 @@
-use super::cache::CBNCache;
+use super::cache::CacheImpl;
 use super::*;
 use crate::cache::resolvers::{DummyResolver, SimpleResolver};
 use crate::error::ImportError;
@@ -10,11 +10,9 @@ use crate::transform::import_resolution::strict::resolve_imports;
 use crate::{mk_app, mk_fun};
 use codespan::Files;
 
-type EC = CBNCache;
-
 /// Evaluate a term without import support.
 fn eval_no_import(t: RichTerm) -> Result<Term, EvalError> {
-    VirtualMachine::<_, EC>::new(DummyResolver {})
+    VirtualMachine::<_, CacheImpl>::new(DummyResolver {})
         .eval(t, &Environment::new())
         .map(Term::from)
 }
@@ -132,7 +130,7 @@ fn imports() {
         var: &str,
         import: &str,
         body: RichTerm,
-        vm: &mut VirtualMachine<R, EC>,
+        vm: &mut VirtualMachine<R, CacheImpl>,
     ) -> Result<RichTerm, ImportError>
     where
         R: ImportResolver,
@@ -245,7 +243,7 @@ fn interpolation_nested() {
 #[test]
 fn initial_env() {
     let mut initial_env = Environment::new();
-    let mut eval_cache = EC::new();
+    let mut eval_cache = CacheImpl::new();
     initial_env.insert(
         Ident::from("g"),
         eval_cache.add(
@@ -281,7 +279,7 @@ fn initial_env() {
     );
 }
 
-fn mk_env(bindings: Vec<(&str, RichTerm)>, eval_cache: &mut EC) -> Environment {
+fn mk_env(bindings: Vec<(&str, RichTerm)>, eval_cache: &mut CacheImpl) -> Environment {
     bindings
         .into_iter()
         .map(|(id, t)| {
@@ -299,7 +297,7 @@ fn mk_env(bindings: Vec<(&str, RichTerm)>, eval_cache: &mut EC) -> Environment {
 
 #[test]
 fn substitution() {
-    let mut eval_cache = EC::new();
+    let mut eval_cache = CacheImpl::new();
     let initial_env = mk_env(
         vec![
             ("glob1", Term::Num(1.0).into()),
diff --git a/tests/integration/pass/typechecking.ncl b/tests/integration/pass/typechecking.ncl
index 4fe5213c..0b8ab096 100644
--- a/tests/integration/pass/typechecking.ncl
+++ b/tests/integration/pass/typechecking.ncl
@@ -30,7 +30,7 @@ let typecheck = [
     ((if (f true 3) then (f 2 false) else 3) : Num),
 
   let f : forall a. (forall b. b -> b) -> a -> a = fun f x => f x in
-    f (fun z => z : forall y. y -> y),
+    f ((fun z => z) : forall y. y -> y),
 
   # forall nested
   let f : forall a. a -> a =