Allow for Structural Checking of Generic Parameters within Type Constraints

[robkuz]

Allow expressions within type constraints to check for generic paramters within a generic parameter

    let inline inj<'A, 'T when 'T : HasGenericParamsOf<'A>> (value: 'T) : Brand<FinishedTag, 'A> = new Brand<_,_>(value)

    type FinishedTag = FinishedTag
    type FinishedKind<'A> = FinishedKind of 'A
    type Brand<'A, 'B> = {a: 'A, b : 'B}

    let x = inj (FinishedKind 1)
    //val x: Brand<FinishedTag, int>

whereas this wouldn't work

    type FinishedKind2<'A, 'B> = FinishedKind2 of 'A * 'B

    let x = inj (FinishedKind2 "Foo" true)
    //Error as FinishedKind2 has 2 generic params 

Also when doing this we should allow for

    let inline inj<'A, 'T when 'T : HasGenericParamsOf<_,_>> (x: 'T) ...
    //Has 2 generic params. Important: No defaulting to Object
    let inline inj<'A, 'T when 'T : HasGenericParamsOf<_,'A>> (x: 'T) ...
    //Only check that 2nd param is of type 'A

Why? Because we could then express methods like this (FSharpPlus) that are using namemangling at the moment (to at least express the intent)

 static member inline Invoke (mapping :'T->'U) (source : '``Functor<'T>``) : '``Functor<'U>`` = 
 static member inline Invoke (f : 'T->'U) (source : '``Bifunctor<'T,'V>``) : '``Bifunctor<'U,'V>`` =

and express it like this

 static member inline Invoke<'A, 'B, 'S, 'T 
                                   when 'S :  HasGenericParamsOf<'A> 
                                   and 'T : HasGenericParamsOf<'B>> 
                                   (mapping :'A -> 'B) (source : 'S) : 'T = 

There is no way to do that at the moment in F#. The only thing is to express intent via F#'s rather lax naming rules for identifiers

Pros and Cons

The advantages of making this adjustment to F# are

• much stronger assurance on the contracts of a function.
• It is a good step into the direction of having higher kinded types yet shying away to implement HKTs as a full feature (CLR, C# interop etc.).
• This could probably be implemented as an erasing feature

The disadvantages of making this adjustment to F# are:

• It needs to be implemented of course
• It makes the learning of type constraints slightly more complicated. But as this is complex already it doesn't seem so much of an issue.
• F# beginners might be having a hard time to understand this. However as mastering type constraints is hard anyways and beginners usually aren't going to learn them I don't see that as a real issue

Extra informtion

Estimated cost (XS, S, M, L, XL, XXL): Sorry! I can't answer this

Related suggestions: (put links to reated suggestions here)

Affadavit (must be submitted)

Please tick this by placing a cross in the box:

• [x] This is not a question (e.g. like one you might ask on stackoverflow) and I have searched stackoverflow for discussions of this issue
• [x] I have searched both open and closed suggestions on this site and believe this is not a duplicate
• [x] This is not something which has obviously "already been decided" in previous versions of F#. If you're questioning a fundamental design decision that has obviously already been taken (e.g. "Make F# untyped") then please don't submit it.

Please tick all that apply:

• [x] This is not a breaking change to the F# language design
• [ ] I would be willing to help implement and/or test this
• [x] I or my company would be willing to help crowdfund F# Software Foundation members to work on this

[Rickasaurus]

This seems like not a bad compromise. No idea how much work something like this would be to add to SRTPs though.

[gusty]

The question is how much less effort is, compared to full HKT. I think HKT might be implemented in a similar way as Static Constraints, I mean by requiring the inline keyword.

[robkuz]

@gusty I can't answer how much more effort that would be - maybe @dsyme can My main focus in this was to not interfere with the CLR/c# interop.

How would your proposal (HKTs via inline) look like in terms of

• syntax
• compiled artifacts?

[robkuz]

Some more example

type Progress<'a>(value:'a) = class end
type Done<'a>(value:'a) = class end
    
 type LineItem = class end
 type PositionData<'a> = PositionData of List<'a>
    
 type Progress = Progress<PositionData<Progress<LineItem>>
 type Done = Done<PositionData<Done<LineItem>>
    
 type PositionData<'a> with
     static member ToDone (x :Progress<PositionData<Progress<LineItem>>>) : 
     Result<Done<PositionData<Done<LineItem>>>, string> = Unchecked.defaultof<_> 
    
 let toDone< ^D, ^P, ^V 
                    when ^P : HasGenericParamsOf<Progress< ^V>> 
                    and  ^D : HasGenericParamsOf<Done< ^V>>> 
                    x =
        (^P : (static member ToDone: Progress< ^P> -> Result<Done< ^D>, string>) x))

 type Coin= class end
 type Wallet<'a> = Coin of List<'a>
    
 type Progress = Progress<Wallet<Progress<Coint>>
 type Done = Done<Wallet<Done<Coin>>

Basically I'd like to express the intention that given a Progress container I want to able to create a container of Dones of the same type as the wrapped Progresses

At the moment I can only express this

 let toDone =
        (^P : (static member ToDone: Progress< ^P> -> Result<Done< ^D>, string>) x))

Which checks the outer containers but not what is within them