Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Anonymous generic parameter in recursive record definition

Tags:

f#

I'm building a HFSM and using a record to keep track of the state:

type State<'a> =
    {
        CurrentNodeId : int
        Data : 'a
    }

When the current node has another HFSM as part of it, I need to keep track of that state as well. So I wanted to do something like this

type State<'a> =
    {
        CurrentNodeId : int
        Data : 'a
        SubState : State<_> list
    }

Because I don't really care what type the SubState list is, but it errors out with:

Anonymous type variables are not permitted in this declaration

Is there a different, more idiomatic F# way to do this or will I have to come with a different solution?

like image 556
hvidgaard Avatar asked May 13 '26 19:05

hvidgaard


1 Answers

Tomas is right that there's no super-clean way to do this in F#, but I think it's possible to do it a bit more nicely than his approach. The basic idea is that you want a type like this:

type State<'a> = {
    CurrentNodeId : int
    Data : 'a
    SubState : ∃'x. State<'x> list
}

except that F# doesn't directly support existential types. It turns out that there's a fairly standard way to encode existential types in terms of universal types (which F# does support):

∃'x.T<'x> ≡ ∀'z.(∀'x.T<'x> -> 'z) -> 'z

Unfortunately, this actually requires two extra types because each universal quantification is encoded as a single generic method on a unique type:

type State<'a> = {
    CurrentNodeId : int
    Data : 'a
    SubStates : SomeStateList
}
and SomeStateList =
    abstract Apply : StateListApplication<'z> -> 'z
and StateListApplication<'z> =
    abstract Apply : State<'x> list -> 'z

Note that there's an extra type here compared to Tomas's solution, but the benefit is that you don't have to pick a single return type for all uses of a particular State (Tomas's encoding basically inlines the SomeStateList type into State and lifts the type parameter 'z to the State type in the process).

Now we want to be able to pack up a list of states of some arbitrary type as a SomeStateList:

let pack states = { new SomeStateList with member __.Apply a = a.Apply states }

and we can demonstrate how to use these types with the analogous definition to Tomas's recursive depth function. We wish we could just write

let rec depth = 1 + s.SubStates |> List.map depth |> List.fold max 0

But we need to add some extra syntax to take care of creating and applying our generic types (though hopefully the core logic is still apparent if you squint):

// Full type annotation necessary here to get inner use to typecheck
let rec depth<'a> (s:State<'a>) : int = 
    1 + s.SubStates.Apply { 
        new StateListApplication<_> with 
            member __.Apply l = l |> List.map depth |> List.fold max 0 
}

And creating a graph and applying the function is pretty clean:

depth {
    CurrentNodeId = 1
    Data = "test"
    SubStates = pack [{ CurrentNodeId = 2
                        Data = 1uy
                        SubStates = pack []}]
}
like image 130
kvb Avatar answered May 19 '26 03:05

kvb