[a while ago]
From: Tom Pledger
> Claus Reinke writes:
> > - one would think that () simply takes its role as a unit, so that
> > (),a == a == a,()
> > but if we know x::() does that imply that x,a == a ?
> > x could be bottom, and the equations for the unit look strict in
> > their unit parameter, so probably not;
>
> <possible gross ignorance>
> Does that matter, if the () can't be retrieved from the product by
> pattern matching? Could Void be (reinstated and) used as the unit for
> products?
> </possible>
In the language I had in mind, I would expect to be able to "retrieve" the
() from any product, at any position (which makes it slightly useless to do
so, and also requires that we extend the theory, from associative to an
added identity). But the unit-problem is independent from the suggested
extension.
Note that, in Haskell, the typed expression e::() only promises that
*if the evaluation of expression e ever terminates successfully*, it will
give
a (). Without further proofs, there are always other options: the evaluation
of e could fail to terminate at all, or it could terminate exceptionally,
thus
failing to terminate within the expected type.. And so, the following two
program fragments are not equivalent, however tempting the similarity:
no_unit = no_unit
mainA = case no_unit::() of { () -> system <your favourite bad command> }
mainB = system <your favourite bad command>
You might be slightly unhappy if your compiler "improved" mainA to
mainB (it is probably not wise to rely on a compiler not being overly
optimistic wrt improvements, whatever the language definition says..).
There are at least two ways to look at this: (a) () includes two or more
values, including ()::() and _|_::(), which have to be distinguished, or
(b) () includes only one value, ()::(), but we have to make sure that we
actually get it (a is the more common view).
A transformation that noticed the cycle and *stopped* the execution
with an error message would still be invalid, strictly speaking, even
though one could argue that, in most cases, the programmer doesn't
want the cycle, so it's likely to be an error.
..[finding some route from here to the type of join;-)]..
> This is relevant to my (continuing) attempts to type a natural join.
> Starting with TREX row types like this:
>
> (foo::a, bar::b | r)
> -- Rows with a type a field labelled foo, a type b field labelled
> -- bar, and possibly some other fields
>
> I'd like to add row type constructors (||), (-), and (&&):
>
> (r || s)
> -- The catenation of r with s, which would always be predicated by
> -- r and s having no common labels
The absence of a record concatenation operation seems to be the biggest
single shortcoming of TREX. It is possible to get concatenable "records"
by the old continuation (or difference structure) trick, in this context
known as "Typing record concatenation for free" by D. Remy:
Instead of records, you use record extension functions that add fields
to their parameter, something along the lines of (the unchecked)
add_foo r = (foo=1|r)
add_bar r = (bar=2|r)
add_foo_bar = add_foo . add_bar
to_record r = r ()
Unfortunately, even though (.) serves as a record concatenation operation
here, it isn't possible to give an explicit type for the variant restricted
to
record concatenation. This kills the idea in all contexts in which you need
both explicit type declarations and record concatenation, as in type
classes, for instance..
It wasn't necessary to convince the TREX authors of the usefulness of
record concatenation, but no elegant solution to the typing issues emerged
in time to be added to the implementation.
I don't quite remember the technical issues..(one was the indexing evidence
scheme used in the current implementation - I think that could be overcome
by using a has_field predicate instead of a lacks_field predicate, but I
don't know whether that would bite elsewhere; another alternative would
be to try and define concatenation via type classes - I tried that but
bumped
into the problem mentioned above.. it would help if labels where
first-class,
but I don't remember whether that would be enough..).
> (r - s)
> -- The row type with the fields of r whose labels are not in s
Single, explicit field restriction used to be part of one of the proposals.
Wouldn't the step to implicit, multiple field restriction suffer from the
same problems as the step from single, explicit field extension to record
concatenation?
> (r && s)
> -- The row type with the fields of r whose labels are also in s,
> -- which would always be predicated by r and s having unifiable
> -- types for those fields
How would that predicate be expressed in the type?
> so that a natural join (of records) could have this type:
>
> Eq (Rec (r && s)) => Rec r -> Rec s -> Maybe (Rec (r || (s - r)))
>
> with extensions to the predicate because of the use of (&&).
Which extensions?
I recall that typing join is even trickier than typing record concatenation,
so it might be worthwhile to work out the details of the types you would
hope for in such an extended system, even if you don't have the inference
rules yet. I assume that you've been pointed to Machiavelli and it's type
system already?
If not, see http://www.cis.upenn.edu/~db/langs/allpapers.html for
Database Programming in Machiavelli -- a Polymorphic Language with
Static Type Inference (75K) Atsushi Ohori, Peter Buneman and Val
Breazu-Tannen. In Proceedings of 1989 ACM SIGMOD International
Conference on Management of Data, Portland, May 1989, pp 46-57.
or
Polymorphism and Type Inference in Database Programming (165K)
Peter Buneman and Atsushi Ohori. ACM Transactions on Database
Systems 21 (1996), pp 30-76.
> An issue arises in unifying two types like (r || s) and (foo::a). It
> isn't apparent whether to substitute (foo::a)/r and EmptyRow/s, or
> vice versa. With modular compilation, the information simply isn't
> there, so some further rule would need to be imposed.
If the information isn't there, and you don't want modularity to
change your semantics, it seems you have to delay the decision
until the information becomes available, however inconvenient that
might seem.
Claus
