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
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
The idea is to hide the internal representation from the user and implement it similarly to a macro with additional type rules.
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 }
@rafoo,
bytes
have many error values (that can't be parsed into any valid Michelson value), but otherwise it behaves exactly likePACK
/UNPACK
with much better performance.One use case, which currently uses
bytes
in production, allows extending a contract with entrypoints of "arbitrary types" by storingbig_map string (lambda dyn fixed_input_type)
and exposing an entrypoint:
(string, dyn)
that finds the appropriatelambda
and passes thefixed_input_type
to the rest of the contract.