Nomenclature: "application", "specialization", "instantiation", "type synonyms"

Chatroom Cross-posts
#1

paluh
I’m not familiar with compilers nomenclature so please excuse this lame question :wink:
Let’s say that I have: type T a b c = .... (or data T a b c or newtype T a b c) and now I create something like type C = T Int String String where I specify some set of specific types which I want to use in this case. How would you call this step where from a polymorphic (I should say probably “parametric” here?) type I’m constructing some monomorphic one?

natefaubion
At the type-level, there’s nothing really polymorphic about this, in the same sense that a function argument at runtime is not indicative of polymorphism. The language of types in PS is symbolic (just data), so it’s not exactly a function, but you can think of it like a data constructor that takes an Int and putting any number you want in it. That is, this is analogous to normal argument application in the language of types.

paluh
Thanks! So can I call this “application”?

natefaubion
Yep

natefaubion
To be clear, I would not call it “type application” even though it is in the language of types.
It’s just regular “application”

paluh
But “application” seems a bit more general - I mean it doesn’t indicate that I’m not doing something like: type C a = T a Int String. Am I right?

natefaubion
I don’t quite follow. Can you elaborate?

paluh
When I say “application” does this mean that I apply all the arguments and get non parametric type as a result?

natefaubion
No, the type language is curried just like the term language.
So the semantics are the same as term-level application.
That is, type constructors always take a single argument and yield a type, which may itself be another type constructor.

Type synonyms are semantically wishy-washy IMO. They are kind of like functions, but not really since they are reduced as a separate meta-level, making them more like syntactic macros for the type language.
And their kinds do not reflect this. Their kinds pretend they are normal type constructors, but it’s not really true.

monoidmusician
More abstractly, you could also call it specialization, because you are choose values for those parameters.
But specialization still does not necessarily mean you have chosen values for all parameters.

paluh
Are “instatiation” or “monomorphization” inaccurate in this case?

natefaubion
I would consider it inaccurate, because instantiation of types is something that happens at the term-level, not type-level.

That is, instantiation is picking something for some type/meta-level (types for terms, kinds for types) abstraction

So instantiation happens on terms, picking some type. It can happen at types, picking some kind.
Which is what “type application” really is, type application being a way to syntactically specify how to instantiate something in the term language.

It can get confusing because there is a term language, where everything has a type, but in PS types are their own term language, where everything also has a type. With PolyKinds, the type language of types is also types. In dependently-typed languages, the type language and the term languages are unified (the same). (edited)

paluh
Thanks a lot!

3 Likes