>> Personally I'd appreciate a type system that's able to express SI units,
which C++ and Haskell are powerful enough to do[1].
>
>I agree. This is of huge importance when it comes to providing compile
time safety guarantees. And if the language is powerful enough to express
SI units, then it also demonstrates that it might be powerful enough to
allow users to grow the language in other directions not anticipated by the
language designers.
While I'm no type system expert, I implemented a unit inference system for
boo (though boo's developers weren't interested and did not use it). So I
thought I'd just share some thoughts about how I view types and unit
checking (as someone whose university education included absolutely no type
theory).
I've started to view types as three partly or wholly independent elements:
1. Physical structure. Under this view, two structs with members "x: int,
y: int" can be considered the same structure, and while direct assignment
between them may not be allowed, the compiler can safely treat them as the
same type IF the language allows it to.
2. Name and attributes. This encompasses things like names and modules
where structures live (e.g. a "Point" structure defined in two different
namespaces), const/non-const in C++, mutable-immutable in D, and units
(km/L, bytes/sec). Unlike a typing error in (1), a typing error or cast
that changes these attributes does not compromise the memory safety of the
language.
3. Operations. Often a type has multiple interfaces, e.g. in Java, an
object can be accessed through several different interfaces without
changing its type. I've been designing a language where this is extended to
allow arbitrary user-defined "views" on a type (a concept which might be
very useful in my Loyc project, whose goal is to allow cross-language
programming; often there are some types in two different languages that are
very similar and just need someone to define a mapping between them.)
I wonder if anyone has formalized a view like this before.
Anyway, viewing (2) as a plurality of attributes, independent from (1),
might allow one to develop a type system where user-defined "attribute"
typing is straightforwardly possible. A simple version of this would be to
allow users to install a plug-in shared library that the compiler uses for
additional analysis following standard typing. Then unit inference could be
installed as one such library. These libraries would not necessarily be
allowed to change the behavior of the program; it would be useful enough
just to allow them to perform analysis, but it would be more useful if they
could alter behavior too (e.g. the unit-checking module could automatically
coerce "km" to "mi" or "m" or "yd", adding a scaling factor; or in a
language with overloading, functions could be overloaded based on unit
types.)
Note that typing failure in (2) need not prevent the code from being
compiled (in general I like a language that doesn't force me to fix every
little problem before running the code.)
A general facility for annotating code is necessary to allow extra typing
without changing the language grammar (e.g. in my languages LES and EC# my
expression grammar allows attributes in [SquareBracks] at the beginning of
any expression or subexpression in parentheses, plus I support some
user-defined operators.)
One thing I want to say about unit checking, it's much more useful to
provide unit inference rather than unit checking, because users don't want
to write annotations all over the place. A function like
fn abs(x: int) -> int { if x < 0 { -x } else { x } }
should need no annotation for the unit inferer to understand that 'x' has
polymorphic units, and in
fn length(&self) { sqrt(self.x * self.x, self.y * self.y) }
'x' and 'y' can be constrained automatically to have the same units. (there
are a bunch of subtle details of course, but since I wrote the inference
engine about 7 years ago, I forgot many of them...)
--
- David
http://loyc-etc.blogspot.com
_______________________________________________
Rust-dev mailing list
[email protected]
https://mail.mozilla.org/listinfo/rust-dev
