What type functions mean on a language level

[Stefan Koch]

On Wednesday, 13 January 2021 at 20:41:38 UTC, Max Haughton wrote:
> On Wednesday, 13 January 2021 at 17:09:59 UTC, Stefan Koch 
> wrote:
>> On Tuesday, 12 January 2021 at 20:41:02 UTC, Q. Schroll wrote:
>>> On Wednesday, 6 January 2021 at 13:52:39 UTC, sighoya wrote:
>>>> If we allow a __type__ in type position, indirectly or 
>>>> directly, we're able to implement generics known from other 
>>>> languages, e.g.:
>>>>
>>>> ```
>>>> method(__type__ type)(type value){...}
>>>> ```
>>>> vs
>>>>
>>>> ```
>>>> method(T)(T value){...}
>>>> ```
>>>
>>> Is this a suggestion or what you think the semantics' 
>>> consequences are? Because I fail to see how the first one is 
>>> any different from a template. If I replace `__type__ type` 
>>> by `int i`, it is still a compile-time argument. In one 
>>> instance, the value argument is (or represents) a type. That 
>>> doesn't change the semantics, or does it?
>>
>> A value type can only be used as type if it a statically known 
>> value,
>> which in the above example is the case.
>> But I doubt it will work with the ITFI functionality as it is 
>> currently implemented.
>>
>> I have never intended this usecase, I think that we should be 
>> able to get it to work,
>> but I am not sure if that's the most productive thing to do.
>
> I think the usefulness of typefunctions will derive from 
> treating them as an instance of some type like any other. 
> __type__ is conceptually equivalent to having some string mixin 
> of the type it represents. Maybe you shouldn't do so, but a 
> __type__ in a template is just any other template argument - it 
> shouldn't be rewritten to anything else.
>
> Stefan, I'm thinking of writing a short document (DIP-lite) to 
> document where I think typefunctions should be specified and 
> used, maybe you could look over it?

Sure I am happy to have a look at your document.

One of the reasons that __type__ is not actually a real type.
But a type value is because I want typefunctions to be well 
functions.
They should be mono-morphic (Only have one shape). Such that you 
do not need to generate new function bodies on every call with a 
different type argument.
In order for that to be the case, type arguments must not be able 
to change the shape of the body.
Because if they did, you would be equivalent to templates. (I.E. 
you cannot proof that the shape does not change from one set of 
template arguments to the other)
Since generation of the multiple shapes + symbols that templates 
produce such a big strain on the compiler, and compile time;
Typefunctions disallow that statically.
It also makes it easier to reason about as multiple shapes are 
hard to keep in ones head.