Are dependent types necessary for the translation?

[hirrolot]

In the "Notes on Polymorphic Functions" section of README.md, you are claiming that dependent types are essential for the translation of polymorphic functions, inasmuch as types are passed as ordinary arguments and so their copying/discarding functions can be determined. However, I don't fully understand what dependent types have to do with the behaviour you are mentioning.

In System F (polymorphic lambda calculus), we can also pass types as ordinary arguments, and therefore we should be able to access their copying/discarding functions in the same way. Dependent types come into play when you have a function that accepts a value, such as 123, and returns a type, which is different from ordinary polymorphic functions as in System F. To me, it seems that nothing prevents us from doing the same translation in a less expressive calculus than CoC, or I miss something important.

[vekatze]

Hi.

it seems that nothing prevents us from doing the same translation in a less expressive calculus than CoC

You are correct. As long as the calculus has first-class types, I also believe we can do the same translation here.

After receiving your comment, I re-read the section of the readme and realized that the following sentence was very misleading:

That is again a valid question, and here comes dependent-type.

As you pointed out, this gives readers (including me) the impression that dependent type is a necessary condition, even though it was actually only a sufficient condition. This is my mistake.

I'll reflect your feedback to the currently unreleased website that I've been working on recently to replace the readme.

(The website is at the very early stage, so pasting the link here is a bit embarrassing, but anyway)

[hirrolot]

Thanks for your reply!

As long as the calculus has first-class types, I also believe we can do the same translation here.

Do we need first-class types for this translation though? System F has no first-class types as far as I remember; you just need to pass types and ordinary values using different syntax, e.g., f[A] for type A and f x for some value x. But the compiler would anyway be able to retrieve type information, such as copying/discarding functions for types passed as arguments. If this is the case, the approach of Neut would be even more promising, since it would mean that the translation works for less expressive type systems and not only for those with first-class types such as CoC.

I'll reflect your feedback to the currently unreleased website that I've been working on recently to replace the readme.

Thanks for working on this website by the way. I've read half of it and it's already pretty good for Neut beginners like me (more content would be apt though).

[vekatze]

Maybe I was half asleep? You're correct once again. What I tried to say was that we need runtime representations for types (I think I was thinking about "first-class types at the runtime" in my confused mind).

Let me retry: As long as we can translate the calculus into the CoC, we can do the same translation. Since System F (or STLC or whatever) can be trivially embedded into the CoC, we should be able to do the same translation. In this sense, the source calculus doesn't need dependent types. I believe I'm not half asleep now.

Thanks for working on this website by the way. I've read half of it and it's already pretty good for Neut beginners like me (more content would be apt though).

Thanks! I'll make it better and better.

[hirrolot]

Thanks, now it makes sense to me. All the best, keep up the good work!