Thoughts about "Compile-time types" talk

[Timon Gehr]

On 14.05.19 19:58, H. S. Teoh wrote:
> The underlying idea behind my proposal is to remove artificial
> distinctions and unify CT and RT so that, as far as is practical, they
> are symmetric to each other.

As long as templates are not statically type checked, this does not seem 
particularly appealing. The main argument Andrei uses against typed 
templates is precisely that it is not necessary because they are 
expanded at compile time.

The vision itself makes sense of course, it's basically system λ* [1].

[1] 
https://en.wikiversity.org/wiki/Foundations_of_Functional_Programming/Pure_type_systems#%CE%BB*_(na%C3%AFve_type_theory)