Currently, we can use universal quantifier for lifetime, for example:
struct Foobar {
val: i32
}
fn foobar<'a>(get_val: &for<'b> fn(&'b Foobar) -> &'b i32, x: &'a Foobar) -> &'a i32 {
get_val(x)
}
And it's impossible for now if we want to write this code, because here it need universal quantifier for types in a dyn context.
fn foobar<'a, T>(id: &for<'b, U> fn(&'b U) -> &'b U, x: &'a T) -> &'a T {
id(x)
}
Currently we can only use universal quantifier in compile time scope.
#![feature(non_lifetime_binders)]
trait HKT {
type Item<T>;
fn get<T>(self) -> Self::Item<T>;
}
fn foobar<H, T>(x: H, vec: &Vec<T>) -> usize
where
H: HKT,
for<A> <H as HKT>::Item<A>: Fn(&Vec<A>) -> usize
{
let f = x.get::<T>();
f(vec)
}
In other language which supports universal quantifier for types, they perform type erasure, so values can still be parameterized because there will only be one implementation of the callee interface, no need to generate different codes for different types.
We can add a dyn modifier over type parameters to tell compiler that, this parameter doesn't decide how the type/function should be compiled.
For example we can create a container for different types, but the runtime implementation stays the same for all types.
#[repr(C)]
struct Box<dyn T> {
val: *mut (),
layout: std::mem::Layout
}
its memory representation should all be [usize, Layout]. We don't need additional PhantomMarker for such type constructor.
If we write a function to compute length for different Vec<Box>
fn len<dyn T>(vec: &Vec<Box<T>>) -> usize {
vec.len()
}
then we only need a single compiled function for every different type
fn len(vec: &Vec<struct{*mut (), std::mem::Layout}>) -> usize {
vec.len()
}
so it will enables us to write such code
fn foobar<'a, dyn T>(f: &for<'s, dyn U> dyn fn(&'s Vec<Box<U>>) -> usize, vec: &'a Vec<Box<T>>) -> usize {
f(vec)
}
as the f should only have a single runtime interface:
fn (vec: *const Vec<Box>) -> usize
I think it will be useful if someone really need parametric polymorphism.
And of course, to make it more useful we might need bounded qualification. It's not a easy problem to solve.