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.)

Saudades

É muito bom ficar sozinho alguns dias, pensando e trabalhando em paz. Mas quando as semanas passam a distância parece que aumenta e a ausência começa de doer.

Meus amores sinto muito falta de voces, quero que voltam logo.

Meme evolution

While I am missing family induced distraction, I use the opportunity of reading old papers that I always wanted to revisit.

Yesterday, while reading "A History of Haskell" I was amused by the sentence:

"Wadler misunderstood what Fasel had in mind, and type classes were born!"

This is a concrete case of "meme evolution" (in Dawkins' sense): a mutation of a meme (by transcription error) finds a new habitat where it thrives and blossoms.

Some preconditions are needed for this to happen:

• communication
• loosening of amorphous ideas
• an open mind, not shying away from listening to the unknown

Many great ideas come to me while reading conference papers of others and where I have no idea what they are talking about :-) While trying to make vague sense of what I have in front of me a fireworks of ideas commence, all building in some way on foundations of things (pet projects) I have done in the past.

Now, how can I ensure that I periodically can enjoy the state of minimal disturbances?