Data Declaration Using Row Type

#1

Hi,

I’ve been reading some of the Halogen source code to try and gain a better understanding for how it works, and I found the following declaration for Component:

data Component
    (surface :: Type -> Type -> Type)
    (query :: Type -> Type)
    (input :: Type)
    (output :: Type)
    (m :: Type -> Type)

It looks like this declaration is leveraged a little later in the code by way of calling unsafeCoerce. I’ve never seen a data declaration in this form before (tagged unions typically have an = sign). Is this type of declaration documented anywhere? Is this a common construct that I should know about?

#2

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.

10 Likes
#3

Thank you for the thorough explanation. Would it be worth documenting the existential constructor pattern somewhere to help facilitate understanding within the community?

#4

I think if one were to document existential encodings, one should use a closure instead, since it doesn’t require unsafe facilities. Existentials and closures are isomorphic, it’s just that closures result in additional allocations for larger interfaces and so can be heavyweight. As an example, halogen-vdom used to use a closure encoding, and switching to existentials resulted in around a 40% reduction in memory usage.

As an example, you can make get an equivalent closure encoding by closing over the subject.

type ShowBox = Unit -> String

mkShowBox :: forall a. Show a => a -> ShowBox
mkShowBox a = \_ -> show a

Instead of exposing show and value directly, I’ve just bundled the application up. This supports the same operation of getting a String on demand. For larger interfaces, this usually involves partially applying functions to their subject and sticking it in a record, which requires an allocation for each partial application. This is also why existentials are often called an anti-pattern, or for usage when you know you really need one, since they aren’t strictly necessary and the alternatives may be easier to understand.

#5

This is also possible, but it uses closure:


type ShowBoxF a =
  { show :: a -> String
  , value :: a
  }

newtype ShowBox = ShowBox (forall r. (forall a. ShowBoxF a -> r) -> r)

mkShowBox :: forall a. ShowBoxF a -> ShowBox
mkShowBox box = ShowBox (\onBox -> onBox box)

unShowBox :: forall r. (forall a. ShowBoxF a -> r) -> ShowBox -> r
unShowBox onBox (ShowBox runOnBox) = runOnBox onBox