Friday, July 23, 2021

Notes on "The Meta-Object Facility Typed"

 Obligatory meta-note: why am I even reading this #$%#$% on anything OO, related to the OMG and MOF? Because I'm involved in a project doing model-based development (MDD) and model-based engineering (MDE). Both of which are cool. It's just my pain that some of the relevant work comes from places that I'd much prefer to ignore entirely. The paper in question has gotten quite a few cites.

So the paper starts off well: using type theory to formalize things. Of course, it calls it CTT (constructive type theory) which, while not wrong, does not bode well.

The problem with the MOF is that it embeds the ideas of objects and classes too deeply into its very 'foundations'. If I was doing modelling, I wouldn't put typeclasses (or traits or ...) in my foundations either: they are all just a little too narrowly associated with a particular point of view. The 4 levels is also a bit of an illusion: yes, absolutely, there needs to be a tower of models. But the point isn't about the levels themselves, but about the relations between the levels. In particular, the conforms to relation, which should be central. Sigh So many of the details of MOF (and explanations thereof) seem like over-complicating things. Oh, it's not wrong, but it feels like trying to understand things by doing massive inlining (i.e. abstraction breaking).

Section 3 is an introduction to type theory. Not much to see here.

Section 4 starts with the actual encoding. Already the very first definition is weird because it uses set-encoding (i.e which isn't type theory). And it uses a predicate for well-formedness when the natural way of doing this would be to use a context / sequent / telescope instead. This is dependently-typed after all, why not go all the way? It's way too verbatim translation. Of course, some of this is due to the fact that metamodels themselves allow ridiculous amounts of self-reference. 

As the paper is old, it suffers from non-reproducibility: there are no available artifacts.

Going through who cites this paper, one finds "An Algebraic Semantics for MOF" by A. Boronat and J. Meseguer, which is indeed promising.

No comments: