proof techniques – How to specify mutated types mathematically?

Say I have an object which I pass to a method, and the method returns that same object, just mutated.

So it goes like this:

doSomething({ a: 1 })
// { b: '1' }

function doSomething(input) {
  input.b = String(input.a)
  delete input.a
  return input
}

How do you specify a type for this object and type for the action properly in detail? Not necessarily using any particular language or framework or tool, but generically, mathematically? What should happen here? I understand this is why you introduce immutability and pure functions. That would make it easier, so you start with one thing, leave it unchanged, and then receive a completely new object, which starts as output in an “unchanged” state sort of.

But without resorting to this immutability and pure-function state, how would you mathematically specify the types and the “transformation” (function) in this case?

type DoSomethingInput {
  a: Int
}

type DoSomethingOutput {
  b: String
}

This is partially true. However, it doesn’t take into account the fact that the DoSomethingInput object is no longer of that type! It got mutated in the process. So part of me just wants to do this:

type DoSomethingObject {
  a?: Int
  b?: String
}

Then at the start, the optional a is present but b is absent, and at the end a is absent and b is present.

But imagine we had a way more complex deeply nested object structure to start with, and then we mutate that object in extremely complicated ways. Too much to try to write an example of this, so just imagine that. Then we would probably have a type DoSomethingObject with almost every of 100 deeply nested properties all optional, which would start to not make sense. Perhaps there are 5 or 10 intermediate “clearly distinguishable” substates of this object while it’s being transformed. Then it would make more sense to organize the type differently. But in the end, still, it is being mutated in crazy ways… So how do you say “this type starts as x and ends as y”?

That is, to put it in a different way, we start with DoSomethingInput, and that is replaced physically by DoSomethingOutput I guess. After the action/function/transformation, there no longer exists an object of type DoSomethingInput, that object is now of type DoSomethingOutput. It’s as if like this:

globalWorldState = ( { a: 1 } )
actionApplied(globalWorldState) // doSomething
globalWorldState = ( { b: '1' } )
where globalWorldState(0) = globalWorldState(0)'

But even something like that doesn’t make sense, it doesn’t capture it. You would have to say more like:

where globalWorldState(0) = globalWorldState(0)'
  yet added b: String(a)
  and then removed a

Basically I’m wondering how to do I conceptualize this and capture it in type definitions, in a mathematically general way? I would like to say that some input object to an action becomes the output after being mutated, and so the original typed input is gone and it’s now of a new type. How could that be stated mathematically?