Add Dynamic Type to Michelson
Motivation
A primary use case, which currently uses bytes
in production, allows extending a contract with entrypoints of "arbitrary types" by storing big_map string (lambda dyn fixed_input_type)
and exposing an entrypoint: (string, dyn)
that finds the appropriate lambda
and passes the fixed_input_type
to the rest of the contract.
Why not just use bytes
?
-
PACK
/UNPACK
use a lot of gas - A particular
bytes
value may not encode any Michelson value - A dynamic literal can be encoded in a human-readable way, e.g.
Dyn string "ok" : dyn
Data.Dynamic in Haskell
Haskell has Data.Dynamic
:
a method of hiding types in such a way that they may be conditionally resolved at run-time in a type-safe manner.
Here's the implementation in Haskell:
data Dynamic where
Dynamic :: forall a. TypeRep a -> a -> Dynamic
dyn type for Michelson in morley in Haskell:
Since I'm not familiar with the Tezos core, here's what an implementation
might look like using morley
:
-
morley
embedding of Michelson types:data T :: *
-
morley
embedding of Michelson values:data Value (t :: T) :: *
- Haskell singleton embedding of types in values:
Sing :: k -> *
- For our purposes,
k ~ T
here soSing :: T -> *
.
- For our purposes,
data Dyn where
ToDyn :: forall (t :: T). Sing t -> Value t -> Dyn
toDyn :: Sing t -> Value t -> Dyn
toDyn = ToDyn
-- | equality on T, given `Sing`leton representations
eqT :: forall (t1 :: T) (t2 :: T). Sing t1 -> Sing t2 -> Either (t1 :~: t2 -> Void) (t1 :~: t2)
eqT = ..
fromDyn :: Sing t -> Dyn -> Maybe (Value t)
fromDyn st1 (ToDyn st2 xs) =
case eqT st1 st2 of
Left _ -> Nothing
Right Refl -> Just xs
dyn type in (pseudo) Michelson:
The original idea was to implement this similarly-to a macro,
but after discussion with @rafoo_
it may be simpler to implement dyn
, FROM_DYN
, TO_DYN
directly:
Sing t := bytes(t) -- the binary encoding of (t)
eqT := equality on bytes + type rule for dyn
dyn := pair bytes a -- (implementation detail)
:: a' : S => dyn : S
> TO_DYN / x : S => Pair (bytes(a')) x : S
:: dyn : S => option a' : S
> FROM_DYN a' / Pair (bytes(b')) x : S => Some x : S
where a' == b'
> FROM_DYN a' / Pair (bytes(b')) x : S => None : S
where a' /= b'
Possible implementation as macro:
TO_DYN 'a =
PUSH bytes (bytes_of_type 'a);
PAIR
FROM_DYN 'a =
DUP;
CAR;
PUSH bytes (bytes_of_type 'a);
IFCMPEQ
{ CDR; SOME }
{ DROP; NONE }