(really) abstract variables

[zenna]

I recently engaged in an exercise in translating a formalism I've been working on (causal abstraction, if it maters) into Omega. In doing so, I found there were several instances where Omega and Julia were forcing me to be more concrete earlier than I wanted.

Omega allows us to be pretty abstract -- free and random variables allow us to specify unknown values. Even so, it's not quite abstract enough. We sill need to specify the type of variables before we use them. It seems like we want a kind of type polymorphism for values, akin to the way we have We want a kind of type polymorphism that we have with functions but for random/free variables.

An example

Let. $$S$$ be a state space, $$A$$ an action space, and $$\pi(a | s)$$ be a policy, define a distribution over actions $$a$$ conditional on a current state $$s$$. We want to find some optimal policy $$\pi^* = argmin f(\pi, ...)$$.

We haven't given the exact nature of $$S$$ or $$A$$ or much at all.

One way to think about this is that this whole model is really a function of some type variables. We could explicitly do this in Julia, creating a function which takes as input some types and outputs a concrete model. Something like

function modelgen(::Type{S}, ::Type{A}, ::Type{\Pi}) where {S, A, \PI}
  \pi(s::S).= \omega -> .... what do put here?
  \ell = f.(\pi)
  \pi* = argmin(\pi, \wll)
end

One interesting thing is that \pi is both abstract but it's also not anything. It is a function from $$S$$ to a random variable over $$A$$, but even within that there are many forms that the function could take.

How about something like:

struct TypeVariable{T} end
α = TypeVariable
β = TypeVariable
v. = FreeVariable.(α)
u = FreeVariable.(β)
a = v .+ u
argmin((v, u), a, (α => Int, β => Int))

v then is something like
v(\omega) = FreeVariable(Int)(\omega)

....Somethign like this? Can we do this and remain type safe. Also, it would be kinda annoying if we had to augment every function like argmin where we want to instantiate the types. Is there a way to do that.

Maybe there could be something like instantiate((v, u), (α => Int, β => Int)))

Need to prototype this.