Hoare Triples and Thrists

While mousing through the L4.verified presentation that took place at Galois, I could not help but build an association bridge between Hoare triples and thrists. Especially when you go to p. 52 and thereabout.
Here is my take on the connection:

We have some commands that belong to a data type C, and C has two type parameters:

data C :: * -> * -> * where
  C1 :: ... -> C a b

The first type parameter can be interpreted as the precondition of the command while the second as its postcondition ({P} and {Q} in Hoare's notation). This convention employs the types-as-properties interpretation.
If commands are sequenced, the postconditions of the former commands must imply the preconditions of the latter. This is referred to as the composition rule and corresponds to appending two thrists.

Now, in Ωmega the situation is even prettier, because C need not be a two-type-parameter entity, but can be parameterized over arbitrary kinds. The built-in evaluation mechanism (type functions) allow the most powerful constructs. (Haskell will get something similar at the type level, called type families, with GHC v6.10.)