Daniel Jackson on types in Alloy


Subject: Daniel Jackson on types in Alloy
From: Jonathan Edwards (edwards@intranet.com)
Date: Sun Feb 24 2002 - 12:41:43 EST


 

On Monday, February 11, 2002, at 11:57 am, Jonathan Edwards wrote:

An interesting question (since I come from Matthias' Type Theory class)
is: what is the formal role of types in Alloy? Alloy dispenses with
subtypes in favor of subsets (which I applaud). One might ask: why not
go all the way and dispense with types altogether? There is just one
type: the universe, and everything else is a subset of that. What were
types before become a partitioning of the universe. What were type
declarations on relations become subset constraints. This adds
expressive power: sets that cross types, arbitrary union types,
polymorphic relations, and multiple independent type-partitionings.

Types in programming languages catch certain errors at compile-time
rather than run-time. It is not clear to me that the
compile-time/run-time distinction makes sense for a modeling language.
There is just analysis-time. What would a type-safety theorem for Alloy
assert? Finding that the model is inconsistent at an earlier phase of
the analysis does not seem that big a win. In any case, one could
simulate type-checking by treating partitionings of the universe as
types and inferring the types of all expressions as usual, with the
addition of union types. Multiple partitionings would lead to multiple
type checks.

Types are utilized in the analyzer. Scopes of a model are cardinalities
on types. The boolean matrices that relations are translated into get
their dimensions from the cardinalities of their types. Types are thus a
performance optimization, but we could again simulate them from the fact
of a universe partitioning.

So my tentative (and probably naive) answer is that there is no formal
need for types in Alloy: that their function could be replaced with some
cleverness in the tools while increasing the expressive power of the
language. If true, this leads to the more interesting question of
whether typed models are a Good Thing.

From: Daniel Jackson [mailto:dnj@mit.edu]
Sent: Friday, February 22, 2002 1:42 AM

good question. you're right that there is no compile-time/run-time
distinction for a modelling language. but types do have a purpose beyond
the ones you list within the analyzer. when you make what's now a type
error, you get an error message much more quickly than you would if you
had to wait to formulate an assertion and check it. even with our not
always that helpful error messages, it's also easier to diagnose. if
type errors were left in the model, many would also go undetected until
that bit of the model were exercised.

most of the time, a type error arises from misunderstanding precedence
rules, applying a relation backwards (eg, using r when ~r would be
appropriate), or confusing two relations. i at least find it very
helpful to weed these bugs out early.

you're right that there's no obvious type soundness theorem. one idea
i've had is that a type error is when an expression evaluates to a
constant. the idea is that presumably you wrote the expression because
you thought it meant something different from the constant. so if i
wrote student.ip when i meant router.ip, student.ip would be the empty
set if ip didn't map students. the obvious flaw with this definition is
that a valid assertion reduces to the constant "true", and would thus be
a type error! so we'd need some notion of "easy evaluation", which is a
bit suspect.

 



This archive was generated by hypermail 2b28 : Sun Feb 24 2002 - 12:41:04 EST