Add `some` type with existential quantification
In some cases, we need a type that would hide any other type inside of it.
Let's further call it some
; this name is subject to change.
Use cases: storage and parameter of in-place-upgradeable contract. In both of these cases we can't know types of entries in advance, so we have to circumvent type system and assume that we store/accept some unknown type.
Currently, we work around this via using bytes and applying PACK
/UNPACK
for hiding type of entry. But this is very costly in terms of gas.
Another use case - loading large pieces of code lazily, currently the only way to do this is putting a lambda in BigMap
.
Objects of some
type should keep an already typechecked value and its type, and on an attempt to extract it, the engine should compare this stored type with the one user expects, and return a typed value if they match. Operations involving some
type are expected to take O(1)
gas (in the worst case - O(|type|)
).
We need to propose a standard which would describe this type, instructions to work with it, its motivation in detail, and then we should ask Tezos developers what do they think about adding support for this thing.
However, this issue is minor as chances for this type being added to Michelson at this stage seems to be small. As we know, currently contract code and storage are stored in some raw representation, so contract execution first requires decoding and typechecking of those; and code typechecking usually takes most of the gas. Implementing some
type can probably occur not earlier than this paradigma changes.