Specialization for generics

[Xyncgas]

I propose we allow specialization on generics :

type origin<'a> = unit -> 'a
type asyncOrigin <'a> = unit -> Async<'a>
type construct<'generic> =
    | A of A : 'generic<construct>

type usage_ = construct<origin> //because construct's generic specialized, origin doesn't require generic definition (*e.g. origin<int>)
type asyncUsage_ = construct<asyncOrigin>

And for now the construct<'generic> (types using specialization for generic) is not directly usable (???usable???) and more like a template
Functions would either use usage_ or asyncUsage_

It helps by introducing possibility of template programming (meta programming) to reduce code usage (writing codes) in one scenario (as specialized generics are accepted on more places it helps more) :

type construct<'generic> =
    | A of A : 'generic<construct<'generic>> //or better yet, 'generic<construct> implies 'generic<construct<'generic>>
    | B of B : int
    static member op_Implicit (arg : origin<construct>) = B(0)
    static member op_Implicit (arg : asyncOrigin<construct>) = B(0)

type platform =
    struct
        val x : int
        new (arg : construct) = {x = 0}
    end

let killSwitch () =
    let c1 = platform(fun construct -> async {return ()})
    match c1 with
    | A asyncOp -> asyncOp |> Async.RunSynchronously
    | B integer   -> ()

    let c2 = platform(fun construct -> ())
    match c1 with
    | A Op -> ()
    | B integer   -> ()

For now one can just write this instead :

type construct =
    |Async_ of Async_ : unit -> Async<construct>
    |Sync_   of Sync_   : unit -> construct

This might be a way to overload functions with identical argument types but different return types
Now people can write that template and depending on return type expected select the function smartly
Specialization for generics would be the missing piece needed to start writing C++ style templates in F#

[Xyncgas]

As F# language evolves I would like to see it

[Tarmil]

This looks a lot like a well known concept in type theory called Generalized Algebraic Data Types (GADT). It is implemented in Haskell and OCaml, notably. It is more complex to implement than it may seem at first glance though. Notably because when you match on a value of type construct<'a>, the different branches have different specializations of 'a.

See this previous proposal, where the difficulties in implementing this are discussed.

[Xyncgas]

Thanks for introducing the 'Generalized Algebraic Data Types (GADT)' concept to me as I didn't know about what it's called and I'm happy I can talk to people about it.

I thought bit further to provide the actual way it would be used after implemented :

type origin<'a> = unit -> 'a
type asyncOrigin <'a> = unit -> Async<'a>

type construct<'generic> =
    | A of A : 'generic<construct<'generic>>
    | B of B : int
    | C of C : construct<'generic> //not allowed in F# union, since 'generic is expected to be a generic itself, it can not too have expectation that it's not or we do not get strong typing on union case matches
    static member op_Implicit (arg : origin<construct<'generic>>)      = A(arg)
    static member op_Implicit (arg : asyncOrigin<construct<'generic>>) = A(arg)
    static member op_Implicit (arg : int)                              = B(arg)

type platform<'origin> =
    struct
        val x : int
        new (arg : construct<'origin>) = {x = 0}
    end

let killSwitch () =
    let c1 = platform(fun construct -> async {return 0})
    //typeof<c1> = platform<(asyncOrigin<construct<:>>)>, ':' meaning it's recursive. 0 would be implicitly casted to (construct<asyncOrigin<:>>) like usual.
    match c1 with
    | A asyncOp -> asyncOp |> Async.RunSynchronously
    | B integer   -> ()

    let c2 = platform(fun construct -> 0)
    //typeof<c2> = platform<(origin<construct<:>>)>,      ':' meaning it's recursive. 0 would be implicitly casted to (construct<asyncOrigin<:>>) like usual.
    match c2 with
    | A Op -> ()
    | B integer   -> ()

Specialization for generic was allowing me to write a construct that's async and not async without me actually having two types or two cases like I would today. Generics are basically still generics and 'generic could've been an int or a float like you usually would have if weren't for the way the generic was used (it has specialization) that basically was giving it a constrain that say ('generic where 'generic : 'generic<a>) but let's not make people write that constrain so the language looks smarter. It's specialization on generic that which basically is saying "ok what's generic about this construct is not either it's related to integer or string but it is maybe sync maybe async" and the specialization was defining what it's Async or not Async about (in example it was about itself)

Meanwhile how it would be implemented is exactly having multiple types (likely) or multiple cases of construct for as many specialization as needed, after detecting generic specialization usages. outer<inner_<:>> would be introduced specifically for specialization for generics has been allowed as simply a tooltip / documentation / string for describing these specialized types (construct<'generic> still is construct<'generic> but c1 was platform<(asyncOrigin<construct<:>>)>)

For example, platform<(origin<construct<:>>)> looks like construct_Sync, and platform<(asyncOrigin<construct<:>>)> looks like construct_Async :

type construct_Sync =
    | A of A : unit -> construct_sync
    | B of B : int

type construct_Async =
    | A of A : unit -> Async<construct_Async>
    | B of B : int

So far I've not seen a problem of the type recursion in my example, since it's not immediate recursion, so the construct can be a struct and recursion is allowed like it's allowed today when A of A : unit -> <construct<'generic>> because I can see I might be right that there is no way for you to write a construct<'generic> union as is in the example that's immediately recursive before & after specialization for generics is allowed

For people who are really curious about benefits, I can say specialization on generics can for example, be easier for library authors to write both sync and async version of their infrastructures without adding new types and just let codes written without async in design to adopt the new features like async programming that's available in moving forward

I haven't studied #179 yet and I am going to now