These look a lot like row types, but they are actually kind annotated variable binders. Kinds are the types of types.
data Maybe a = Nothing | Just a
is actually
data Maybe (a :: Type) = Nothing | Just a
And Maybe itself has the kind Type -> Type. That is, it takes a single type argument of kind Type, and produces a Type.
That particular Component declaration is actually an empty data declaration, since there are no declared constructors. There is no safe way to construct a value of that type at the term level. Halogen uses this pattern a lot internally to encode existential types. PureScript does not have existential types at the language level (yet, at least). Existential types are a way to hide type variables, making them opaque to a consumer. You can think of them like a black box for types, and the only way to interact with these opaque types is by providing an interface that lets you observe specific properties of the type.
The primary example in Halogen is component state. Component state is completely internal to the component. When you construct a component, all the functions and values must agree with each other on this internal state type, but you can’t see what the state is once you construct a component. In that sense, state is an opaque type to outside consumers, and outside consumers can all talk about this state in a polymorphic (forall) way. We know that the state exists, however we don’t know what it is, so we have to be able to handle it for all types.
The purescript-exists library exists as a way to hide a single type variable of kind Type. However, Halogen hides more type variables, and of different kinds, so it’s not a viable solution. Instead it uses something I call the existential constructor pattern, which goes something like:
-- Declare a data type or synonym with the type parameter we want to hide.
type ShowBoxF a =
{ show :: a -> String
, value :: a
}
-- Declare an opaque type with the type parameter hidden
data ShowBox
-- Declare a constructor with a coercion
mkShowBox :: forall a. ShowBoxF a -> ShowBox
mkShowBox = unsafeCoerce
-- Declare an eliminator with a coercion
unShowBox :: forall r. (forall a. ShowBoxF a -> r) -> ShowBox -> r
unShowBox = unsafeCoerce
Notice the rank-n type in the eliminator. This says that you can consume a ShowBox, as long as you can handle a ShowBoxF for all as. That is, you can do something with a show box, as long as you don’t care what the underlying value is. This only works because we’ve provided a function show in ShowBoxF that lets us do something with a.
box =
mkShowBox { show, value: 41 }
example =
runShowBox (\{ show, value } -> show value) box
A language level solution would look like this (using Haskell existential syntax, which puns on the forall eliminator)
data ShowBox = forall a. Show a => ShowBox a
box =
ShowBox 41
example = case box of
ShowBox a -> show a
So the Show dictionary is bundled up and made available automatically.
Halogen will package up existential state and eval functions, and it since it only cares that it’s internally consistent, and not what the actual state values are, it can store the internal state somewhere, and run your component against it, updating it as necessary.