molikto’s weblog

Recursive definition and mutable records in dependent types

• Q: How to integrate dependent type with mutability?
  • motivation: I am amazed by how lean4 write it’s elaborator in Lean itself: the elaborator code uses monadic code all the time. So I wonder if one can create a dependent typed language with good old mutable states?
  • mutable reference is easy: link
  • mutable cells? It seems we can just create a new sort prop < set < mem
    • mutable state is done by having fields in a telescope mutable, def list(T: mem): men = record { mut head: T, tail: list(T) }
    • a records/enum with mutable state will not allow dependency on mut field
    • do we need sort polymorphic definitions, like def point(T: α): α = record { first: T, second: T}?
      • much like universe lifting, no actual variable is introduced, but we just duplicate the definition at all sorts, and type check all of them
      • does these non-first-class features enough? It reminds me of non first class blocks in Effekt language
    • another thing is: some record field can be used to save data inside the telescope, as cached values
• Q: Then how does other languages handle recursive functions in semantic domain?
  • in MiniTT this line is the key. The evaluation environment doesn’t contain semantical values of the recursive definition, but syntax of the recursive definition, with cycle broke by indirection.