I’m not familiar with compilers nomenclature so please excuse this lame question
Let’s say that I have:
type T a b c = ....(or
data T a b cor
newtype T a b c) and now I create something like
type C = T Int String Stringwhere 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?
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.
Thanks! So can I call this “application”?
To be clear, I would not call it “type application” even though it is in the language of types.
It’s just regular “application”
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?
I don’t quite follow. Can you elaborate?
When I say “application” does this mean that I apply all the arguments and get non parametric type as a result?
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.
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.
Are “instatiation” or “monomorphization” inaccurate in this case?
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)
Thanks a lot!