Those of you who are watching with nit-picking detail will have noticed item
4 on the first release to-do list:

Implement literal instantiation

We're dropping this. I want to explain what problem it was supposed to solve
and why we are doing away with it.

*** What We Wanted To Accomplish

We had intended that literal instantiation would deal with two issues:

1. Parameterizing procedures over multiple array sizes
2. A means for typing low-level I/O procedures so that we could do in-place
I/O.

The idea (which was good) was that we could "lift" literals into a
corresponding space of literal types, so that
 the literal "#\c" would now be typed as:

  (literal char #\c)

Once we had this expressed as a type, we could then apply all of the current
type class work to give us the ability to parameterize over literals. Sounds
good on paper, doesn't work so well in practice.

*** Why This is Not So Good

There are two ways to introduce these types into the language:

1. Literals are now given (only) literal type, and if T is a type having
literals, then T := (literal T <any>) is copy compatible. The problem with
this is that we are now forced either to introduce subtyping or to lose
completeness in the type system. Subtyping is more than we want to do, and
we have (so far) managed to dodge that bullet. Personally, I don't think
that is so bad, but it does seem mildly unfortunate.

2. A new family of type classes is introduced to capture the notion "This
thing is either a T or a (literal T <some value>) we'll figure out which
later." This preserves completeness, but it would probably force us to
switch to a three-typed Arith type class, and would likely lead to
potentially explosive expansion at instantiation time. A lot of work for a
not-so-great result.

So it looked like we had two bad options here.

At the same time, I have been looking at hybrid region typing, and it dawned
on me that there were really two very different things getting conflated in
the notion of literal types. The first is compile-time computability, which
can be handled by a region typing system. That is something that we are
definitely going to want at some point, and it seems silly to put a lot of
work into literal types if they aren't the right long-term answer.

The second issue is "agreement", specifically: "we know from the types that
this variable over here matches the size of that array over there".
Agreement is generally something that you would want to solve with dependent
types. We were attempting to dodge the dependent type bullet by forcing the
problem into literal types.

Meanwhile, we have *also* been looking at introducing record polymorphism
via HAS-FIELD. Introducing array size polymorphism in a similar way is
pretty simple as long as we find an alternative solution to the agreement
problem.

So now we were down to agreement, and the only real motivating case for
agreement has to do with connecting to the C runtime's implementation of
efficient I/O. For that problem, there is a simpler solution.

*** What We Are Doing

What we are going to do is introduce a new type, similar to BY-REF, which I
will call BY-REF-ARRAY. As with BY-REF, this is only legal on parameters,
and it is never inferred. A formal parameter of type (BY-REF-ARRAY T) will
accept an actual parameter of type (array T <any>). The actual data
structure is passed as a pair consisting of a size and a pointer to the
array content. We will introduce -NTH and -LEN operations similar to those
provided for arrays and vectors. Bounds checks are enforced similarly to
vector and array bounds checks.

This is not an ideal solution, but it should let us move forward, which is
what we really need to do right now.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to