On Sat, Dec 27, 2014 at 10:20 AM, Matt Oliveri <[email protected]> wrote:
> Well with an array, there's a non-type-specific meaning for the
> indexes--they're just unsigned integers.
At the language level type system, what you say is true. At the instruction
level type system, *both* forms of indices are actually offsets.
Yes, I agree the offsets are type-specific, but that's mainly so that we
know the type of a[i] without knowing the value of i. And I certainly agree
from a pragmatic perspective that we would very much like to know that
type. But if restrict ourselves - just for a moment - to literal indices
like a[2], we would be looking at something much more like a record,
because that literal tells us explicitly which cell we are looking at,
after which there's no real reason to require all of the cells to have the
same type.
> In other words, if you try to have a single type of "literal
> identifiers", it's not clear to me how you'd implement efficient
> record projection.
>
But that's not what I'm suggesting. I'm suggesting a single *kind* of
"literal identifier". Let's back up a second here.
Assume that tuples are unboxed. If that's the case, then I can form an
offset for ( 5.6247, "abc" )#2 just as easily as I can form the offset for
(5.6247, "abc").snd. This is true because the indexing expression is a
literal, not a variable. That's the kind of thing I'm saying when I talk
about literal identifiers. Identifiers as actual *values* is another matter
entirely.
> But copy-and-update does seem like adding environment entries,
> assuming the type is allowed to change. (I guess I'm not following
> your train of thought, from copy-and-update to literal identifiers.)
>
The type only changes if new field names are introduced by the
copy-and-update operation, or if the type of an existing field name is
altered (comparable to shadowing with let).
What I'm saying about literal identifiers in the copy-and-update context is
that when we see something like
(r:'R) with myField = 42.3
we can view the "with" as a polymorphic ternary function:
HasField('R :: Record, 'id :: Ident, 'fieldType) =>
with: 'R -> 'id -> 'fieldType
in exactly the same way that we can view array indexing as a polymorphoc
binary function:
forall 'index :: Nat < 'bound :: Nat =>
arrayLookup: 'a[bound] -> 'index -> 'a
That is: literals can be "lifted" to types and then we can do polymorphism
over them in the usual way.
And in that (admittedly odd) view of things, an environment is merely a
function
tyfn 'ident -> 'valueType =>
env : ('ident :: Ident) -> 'valueType
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
