data_dynamic_michelson_prototype.md

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:

• 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 so Sing :: T -> *.

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 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 }

I don't see how this Dyn type would behave differently from bytes with TO_DYN being PACK and FROM_DYN being UNPACK. Can you show us a use-case?

@rafoo, bytes have many error values (that can't be parsed into any valid Michelson value), but otherwise it behaves exactly like PACK/UNPACK with much better performance.

One 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.