un-deprecate unused parameters in type abbreviations

[A-Manning]

I propose we allow unused parameters in type abbreviations. As it stands, type t<'a,'b> = 'a gives an error:

FS0035: This construct is deprecated: This type abbreviation has one or more declared type parameters that do not appear in the type being abbreviated. Type abbreviations must use all declared type parameters in the type being abbreviated. Consider removing one or more type parameters, or use a concrete type definition that wraps an underlying type, such as 'type C<'a> = C of ...'.

Type abbreviations of this form can be very useful in enforcing abstractions through abstract, private, etc. Type abbreviations of this form are allowed in OCaml.

The existing way of approaching this problem in F# is to either use a constructor, as in type t<'a,'b> = C of 'a, or sometimes use hacks with measure types. This seems unnecessary and burdensome.

Pros and Cons

The advantages of making this adjustment to F# are that it would be easier to use these types for abstraction. The construct was previously allowed, so this is unlikely to require significant changes.

The disadvantages of making this adjustment to F# are that perhaps this could be seen as obfuscatory? I think such definitions are clear though. Unused parameters are allowed in function definitions, so why not type abbreviations?

Extra information

Estimated cost XS: Since F# allowed this in the past, it doesn't seem that it should be too hard to bring this back.

Affidavit (please submit!)

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
• [ x] I or my company would be willing to help implement and/or test this

[dsyme]

Type abbreviations of this form can be very useful in enforcing abstractions through abstract, private, etc.

@A-Manning Could you give a couple of detailed examples please? Many thanks

[A-Manning]

One example would be to express a relation of something to another type;

type private Related'<'a,'b> = R of 'a
type Related<'a,'b> = Related'<'a,'b> 

All of the functions in the module defining Related are going to have to add and remove the R constructor a lot, whereas they wouldn't if type private Related<'a,'b> = 'a were allowed.

These types occur frequently in F* code (where the unused parameter is erased), and can't extract to F# correctly because of this restriction - so I suppose another example would be if we want to use F# to implement dependently typed languages. For example, I might want to have a type of arrays indexed by their length, as type private indexedArray<'a,n> = array<'a>

Perhaps this should just generate a warning, rather than an error?

[A-Manning]

Another use of types of this form is to express OCaml-style phantom types.

[Rickasaurus]

This is a pretty neat trick!

[A-Manning]

One of my coworkers has a version of F# Compiler Services that gives warnings rather than errors for this, here https://github.com/zenprotocol/FSharp.Compiler.Service/commit/1201088355c9cc58ff244fcdc8bc98477d0df230

[dsyme]

There are technical reasons why this wasn't allowed in F# - though you could argue about their importance, and it depends what features of F# and .NET you use

For example, consider

type X<'T> = int

let f0 (x: int) = x
let f1 (x: X<'T>) = x
let f2 (xint) = (x: X<'T>)
let f3 (x: X<'T>) = typeof<'T>

Does the compiled form of f1, f2, f3 have a generic type parameter or not? This is significant in F# because F# is type passing and the values of type parameters can be observed (e.g. f3). If we erase all type abbreviations prior to generalization, then type variables disappear.

There may be ways to navigate this technical difficulty but I'm not sure, and it may be very subtle, involving extensive type annotations. There are some similarities to units of measure inference, for example.

Of course, if you never rely on the type passing capabilities of F# (don't use typeof<'T> for example), nor binary compiled form (e.g. .NET interop to F# code) then the above is less important - it really doesn't matter if there's a type parameter in the compiled form or not.

[A-Manning]

Thanks for your response!

I think it's ok if typeof<'T> doesn't work for unused parameters, since it is clear from the type abbreviation that <'T> is unused, and it's also possible to give a warning when this happens. It seems to me that there is not much of a reason to be using typeof<'T> in cases where <'T> is unused, but I can see why this behaviour would be an issue.

For F* interop with F#, this is an annoying and pervasive issue, since allowing type-level functions and higher types means that I can write

type const 'a 'b : Type = 'a

which would have to extract to

type const<'a, 'b> = 'a 

This pops up frequently in extracted F* code, and has to be handled manually somehow (this is not always possible), which is not fun! I don't think that there is much that can be done to prevent types like this from being extracted, unless it's possible to pull some tricks with measure types. OCaml allows this form of type definition, which makes it much more stable as an extraction target for F*.

What would the issues with binary compiled form be?

[dsyme]

What would the issues with binary compiled form be?

Basically the same - would the C# consumer see a generic method or not, and if so how many type parameters

The F# compiler freely eliminates type abbreviations wherever it wants - so I'm not actually sure what would happen with things like

let f3 (x: X<'T>) = typeof<'T>

I assume it would be treated as the equivalent of

let f3 (x: int) = typeof<'T>

which is a non-generic function, and give a warning that 'T has been instantiated to obj. But the user will certainly be surprised by this.

[A-Manning]

@dsyme What do you think is the right solution then? If this is added to F#, users might have surprising issues when making use of type passing. If this is not, then there will continue to be issues with F* interop, and most likely a fork of F# will need to be maintained specifically for F*. Should this be allowed with warnings rather than errors? Should the compiler have a flag to allow this? Or should this be maintained as a fork?

There may be ways to navigate this technical difficulty but I'm not sure, and it may be very subtle, involving extensive type annotations. There are some similarities to units of measure inference, for example.

I'd be happy to work on a more sophisticated workaround, but I'm not sure what would need to be done. I'd be happy to discuss this further.

[dsyme]

@dsyme What do you think is the right solution then?

@A-Manning I'm not sure there is a solution :) That's why we made this an error.

One way to move forward would be for you to change the error to a warning in a branch of your own, and recruit/hassle/invite/bribe people to work out what happens in various corner cases like the ones above (and find even more challenging versions), and write that up here?

[kurtschelfthout]

What about we allow this provided the unused type parameters have an attribute Erased - inspired by Measure - at the type alias declaration and are always erased in compiled form? And we give specific warnings if any erased types are used in typeof or typedefof.

[dsyme]

What about we allow this provided the unused type parameters have an attribute Erased - inspired by Measure - at the type alias declaration and are always erased in compiled form? And we give specific warnings if any erased types are used in typeof or typedefof.

Yes. We could probably infer that without even needing any attribute, though in general having a notion of Erased type parameters (and indeed a first-class notion of erased types - rather than just the ones you get from type providers) would be useful in general.

[travis-leith]

Has there been any movement on this? Seems like you guys sort of agreed on a possible way forward.

[A-Manning]

@ChechyLevas My bad, I seem to have let this slip - I'll make a branch that uses the Erased attribute ASAP