CategoricalData
Rewrite inline let terms and case statements for targets like Python
The Hydra kernel previously had quite a few definitions which could not be directly translated into Python. For example, case statements within lambdas could not be translated unless the lambda could be turned into a def, as Python's match statements are statements, not expressions (i.e. they can only appear at the top level of a definition). While other problems were solved through rewriting, inline let and cases were solved by simply editing the Hydra sources -- it is usually easy to avoid these constructions by creating more let bindings.
However, that is not a good long-term solution. Users should be able to write any valid Hydra programs, and expect that they will map without failure into each target language, including Python. All of the previously unsupported definitions have been rewritten for Python compatibility; we just need to find a way to automate this rewriting.
Another reason we sometimes need to propagate lambdas up into let bindings is for type annotations. Inline definitions (using the walrus operator := do not support type annotations, but we often need to introduce type variables in annotations so that we don't have dangling variable references in cast expressions. E.g. the following Hydra definition:
mutateTraceDef :: TBinding ((Trace -> Hydra.Mantle.Either String Trace) -> (Trace -> Trace -> Trace) -> Flow s a -> Flow s a)
mutateTraceDef = define "mutateTrace" $
"mutate" ~> "restore" ~> "f" ~>
"choose" <~ ("forLeft" ~> "forRight" ~> "e" ~> cases _Either (var "e") Nothing [
_Either_left>>: "e" ~> var "forLeft" @@ var "e",
_Either_right>>: "e" ~> var "forRight" @@ var "e"]) $
Compute.flow (
"s0" ~> "t0" ~>
"forLeft" <~ ("msg" ~>
Compute.flowState nothing (var "s0") (ref pushErrorDef @@ var "msg" @@ var "t0")) $
"forRight" <~ ("t1" ~>
"f2" <~ Compute.unFlow (var "f") (var "s0") (var "t1") $
Compute.flowState
(Compute.flowStateValue (var "f2"))
(Compute.flowStateState (var "f2"))
(var "restore" @@ var "t0" @@ (Compute.flowStateTrace (var "f2")))) $
var "choose" @@ var "forLeft" @@ var "forRight" @@ (var "mutate" @@ var "t0"))
Leads to invalid type expressions in the generated Python:
def mutate_trace[T0, T1](mutate: Callable[[hydra.compute.Trace], hydra.mantle.Either[str, hydra.compute.Trace]], restore: Callable[[hydra.compute.Trace, hydra.compute.Trace], hydra.compute.Trace], f: hydra.compute.Flow[T0, T1]) -> hydra.compute.Flow[T0, T1]:
def choose[T2, T3, T4](for_left: Callable[[T2], T3], for_right: Callable[[T4], T3], e: hydra.mantle.Either[T2, T4]) -> T3:
match e:
case hydra.mantle.EitherLeft(value=e2):
return for_left(e2)
case hydra.mantle.EitherRight(value=e22):
return for_right(e22)
return cast(hydra.compute.Flow[T0, T1], hydra.compute.Flow((lambda s0, t0: (
for_left := (lambda msg: cast(hydra.compute.FlowState[T0, T2], hydra.compute.FlowState(cast(Maybe[T2], Nothing()), s0, push_error(msg, t0)))),
for_right := (lambda t1: (f2 := f.value(s0, t1), cast(hydra.compute.FlowState[T0, T1], hydra.compute.FlowState(f2.value, f2.state, restore(t0, f2.trace))))[1]), choose(cast(Callable[[str], hydra.compute.FlowState[T0, T1]], for_left), for_right, mutate(t0)))[2])))
Rewriting the original definition to:
mutateTraceDef :: TBinding ((Trace -> Hydra.Mantle.Either String Trace) -> (Trace -> Trace -> Trace) -> Flow s a -> Flow s a)
mutateTraceDef = define "mutateTrace" $
"mutate" ~> "restore" ~> "f" ~>
"choose" <~ ("forLeft" ~> "forRight" ~> "e" ~> cases _Either (var "e") Nothing [
_Either_left>>: "e" ~> var "forLeft" @@ var "e",
_Either_right>>: "e" ~> var "forRight" @@ var "e"]) $
"flowFun" <~ ("s0" ~> "t0" ~>
"forLeft" <~ ("msg" ~>
Compute.flowState nothing (var "s0") (ref pushErrorDef @@ var "msg" @@ var "t0")) $
"forRight" <~ ("t1" ~>
"f2" <~ Compute.unFlow (var "f") (var "s0") (var "t1") $
Compute.flowState
(Compute.flowStateValue (var "f2"))
(Compute.flowStateState (var "f2"))
(var "restore" @@ var "t0" @@ (Compute.flowStateTrace (var "f2")))) $
var "choose" @@ var "forLeft" @@ var "forRight" @@ (var "mutate" @@ var "t0")) $
Compute.flow $ var "flowFun"
...gives us a valid definition:
def mutate_trace[T0, T1](mutate: Callable[[hydra.compute.Trace], hydra.mantle.Either[str, hydra.compute.Trace]], restore: Callable[[hydra.compute.Trace, hydra.compute.Trace], hydra.compute.Trace], f: hydra.compute.Flow[T0, T1]) -> hydra.compute.Flow[T0, T1]:
def choose[T2, T3, T4](for_left: Callable[[T2], T3], for_right: Callable[[T4], T3], e: hydra.mantle.Either[T2, T4]) -> T3:
match e:
case hydra.mantle.EitherLeft(value=e2):
return for_left(e2)
case hydra.mantle.EitherRight(value=e22):
return for_right(e22)
def flow_fun(s0: T0, t0: hydra.compute.Trace) -> hydra.compute.FlowState[T0, T1]:
def for_left[T2](msg: str) -> hydra.compute.FlowState[T0, T2]:
return cast(hydra.compute.FlowState[T0, T2], hydra.compute.FlowState(cast(Maybe[T2], Nothing()), s0, push_error(msg, t0)))
def for_right(t1: hydra.compute.Trace) -> hydra.compute.FlowState[T0, T1]:
f2 = f.value(s0, t1)
return cast(hydra.compute.FlowState[T0, T1], hydra.compute.FlowState(f2.value, f2.state, restore(t0, f2.trace)))
return choose(cast(Callable[[str], hydra.compute.FlowState[T0, T1]], for_left), for_right, mutate(t0))
return cast(hydra.compute.Flow[T0, T1], hydra.compute.Flow(flow_fun))
this reminds me, not all languages support 'scoped type variables' (even haskell 98), if you're allowing annotations to use type variables: https://stackoverflow.com/questions/15800878/scoped-type-variables-require-explicit-foralls-why
Yep. Haskell's convenient syntax can be a little confusing. Personally, I would have just made forall explicit in all type signatures, which Hydra does. At least in Haskell, though, you can annotate any let binding with a forall type. When you get into unrelated languages like Python, there are idiosyncratic constraints around type annotations which we just need to work around. So far, I can report that there have been no actual blockers in Python. All of the important polymorphic functions have been mapped into the language and are being accepted by pyright. However, this required some "cheating" as noted above.