Comment by anon291

Functions that return types are indeed at a higher level than those that don't.

Values can be seen as Singleton types. The key difference is the universe they live in. In the universe of types, the level one level below is perceived as a value. Similarly, in the universe of kinds, types appear to be values.

> Basically, 'value' would be a special constraint on a type parameter in normal parametric polymorphism implementations

Yes this is a level constraint.

> But I guess, the same issue of "which refinement types can be defined, while keeping everything decidable" remains as an issue.

If you're dealing with fully computable types. Nothing is decidable.

> Also how to handle runtime values? That will require type assertions, just like union types? Or is it only a compile time concept and there is no runtime instantiations. Only some kind of const generics?

A compiler with dependent types is essentially producing programs that are itself embedded with its input. There cannot be a distinction between runtime and compel time. Because in general type checking requires you to be able to run a program. The compilation essentially becomes deciding which parts you want to evaluate and which parts you want to defer until later.

> A typeof function could be an example of dependent type though? Even at runtime?

Typeof is just const.

Typeof: (T : type) -> (x:T) -> Type

Final note: I've written some compilers for toy dependently typed languages. By far dependent typing makes both the language and the compiler easier not harder. This is because Haskell and c++ and other languages with type systems and metaprogramming or generics actually have several languages: the value language that we are familiar with, but also the type language.

In Haskell, this is the class/instance language which is another logic programming language atop the lambda calculus language. This means to write a Haskell compiler you have to write a compiler for Haskell and the logic programming language (which is turing complete btw) that is the type language

Similarly in c++, you have to implement c++ AND the template system which is a functional programming language with incredibly confusing semantics.

On the other hand for a dependently typed language, you just write one language... The types are talked about in the same way as values. The only difficulty is type inference. However, an explicit dependently typed language is actually the easiest typed compiler to write because it's literally just checking for term equality which is very easy! On the other hand with a dependent language, type inference is never going to be perfect so you're a lot freer to make your own heuristic decisions and forego HM-like perfection.