Why are flexible types not allowed in record type definitions?

Question

I'm trying this:

type TS1<'state, 'action> = {
    actions : 'state -> #seq<'action>
    move    : 'state -> 'action -> 'state
    state0  : 'state
}

But the type checker won't let me:

.../stdin(2,29):error FS0715: Anonymous type variables are not permitted in this declaration

However, if I unfold the definition of the flexible type, I'm good:

type TS2<'state, 'action, 'actions when 'actions :> seq<'action>> = {
    actions : 'state -> 'actions
    move    : 'state -> 'action -> 'state
    state0  : 'state
}

I'm unhappy with having to add the 'actions type variable—it makes the connection to deterministic transition systems as mathematical objects less obvious.

I don't see what could go wrong by allowing flexible types in record definitions. Is it somehow dangerous? Is there some other way I could get the clarity of definition I would like?

Update. I was hoping to be able to write functions on TS types that exploits known implementations; i.e., I want to be able to define a function

let has_action a ts s = Set.contains a <| ts.actions s

This obviously won't type if the type of the actions member is actions : 'state -> seq<'action>. I can do it with the second definition, in which case has_action has type

has_action : a:'a -> ts:TS2<'s,'a,Set<'a>> -> s:'s -> bool when 'a : comparison

The type of this example suggests that the flexible type in TS1 perhaps wouldn't help. There is no way I can avoid the messy third type parameter in TS2? It seems to me the exact implementation of the collection of actions for a state is an implementation detail that should not be exposed in the type.

Judie

It compiles for me if you remove the # from before the seq. – Chalybeate

@MarkPattison has a good point - it's easier to just remove the # - why do you think you need it? – Cutback

concerning your update IMO the third parameter is a vital part of your record so no I don't think you should get rid of it here (btw: you don't have to type it - you can use _ instead if you like) - in case you want to know (but it will not help here): the only place where you can use forall quantification is on (interface)members (I wrote about a similar issue here: gettingsharper.de/2014/09/29/…) – Cutback

Yes, looking at the type of has_parents it seems there's no way around having a third type parameter. – Allocution

Answer 1

This is just a limitation of the current compiler's implementation of the permitted kinds of record signatures. For instance, if you define your type in the same way conceptually, but using an interface or an abstract class instead of a record, it compiles fine:

type TS1<'state, 'action> = 
    abstract actions : 'state -> #seq<'action>
    abstract move    : 'state -> 'action -> 'state
    abstract state0  : 'state

Tegan

Answer 2

You pretty much answered your own question here... The second option works, because you introduce another type argument, i.e. you abstract over 'actions. The point being, that you need cannot really define generic values in a record definition. Consider, that the second option is not generic with respect to types, as 'state and 'actions are defined.

Spotty

I'm not quite following: a record definition is a type definition; I'm not defining any values. And I'm not sure what you mean by "the second option is not generic with respect to types"? – Allocution

I mean the following. By defining a record, you are defining a class (in IL / C# terms). Now, if you could define the members in a generic way, you would immediately make it heterogeneous, as in each object instance of your record would have a different runtime type. – Spotty

Not sure if we are talking about the are thing but: I don't see the problem, since in that perspective, I just want a suitably generic class. I was actually just hoping that the flexible type would automatically introduce a type variable for me. – Allocution

Answer 3

This is because of the way the compiler implements flexible types. According the the F# spec section 8.3:

 Flexible type constraints #type may not be used on the right side of a type 
 abbreviation, because they expand to a type variable that has not been named 
 in the type arguments of the type abbreviation. For example, the following 
 type is disallowed:

       type Bad = #Exception -> int

Simply put, flexible are implemented as standard generics and since it has not been named at the left side or type arguments side, you get an error. This applies for record types too.

Hanus